40 #ifndef _cvc3__minisat_h_
41 #define _cvc3__minisat_h_
515 bool simplifyClause(std::vector<Lit>& literals,
int clausePushID)
const;
520 void orderClause(std::vector<Lit>& literals)
const;
523 void remove(
Clause* c,
bool just_dealloc =
false);
755 std::string
toString(
Lit literal,
bool showAssignment)
const;
758 std::string
toString(
const std::vector<Lit>& clause,
bool showAssignment)
const;
761 std::string
toString(
const Clause& clause,
bool showAssignment)
const;
770 std::vector<std::vector<SAT::Lit> >
curClauses();
std::vector< PushEntry > d_pushes
Push / Pop.
bool simplifyClause(std::vector< Lit > &literals, int clausePushID) const
std::vector< Lit > d_analyze_redundant
void analyze_minimize(std::vector< Lit > &out_learnt, Inference *inference, int &pushID)
bool isImpliedAt(Lit lit, int clausePushID) const
std::vector< double > d_activity
bool analyze_removable(Lit p, unsigned int min_level, int pushID)
std::vector< Clause * > d_clauses
Clause * getReason(Var var) const
double d_cla_inc
heuristics
void checkClause(const Clause &clause) const
std::vector< std::vector< SAT::Lit > > curClauses()
std::vector< signed char > d_assigns
void propLookahead(const SearchParams ¶ms)
const std::vector< Clause * > & getWatches(Lit literal) const
int getPushID(Lit lit) const
MiniSat decision heuristics.
void addClause(std::vector< Lit > &literals, CVC3::Theorem theorem, int clauseID)
void popClauses(const PushEntry &pushEntry, std::vector< Clause * > &clauses)
std::vector< Hash::hash_set< Var > > d_registeredVars
Derivation * d_derivation
proof logging
int d_clauseIDCounter
Clauses.
lbool getValue(Lit p) const
void addFormula(const SAT::CNF_Formula &cnf, bool isTheoryClause)
void orderClause(std::vector< Lit > &literals) const
SAT::DPLLT::Decider * d_decider
void setPushID(Var var, Clause *from)
bool isConflicting() const
bool isConsistent() const
void insertClause(Clause *clause)
PushEntry(int clauseID, size_type trailSize, size_type qhead, size_type thead, bool ok)
void backtrack(int level, Clause *clause)
static const int d_rootLevel
variables
const std::vector< Clause * > & getLemmas() const
std::vector< int > d_pushIDs
bool isRegistered(Var var)
Operations on clauses:
std::vector< Lit > d_analyze_stack
bool enqueue(Lit fact, int decisionLevel, Clause *reason)
void insertLemma(const Clause *lemma, int clauseID, int pushID)
std::vector< Clause * > d_reason
void checkWatched() const
const SolverStats & getStats() const
Statistics.
int getPushID(Var var) const
std::vector< Clause * > d_popLemmas
SAT::DPLLT::TheoryAPI * d_theoryAPI
CVC interface.
void updateConflict(Clause *clause)
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
std::vector< Lit > d_trail
unsigned int d_popRequests
std::vector< Clause * > d_learnts
std::vector< std::vector< Clause * > > d_watches
variable assignments, and pending propagations
void claRescaleActivity()
SAT::Var miniSatToCVC(Var var)
std::string toString(Lit literal, bool showAssignment) const
String representation:
void setLevel(Var var, int level)
Var cvcToMiniSat(const SAT::Var &var)
void registerVar(Var var)
Operations on clauses:
int getLevel(Lit lit) const
void addWatch(Lit literal, Clause *clause)
void protocolPropagation() const
void resolveTheoryImplication(Lit literal)
std::vector< char > d_analyze_seen
Temporaries (to reduce allocation overhead).
std::vector< Clause * > & getWatches(Lit literal)
unit propagation
std::vector< size_type > d_trail_pos
std::vector< SAT::Lit > curAssigns()
int getImplicationLevel(const Clause &clause) const
Clause * analyze(int &out_btlevel)
Conflict handling.
SearchParams(double v=1, double c=1, double r=0)
void varBumpActivity(Lit p)
Activity:
int getLevel(Var var) const
CVC3::QueryResult search()
search
SearchParams d_default_params
Mode of operation:
int decisionLevel() const
Search:
Derivation * getDerivation()
bool allClausesSatisfied()
debugging
std::vector< int > d_trail_lim
void setLevel(Lit lit, int level)
const std::vector< Lit > & getTrail() const
bool isPermSatisfied(Clause *c) const
int getConflictLevel(const Clause &clause) const
std::stack< std::pair< int, Clause * > > d_theoryExplanations
void checkClauses() const
Clause * cvcToMiniSat(const SAT::Clause &clause, int id)
problem specification
std::queue< Clause * > d_pendingClauses
Temporary clauses.
bool isReason(const Clause *c) const
void claBumpActivity(Clause *c)
static Solver * createFrom(const Solver *solver)
void removeWatch(std::vector< Clause * > &ws, Clause *elem)
Conflict handling.
void varRescaleActivity()
Activity.
std::vector< int > d_level
void setActivity(float activity)
std::vector< int >::size_type size_type
Solver(SAT::DPLLT::TheoryAPI *theoryAPI, SAT::DPLLT::Decider *decider, bool logDerivation)
Initialization.
const std::vector< Clause * > & getClauses() const
lbool getValue(Var x) const
clauses / assignment