reduceDB_lt Struct Reference

Collaboration diagram for reduceDB_lt:

Public Member Functions
	reduceDB_lt (ClauseAllocator &ca_)
bool	operator() (CRef x, CRef y)
	reduceDB_lt (ClauseAllocator &ca_)
bool	operator() (CRef x, CRef y)
	reduceDB_lt (ClauseAllocator &ca_)
bool	operator() (CRef x, CRef y)

Public Attributes
ClauseAllocator &	ca

Detailed Description

Definition at line 521 of file Solver.cpp.

Constructor & Destructor Documentation

reduceDB_lt() [1/3]

reduceDB_lt::reduceDB_lt ( ClauseAllocator & ca_ )

inline

Definition at line 523 of file Solver.cpp.

: ca(ca_) {}

reduceDB_lt() [2/3]

reduceDB_lt::reduceDB_lt ( ClauseAllocator & ca_ )

inline

Definition at line 915 of file Glucose.cpp.

: ca(ca_) {}

reduceDB_lt() [3/3]

reduceDB_lt::reduceDB_lt ( ClauseAllocator & ca_ )

inline

Definition at line 1075 of file Glucose2.cpp.

: ca(ca_) {}

Member Function Documentation

operator()() [1/3]

bool reduceDB_lt::operator() ( CRef x, CRef y )

inline

Definition at line 524 of file Solver.cpp.

                                      { 
        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 

operator()() [2/3]

bool reduceDB_lt::operator() ( CRef x, CRef y )

inline

Definition at line 916 of file Glucose.cpp.

                                      { 
 
    // Main criteria... Like in MiniSat we keep all binary clauses
    if(ca[x].size()> 2 && ca[y].size()==2) return 1;
    
    if(ca[y].size()> 2 && ca[x].size()==2) return 0;
    if(ca[x].size()==2 && ca[y].size()==2) return 0;
    
    // Second one  based on literal block distance
    if(ca[x].lbd()> ca[y].lbd()) return 1;
    if(ca[x].lbd()< ca[y].lbd()) return 0;    
    
    // Finally we can use old activity or size, we choose the last one
    return ca[x].activity() < ca[y].activity();
    //return x->size() < y->size();
    //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
    }    

operator()() [3/3]

bool reduceDB_lt::operator() ( CRef x, CRef y )

inline

Definition at line 1076 of file Glucose2.cpp.

                                      { 
 
    // Main criteria... Like in MiniSat we keep all binary clauses
    if(ca[x].size()> 2 && ca[y].size()==2) return 1;
    
    if(ca[y].size()> 2 && ca[x].size()==2) return 0;
    if(ca[x].size()==2 && ca[y].size()==2) return 0;
    
    // Second one  based on literal block distance
    if(ca[x].lbd()> ca[y].lbd()) return 1;
    if(ca[x].lbd()< ca[y].lbd()) return 0;    
    
    // Finally we can use old activity or size, we choose the last one
    return ca[x].activity() < ca[y].activity();
    //return x->size() < y->size();
    //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
    }    

Member Data Documentation

ca

ClauseAllocator & reduceDB_lt::ca

Definition at line 522 of file Solver.cpp.

---

The documentation for this struct was generated from the following files:

• src/sat/bsat2/Solver.cpp
• src/sat/glucose/Glucose.cpp
• src/sat/glucose2/Glucose2.cpp