125 for (j = clause.
begin(), jend = clause.
end(); j != jend; ++j) {
140 vector<MiniSat::Lit> literals;
142 if (getDerivation() != NULL)
159 bool logDerivation) :
165 d_registeredVars (1),
166 d_clauseIDCounter (3),
174 d_order (d_assigns, d_activity),
175 d_simpDB_assigns (0),
177 d_simpRD_learnts (0),
178 d_theoryAPI(theoryAPI),
182 d_expensive_ccmin(true)
194 vector<Lit> literals;
195 lemma->
toLit(literals);
203 for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i) {
227 if (newLemma->
size() >= 2) {
228 addWatch(~(*newLemma)[0], newLemma);
229 addWatch(~(*newLemma)[1], newLemma);
241 DebugAssert(
false,
"MiniSat::Solver::insertLemma: conflicting/implying lemma");
267 const vector<MiniSat::Lit>& trail = oldSolver->
getTrail();
268 for (vector<MiniSat::Lit>::const_iterator i = trail.begin(); i != trail.end(); ++i) {
274 const vector<MiniSat::Clause*>& clauses = oldSolver->
getClauses();
275 for (vector<MiniSat::Clause*>::const_iterator i = clauses.begin(); i != clauses.end(); ++i) {
280 const vector<MiniSat::Clause*>& lemmas = oldSolver->
getLemmas();
281 for (vector<MiniSat::Clause*>::const_iterator i = lemmas.begin();
293 for (vector<Clause*>::const_iterator i =
d_learnts.begin(); i !=
d_learnts.end(); ++i)
296 for (vector<Clause*>::const_iterator i =
d_clauses.begin(); i !=
d_clauses.end(); ++i)
320 ostringstream buffer;
323 if (showAssignment) {
335 ostringstream buffer;
336 for (
size_type j = 0; j < clause.size(); ++j) {
337 buffer <<
toString(clause[j], showAssignment) <<
" ";
345 std::vector<Lit> literals;
346 clause.
toLit(literals);
347 return toString(literals, showAssignment);
352 vector<SAT::Lit> res;
353 cout <<
"current Assignment: " <<
endl;
361 std::vector<std::vector< SAT::Lit> > res;
362 cout <<
"current Clauses: " <<
endl;
363 for (
size_t i = 0; i <
d_clauses.size(); ++i) {
364 std::vector<SAT::Lit> oneClause;
366 for (
int j = 0; j < (*
d_clauses[i]).size(); ++j) {
369 res.push_back(oneClause);
376 cout <<
"Lemmas: " <<
endl;
383 cout <<
"Clauses: " <<
endl;
390 cout <<
"Assignment: " <<
endl;
406 int max_id =
nVars();
410 cout <<
"c minisat test" <<
endl;
411 cout <<
"p cnf " << max_id <<
" " << num_clauses <<
endl;
416 for (
int j = 0; j < clause.
size(); ++j) {
418 cout <<
toString(lit,
false) <<
" ";
434 for (vector<Lit>::const_iterator i =
d_trail.begin(); i !=
d_trail.end(); ++i) {
451 if ((*i).count(var) > 0)
return true;
461 if (
nVars() <= index) {
467 d_level .resize(index + 1, -1);
483 vector<Lit> literals;
484 literals.push_back(p);
489 vector<MiniSat::Lit> literals;
493 if (isTheoryClause) clauseID = -clauseID;
508 vector<Lit> literals;
509 for (
int i = 0; i < clause.
size(); ++i) {
510 literals.push_back(clause[i]);
533 for (i = cnf.
begin(), iend = cnf.
end(); i != iend; i++) {
547 for (
size_type i = 1; i < literals.size(); i++){
548 if (literals[i-1] == ~literals[i]){
555 for (i = j = 0; i < literals.size(); i++) {
568 literals[j++] = literals[i];
589 if (literals.size() >= 2) {
591 int levelFirst =
getLevel(literals[first]);
594 int levelSecond =
getLevel(literals[second]);
596 for (
size_type i = 2; i < literals.size(); i++) {
602 int levelNew =
getLevel(literals[i]);
608 if (levelFirst > levelSecond) {
609 second = i; levelSecond = levelNew; valueSecond = valueNew;
611 first = i; levelFirst = levelNew; valueFirst = valueNew;
614 else if (valueFirst ==
l_False) {
615 first = i; levelFirst = levelNew; valueFirst = valueNew;
618 second = i; levelSecond = levelNew; valueSecond = valueNew;
624 if ((levelNew > levelFirst) && (levelNew > levelSecond)) {
625 if (levelSecond > levelFirst) {
626 first = i; levelFirst = levelNew; valueFirst = valueNew;
629 second = i; levelSecond = levelNew; valueSecond = valueNew;
632 else if (levelNew > levelFirst) {
633 first = i; levelFirst = levelNew; valueFirst = valueNew;
635 else if (levelNew > levelSecond) {
636 second = i; levelSecond = levelNew; valueSecond = valueNew;
639 else if (valueFirst ==
l_False) {
640 if (levelNew > levelFirst) {
641 first = i; levelFirst = levelNew; valueFirst = valueNew;
645 if (levelNew > levelSecond) {
646 second = i; levelSecond = levelNew; valueSecond = valueNew;
652 Lit swap = literals[0]; literals[0] = literals[first]; literals[first] = swap;
653 swap = literals[1]; literals[1] = literals[second]; literals[second] = swap;
665 Lit swap = literals[0]; literals[0] = literals[1]; literals[1] = swap;
673 std::sort(literals.begin(), literals.end());
676 vector<Lit>::iterator end = std::unique(literals.begin(), literals.end());
677 literals.erase(end, literals.end());
680 for (vector<Lit>::const_iterator i = literals.begin(); i != literals.end(); ++i){
685 vector<Lit> simplified(literals);
687 bool replaceReason =
false;
696 replaceReason =
true;
705 if (
getDerivation() != NULL && simplified.size() < literals.size()) {
714 for (
size_type i = 0; i < literals.size(); ++i) {
716 if (j >= simplified.size() || literals[i] != simplified[j]) {
717 inference->
add(literals[i],
getDerivation()->computeRootReason(~literals[i],
this));
733 if (simplified.size() < literals.size()) {
736 c =
Clause_new(simplified, theorem, clauseID);
777 if (c->
size() == 1) {
791 "MiniSat::Solver::insertClause: first literal of new lemma not undefined");
793 for (
int i = 1; i < c->
size(); ++i) {
795 "MiniSat::Solver::insertClause: lemma literal not false");
802 for (
int i = 2; i < c->
size(); i++) {
809 (*c)[1] = (*c)[max_i];
823 for (
int i = 1; i < c->
size(); ++i) {
825 "MiniSat::Solver::insertClause: bogus conflicting clause");
836 "MiniSat::Solver::insertClause: bogus propagating clause");
838 for (
int i = 1; i < c->
size(); ++i) {
840 "MiniSat::Solver::insertClause: bogus propagating clause");
844 DebugAssert(
false,
"MiniSat::Solver::insertClause: conflicting/implying clause");
871 if (!just_dealloc && c->
size() >= 2){
890 if (ws.size() == 0)
return;
892 for (; ws[j] != elem; j++) {
895 DebugAssert(j < ws.size(),
"MiniSat::Solver::removeWatch: elem not in watched list");
914 for (
int i = 1; i < clause.
size(); ++i) {
916 "MiniSat::Solver::getImplicationLevelFull: literal not false");
921 if (newLevel == currentLevel)
925 if (newLevel > maxLevel)
938 for (
int i = 0; i < clause.
size(); ++i) {
942 if (newLevel > decisionLevel)
943 decisionLevel = newLevel;
954 if (!_resolveTheoryImplication)
957 DebugAssert(reason != NULL,
"MiniSat::getReason: reason[var] == NULL.");
968 "MiniSat::getReason: reason[var] == TheoryImplication.");
978 DebugAssert(clause != NULL,
"MiniSat::updateConflict: clause == NULL.");
980 for (
int i = 0; i < clause->
size(); ++i) {
1005 stack<Lit> toRegress;
1006 stack<Clause*> toComplete;
1007 toRegress.push(literal);
1010 while (!toRegress.empty()) {
1012 literal = toRegress.top();
1014 "MiniSat::Solver::resolveTheoryImplication: literal is not true");
1021 for (
int i = 0; i < (*explanation).size(); ++i) {
1022 if ((*explanation)[i] == literal) {
1024 (*explanation)[0] = (*explanation)[i];
1025 (*explanation)[i] = swap;
1032 "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 1");
1034 "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 2");
1035 for (
int i = 1; i < (*explanation).size(); ++i) {
1037 "MiniSat::Solver::resolveTheoryImplication: literal not implied by clause 3");
1044 for (
int i = 1; i < (*explanation).size(); ++i) {
1046 toRegress.push((*explanation)[i]);
1050 toComplete.push(explanation);
1055 while (!toComplete.empty()) {
1056 Clause* explanation = toComplete.top();
1060 for (
int i = 1; i < explanation->
size(); ++i) {
1062 "MiniSat::Solver::resolveTheoryImplication: not done to completion");
1068 setLevel((*explanation)[0], level);
1069 setPushID((*explanation)[0].var(), explanation);
1149 int index =
d_trail.size() - 1;
1151 vector<Lit> out_learnt;
1168 int pushID = confl->
pushID();
1171 if (confl->size() == 1) {
1172 out_learnt.push_back((*confl)[0]);
1185 for (
int j = (p ==
lit_Undef) ? 0 : 1; j < confl->size(); j++){
1186 Lit q = (*confl)[j];
1188 DebugAssert(
getLevel(q) <= UIPLevel,
"MiniSat::Solver::analyze: literal above UIP level");
1208 out_learnt.push_back(q);
1216 if (pathC == 0)
break;
1228 DebugAssert(index >= -1,
"MiniSat::Solver::analyze: index out of bound");
1236 pushID =
max(pushID, confl->pushID());
1238 }
while (pathC > 0);
1246 ||
getLevel(out_learnt[0]) == UIPLevel,
1247 "MiniSat::Solver::analyze: backtracked past UIP level.");
1248 for (
size_type i = 1; i < out_learnt.size(); ++i) {
1250 "MiniSat::Solver::analyze: conflict clause contains literal from UIP level or higher.");
1257 for (vector<Lit>::const_iterator j = out_learnt.begin(); j != out_learnt.end(); ++j) {
1265 return Lemma_new(out_learnt, clauseID, pushID);
1271 lastToFirst_lt(
const vector<MiniSat::size_type>& trail_pos) : d_trail_pos(trail_pos) {}
1274 return d_trail_pos[p.
var()] > d_trail_pos[q.
var()];
1280 if (out_learnt.size() > 1) {
1292 unsigned int min_level = 0;
1293 for (i = 1; i < out_learnt.size(); i++)
1294 min_level |= 1 << (
getLevel(out_learnt[i]) & 31);
1296 for (i = j = 1; i < out_learnt.size(); i++) {
1297 Lit lit(out_learnt[i]);
1299 out_learnt[j++] = lit;
1307 for (i = j = 1; i < out_learnt.size(); i++) {
1308 Lit lit(out_learnt[i]);
1311 out_learnt[j++] = lit;
1315 for (
int k = 1; !keep && k < c.
size(); k++) {
1324 out_learnt[j++] = lit;
1335 out_learnt.resize(j);
1357 if (out_learnt.size() > 0
1367 out_learnt.push_back(lit);
1382 inference->
add(lit, reason);
1404 "MiniSat::Solver::analyze_removable: stack var is a decision.");
1406 "MiniSat::Solver::analyze_removable: stack var is an unresolved theory implication.");
1408 for (
int i = 1; i < c.size(); i++) {
1459 for (
int i = 0; i < c->
size(); i++){
1491 int trail_size =
d_trail.size();
1494 for (
int c = first_invalid; c < trail_size; ++c) {
1511 d_trail.resize(first_invalid);
1543 if (pair.first > toLevel) {
1545 remove(pair.second,
true);
1703 vector<Clause*>::iterator j = ws.begin();
1704 vector<Clause*>::iterator i = ws.begin();
1705 vector<Clause*>::iterator end = ws.end();
1712 if (c[0] == false_lit) {
1723 "MiniSat::Solver:::propagate: True/False");
1728 for (
int k = 2; k < c.
size(); k++) {
1741 for (
int z = 1; z < c.
size(); ++z) {
1743 "MiniSat::Solver:::propagate: Unit Propagation");
1754 if (i != j) ws.erase(j, i);
1763 ws.erase(j, ws.end());
1788 for (i = j = 0; i <
d_learnts.size() / 2; i++){
1828 "MiniSat::Solver::simplifyDB: called while propagation queue was not empty");
1857 for (
int type = 0; type < 2; type++){
1860 bool satisfied =
false;
1861 for (vector<Clause*>::const_iterator i = cs.begin(); i != cs.end(); ++i) {
1872 int end = clause->
size() - 1;
1881 "MiniSat::Solver::simplifyDB: permanently falsified clause found");
1886 Lit lit((*clause)[k]);
1901 (*clause)[k] = (*clause)[end];
1902 (*clause)[end] = lit;
1952 vector<Var> nextVars(prop_lookahead);
1954 while (fetchedVars < nextVars.size()) {
1957 nextVars[fetchedVars] = nextVar;
1969 int first_invalid =
d_trail.size();
1972 Var nextVar = nextVars[i];
1975 for (
int sign = 0; sign < 2; ++sign) {
1991 for (
int i =
d_trail.size() - 1; i >= first_invalid; --i) {
1997 d_trail.resize(first_invalid);
2033 "MiniSat::Solver::search: qhead >= trail_lim[decisionLevel()");
2035 "MiniSat::Solver::search: thead >= trail_lim[decisionLevel()");
2060 int backtrack_level;
2062 backtrack(backtrack_level, learnt_clause);
2064 cout <<
"conflict clause: " <<
toString(*learnt_clause,
true);
2071 cout <<
"backtrack to: " << backtrack_level <<
endl;
2078 cout <<
"theory inconsistency: " <<
endl;
2126 cout <<
"theory clauses: " <<
endl;
2141 cout <<
"theory implication: " << lit.
index() <<
endl;
2153 cout <<
"theory implication reason: " <<
endl;
2185 next = ~
Lit(nextVar,
false);
2192 if (
false && d_simpDB_props <= 0 && d_simpDB_assigns > (
nAssigns() / 10)) {
2194 DebugAssert(
d_ok,
"MiniSat::Solver::search: simplifyDB resulted in conflict");
2213 "MiniSat::Solver::search not undefined split variable chosen.");
2216 cout <<
"Split: " << next.
index() <<
endl;
2228 DebugAssert(
false,
"MiniSat::Solver::search contradictory split variable chosen.");
2238 cout <<
"theory conflict (FULL): " <<
endl;
2256 cout <<
"theory clauses: " <<
endl;
2270 "DPLLTMiniSat::search: consistent result, but decider not done yet.");
2272 "DPLLTMiniSat::search: consistent result, but not all clauses satisfied.");
2276 FatalAssert(
false,
"DPLLTMiniSat::search: unreachable");
2291 for (
int i = 0; i <
nVars(); i++)
2300 for (vector<Clause*>::const_iterator i =
d_learnts.begin(); i !=
d_learnts.end(); i++) {
2301 (*i)->setActivity((*i)->activity() * (float)1e-20);
2318 int size = clause.
size();
2319 bool satisfied =
false;
2320 for (
int j = 0; j < size; ++j) {
2327 cout <<
"Clause not satisfied:" <<
endl;
2330 for (
int j = 0; j < size; ++j) {
2331 Lit lit = clause[j];
2333 const vector<Clause*>& ws =
getWatches(~lit);
2337 for (
size_type j = 0; !found && j < ws.size(); ++j) {
2338 if (ws[j] == &clause) {
2348 cout <<
"not watched: " <<
toString(lit,
true) <<
endl;
2361 if (clause.
size() < 2)
return;
2363 for (
int i = 0; i < 2; ++i) {
2364 Lit lit = clause[i];
2366 const vector<Clause*>& ws =
getWatches(~lit);
2372 for (
size_type j = 0; !found && j < ws.size(); ++j) {
2373 if (ws[j] == &clause) found =
true;
2379 FatalAssert(
false,
"MiniSat::Solver::checkWatched");
2400 if (clause.
size() < 2)
return;
2417 for (
int j = 1; ok && j < clause.
size(); ++j) {
2429 FatalAssert(
false,
"MiniSat::Solver::checkClause");
2460 const Clause& clause = *reason;
2463 FatalAssert(clause.
size() > 0,
"MiniSat::Solver::checkTrail: empty clause as reason for " );
2464 FatalAssert(lit == clause[0],
"MiniSat::Solver::checkTrail: incorrect reason for " );
2468 for (
int j = 1; j < clause.
size(); ++j) {
2469 Lit clauseLit = clause[j];
2470 Var clauseVar = clauseLit.
var();
2472 "MiniSat::Solver::checkTrail: depends on later asserted literal " );
2476 if (
d_trail[k] == ~clauseLit) {
2481 FatalAssert(found,
"MiniSat::Solver::checkTrail: depends on literal not in context " );
2502 for (
int i = 1; i < from->
size(); ++i) {
2528 remove(lemma,
true);
2559 cout <<
"theory implication: " << lit.
index() <<
endl;
2571 cout <<
"theory implication reason: " <<
endl;
2588 cout <<
"theory clauses: " <<
endl;
2649 while (i != clauses.size()) {
2651 if (clauses[i]->pushID() >= 0
2653 clauses[i]->pushID() <= pushEntry.
d_clauseID) {
2662 clauses[i] = clauses.back();
2677 DebugAssert(!
d_ok,
"Minisat::Solver::pop: inconsistent push, but d_ok == true");
2698 d_trail.resize(first_invalid);
2736 if (lemma->
size() >= 2) {
2769 if (pushEntry.
d_ok) {
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)
const_iterator begin() const
std::string toString() const
std::vector< Clause * > d_clauses
const Lit lit_Undef(var_Undef, false)
Clause * getReason(Var var) const
double d_cla_inc
heuristics
const bool defer_theory_propagation
void checkClause(const Clause &clause) const
std::vector< std::vector< SAT::Lit > > curClauses()
std::vector< signed char > d_assigns
void propLookahead(const SearchParams ¶ms)
void toLit(std::vector< Lit > &literals) const
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.
const bool eager_explanation
theory implications
void addFormula(const SAT::CNF_Formula &cnf, bool isTheoryClause)
void orderClause(std::vector< Lit > &literals) const
SAT::DPLLT::Decider * d_decider
void registerInputClause(int clauseID)
static void xfree(T *ptr)
void setPushID(Var var, Clause *from)
lastToFirst_lt(const vector< MiniSat::size_type > &trail_pos)
bool isConflicting() const
bool isConsistent() const
void insertClause(Clause *clause)
void registerClause(Clause *clause)
#define DebugAssert(cond, str)
const bool keep_lazy_explanation
Clause * Lemma_new(const vector< Lit > &ps, int id, int pushID)
void backtrack(int level, Clause *clause)
void add(Lit lit, int clauseID)
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
virtual bool outOfResources()=0
Check if the work budget has been exceeded.
bool enqueue(Lit fact, int decisionLevel, Clause *reason)
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void insertLemma(const Clause *lemma, int clauseID, int pushID)
std::vector< Clause * > d_reason
void checkWatched() const
int getPushID(Var var) const
std::vector< Clause * > d_popLemmas
CVC3::Theorem getClauseTheorem() const
CVC3::Theorem getTheorem() const
SAT::DPLLT::TheoryAPI * d_theoryAPI
CVC interface.
const vector< MiniSat::size_type > & d_trail_pos
Clause * Clause_new(const vector< Lit > &ps, CVC3::Theorem theorem, int id)
void updateConflict(Clause *clause)
void registerInference(int clauseID, Inference *inference)
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
std::vector< Lit > d_trail
void finish(Clause *clause, Solver *solver)
unsigned int d_popRequests
static Clause * TheoryImplication()
std::vector< Clause * > d_learnts
std::vector< std::vector< Clause * > > d_watches
variable assignments, and pending propagations
const bool push_theory_propagation
pushes
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)
const vector< Var >::size_type prop_lookahead
virtual bool getNewClauses(CNF_Formula &cnf)=0
Get new clauses from the theory.
void registerVar(Var var)
Operations on clauses:
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
void remove(Clause *c, bool just_dealloc=false)
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.
virtual void getExplanation(Lit l, CNF_Formula &c)=0
Get an explanation for a literal that was implied.
const_iterator end() const
std::vector< Lit >::const_iterator const_iterator
void varBumpActivity(Lit p)
Activity:
static Clause * Decision()
int getLevel(Var var) const
CVC3::QueryResult search()
search
SearchParams d_default_params
Mode of operation:
void removedClause(Clause *clause)
int decisionLevel() const
Search:
Derivation * getDerivation()
virtual Lit getImplication()=0
Get a literal that is implied by the current assignment.
bool allClausesSatisfied()
debugging
std::vector< int > d_trail_lim
const std::vector< Lit > & getTrail() const
bool isPermSatisfied(Clause *c) const
virtual void push()=0
Set a checkpoint for backtracking.
Var select(double random_freq=.0)
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)
virtual void pop()=0
Restore most recent checkpoint.
virtual Lit makeDecision()=0
Make a decision.
void removeWatch(std::vector< Clause * > &ws, Clause *elem)
Conflict handling.
void varRescaleActivity()
Activity.
virtual void assertLit(Lit l)=0
Notify theory when a literal is set to true.
std::vector< int > d_level
void setActivity(float activity)
const bool push_theory_clause
std::vector< int >::size_type size_type
Adaptation of MiniSat to DPLL(T)
const bool push_theory_implication
virtual ConsistentResult checkConsistent(CNF_Formula &cnf, bool fullEffort)=0
Check consistency of the current assignment.
const std::vector< Clause * > & getClauses() const
lbool getValue(Var x) const
clauses / assignment