diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/prop | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 37 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 11 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 407 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 82 | ||||
-rw-r--r-- | src/prop/bvminisat/core/SolverTypes.h | 27 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 20 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 20 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 212 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 58 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 132 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 61 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 37 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 41 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 5 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 12 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 30 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 9 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 19 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 4 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 3 |
20 files changed, 860 insertions, 367 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index be266b6d8..936778e0d 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -19,6 +19,7 @@ #include "prop/bvminisat/bvminisat.h" #include "prop/bvminisat/simp/SimpSolver.h" +#include "proof/sat_proof.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -47,14 +48,18 @@ void BVMinisatSatSolver::setNotify(Notify* notify) { d_minisat->setNotify(d_minisatNotify); } -void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { +ClauseId BVMinisatSatSolver::addClause(SatClause& clause, + bool removable) { Debug("sat::minisat") << "Add clause " << clause <<"\n"; BVMinisat::vec<BVMinisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); // for(unsigned i = 0; i < minisat_clause.size(); ++i) { // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); // } - d_minisat->addClause(minisat_clause); + ClauseId clause_id = ClauseIdError; + d_minisat->addClause(minisat_clause, clause_id); + THEORY_PROOF(Assert (clause_id != ClauseIdError);); + return clause_id; } SatValue BVMinisatSatSolver::propagate() { @@ -91,6 +96,10 @@ void BVMinisatSatSolver::popAssumption() { d_minisat->popAssumption(); } +void BVMinisatSatSolver::setProofLog( BitVectorProof * bvp ) { + d_minisat->setProofLog( bvp ); +} + SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ return d_minisat->newVar(true, true, !canErase); } @@ -126,6 +135,10 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } +bool BVMinisatSatSolver::ok() const { + return d_minisat->okay(); +} + void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { // TODO add assertion to check the call was after an unsat call for (int i = 0; i < d_minisat->conflict.size(); ++i) { @@ -199,8 +212,8 @@ void BVMinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, - SatClause& sat_clause) { +void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause, + SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); } @@ -281,3 +294,19 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ } /* namespace CVC4::prop */ } /* namespace CVC4 */ + +namespace CVC4 { +template<> +prop::SatLiteral toSatLiteral< BVMinisat::Solver>(BVMinisat::Solver::TLit lit) { + return prop::BVMinisatSatSolver::toSatLiteral(lit); +} + +template<> +void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl, + prop::SatClause& sat_cl) { + prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl); +} + +} + + diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 986fbf339..383948e3e 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -43,7 +43,9 @@ private: } void notify(BVMinisat::vec<BVMinisat::Lit>& clause) { SatClause satClause; - toSatClause(clause, satClause); + for (int i = 0; i < clause.size(); ++i) { + satClause.push_back(toSatLiteral(clause[i])); + } d_notify->notify(satClause); } @@ -73,7 +75,7 @@ public: void setNotify(Notify* notify); - void addClause(SatClause& clause, bool removable, uint64_t proof_id); + ClauseId addClause(SatClause& clause, bool removable); SatValue propagate(); @@ -88,6 +90,7 @@ public: SatValue solve(); SatValue solve(long unsigned int&); + bool ok() const; void getUnsatCore(SatClause& unsatCore); SatValue value(SatLiteral l); @@ -106,7 +109,7 @@ public: static SatValue toSatLiteralValue(BVMinisat::lbool res); static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); - static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); + static void toSatClause (const BVMinisat::Clause& clause, SatClause& sat_clause); void addMarkerLiteral(SatLiteral lit); void explain(SatLiteral lit, std::vector<SatLiteral>& explanation); @@ -114,6 +117,8 @@ public: SatValue assertAssumption(SatLiteral lit, bool propagate); void popAssumption(); + + void setProofLog( BitVectorProof * bvp ); private: /* Disable the default constructor. */ diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 5a37da27c..2100160de 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -31,6 +31,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "options/bv_options.h" #include "options/smt_options.h" #include "theory/interrupted.h" +#include "proof/proof_manager.h" +#include "proof/bitvector_proof.h" +#include "proof/sat_proof.h" +#include "proof/sat_proof_implementation.h" #include "util/utility.h" namespace CVC4 { @@ -60,19 +64,6 @@ std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) { static const char* _cat = "CORE"; -// static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); -// static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); -// static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true)); -// static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false)); -// static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2)); -// static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); -// static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); -// static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); -// static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); -// static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false)); -// static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); - - static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false)); static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true)); @@ -86,6 +77,12 @@ static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interv static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); //================================================================================================= +// Proof declarations +CRef Solver::TCRef_Undef = CRef_Undef; +CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here + + +//================================================================================================= // Constructor/Destructor: @@ -150,6 +147,7 @@ Solver::Solver(CVC4::context::Context* c) : , conflict_budget (-1) , propagation_budget (-1) , asynch_interrupt (false) + , d_bvp (NULL) { // Create the constant variables varTrue = newVar(true, false); @@ -193,37 +191,114 @@ Var Solver::newVar(bool sign, bool dvar) } -bool Solver::addClause_(vec<Lit>& ps) +bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) { if (decisionLevel() > 0) { cancelUntil(0); } - if (!ok) return false; + if (!ok) { + id = ClauseIdUndef; + return false; + } // Check if clause is satisfied and remove false/duplicate literals: + // TODO proof for duplicate literals removal? sort(ps); Lit p; int i, j; - for (i = j = 0, p = lit_Undef; i < ps.size(); i++) - if (value(ps[i]) == l_True || ps[i] == ~p) - return true; - else if (value(ps[i]) != l_False && ps[i] != p) - ps[j++] = p = ps[i]; + int falseLiteralsCount = 0; + + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { + // tautologies are ignored + if (value(ps[i]) == l_True || ps[i] == ~p) { + id = ClauseIdUndef; + return true; + } + + // Ignore repeated literals + if (ps[i] == p) { + continue; + } + + if (value(ps[i]) == l_False) { + if (!THEORY_PROOF_ON()) + continue; + ++falseLiteralsCount; + } + ps[j++] = p = ps[i]; + } + ps.shrink(i - j); clause_added = true; - if (ps.size() == 0) + Assert(falseLiteralsCount == 0 || THEORY_PROOF_ON()); + + if(falseLiteralsCount == 0) { + if (ps.size() == 0) { + Assert (!THEORY_PROOF_ON()); return ok = false; - else if (ps.size() == 1){ + } + else if (ps.size() == 1){ + if(d_bvp){ id = d_bvp->getSatProof()->registerUnitClause(ps[0], INPUT);} uncheckedEnqueue(ps[0]); - return ok = (propagate() == CRef_Undef); - } else { + CRef confl_ref = propagate(); + ok = (confl_ref == CRef_Undef); + if(d_bvp){ if (!ok) d_bvp->getSatProof()->finalizeProof(confl_ref); } + return ok; + } else { CRef cr = ca.alloc(ps, false); clauses.push(cr); attachClause(cr); + if(d_bvp){ id = d_bvp->getSatProof()->registerClause(cr, INPUT);} + } + return ok; } - return ok; + + if (falseLiteralsCount != 0 && THEORY_PROOF_ON()) { + // we are in a conflicting state + if (ps.size() == falseLiteralsCount && falseLiteralsCount == 1) { + if(d_bvp){ id = d_bvp->getSatProof()->storeUnitConflict(ps[0], INPUT); } + if(d_bvp){ d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy); } + return ok = false; + } + + assign_lt lt(*this); + sort(ps, lt); + + CRef cr = ca.alloc(ps, false); + clauses.push(cr); + attachClause(cr); + + if(d_bvp){id = d_bvp->getSatProof()->registerClause(cr, INPUT);} + + if(ps.size() == falseLiteralsCount) { + if(d_bvp){ d_bvp->getSatProof()->finalizeProof(cr); } + return ok = false; + } + + // Check if it propagates + if (ps.size() == falseLiteralsCount + 1) { + Clause& cl = ca[cr]; + + Assert (value(cl[0]) == l_Undef); + uncheckedEnqueue(cl[0], cr); + Assert (cl.size() > 1); + CRef confl = propagate(); + ok = (confl == CRef_Undef); + if(!ok) { + if(d_bvp){ + if(ca[confl].size() == 1) { + id = d_bvp->getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); + d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy); + } else { + d_bvp->getSatProof()->finalizeProof(confl); + } + } + } + } + } + return ok; } void Solver::attachClause(CRef cr) { @@ -237,6 +312,8 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; + if(d_bvp){ d_bvp->getSatProof()->markDeleted(cr); } + assert(c.size() > 1); if (strict){ @@ -342,6 +419,9 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip int index = trail.size() - 1; bool done = false; + + if(d_bvp){ d_bvp->getSatProof()->startResChain(confl); } + do{ assert(confl != CRef_Undef); // (otherwise should be UIP) Clause& c = ca[confl]; @@ -352,7 +432,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ Lit q = c[j]; - if (!seen[var(q)] && level(var(q)) > 0){ + if (!seen[var(q)] && level(var(q)) > 0) { varBumpActivity(var(q)); seen[var(q)] = 1; if (level(var(q)) >= decisionLevel()) @@ -360,6 +440,10 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip else out_learnt.push(q); } + + if (level(var(q)) == 0) { + if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(q); } + } } // Select next clause to look at: @@ -369,6 +453,10 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip seen[var(p)] = 0; pathC--; + if ( pathC > 0 && confl != CRef_Undef ) { + if(d_bvp){ d_bvp->getSatProof()->addResolutionStep(p, confl, sign(p));} + } + switch (uip) { case UIP_FIRST: done = pathC == 0; @@ -392,11 +480,22 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - for (i = j = 1; i < out_learnt.size(); i++) - if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) + for (i = j = 1; i < out_learnt.size(); i++) { + if (reason(var(out_learnt[i])) == CRef_Undef) { + out_learnt[j++] = out_learnt[i]; + } else { + // Check if the literal is redundant + if (!litRedundant(out_learnt[i], abstract_level)) { + // Literal is not redundant out_learnt[j++] = out_learnt[i]; + } else { + if(d_bvp){ d_bvp->getSatProof()->storeLitRedundant(out_learnt[i]); } + } + } + } }else if (ccmin_mode == 1){ + Unreachable(); for (i = j = 1; i < out_learnt.size(); i++){ Var x = var(out_learnt[i]); @@ -452,10 +551,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ - assert(reason(var(analyze_stack.last())) != CRef_Undef); - Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop(); + CRef c_reason = reason(var(analyze_stack.last())); + assert(c_reason != CRef_Undef); + Clause& c = ca[c_reason]; + int c_size = c.size(); + analyze_stack.pop(); - for (int i = 1; i < c.size(); i++){ + for (int i = 1; i < c_size; i++){ Lit p = c[i]; if (!seen[var(p)] && level(var(p)) > 0){ if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ @@ -495,21 +597,36 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { seen[var(cl[i])] = 1; } - for (int i = trail.size() - 1; i >= trail_lim[0]; i--) { + int end = options::proof() ? 0 : trail_lim[0]; + for (int i = trail.size() - 1; i >= end; i--) { Var x = var(trail[i]); if (seen[x]) { if (reason(x) == CRef_Undef) { // we skip p if was a learnt unit if (x != var(p)) { - assert (marker[x] == 2); - assert (level(x) > 0); - out_conflict.push(~trail[i]); + if (marker[x] == 2) { + assert (level(x) > 0); + out_conflict.push(~trail[i]); + } else { + if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); } + } + } else { + if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} } } else { Clause& c = ca[reason(x)]; - for (int j = 1; j < c.size(); j++) + if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));} + + for (int j = 1; j < c.size(); j++) { if (level(var(c[j])) > 0) seen[var(c[j])] = 1; + if(d_bvp){ + if (level(var(c[j])) == 0) { + d_bvp->getSatProof()->resolveOutUnit(c[j]); + seen[var(c[j])] = 0; // we don't need to resolve it out again + } + } + } } seen[x] = 0; } @@ -534,12 +651,23 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) out_conflict.push(p); } - if (decisionLevel() == 0) - return; + if(d_bvp){ + if (level(var(p)) == 0 && d_bvp->isAssumptionConflict()) { + Assert ( marker[var(p)] == 2); + if (reason(var(p)) == CRef_Undef) { + d_bvp->startBVConflict(p); + } + } + } + + if (decisionLevel() == 0 && !options::proof()) { + return; + } seen[var(p)] = 1; - - for (int i = trail.size()-1; i >= trail_lim[0]; i--){ + int end = options::proof() ? 0 : trail_lim[0]; + + for (int i = trail.size()-1; i >= end; i--){ Var x = var(trail[i]); if (seen[x]) { if (reason(x) == CRef_Undef) { @@ -548,9 +676,24 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) out_conflict.push(~trail[i]); } else { Clause& c = ca[reason(x)]; - for (int j = 1; j < c.size(); j++) - if (level(var(c[j])) > 0) + if(d_bvp){ + if (d_bvp->isAssumptionConflict() && + trail[i] == p) { + d_bvp->startBVConflict(reason(x)); + } else { + d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i])); + } + } + for (int j = 1; j < c.size(); j++) { + if (level(var(c[j])) > 0) { seen[var(c[j])] = 1; + } + if(d_bvp){ + if (level(var(c[j])) == 0) { + d_bvp->getSatProof()->resolveOutUnit(c[j]); + } + } + } } seen[x] = 0; } @@ -588,9 +731,12 @@ lbool Solver::propagateAssumptions() { } lbool Solver::assertAssumption(Lit p, bool propagate) { + // TODO need to somehow mark the assumption as unit in the current context? + // it's not always unit though, but this would be useful for debugging // assert(marker[var(p)] == 1); + if (decisionLevel() > assumptions.size()) { cancelUntil(assumptions.size()); } @@ -601,7 +747,8 @@ lbool Solver::assertAssumption(Lit p, bool propagate) { if (c->getLevel() > 0) { assumptions.push(p); } else { - if (!addClause(p)) { + ClauseId id; + if (!addClause(p, id)) { conflict.push(~p); return l_False; } @@ -618,6 +765,14 @@ lbool Solver::assertAssumption(Lit p, bool propagate) { } } +void Solver::addMarkerLiteral(Var var) { + // make sure it wasn't already marked + Assert(marker[var] == 0); + marker[var] = 1; + if(d_bvp){d_bvp->getSatProof()->registerAssumption(var);} +} + + /*_________________________________________________________________________________________________ | | propagate : [void] -> [Clause*] @@ -730,8 +885,13 @@ void Solver::removeSatisfied(vec<CRef>& cs) int i, j; for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; - if (satisfied(c)) + if (satisfied(c)) { + if (locked(c)) { + // store a resolution of the literal c propagated + if(d_bvp){ d_bvp->getSatProof()->storeUnitResolution(c[0]); } + } removeClause(cs[i]); + } else cs[j++] = cs[i]; } @@ -807,7 +967,12 @@ lbool Solver::search(int nof_conflicts, UIP uip) if (confl != CRef_Undef){ // CONFLICT conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; + + if (decisionLevel() == 0) { + // can this happen for bv? + if(d_bvp){ d_bvp->getSatProof()->finalizeProof(confl);} + return l_False; + } learnt_clause.clear(); analyze(confl, learnt_clause, backtrack_level, uip); @@ -821,15 +986,42 @@ lbool Solver::search(int nof_conflicts, UIP uip) learnts.push(cr); attachClause(cr); claBumpActivity(ca[cr]); + if(d_bvp){ + ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT); + PSTATS( + __gnu_cxx::hash_set<int> cl_levels; + for (int i = 0; i < learnt_clause.size(); ++i) { + cl_levels.insert(level(var(learnt_clause[i]))); + } + if( d_bvp ){ d_bvp->getSatProof()->storeClauseGlue(id, cl_levels.size()); } + ) + d_bvp->getSatProof()->endResChain(id); + } } - + + if (learnt_clause.size() == 1) { + // learning a unit clause + if(d_bvp){ d_bvp->getSatProof()->endResChain(learnt_clause[0]);} + } + // if the uip was an assumption we are unsat if (level(var(p)) <= assumptions.size()) { for (int i = 0; i < learnt_clause.size(); ++i) { assert (level(var(learnt_clause[i])) <= decisionLevel()); seen[var(learnt_clause[i])] = 1; } + + // Starting new resolution chain for bit-vector proof + if( d_bvp ){ + if (cr == CRef_Undef) { + d_bvp->startBVConflict(learnt_clause[0]); + } + else { + d_bvp->startBVConflict(cr); + } + } analyzeFinal(p, conflict); + if(d_bvp){ d_bvp->endBVConflict(conflict); } Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl; return l_False; } @@ -843,7 +1035,10 @@ lbool Solver::search(int nof_conflicts, UIP uip) CRef new_confl = propagate(); if (new_confl != CRef_Undef) { // we have a conflict we now need to explain it - analyzeFinal2(p, new_confl, conflict); + // TODO: proof for analyzeFinal2 + if(d_bvp){ d_bvp->startBVConflict(new_confl); } + analyzeFinal2(p, new_confl, conflict); + if(d_bvp){ d_bvp->endBVConflict(conflict); } return l_False; } } @@ -912,7 +1107,10 @@ lbool Solver::search(int nof_conflicts, UIP uip) newDecisionLevel(); }else if (value(p) == l_False){ marker[var(p)] = 2; + + if(d_bvp){ d_bvp->markAssumptionConflict(); } analyzeFinal(~p, conflict); + if(d_bvp){ d_bvp->endBVConflict(conflict); } Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl; return l_False; }else{ @@ -1044,39 +1242,76 @@ lbool Solver::solve_() // void Solver::explain(Lit p, std::vector<Lit>& explanation) { - vec<Lit> queue; - queue.push(p); - Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl; - __gnu_cxx::hash_set<Var> visited; - visited.insert(var(p)); + // top level fact, no explanation necessary + if (level(var(p)) == 0) { + if(d_bvp){ + // the only way a marker variable is + if (reason(var(p)) == CRef_Undef) { + d_bvp->startBVConflict(p); + vec<Lit> confl; + confl.push(p); + d_bvp->endBVConflict(confl); + return; + } + } + if (!THEORY_PROOF_ON()) + return; + } - while(queue.size() > 0) { - Lit l = queue.last(); - - Debug("bvminisat::explain") << OUTPUT_TAG << "processing " << l << std::endl; - - assert(value(l) == l_True); - queue.pop(); - if (reason(var(l)) == CRef_Undef) { - if (level(var(l)) == 0) continue; - Assert(marker[var(l)] == 2); - explanation.push_back(l); - visited.insert(var(l)); - } else { - Clause& c = ca[reason(var(l))]; - for (int i = 1; i < c.size(); ++i) { - if (level(var(c[i])) > 0 && visited.count(var(c[i])) == 0) { - queue.push(~c[i]); - visited.insert(var(c[i])); + seen[var(p)] = 1; + + // if we are called at decisionLevel = 0 trail_lim is empty + int bottom = options::proof() ? 0 : trail_lim[0]; + for (int i = trail.size()-1; i >= bottom; i--){ + Var x = var(trail[i]); + if (seen[x]) { + if (reason(x) == CRef_Undef) { + if (marker[x] == 2) { + assert(level(x) > 0); + explanation.push_back(trail[i]); + } else { + Assert (level(x) == 0); + if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); } + } + + } else { + Clause& c = ca[reason(x)]; + if(d_bvp){ + if (p == trail[i]) { + d_bvp->startBVConflict(reason(var(p))); + } else { + d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i])); + } + } + for (int j = 1; j < c.size(); j++) { + if (level(var(c[j])) > 0 || options::proof()) { + seen[var(c[j])] = 1; + } } } + seen[x] = 0; } } + seen[var(p)] = 0; + + if(d_bvp){ + vec<Lit> conflict_clause; + conflict_clause.push(p); + for(unsigned i = 0; i < explanation.size(); ++i) { + conflict_clause.push(~explanation[i]); + } + d_bvp->endBVConflict(conflict_clause); + } } - +void Solver::setProofLog( BitVectorProof * bvp ) { + d_bvp = bvp; + d_bvp->initSatProof(this); + d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false)); + d_bvp->getSatProof()->registerFalseLit(mkLit(varFalse, true)); +} //================================================================================================= // Writing CNF to DIMACS: @@ -1171,7 +1406,7 @@ void Solver::relocAll(ClauseAllocator& to) // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1); vec<Watcher>& ws = watches[p]; for (int j = 0; j < ws.size(); j++) - ca.reloc(ws[j].cref, to); + ca.reloc(ws[j].cref, to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); } // All reasons: @@ -1180,18 +1415,20 @@ void Solver::relocAll(ClauseAllocator& to) Var v = var(trail[i]); if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) - ca.reloc(vardata[v].reason, to); + ca.reloc(vardata[v].reason, to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); } // All learnt: // for (int i = 0; i < learnts.size(); i++) - ca.reloc(learnts[i], to); + ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); // All original: // for (int i = 0; i < clauses.size(); i++) - ca.reloc(clauses[i], to); + ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof()->getProxy() : NULL); + + if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); } } @@ -1208,5 +1445,25 @@ void Solver::garbageCollect() to.moveTo(ca); } +void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy) +{ + CRef old = cr; // save the old reference + + Clause& c = operator[](cr); + if (c.reloced()) { cr = c.relocation(); return; } + + cr = to.alloc(c, c.learnt()); + c.relocate(cr); + if (proxy) { + proxy->updateCRef(old, cr); + } + + // Copy extra data-fields: + // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) + to[cr].mark(c.mark()); + if (to[cr].learnt()) to[cr].activity() = c.activity(); + else if (to[cr].has_extra()) to[cr].calcAbstraction(); +} + } /* CVC4::BVMinisat namespace */ } /* CVC4 namespace */ diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 214e425f9..019c09bcd 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -26,13 +26,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Heap.h" #include "prop/bvminisat/mtl/Alg.h" #include "prop/bvminisat/utils/Options.h" - #include "context/cdhashmap.h" +#include "proof/sat_proof.h" #include <ext/hash_set> #include <vector> namespace CVC4 { + +typedef unsigned ClauseId; +namespace BVMinisat { +class Solver; +} + +class BitVectorProof; + namespace BVMinisat { /** Interface for minisat callbacks */ @@ -60,7 +68,17 @@ public: //================================================================================================= // Solver -- the main class: class Solver { - + friend class CVC4::TSatProof< CVC4::BVMinisat::Solver>; +public: + typedef Var TVar; + typedef Lit TLit; + typedef Clause TClause; + typedef CRef TCRef; + typedef vec<Lit> TLitVec; + + static CRef TCRef_Undef; + static CRef TCRef_Lazy; +private: /** To notify */ Notify* notify; @@ -89,12 +107,12 @@ public: Var falseVar() const { return varFalse; } - bool addClause (const vec<Lit>& ps); // Add a clause to the solver. + bool addClause (const vec<Lit>& ps, ClauseId& id); // Add a clause to the solver. bool addEmptyClause(); // Add the empty clause, making the solver contradictory. - bool addClause (Lit p); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps); // Add a clause to the solver without making superflous internal copy. Will + bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver. + bool addClause_( vec<Lit>& ps, ClauseId& id); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -188,16 +206,14 @@ public: // Bitvector Propagations // - void addMarkerLiteral(Var var) { - // make sure it wasn't already marked - Assert(marker[var] == 0); - marker[var] = 1; - } + void addMarkerLiteral(Var var); bool need_to_propagate; // true if we added new clauses, set to true in propagation bool only_bcp; // solving mode in which only boolean constraint propagation is done void setOnlyBCP (bool val) { only_bcp = val;} void explain(Lit l, std::vector<Lit>& explanation); + + void setProofLog( CVC4::BitVectorProof * bvp ); protected: @@ -274,6 +290,9 @@ protected: int64_t conflict_budget; // -1 means no budget. int64_t propagation_budget; // -1 means no budget. bool asynch_interrupt; + + //proof log + CVC4::BitVectorProof * d_bvp; // Main internal methods: // @@ -340,6 +359,35 @@ protected: // Returns a random integer 0 <= x < size. Seed must never be 0. static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); } + + // Less than for literals in an added clause when proofs are on. + struct assign_lt { + Solver& solver; + assign_lt(Solver& solver) : solver(solver) {} + bool operator () (Lit x, Lit y) { + lbool x_value = solver.value(x); + lbool y_value = solver.value(y); + // Two unassigned literals are sorted arbitrarily + if (x_value == l_Undef && y_value == l_Undef) { + return x < y; + } + // Unassigned literals are put to front + if (x_value == l_Undef) return true; + if (y_value == l_Undef) return false; + // Literals of the same value are sorted by decreasing levels + if (x_value == y_value) { + return solver.level(var(x)) > solver.level(var(y)); + } else { + // True literals go up front + if (x_value == l_True) { + return true; + } else { + return false; + } + } + } + }; + }; @@ -380,11 +428,11 @@ inline void Solver::checkGarbage(double gf){ // NOTE: enqueue does not set the ok flag! (only public methods do) inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } -inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } -inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); } -inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } -inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } -inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } +inline bool Solver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, id); } +inline bool Solver::addEmptyClause () { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, tmp); } +inline bool Solver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); } +inline bool Solver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); } +inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index aa0921b78..1fd7ac5a7 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -31,6 +31,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace CVC4 { namespace BVMinisat { +class Solver; +} +template <class Solver> class ProofProxy; +typedef ProofProxy<BVMinisat::Solver> BVProofProxy; +} + +namespace CVC4 { + +namespace BVMinisat { //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -205,6 +214,8 @@ public: const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef; +const CRef CRef_Lazy = RegionAllocator<uint32_t>::Ref_Undef - 1; + class ClauseAllocator : public RegionAllocator<uint32_t> { static int clauseWord32Size(int size, bool has_extra){ @@ -245,21 +256,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to) - { - Clause& c = operator[](cr); - - if (c.reloced()) { cr = c.relocation(); return; } - - cr = to.alloc(c, c.learnt()); - c.relocate(cr); - - // Copy extra data-fields: - // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) - to[cr].mark(c.mark()); - if (to[cr].learnt()) to[cr].activity() = c.activity(); - else if (to[cr].has_extra()) to[cr].calcAbstraction(); - } + void reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy = NULL); }; diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index c5b185c95..311ed1dd1 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "options/bv_options.h" #include "options/smt_options.h" #include "utils/System.h" +#include "proof/proof.h" namespace CVC4 { namespace BVMinisat { @@ -62,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : , asymm_lits (0) , eliminated_vars (0) , elimorder (1) - , use_simplification (true) + , use_simplification (!PROOF_ON()) , occurs (ClauseDeleted(ca)) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) @@ -162,7 +163,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps) +bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) { #ifndef NDEBUG for (int i = 0; i < ps.size(); i++) @@ -174,7 +175,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps)) + if (!Solver::addClause_(ps, id)) return false; if (use_simplification && clauses.size() == nclauses + 1){ @@ -544,9 +545,12 @@ bool SimpSolver::eliminateVar(Var v) // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent)) - return false; + for (int j = 0; j < neg.size(); j++) { + ClauseId id = -1; + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && + !addClause_(resolvent, id)) + return false; + } // Free occurs list for this variable: occurs[v].clear(true); @@ -582,8 +586,8 @@ bool SimpSolver::substitute(Var v, Lit x) } removeClause(cls[i]); - - if (!addClause_(subst_clause)) + ClauseId id; + if (!addClause_(subst_clause, id)) return ok = false; } diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 85556e935..5f6f46b91 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -42,12 +42,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool freeze = false); - bool addClause (const vec<Lit>& ps); + bool addClause (const vec<Lit>& ps, ClauseId& id); bool addEmptyClause(); // Add the empty clause to the solver. - bool addClause (Lit p); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps); + bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver. + bool addClause_( vec<Lit>& ps, ClauseId& id); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -178,11 +178,11 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } -inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); } -inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } -inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } +inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, id); } +inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); ClauseId id; return addClause_(add_tmp, id); } +inline bool SimpSolver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline lbool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index b3666875d..a3d411738 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -24,6 +24,7 @@ #include "options/bv_options.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" +#include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" @@ -47,7 +48,7 @@ namespace prop { CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, - bool fullLitToNodeMap) + bool fullLitToNodeMap, std::string name) : d_satSolver(satSolver), d_booleanVariables(context), d_nodeToLiteralMap(context), @@ -55,19 +56,21 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, d_fullLitToNodeMap(fullLitToNodeMap), d_convertAndAssertCounter(0), d_registrar(registrar), - d_assertionTable(context), + d_name(name), + d_cnfProof(NULL), d_globals(globals), d_removable(false) { } TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, - SmtGlobals* globals, bool fullLitToNodeMap) - : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap) + SmtGlobals* globals, bool fullLitToNodeMap, + std::string name) + : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap, name) {} -void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) { - Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl; +void CnfStream::assertClause(TNode node, SatClause& c) { + Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl; if(Dump.isOn("clauses")) { if(c.size() == 1) { Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr())); @@ -81,31 +84,41 @@ void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) { Dump("clauses") << AssertCommand(Expr(n.toExpr())); } } - //store map between clause and original formula - PROOF(ProofManager::currentPM()->setRegisteringFormula( node, proof_id ); ); - d_satSolver->addClause(c, d_removable, d_proofId); - PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); ); + + PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node);); + + ClauseId clause_id = d_satSolver->addClause(c, d_removable); + if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added) + + PROOF + ( + if (d_cnfProof) { + Assert (clause_id != ClauseIdError); + d_cnfProof->registerConvertedClause(clause_id); + d_cnfProof->popCurrentDefinition(); + } + ); } -void CnfStream::assertClause(TNode node, SatLiteral a, ProofRule proof_id) { +void CnfStream::assertClause(TNode node, SatLiteral a) { SatClause clause(1); clause[0] = a; - assertClause(node, clause, proof_id); + assertClause(node, clause); } -void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id) { +void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) { SatClause clause(2); clause[0] = a; clause[1] = b; - assertClause(node, clause, proof_id); + assertClause(node, clause); } -void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id) { +void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) { SatClause clause(3); clause[0] = a; clause[1] = b; clause[2] = c; - assertClause(node, clause, proof_id); + assertClause(node, clause); } bool CnfStream::hasLiteral(TNode n) const { @@ -116,7 +129,6 @@ bool CnfStream::hasLiteral(TNode n) const { void TseitinCnfStream::ensureLiteral(TNode n) { // These are not removable and have no proof ID d_removable = false; - d_proofId = uint64_t(-1); Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { @@ -165,7 +177,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) { } SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) { - Debug("cnf") << "newLiteral(" << node << ", " << isTheoryAtom << ")" << endl; + Debug("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom << ")" << endl; Assert(node.getKind() != kind::NOT); // Get the literal for this node @@ -200,10 +212,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister if (preRegister) { // In case we are re-entered due to lemmas, save our state bool backupRemovable = d_removable; - uint64_t backupProofId= d_proofId; + // Should be fine since cnfProof current assertion is stack based. d_registrar->preRegister(node); d_removable = backupRemovable; - d_proofId = backupProofId; } // Here, you can have it @@ -225,6 +236,11 @@ void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { } } +void CnfStream::setProof(CnfProof* proof) { + Assert (d_cnfProof == NULL); + d_cnfProof = proof; +} + SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; @@ -268,10 +284,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { SatLiteral xorLit = newLiteral(xorNode); - assertClause(xorNode.negate(), a, b, ~xorLit, RULE_TSEITIN); - assertClause(xorNode.negate(), ~a, ~b, ~xorLit, RULE_TSEITIN); - assertClause(xorNode, a, ~b, xorLit, RULE_TSEITIN); - assertClause(xorNode, ~a, b, xorLit, RULE_TSEITIN); + assertClause(xorNode.negate(), a, b, ~xorLit); + assertClause(xorNode.negate(), ~a, ~b, ~xorLit); + assertClause(xorNode, a, ~b, xorLit); + assertClause(xorNode, ~a, b, xorLit); return xorLit; } @@ -300,14 +316,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { // lit | ~(a_1 | a_2 | a_3 | ... | a_n) // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) for(unsigned i = 0; i < n_children; ++i) { - assertClause(orNode, orLit, ~clause[i], RULE_TSEITIN); + assertClause(orNode, orLit, ~clause[i]); } // lit -> (a_1 | a_2 | a_3 | ... | a_n) // ~lit | a_1 | a_2 | a_3 | ... | a_n clause[n_children] = ~orLit; // This needs to go last, as the clause might get modified by the SAT solver - assertClause(orNode.negate(), clause, RULE_TSEITIN); + assertClause(orNode.negate(), clause); // Return the literal return orLit; @@ -337,7 +353,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // ~lit | (a_1 & a_2 & a_3 & ... & a_n) // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) for(unsigned i = 0; i < n_children; ++i) { - assertClause(andNode.negate(), ~andLit, ~clause[i], RULE_TSEITIN); + assertClause(andNode.negate(), ~andLit, ~clause[i]); } // lit <- (a_1 & a_2 & a_3 & ... a_n) @@ -345,7 +361,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n clause[n_children] = andLit; // This needs to go last, as the clause might get modified by the SAT solver - assertClause(andNode, clause, RULE_TSEITIN); + assertClause(andNode, clause); return andLit; } @@ -364,13 +380,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { // lit -> (a->b) // ~lit | ~ a | b - assertClause(impliesNode.negate(), ~impliesLit, ~a, b, RULE_TSEITIN); + assertClause(impliesNode.negate(), ~impliesLit, ~a, b); // (a->b) -> lit // ~(~a | b) | lit // (a | l) & (~b | l) - assertClause(impliesNode, a, impliesLit, RULE_TSEITIN); - assertClause(impliesNode, ~b, impliesLit, RULE_TSEITIN); + assertClause(impliesNode, a, impliesLit); + assertClause(impliesNode, ~b, impliesLit); return impliesLit; } @@ -393,16 +409,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { // lit -> ((a-> b) & (b->a)) // ~lit | ((~a | b) & (~b | a)) // (~a | b | ~lit) & (~b | a | ~lit) - assertClause(iffNode.negate(), ~a, b, ~iffLit, RULE_TSEITIN); - assertClause(iffNode.negate(), a, ~b, ~iffLit, RULE_TSEITIN); + assertClause(iffNode.negate(), ~a, b, ~iffLit); + assertClause(iffNode.negate(), a, ~b, ~iffLit); // (a<->b) -> lit // ~((a & b) | (~a & ~b)) | lit // (~(a & b)) & (~(~a & ~b)) | lit // ((~a | ~b) & (a | b)) | lit // (~a | ~b | lit) & (a | b | lit) - assertClause(iffNode, ~a, ~b, iffLit, RULE_TSEITIN); - assertClause(iffNode, a, b, iffLit, RULE_TSEITIN); + assertClause(iffNode, ~a, ~b, iffLit); + assertClause(iffNode, a, b, iffLit); return iffLit; } @@ -437,9 +453,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // lit -> (t | e) & (b -> t) & (!b -> e) // lit -> (t | e) & (!b | t) & (b | e) // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) - assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit, RULE_TSEITIN); - assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit, RULE_TSEITIN); - assertClause(iteNode.negate(), ~iteLit, condLit, elseLit, RULE_TSEITIN); + assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit); + assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit); + assertClause(iteNode.negate(), ~iteLit, condLit, elseLit); // If ITE is false then one of the branches is false and the condition // implies which one @@ -447,9 +463,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // !lit -> (!t | !e) & (b -> !t) & (!b -> !e) // !lit -> (!t | !e) & (!b | !t) & (b | !e) // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) - assertClause(iteNode, iteLit, ~thenLit, ~elseLit, RULE_TSEITIN); - assertClause(iteNode, iteLit, ~condLit, ~thenLit, RULE_TSEITIN); - assertClause(iteNode, iteLit, condLit, ~elseLit, RULE_TSEITIN); + assertClause(iteNode, iteLit, ~thenLit, ~elseLit); + assertClause(iteNode, iteLit, ~condLit, ~thenLit); + assertClause(iteNode, iteLit, condLit, ~elseLit); return iteLit; } @@ -514,14 +530,14 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { else return ~nodeLit; } -void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id) { +void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) { Assert(node.getKind() == AND); if (!negated) { // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); conjunct != node_end; ++conjunct ) { - PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).toExpr(), node.toExpr() ) ); - convertAndAssert(*conjunct, false, proof_id); + PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(*conjunct, node);); + convertAndAssert(*conjunct, false); } } else { // If the node is a disjunction, we construct a clause and assert it @@ -533,11 +549,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule p clause[i] = toCNF(*disjunct, true); } Assert(disjunct == node.end()); - assertClause(node.negate(), clause, proof_id); + assertClause(node.negate(), clause); } } -void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule proof_id) { +void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) { Assert(node.getKind() == OR); if (!negated) { // If the node is a disjunction, we construct a clause and assert it @@ -549,18 +565,18 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule pr clause[i] = toCNF(*disjunct, false); } Assert(disjunct == node.end()); - assertClause(node, clause, proof_id); + assertClause(node, clause); } else { // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); conjunct != node_end; ++conjunct ) { - PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).negate().toExpr(), node.negate().toExpr() ) ); - convertAndAssert(*conjunct, true, proof_id); + PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence((*conjunct).negate(), node.negate());); + convertAndAssert(*conjunct, true); } } } -void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule proof_id) { +void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { if (!negated) { // p XOR q SatLiteral p = toCNF(node[0], false); @@ -569,11 +585,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule p SatClause clause1(2); clause1[0] = ~p; clause1[1] = ~q; - assertClause(node, clause1, proof_id); + assertClause(node, clause1); SatClause clause2(2); clause2[0] = p; clause2[1] = q; - assertClause(node, clause2, proof_id); + assertClause(node, clause2); } else { // !(p XOR q) is the same as p <=> q SatLiteral p = toCNF(node[0], false); @@ -582,15 +598,15 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule p SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; - assertClause(node.negate(), clause1, proof_id); + assertClause(node.negate(), clause1); SatClause clause2(2); clause2[0] = p; clause2[1] = ~q; - assertClause(node.negate(), clause2, proof_id); + assertClause(node.negate(), clause2); } } -void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule proof_id) { +void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { if (!negated) { // p <=> q SatLiteral p = toCNF(node[0], false); @@ -599,11 +615,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule p SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; - assertClause(node, clause1, proof_id); + assertClause(node, clause1); SatClause clause2(2); clause2[0] = p; clause2[1] = ~q; - assertClause(node, clause2, proof_id); + assertClause(node, clause2); } else { // !(p <=> q) is the same as p XOR q SatLiteral p = toCNF(node[0], false); @@ -612,15 +628,15 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule p SatClause clause1(2); clause1[0] = ~p; clause1[1] = ~q; - assertClause(node.negate(), clause1, proof_id); + assertClause(node.negate(), clause1); SatClause clause2(2); clause2[0] = p; clause2[1] = q; - assertClause(node.negate(), clause2, proof_id); + assertClause(node.negate(), clause2); } } -void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id) { +void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { if (!negated) { // p => q SatLiteral p = toCNF(node[0], false); @@ -629,17 +645,17 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRu SatClause clause(2); clause[0] = ~p; clause[1] = q; - assertClause(node, clause, proof_id); + assertClause(node, clause); } else {// Construct the - PROOF(ProofManager::currentPM()->setCnfDep( node[0].toExpr(), node.negate().toExpr() ) ); - PROOF(ProofManager::currentPM()->setCnfDep( node[1].negate().toExpr(), node.negate().toExpr() ) ); + PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[0], node.negate());); + PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[1].negate(), node.negate());); // !(p => q) is the same as (p && ~q) - convertAndAssert(node[0], false, proof_id); - convertAndAssert(node[1], true, proof_id); + convertAndAssert(node[0], false); + convertAndAssert(node[1], true); } } -void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule proof_id) { +void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { // ITE(p, q, r) SatLiteral p = toCNF(node[0], false); SatLiteral q = toCNF(node[1], negated); @@ -653,35 +669,47 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule p SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; - assertClause(nnode, clause1, proof_id); + assertClause(nnode, clause1); SatClause clause2(2); clause2[0] = p; clause2[1] = r; - assertClause(nnode, clause2, proof_id); + assertClause(nnode, clause2); } // At the top level we must ensure that all clauses that are asserted are // not unit, except for the direct assertions. This allows us to remove the // clauses later when they are not needed anymore (lemmas for example). -void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from) { - Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; +void TseitinCnfStream::convertAndAssert(TNode node, + bool removable, + bool negated, + ProofRule proof_id, + TNode from) { + Debug("cnf") << "convertAndAssert(" << node + << ", removable = " << (removable ? "true" : "false") + << ", negated = " << (negated ? "true" : "false") << ")" << endl; d_removable = removable; - if(options::proof() || options::unsatCores()) { - // Encode the assertion ID in the proof_id to store with generated clauses. - uint64_t assertionTableIndex = d_assertionTable.size(); - Assert((uint64_t(proof_id) & 0xffffffff00000000llu) == 0 && (assertionTableIndex & 0xffffffff00000000llu) == 0, "proof_id/table_index collision"); - d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32); - d_assertionTable.push_back(from.isNull() ? node : from); - Debug("cores") << "; cnf is " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; - } else { - // We aren't producing proofs or unsat cores; use an invalid proof id. - d_proofId = uint64_t(-1); - } - convertAndAssert(node, negated, proof_id); + PROOF + (if (d_cnfProof) { + Node assertion = negated ? node.notNode() : (Node)node; + Node from_assertion = negated? from.notNode() : (Node) from; + + if (proof_id != RULE_INVALID) { + d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion); + d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id); + } + else { + d_cnfProof->pushCurrentAssertion(assertion); + d_cnfProof->registerAssertion(assertion, proof_id); + } + }); + + convertAndAssert(node, negated); + PROOF(if (d_cnfProof) d_cnfProof->popCurrentAssertion(); ); } -void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id) { - Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; +void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { + Debug("cnf") << "convertAndAssert(" << node + << ", negated = " << (negated ? "true" : "false") << ")" << endl; if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) { NodeManager::currentResourceManager()->spendResource(options::cnfStep()); @@ -691,25 +719,25 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo switch(node.getKind()) { case AND: - convertAndAssertAnd(node, negated, proof_id); + convertAndAssertAnd(node, negated); break; case OR: - convertAndAssertOr(node, negated, proof_id); + convertAndAssertOr(node, negated); break; case IFF: - convertAndAssertIff(node, negated, proof_id); + convertAndAssertIff(node, negated); break; case XOR: - convertAndAssertXor(node, negated, proof_id); + convertAndAssertXor(node, negated); break; case IMPLIES: - convertAndAssertImplies(node, negated, proof_id); + convertAndAssertImplies(node, negated); break; case ITE: - convertAndAssertIte(node, negated, proof_id); + convertAndAssertIte(node, negated); break; case NOT: - convertAndAssert(node[0], !negated, proof_id); + convertAndAssert(node[0], !negated); break; default: { @@ -718,7 +746,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo nnode = node.negate(); } // Atoms - assertClause(nnode, toCNF(node, negated), proof_id); + assertClause(nnode, toCNF(node, negated)); } break; } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index cfab216fe..a07944a58 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -84,8 +84,11 @@ protected: /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; - /** A table of assertions, used for regenerating proofs. */ - context::CDList<Node> d_assertionTable; + /** The name of this CNF stream*/ + std::string d_name; + + /** Pointer to the proof corresponding to this CnfStream */ + CnfProof* d_cnfProof; /** Container for misc. globals. */ SmtGlobals* d_globals; @@ -117,14 +120,6 @@ protected: } /** - * A reference into the assertion table, used to map clauses back to - * their "original" input assertion/lemma. This variable is manipulated - * by the top-level convertAndAssert(). This is needed in proofs-enabled - * runs, to justify where the SAT solver's clauses came from. - */ - uint64_t d_proofId; - - /** * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the beginning of convertAndAssert so that it doesn't * need to be passed on over the stack. Only pure clauses can be asserted @@ -137,14 +132,14 @@ protected: * @param node the node giving rise to this clause * @param clause the clause to assert */ - void assertClause(TNode node, SatClause& clause, ProofRule proof_id); + void assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. * @param node the node giving rise to this clause * @param a the unit literal of the clause */ - void assertClause(TNode node, SatLiteral a, ProofRule proof_id); + void assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. @@ -152,7 +147,7 @@ protected: * @param a the first literal in the clause * @param b the second literal in the clause */ - void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id); + void assertClause(TNode node, SatLiteral a, SatLiteral b); /** * Asserts the ternary clause to the sat solver. @@ -161,7 +156,7 @@ protected: * @param b the second literal in the clause * @param c the thirs literal in the clause */ - void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id); + void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** * Acquires a new variable from the SAT solver to represent the node @@ -193,9 +188,15 @@ public: * @param registrar the entity that takes care of preregistration of Nodes * @param context the context that the CNF should respect * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, + * @param name string identifier to distinguish between different instances * even for non-theory literals */ - CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + SmtGlobals* globals, + bool fullLitToNodeMap = false, + std::string name=""); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -244,13 +245,6 @@ public: SatLiteral getLiteral(TNode node); /** - * Get the assertion with a given ID. (Used for reconstructing proofs.) - */ - TNode getAssertion(uint64_t id) { - return d_assertionTable[id]; - } - - /** * Returns the Boolean variables from the input problem. */ void getBooleanVariables(std::vector<TNode>& outputVariables) const; @@ -263,6 +257,7 @@ public: return d_literalToNodeMap; } + void setProof(CnfProof* proof); };/* class CnfStream */ @@ -286,7 +281,8 @@ public: * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()); + void convertAndAssert(TNode node, bool removable, + bool negated, ProofRule rule, TNode from = TNode::null()); /** * Constructs the stream to use the given sat solver. @@ -295,14 +291,14 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false, std::string name = ""); private: /** * Same as above, except that removable is remembered. */ - void convertAndAssert(TNode node, bool negated, ProofRule proof_id); + void convertAndAssert(TNode node, bool negated); // Each of these formulas handles takes care of a Node of each Kind. // @@ -322,12 +318,12 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - void convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertOr(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertXor(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertIff(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertIte(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertAnd(TNode node, bool negated); + void convertAndAssertOr(TNode node, bool negated); + void convertAndAssertXor(TNode node, bool negated); + void convertAndAssertIff(TNode node, bool negated); + void convertAndAssertImplies(TNode node, bool negated); + void convertAndAssertIte(TNode node, bool negated); /** * Transforms the node into CNF recursively. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 4c431a9b1..f4489c4be 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "options/prop_options.h" #include "proof/proof_manager.h" +#include "proof/sat_proof_implementation.h" #include "proof/sat_proof.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/minisat.h" @@ -32,6 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/theory_proxy.h" #include "smt_util/command.h" + using namespace CVC4::prop; namespace CVC4 { @@ -40,7 +42,6 @@ namespace Minisat { //================================================================================================= // Options: - static const char* _cat = "CORE"; static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false)); @@ -55,6 +56,10 @@ static IntOption opt_restart_first (_cat, "rfirst", "The base resta static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false)); static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); +//================================================================================================= +// Proof declarations +CRef Solver::TCRef_Undef = CRef_Undef; +CRef Solver::TCRef_Lazy = CRef_Lazy; class ScopedBool { bool& watch; @@ -135,8 +140,12 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); ) - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); ) + // FIXME: these should be axioms I believe + PROOF + ( + ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false)); + ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true)); + ); } @@ -217,7 +226,9 @@ CRef Solver::reason(Var x) { // Get the explanation from the theory SatClause explanation_cl; - proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl); + // FIXME: at some point return a tag with the theory that spawned you + proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), + explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); @@ -263,7 +274,12 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); ); + // FIXME: at some point will need more information about where this explanation + // came from (ie. the theory/sharing) + PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); + ProofManager::getCnfProof()->registerConvertedClause(id, true); + // no need to pop current assertion as this is not converted to cnf + ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -271,7 +287,7 @@ CRef Solver::reason(Var x) { return real_reason; } -bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) +bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { if (!ok) return false; @@ -289,11 +305,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) clauseLevel = std::max(clauseLevel, intro_level(var(ps[i]))); // Tautologies are ignored if (ps[i] == ~p) { + id = ClauseIdUndef; // Clause can be ignored return true; } // Clauses with 0-level true literals are also ignored if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + id = ClauseIdUndef; return true; } // Ignore repeated literals @@ -321,8 +339,19 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); - Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; - lemmas_proof_id.push(proof_id); + PROOF( + // Store the expression being converted to CNF until + // the clause is actually created + Node assertion = ProofManager::getCnfProof()->getCurrentAssertion(); + Node def = ProofManager::getCnfProof()->getCurrentDefinition(); + lemmas_cnf_assertion.push_back(std::make_pair(assertion, def)); + id = ClauseIdUndef; + ); + // does it have to always be a lemma? + // PROOF(id = ProofManager::getSatProof()->registerUnitClause(ps[0], THEORY_LEMMA);); + // PROOF(id = ProofManager::getSatProof()->registerTheoryLemma(ps);); + // Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; + // lemmas_proof_id.push(proof_id); } else { // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { @@ -331,7 +360,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) // construct the clause below to give to the proof manager // as the final conflict. if(falseLiteralsCount == 1) { - PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); ) + PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); ) PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); ) return ok = false; } @@ -353,7 +382,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) attachClause(cr); if(PROOF_ON()) { - PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); ) + PROOF( + id = ProofManager::getSatProof()->registerClause(cr, INPUT); + ) if(ps.size() == falseLiteralsCount) { PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) return ok = false; @@ -366,12 +397,16 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - Debug("cores") << "i'm registering a unit clause, input, proof id " << proof_id << std::endl; - PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } ); + Debug("cores") << "i'm registering a unit clause, input" << std::endl; + PROOF( + if(ps.size() == 1) { + id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); + } + ); CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { if(ca[confl].size() == 1) { - PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); ); + PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); ); PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); ) } else { PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); @@ -604,7 +639,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ Lit q = c[j]; - if (!seen[var(q)] && level(var(q)) > 0){ + if (!seen[var(q)] && level(var(q)) > 0) { varBumpActivity(var(q)); seen[var(q)] = 1; if (level(var(q)) >= decisionLevel()) @@ -646,7 +681,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) uint32_t abstract_level = 0; for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - + for (i = j = 1; i < out_learnt.size(); i++) { if (reason(var(out_learnt[i])) == CRef_Undef) { out_learnt[j++] = out_learnt[i]; @@ -901,7 +936,8 @@ void Solver::propagateTheory() { proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); - addClause(explanation, true, 0); + ClauseId id; // FIXME: mark it as explanation here somehow? + addClause(explanation, true, id); } } } @@ -1159,8 +1195,17 @@ lbool Solver::search(int nof_conflicts) attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); - - PROOF( ProofManager::getSatProof()->endResChain(cr); ) + PROOF( + ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); + PSTATS( + __gnu_cxx::hash_set<int> cl_levels; + for (int i = 0; i < learnt_clause.size(); ++i) { + cl_levels.insert(level(var(learnt_clause[i]))); + } + ProofManager::getSatProof()->storeClauseGlue(id, cl_levels.size()); + ) + ProofManager::getSatProof()->endResChain(id); + ); } varDecayActivity(); @@ -1650,14 +1695,14 @@ CRef Solver::updateLemmas() { // Last index in the trail int backtrack_index = trail.size(); + PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size());); + // Attach all the clauses and enqueue all the propagations for (int i = 0; i < lemmas.size(); ++ i) { // The current lemma vec<Lit>& lemma = lemmas[i]; bool removable = lemmas_removable[i]; - uint64_t proof_id = lemmas_proof_id[i]; - Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; // Attach it if non-unit CRef lemma_ref = CRef_Undef; @@ -1672,7 +1717,15 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); ); + PROOF + ( + TNode cnf_assertion = lemmas_cnf_assertion[i].first; + TNode cnf_def = lemmas_cnf_assertion[i].second; + + ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); + ); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1680,7 +1733,15 @@ CRef Solver::updateLemmas() { } attachClause(lemma_ref); } else { - PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); ); + PROOF + ( + Node cnf_assertion = lemmas_cnf_assertion[i].first; + Node cnf_def = lemmas_cnf_assertion[i].second; + + ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); + ); } // If the lemma is propagating enqueue its literal (or set the conflict) @@ -1694,7 +1755,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; - PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); ); + PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); ); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; @@ -1704,10 +1765,11 @@ CRef Solver::updateLemmas() { } } + PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size());); // Clear the lemmas lemmas.clear(); + lemmas_cnf_assertion.clear(); lemmas_removable.clear(); - lemmas_proof_id.clear(); if (conflict != CRef_Undef) { theoryConflict = true; @@ -1718,6 +1780,28 @@ CRef Solver::updateLemmas() { return conflict; } +void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy) +{ + + // FIXME what is this CRef_lazy + if (cr == CRef_Lazy) return; + + CRef old = cr; // save the old reference + Clause& c = operator[](cr); + if (c.reloced()) { cr = c.relocation(); return; } + + cr = to.alloc(c.level(), c, c.removable()); + c.relocate(cr); + if (proxy) { + proxy->updateCRef(old, cr); + } + // Copy extra data-fields: + // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) + to[cr].mark(c.mark()); + if (to[cr].removable()) to[cr].activity() = c.activity(); + else if (to[cr].has_extra()) to[cr].calcAbstraction(); +} + inline bool Solver::withinBudget(uint64_t ammount) const { Assert (proxy); // spendResource sets async_interrupt or throws UnsafeInterruptException diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 3be6b1b22..a239eba72 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -37,13 +37,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace CVC4 { - class SatProof; +template <class Solver> class TSatProof; - namespace prop { - class TheoryProxy; - }/* CVC4::prop namespace */ +namespace prop { + class TheoryProxy; +}/* CVC4::prop namespace */ }/* CVC4 namespace */ +typedef unsigned ClauseId; + namespace CVC4 { namespace Minisat { @@ -54,7 +56,18 @@ class Solver { /** The only two CVC4 entry points to the private solver data */ friend class CVC4::prop::TheoryProxy; - friend class CVC4::SatProof; + friend class CVC4::TSatProof<Minisat::Solver>; + +public: + static CRef TCRef_Undef; + static CRef TCRef_Lazy; + + typedef Var TVar; + typedef Lit TLit; + typedef Clause TClause; + typedef CRef TCRef; + typedef vec<Lit> TLitVec; + protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ @@ -85,8 +98,8 @@ protected: /** Is the lemma removable */ vec<bool> lemmas_removable; - /** Proof IDs for lemmas */ - vec<uint64_t> lemmas_proof_id; + /** Nodes being converted to CNF */ + std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion; /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -157,14 +170,14 @@ public: void push (); void pop (); - // CVC4 adds the "proof_id" here to refer to the input assertion/lemma - // that produced this clause - bool addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id); // Add a clause to the solver. - bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. - bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps, bool removable, uint64_t proof_id); // Add a clause to the solver without making superflous internal copy. Will + // addClause returns the ClauseId corresponding to the clause added in the + // reference parameter id. + bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); // Add a clause to the solver. + bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. + bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver. + bool addClause_( vec<Lit>& ps, bool removable, ClauseId& id); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -495,15 +508,15 @@ inline void Solver::checkGarbage(double gf){ // NOTE: enqueue does not set the ok flag! (only public methods do) inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } -inline bool Solver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id) - { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } -inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable, uint64_t(-1)); } -inline bool Solver::addClause (Lit p, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } -inline bool Solver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } -inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } +inline bool Solver::addClause (const vec<Lit>& ps, bool removable, ClauseId& id) + { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); } +inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, removable, tmp); } +inline bool Solver::addClause (Lit p, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); } +inline bool Solver::addClause (Lit p, Lit q, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); } +inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index b0d78242c..116a39a49 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -169,20 +169,22 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { } -} /* Minisat */ -} - +class Solver; - -namespace CVC4 { class ProofProxyAbstract { public: virtual ~ProofProxyAbstract() {} virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; }; -} + +} /* namespace CVC4::Minisat */ +} /* namespace CVC4 */ +namespace CVC4 { +template <class Solver> class ProofProxy; +typedef ProofProxy<CVC4::Minisat::Solver> CoreProofProxy; +} namespace CVC4 { namespace Minisat{ @@ -305,27 +307,8 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, ClauseAllocator& to, CVC4::ProofProxyAbstract* proxy = NULL) - { - - // FIXME what is this CRef_lazy - if (cr == CRef_Lazy) return; - - CRef old = cr; // save the old reference - Clause& c = operator[](cr); - if (c.reloced()) { cr = c.relocation(); return; } - - cr = to.alloc(c.level(), c, c.removable()); - c.relocate(cr); - if (proxy) { - proxy->updateCRef(old, cr); - } - // Copy extra data-fields: - // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) - to[cr].mark(c.mark()); - if (to[cr].removable()) to[cr].activity() = c.activity(); - else if (to[cr].has_extra()) to[cr].calcAbstraction(); - } + void reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy = NULL); + // Implementation moved to Solver.cc. }; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ce5c1eb92..739d9087a 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -23,6 +23,7 @@ #include "options/prop_options.h" #include "options/smt_options.h" #include "prop/minisat/simp/SimpSolver.h" +#include "proof/sat_proof.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -94,14 +95,6 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, - SatClause& sat_clause) { - for (int i = 0; i < clause.size(); ++i) { - sat_clause.push_back(toSatLiteral(clause[i])); - } - Assert((unsigned)clause.size() == sat_clause.size()); -} - void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { @@ -149,10 +142,18 @@ void MinisatSatSolver::setupOptions() { d_minisat->restart_inc = options::satRestartInc(); } -void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { +ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { Minisat::vec<Minisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable, proof_id); + ClauseId clause_id = ClauseIdError; + // FIXME: This relies on the invariant that when ok() is false + // the SAT solver does not add the clause (which is what Minisat currently does) + if (!ok()) { + return ClauseIdUndef; + } + d_minisat->addClause(minisat_clause, removable, clause_id); + PROOF( Assert (clause_id != ClauseIdError);); + return clause_id; } SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { @@ -182,6 +183,9 @@ SatValue MinisatSatSolver::solve() { return toSatLiteralValue(d_minisat->solve()); } +bool MinisatSatSolver::ok() const { + return d_minisat->okay(); +} void MinisatSatSolver::interrupt() { d_minisat->interrupt(); @@ -280,3 +284,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ } /* namespace CVC4::prop */ } /* namespace CVC4 */ + + +namespace CVC4 { +template<> +prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) { + return prop::MinisatSatSolver::toSatLiteral(lit); +} + +template<> +void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl, + prop::SatClause& sat_cl) { + prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl); +} + +} /* namespace CVC4 */ + + diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index f279b3a5b..535ce1a47 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -40,11 +40,10 @@ public: //(Commented because not in use) static bool tobool(SatValue val); static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); - static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); - void addClause(SatClause& clause, bool removable, uint64_t proof_id); + ClauseId addClause(SatClause& clause, bool removable); SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } @@ -53,6 +52,8 @@ public: SatValue solve(); SatValue solve(long unsigned int&); + bool ok() const; + void interrupt(); SatValue value(SatLiteral l); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 235c97e8f..5bdaea950 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -160,7 +160,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) +bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { #ifndef NDEBUG if (use_simplification) { @@ -174,7 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, removable, proof_id)) + if (!Solver::addClause_(ps, removable, id)) return false; if (use_simplification && clauses_persistent.size() == nclauses + 1){ @@ -541,12 +541,14 @@ bool SimpSolver::eliminateVar(Var v) for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); + ClauseId id = ClauseIdUndef; // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) { bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable(); - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) { + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && + !addClause_(resolvent, removable, id)) { return false; } } @@ -585,8 +587,8 @@ bool SimpSolver::substitute(Var v, Lit x) } removeClause(cls[i]); - - if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) { + ClauseId id = ClauseIdUndef; + if (!addClause_(subst_clause, c.removable(), id)) { return ok = false; } } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 0c5062726..a19bec1ef 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -48,12 +48,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); - bool addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id); - bool addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver. - bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. - bool addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id); + bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); + bool addEmptyClause(bool removable); // Add the empty clause to the solver. + bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -183,15 +183,15 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id) - { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id) { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addClause (Lit p, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) - { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id) +{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addClause (Lit p, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } // the solver can always return unknown due to resource limiting diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 9767ac7c7..593c522a8 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -99,7 +99,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); - PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); ); + PROOF ( + ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); + ); } PropEngine::~PropEngine() { @@ -117,7 +119,10 @@ void PropEngine::assertFormula(TNode node) { d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN); } -void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) { +void PropEngine::assertLemma(TNode node, bool negated, + bool removable, + ProofRule rule, + TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 1c1dae410..1383308a3 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -30,10 +30,15 @@ #include "util/statistics_registry.h" namespace CVC4 { + +class BitVectorProof; + namespace prop { class TheoryProxy; +typedef unsigned ClauseId; + class SatSolver { public: @@ -42,7 +47,8 @@ public: virtual ~SatSolver() throw(AssertionException) { } /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0; + virtual ClauseId addClause(SatClause& clause, + bool removable) = 0; /** * Create a new boolean variable in the solver. @@ -77,6 +83,10 @@ public: /** Get the current assertion level */ virtual unsigned getAssertionLevel() const = 0; + /** Check if the solver is in an inconsistent state */ + virtual bool ok() const = 0; + + };/* class SatSolver */ @@ -121,6 +131,10 @@ public: virtual void popAssumption() = 0; + virtual bool ok() const = 0; + + virtual void setProofLog( BitVectorProof * bvp ) {} + };/* class BVSatSolverInterface */ @@ -139,7 +153,8 @@ public: virtual bool flipDecision() = 0; virtual bool isDecision(SatVariable decn) const = 0; - + + virtual bool ok() const = 0; };/* class DPLLSatSolverInterface */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 434bf849d..6a3053a18 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -31,7 +31,9 @@ namespace prop { class SatSolverFactory { public: - static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = ""); + static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, + StatisticsRegistry* registry, + const std::string& name = ""); static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); };/* class SatSolverFactory */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index e87046ad5..5304691a6 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -22,6 +22,7 @@ #include "options/decision_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" +#include "proof/cnf_proof.h" #include "smt_util/lemma_input_channel.h" #include "smt_util/lemma_output_channel.h" #include "smt/smt_statistics_registry.h" @@ -29,6 +30,7 @@ #include "theory/theory_engine.h" #include "util/statistics_registry.h" + namespace CVC4 { namespace prop { @@ -100,6 +102,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; Node theoryExplanation = d_theoryEngine->getExplanation(lNode); + PROOF(ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); ); Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; if (theoryExplanation.getKind() == kind::AND) { Node::const_iterator it = theoryExplanation.begin(); |