diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 34 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 9 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 403 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 50 | ||||
-rw-r--r-- | src/prop/bvminisat/core/SolverTypes.h | 49 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 55 | ||||
-rw-r--r-- | src/prop/cadical.cpp | 1 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 60 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 14 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 44 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 3 | ||||
-rw-r--r-- | src/prop/kissat.cpp | 1 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 313 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 64 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 96 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 23 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 6 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 12 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 20 |
21 files changed, 541 insertions, 724 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index c1aac33be..0b531c498 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -18,7 +18,6 @@ #include "prop/bvminisat/simp/SimpSolver.h" #include "proof/clause_id.h" -#include "proof/sat_proof.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -66,7 +65,6 @@ ClauseId BVMinisatSatSolver::addClause(SatClause& clause, // } ClauseId clause_id = ClauseIdError; d_minisat->addClause(minisat_clause, clause_id); - THEORY_PROOF(Assert(clause_id != ClauseIdError);); return clause_id; } @@ -76,14 +74,14 @@ SatValue BVMinisatSatSolver::propagate() { void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) { d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit))); - markUnremovable(lit); + markUnremovable(lit); } void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) { std::vector<BVMinisat::Lit> minisat_explanation; d_minisat->explain(toMinisatLit(lit), minisat_explanation); for (unsigned i = 0; i < minisat_explanation.size(); ++i) { - explanation.push_back(toSatLiteral(minisat_explanation[i])); + explanation.push_back(toSatLiteral(minisat_explanation[i])); } } @@ -104,12 +102,6 @@ void BVMinisatSatSolver::popAssumption() { d_minisat->popAssumption(); } -void BVMinisatSatSolver::setResolutionProofLog( - proof::ResolutionBitVectorProof* bvp) -{ - d_minisat->setProofLog( bvp ); -} - SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ return d_minisat->newVar(true, true, !canErase); } @@ -148,9 +140,7 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } -bool BVMinisatSatSolver::ok() const { - return d_minisat->okay(); -} +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 @@ -160,11 +150,11 @@ void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { } SatValue BVMinisatSatSolver::value(SatLiteral l){ - return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); + return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } SatValue BVMinisatSatSolver::modelValue(SatLiteral l){ - return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); + return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } void BVMinisatSatSolver::unregisterVar(SatLiteral lit) { @@ -309,17 +299,3 @@ 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 01a0a518e..f93dc8048 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -21,8 +21,6 @@ #include <memory> #include "context/cdo.h" -#include "proof/clause_id.h" -#include "proof/resolution_bitvector_proof.h" #include "prop/bv_sat_solver_notify.h" #include "prop/bvminisat/simp/SimpSolver.h" #include "prop/sat_solver.h" @@ -57,8 +55,8 @@ class BVMinisatSatSolver : public BVSatSolverInterface, } }; - std::unique_ptr<BVMinisat::SimpSolver> d_minisat; - std::unique_ptr<MinisatNotify> d_minisatNotify; + std::unique_ptr<BVMinisat::SimpSolver> d_minisat; + std::unique_ptr<MinisatNotify> d_minisatNotify; unsigned d_assertionsCount; context::CDO<unsigned> d_assertionsRealCount; @@ -79,6 +77,7 @@ public: ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override { Unreachable() << "Minisat does not support native XOR reasoning"; + return ClauseIdError; } SatValue propagate() override; @@ -123,8 +122,6 @@ public: void popAssumption() override; - void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override; - private: /* Disable the default constructor. */ BVMinisatSatSolver() = delete; diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 84ab62fd8..f7ba14acd 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -29,11 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "options/bv_options.h" #include "options/smt_options.h" -#include "proof/clause_id.h" -#include "proof/proof_manager.h" -#include "proof/resolution_bitvector_proof.h" -#include "proof/sat_proof.h" -#include "proof/sat_proof_implementation.h" #include "prop/bvminisat/mtl/Sort.h" #include "theory/interrupted.h" #include "util/utility.h" @@ -170,8 +165,7 @@ Solver::Solver(CVC4::context::Context* context) , conflict_budget(-1), propagation_budget(-1), - asynch_interrupt(false), - d_bvp(NULL) + asynch_interrupt(false) { // Create the constant variables varTrue = newVar(true, false); @@ -220,7 +214,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) if (decisionLevel() > 0) { cancelUntil(0); } - + if (!ok) { id = ClauseIdUndef; return false; @@ -231,7 +225,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) sort(ps); Lit p; int i, j; 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) { @@ -245,82 +239,30 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) } if (value(ps[i]) == l_False) { - if (!THEORY_PROOF_ON()) - continue; - ++falseLiteralsCount; + continue; } ps[j++] = p = ps[i]; } - + ps.shrink(i - j); clause_added = true; - 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){ - if(d_bvp){ id = d_bvp->getSatProof()->registerUnitClause(ps[0], INPUT);} uncheckedEnqueue(ps[0]); 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; - } - - 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; } return ok; } @@ -338,9 +280,6 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& clause = ca[cr]; - if (d_bvp) - { - d_bvp->getSatProof()->markDeleted(cr); } assert(clause.size() > 1); @@ -425,23 +364,24 @@ Lit Solver::pickBranchLit() return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]); } - /*_________________________________________________________________________________________________ | -| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void] -| +| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> +[void] +| | Description: | Analyze conflict and produce a reason clause. -| +| | Pre-conditions: | * 'out_learnt' is assumed to be cleared. | * Current decision level must be greater than root level. -| +| | Post-conditions: | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. -| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the -| rest of literals. There may be others from the same level though. -| +| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision +level of the | rest of literals. There may be others from the same level +though. +| |________________________________________________________________________________________________@*/ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip) { @@ -454,8 +394,6 @@ 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) @@ -477,13 +415,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip out_learnt.push(q); } - if (level(var(q)) == 0) - { - if (d_bvp) - { - d_bvp->getSatProof()->resolveOutUnit(q); - } - } } // Select next clause to look at: @@ -493,10 +424,6 @@ 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; @@ -536,13 +463,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip // Literal is not redundant out_learnt[j++] = out_learnt[i1]; } - else - { - if (d_bvp) - { - d_bvp->getSatProof()->storeLitRedundant(out_learnt[i1]); - } - } } } }else if (ccmin_mode == 1){ @@ -640,10 +560,10 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) return true; } -/** +/** * Specialized analyzeFinal procedure where we test the consistency * of the assumptions before backtracking bellow the assumption level. - * + * * @param p the original uip (may be unit) * @param confl_clause the conflict clause * @param out_conflict the conflict in terms of assumptions we are building @@ -653,14 +573,14 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { assert (decisionLevel() == assumptions.size()); assert (level(var(p)) == assumptions.size()); - out_conflict.clear(); - + out_conflict.clear(); + Clause& cl = ca[confl_clause]; for (int i = 0; i < cl.size(); ++i) { seen[var(cl[i])] = 1; } - int end = options::proof() ? 0 : trail_lim[0]; + int end = trail_lim[0]; for (int i = trail.size() - 1; i >= end; i--) { Var x = var(trail[i]); if (seen[x]) { @@ -670,44 +590,31 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { 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& clause = ca[reason(x)]; - if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));} for (int j = 1; j < clause.size(); j++) { if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1; - if(d_bvp){ - if (level(var(clause[j])) == 0) - { - d_bvp->getSatProof()->resolveOutUnit(clause[j]); - seen[var(clause[j])] = - 0; // we don't need to resolve it out again - } - } } } seen[x] = 0; } - assert (seen[x] == 0); + assert(seen[x] == 0); } - assert (out_conflict.size()); + assert(out_conflict.size()); } /*_________________________________________________________________________________________________ | | analyzeFinal : (p : Lit) -> [void] -| +| | Description: -| Specialized analysis procedure to express the final conflict in terms of assumptions. -| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and -| stores the result in 'out_conflict'. +| Specialized analysis procedure to express the final conflict in terms of +assumptions. | Calculates the (possibly empty) set of assumptions that led to +the assignment of 'p', and | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) { @@ -716,22 +623,14 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) out_conflict.push(p); } - 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()) { + if (decisionLevel() == 0) + { return; } seen[var(p)] = 1; - int end = options::proof() ? 0 : trail_lim[0]; - + int end = trail_lim[0]; + for (int i = trail.size()-1; i >= end; i--){ Var x = var(trail[i]); if (seen[x]) { @@ -744,26 +643,12 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) } } else { Clause& clause = ca[reason(x)]; - 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 < clause.size(); j++) { if (level(var(clause[j])) > 0) { seen[var(clause[j])] = 1; } - if(d_bvp){ - if (level(var(clause[j])) == 0) - { - d_bvp->getSatProof()->resolveOutUnit(clause[j]); - } - } } } seen[x] = 0; @@ -805,10 +690,9 @@ 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()); } @@ -829,9 +713,9 @@ lbool Solver::assertAssumption(Lit p, bool propagate) { // run the propagation if (propagate) { only_bcp = true; - ccmin_mode = 0; + ccmin_mode = 0; lbool result = search(-1); - return result; + return result; } else { return l_True; } @@ -841,18 +725,16 @@ 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*] -| +| | Description: -| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, -| otherwise CRef_Undef. -| +| Propagates all enqueued facts. If a conflict arises, the conflicting clause +is returned, | otherwise CRef_Undef. +| | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ @@ -920,20 +802,24 @@ CRef Solver::propagate() return confl; } - /*_________________________________________________________________________________________________ | | reduceDB : () -> [void] -| +| | Description: -| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked -| clauses are clauses that are reason to some assignment. Binary clauses are never removed. +| Remove half of the learnt clauses, minus the clauses locked by the current +assignment. Locked | clauses are clauses that are reason to some assignment. +Binary clauses are never removed. |________________________________________________________________________________________________@*/ -struct reduceDB_lt { - ClauseAllocator& ca; - reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} - bool operator () (CRef x, CRef y) { - return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } +struct reduceDB_lt +{ + ClauseAllocator& ca; + reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} + bool operator()(CRef x, CRef y) + { + return ca[x].size() > 2 + && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); + } }; void Solver::reduceDB() { @@ -963,14 +849,6 @@ void Solver::removeSatisfied(vec<CRef>& cs) Clause& clause = ca[cs[i]]; if (satisfied(clause)) { - if (locked(clause)) - { - // store a resolution of the literal clause propagated - if (d_bvp) - { - d_bvp->getSatProof()->storeUnitResolution(clause[0]); - } - } removeClause(cs[i]); } else @@ -989,14 +867,14 @@ void Solver::rebuildOrderHeap() order_heap.build(vs); } - /*_________________________________________________________________________________________________ | | simplify : [void] -> [bool] -| +| | Description: -| Simplify the clause database according to the current top-level assigment. Currently, the only -| thing done here is the removal of satisfied clauses, but more things can be put here. +| Simplify the clause database according to the current top-level assigment. +Currently, the only | thing done here is the removal of satisfied clauses, +but more things can be put here. |________________________________________________________________________________________________@*/ bool Solver::simplify() { @@ -1021,19 +899,19 @@ bool Solver::simplify() return true; } - /*_________________________________________________________________________________________________ | | search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] -| +| | Description: -| Search for a model the specified number of conflicts. +| Search for a model the specified number of conflicts. | NOTE! Use negative value for 'nof_conflicts' indicate infinity. -| +| | Output: -| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If -| all variables are decision variables, this means that the clause set is satisfiable. 'l_False' -| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +| 'l_True' if a partial assigment that is consistent with respect to the +clauseset is found. If | all variables are decision variables, this means +that the clause set is satisfiable. 'l_False' | if the clause set is +unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. |________________________________________________________________________________________________@*/ lbool Solver::search(int nof_conflicts, UIP uip) { @@ -1051,7 +929,6 @@ lbool Solver::search(int nof_conflicts, UIP uip) if (decisionLevel() == 0) { // can this happen for bv? - if(d_bvp){ d_bvp->getSatProof()->finalizeProof(confl);} return l_False; } @@ -1067,59 +944,34 @@ 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( - std::unordered_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()); + 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; } if (!CVC4::options::bvEagerExplanations()) { - // check if uip leads to a conflict + // check if uip leads to a conflict if (backtrack_level < assumptions.size()) { cancelUntil(assumptions.size()); uncheckedEnqueue(p, cr); - + CRef new_confl = propagate(); if (new_confl != CRef_Undef) { // we have a conflict we now need to explain it - // 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; } } @@ -1127,8 +979,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) cancelUntil(backtrack_level); uncheckedEnqueue(p, cr); - - + varDecayActivity(); claDecayActivity(); @@ -1138,10 +989,17 @@ lbool Solver::search(int nof_conflicts, UIP uip) max_learnts *= learntsize_inc; if (verbosity >= 1) - printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", - (int)conflicts, - (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, - (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", + (int)conflicts, + (int)dec_vars + - (trail_lim.size() == 0 ? trail.size() + : trail_lim[0]), + nClauses(), + (int)clauses_literals, + (int)max_learnts, + nLearnts(), + (double)learnts_literals / nLearnts(), + progressEstimate() * 100); } }else{ @@ -1152,9 +1010,9 @@ lbool Solver::search(int nof_conflicts, UIP uip) withinBudget(ResourceManager::Resource::BvSatConflictsStep); } catch (const CVC4::theory::Interrupted& e) { - // do some clean-up and rethrow - cancelUntil(assumptions.size()); - throw e; + // do some clean-up and rethrow + cancelUntil(assumptions.size()); + throw e; } if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0 @@ -1192,10 +1050,8 @@ 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{ @@ -1283,7 +1139,7 @@ lbool Solver::solve_() conflict.clear(); ccmin_mode = 0; - + if (!ok) return l_False; solves++; @@ -1324,31 +1180,20 @@ lbool Solver::solve_() //================================================================================================= // Bitvector propagations -// +// void Solver::explain(Lit p, std::vector<Lit>& explanation) { Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl; // 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; + return; } - + seen[var(p)] = 1; // if we are called at decisionLevel = 0 trail_lim is empty - int bottom = options::proof() ? 0 : trail_lim[0]; + int bottom = trail_lim[0]; for (int i = trail.size()-1; i >= bottom; i--){ Var x = var(trail[i]); if (seen[x]) { @@ -1358,21 +1203,12 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { explanation.push_back(trail[i]); } else { Assert(level(x) == 0); - if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); } } - } else { Clause& clause = 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 < clause.size(); j++) { - if (level(var(clause[j])) > 0 || options::proof()) + if (level(var(clause[j])) > 0) { seen[var(clause[j])] = 1; } @@ -1382,28 +1218,11 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { } } 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(proof::ResolutionBitVectorProof* 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: -// +// // FIXME: this needs to be rewritten completely. static Var mapVar(Var x, vec<Var>& map, Var& max) @@ -1454,7 +1273,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) for (int i = 0; i < clauses.size(); i++) if (!satisfied(ca[clauses[i]])) cnt++; - + for (int i = 0; i < clauses.size(); i++) if (!satisfied(ca[clauses[i]])){ Clause& clause = ca[clauses[i]]; @@ -1494,8 +1313,7 @@ void Solver::relocAll(ClauseAllocator& to) Lit p = mkLit(v, s); // 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, d_bvp ? d_bvp->getSatProof() : NULL); + for (int j = 0; j < ws.size(); j++) ca.reloc(ws[j].cref, to); } // All reasons: @@ -1504,20 +1322,16 @@ 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, d_bvp ? d_bvp->getSatProof() : NULL); + ca.reloc(vardata[v].reason, to); } // All learnt: // - for (int i = 0; i < learnts.size(); i++) - ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof() : NULL); + for (int i = 0; i < learnts.size(); i++) ca.reloc(learnts[i], to); // All original: // - for (int i = 0; i < clauses.size(); i++) - ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof() : NULL); - - if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); } + for (int i = 0; i < clauses.size(); i++) ca.reloc(clauses[i], to); } @@ -1525,33 +1339,28 @@ void Solver::garbageCollect() { // Initialize the next region to a size corresponding to the estimated utilization degree. This // is not precise but should avoid some unnecessary reallocations for the new region: - ClauseAllocator to(ca.size() - ca.wasted()); - Debug("bvminisat") << " BVMinisat::Garbage collection \n"; + ClauseAllocator to(ca.size() - ca.wasted()); + Debug("bvminisat") << " BVMinisat::Garbage collection \n"; relocAll(to); if (verbosity >= 2) - printf("| Garbage collection: %12d bytes => %12d bytes |\n", - ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + printf( + "| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size() * ClauseAllocator::Unit_Size, + to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); } -void ClauseAllocator::reloc(CRef& cr, - ClauseAllocator& to, - CVC4::TSatProof<Solver>* proof) +void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to) { - 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 (proof) - { - proof->updateCRef(old, cr); - } - - // Copy extra data-fields: - // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?) + + // 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(); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 7fad72d6d..f2721c88d 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -25,7 +25,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "context/context.h" #include "proof/clause_id.h" -#include "proof/sat_proof.h" #include "prop/bvminisat/core/SolverTypes.h" #include "prop/bvminisat/mtl/Alg.h" #include "prop/bvminisat/mtl/Heap.h" @@ -39,11 +38,6 @@ namespace BVMinisat { class Solver; } -// TODO (aozdemir) replace this forward declaration with an include -namespace proof { -class ResolutionBitVectorProof; -} - namespace BVMinisat { /** Interface for minisat callbacks */ @@ -71,11 +65,10 @@ 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 Clause TClause; typedef CRef TCRef; typedef vec<Lit> TLitVec; @@ -109,12 +102,17 @@ public: Var trueVar() const { return varTrue; } Var falseVar() const { return varFalse; } - - bool addClause (const vec<Lit>& ps, ClauseId& id); // 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, 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(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'. @@ -141,9 +139,9 @@ public: void toDimacs (const char* file, Lit p); void toDimacs (const char* file, Lit p, Lit q); void toDimacs (const char* file, Lit p, Lit q, Lit r); - + // Variable mode: - // + // void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. @@ -211,13 +209,12 @@ public: void addMarkerLiteral(Var var); - bool need_to_propagate; // true if we added new clauses, set to true in propagation + 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::proof::ResolutionBitVectorProof* bvp); - protected: // has a clause been added @@ -293,9 +290,6 @@ public: int64_t conflict_budget; // -1 means no budget. int64_t propagation_budget; // -1 means no budget. bool asynch_interrupt; - - //proof log - CVC4::proof::ResolutionBitVectorProof* d_bvp; // Main internal methods: // @@ -458,13 +452,15 @@ inline int Solver::nLearnts () const { return learnts.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } -inline void Solver::setDecisionVar(Var v, bool b) -{ - if ( b && !decision[v]) dec_vars++; - else if (!b && decision[v]) dec_vars--; +inline void Solver::setDecisionVar(Var v, bool b) +{ + if (b && !decision[v]) + dec_vars++; + else if (!b && decision[v]) + dec_vars--; - decision[v] = b; - insertVarOrder(v); + decision[v] = b; + insertVarOrder(v); } inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; } inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; } diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index 302db104f..cf9ce7e15 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -86,15 +86,14 @@ struct LitHashFunction { const Lit lit_Undef = { -2 }; // }- Useful special constants. const Lit lit_Error = { -1 }; // } - //================================================================================================= // Lifted booleans: // -// NOTE: this implementation is optimized for the case when comparisons between values are mostly -// between one variable and one constant. Some care had to be taken to make sure that gcc -// does enough constant propagation to produce sensible code, and this appears to be somewhat -// fragile unfortunately. - +// NOTE: this implementation is optimized for the case when comparisons between +// values are mostly +// between one variable and one constant. Some care had to be taken to +// make sure that gcc does enough constant propagation to produce sensible +// code, and this appears to be somewhat fragile unfortunately. #ifndef l_True #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants. @@ -121,10 +120,12 @@ public: bool operator != (lbool b) const { return !(*this == b); } lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); } - lbool operator && (lbool b) const { - uint8_t sel = (this->value << 1) | (b.value << 3); - uint8_t v = (0xF7F755F4 >> sel) & 3; - return lbool(v); } + lbool operator&&(lbool b) const + { + uint8_t sel = (this->value << 1) | (b.value << 3); + uint8_t v = (0xF7F755F4 >> sel) & 3; + return lbool(v); + } lbool operator || (lbool b) const { uint8_t sel = (this->value << 1) | (b.value << 3); @@ -163,14 +164,14 @@ class Clause { header.reloced = 0; header.size = ps.size(); - for (int i = 0; i < ps.size(); i++) - data[i].lit = ps[i]; + for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; if (header.has_extra){ if (header.learnt) - data[header.size].act = 0; - else - calcAbstraction(); } + data[header.size].act = 0; + else + calcAbstraction(); + } } public: @@ -256,9 +257,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t> RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra())); } - void reloc(CRef& cr, - ClauseAllocator& to, - CVC4::TSatProof<Solver>* proof = NULL); + void reloc(CRef& cr, ClauseAllocator& to); }; @@ -275,7 +274,7 @@ class OccLists public: OccLists(const Deleted& d) : deleted(d) {} - + void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); } // Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } @@ -334,13 +333,12 @@ class CMap typedef Map<CRef, T, CRefHash> HashTable; HashTable map; - + public: // Size-operations: void clear () { map.clear(); } int size () const { return map.elems(); } - // Insert/Remove/Test mapping: void insert (CRef cr, const T& t){ map.insert(cr, t); } void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility @@ -363,15 +361,14 @@ class CMap printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); } }; - /*_________________________________________________________________________________________________ | | subsumes : (other : const Clause&) -> Lit -| +| | Description: -| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' -| by subsumption resolution. -| +| Checks if clause subsumes 'other', and at the same time, if it can be +used to simplify 'other' | by subsumption resolution. +| | Result: | lit_Error - No subsumption or simplification | lit_Undef - Clause subsumes 'other' diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 6641310cc..9429e4ced 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -23,7 +23,6 @@ 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 "proof/clause_id.h" -#include "proof/proof.h" #include "prop/bvminisat/mtl/Sort.h" #include "prop/bvminisat/utils/System.h" @@ -64,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context) asymm_lits(0), eliminated_vars(0), elimorder(1), - use_simplification(!PROOF_ON()), + use_simplification(true), occurs(ClauseDeleted(ca)), elim_heap(ElimLt(n_occ)), bwdsub_assigns(0), @@ -94,7 +93,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context) SimpSolver::~SimpSolver() { - // CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); + // CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); } @@ -111,7 +110,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) { touched .push(0); elim_heap .insert(v); if (freeze) { - setFrozen(v, true); + setFrozen(v, true); } } return v; @@ -122,7 +121,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) { lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { only_bcp = false; - + vec<Var> extra_frozen; lbool result = l_True; @@ -210,14 +209,15 @@ void SimpSolver::removeClause(CRef cr) const Clause& clause = ca[cr]; if (use_simplification) + { for (int i = 0; i < clause.size(); i++) { n_occ[toInt(clause[i])]--; updateElimHeap(var(clause[i])); occurs.smudge(var(clause[i])); } - - Solver::removeClause(cr); + } + Solver::removeClause(cr); } @@ -546,9 +546,10 @@ bool SimpSolver::eliminateVar(Var v) 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, clause_size) && - (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim))) - return true; + if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) + && (++cnt > cls.size() + grow + || (clause_lim != -1 && clause_size > clause_lim))) + return true; // Delete and store old clauses: eliminated[v] = true; @@ -565,8 +566,7 @@ bool SimpSolver::eliminateVar(Var v) mkElimClause(elimclauses, ~mkLit(v)); } - for (int i = 0; i < cls.size(); i++) - removeClause(cls[i]); + for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; @@ -580,7 +580,7 @@ bool SimpSolver::eliminateVar(Var v) // Free occurs list for this variable: occurs[v].clear(true); - + // Free watchers lists for this variable, if possible: if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true); if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true); @@ -600,7 +600,7 @@ bool SimpSolver::substitute(Var v, Lit x) eliminated[v] = true; setDecisionVar(v, false); const vec<CRef>& cls = occurs.lookup(v); - + vec<Lit>& subst_clause = add_tmp; for (int i = 0; i < cls.size(); i++){ Clause& clause = ca[cls[i]]; @@ -643,7 +643,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) { // CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time); - + if (!simplify()) return false; else if (!use_simplification) @@ -655,9 +655,12 @@ bool SimpSolver::eliminate(bool turn_off_elim) gatherTouchedClauses(); // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns); - if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && - !backwardSubsumptionCheck(true)){ - ok = false; goto cleanup; } + if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) + && !backwardSubsumptionCheck(true)) + { + ok = false; + goto cleanup; + } // Empty elim_heap and return immediately on user-interrupt: if (asynch_interrupt){ @@ -670,7 +673,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size()); for (int cnt = 0; !elim_heap.empty(); cnt++){ Var elim = elim_heap.removeMin(); - + if (asynch_interrupt) break; if (isEliminated(elim) || value(elim) != l_Undef) continue; @@ -720,8 +723,10 @@ bool SimpSolver::eliminate(bool turn_off_elim) } if (verbosity >= 1 && elimclauses.size() > 0) - printf("| Eliminated clauses: %10.2f Mb |\n", - double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + printf( + "| Eliminated clauses: %10.2f Mb " + " |\n", + double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024)); return ok; @@ -772,15 +777,17 @@ void SimpSolver::garbageCollect() { // Initialize the next region to a size corresponding to the estimated utilization degree. This // is not precise but should avoid some unnecessary reallocations for the new region: - ClauseAllocator to(ca.size() - ca.wasted()); + ClauseAllocator to(ca.size() - ca.wasted()); cleanUpClauses(); to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields. relocAll(to); Solver::relocAll(to); if (verbosity >= 2) - printf("| Garbage collection: %12d bytes => %12d bytes |\n", - ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + printf( + "| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size() * ClauseAllocator::Unit_Size, + to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); } diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index ca447cea8..7cc5b16cd 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -19,7 +19,6 @@ #ifdef CVC4_USE_CADICAL #include "base/check.h" -#include "proof/sat_proof.h" namespace CVC4 { namespace prop { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index a6a4b6859..c46cd5136 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -83,22 +83,13 @@ void CnfStream::assertClause(TNode node, SatClause& c) { } } - if (PROOF_ON() && 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) - if (PROOF_ON() && d_cnfProof) + if (d_cnfProof && clause_id != ClauseIdError) { - if (clause_id != ClauseIdError) - { - d_cnfProof->registerConvertedClause(clause_id); - } - d_cnfProof->popCurrentDefinition(); - }; + d_cnfProof->registerConvertedClause(clause_id); + } } void CnfStream::assertClause(TNode node, SatLiteral a) { @@ -171,11 +162,17 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) { // non-empty and that we are not associating a bogus assertion with the // clause. This should be ok because we use the mapping back to assertions // for clauses from input assertions only. - PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); }); + if (d_cnfProof) + { + d_cnfProof->pushCurrentAssertion(Node::null()); + } lit = toCNF(n, false); - PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); }); + if (d_cnfProof) + { + d_cnfProof->popCurrentAssertion(); + } // Store backward-mappings // These may already exist @@ -547,7 +544,6 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool 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(if (d_cnfProof) d_cnfProof->setCnfDependence(*conjunct, node);); convertAndAssert(*conjunct, false); } } else { @@ -581,7 +577,6 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool 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(if (d_cnfProof) d_cnfProof->setCnfDependence((*conjunct).negate(), node.negate());); convertAndAssert(*conjunct, true); } } @@ -658,8 +653,6 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { clause[1] = q; assertClause(node, clause); } else {// Construct the - 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); convertAndAssert(node[1], true); @@ -693,32 +686,23 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, - ProofRule proof_id, - TNode from) { + bool input) +{ Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; d_removable = removable; - 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); - } - }); + if (d_cnfProof) + { + d_cnfProof->pushCurrentAssertion(negated ? node.notNode() : (Node)node, + input); + } convertAndAssert(node, negated); - PROOF - (if (d_cnfProof) { - d_cnfProof->popCurrentAssertion(); - }); + if (d_cnfProof) + { + d_cnfProof->popCurrentAssertion(); + } } void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 40243e5b9..aec4257f2 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -186,10 +186,13 @@ class CnfStream { * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated + * @param input whether it is an input assertion (rather than a lemma). This + * information is only relevant for unsat core tracking. */ - virtual void convertAndAssert(TNode node, bool removable, bool negated, - ProofRule proof_id, - TNode from = TNode::null()) = 0; + virtual void convertAndAssert(TNode node, + bool removable, + bool negated, + bool input = false) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -269,12 +272,13 @@ class TseitinCnfStream : public CnfStream { * @param node the formula to assert * @param removable is this something that can be erased * @param negated true if negated + * @param input whether it is an input assertion (rather than a lemma). This + * information is only relevant for unsat core tracking. */ void convertAndAssert(TNode node, bool removable, bool negated, - ProofRule rule, - TNode from = TNode::null()) override; + bool input = false) override; private: /** diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index cf23758f1..92817a70c 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -19,8 +19,6 @@ #include "prop/cryptominisat.h" #include "base/check.h" -#include "proof/clause_id.h" -#include "proof/sat_proof.h" #include <cryptominisat5/cryptominisat.h> @@ -87,8 +85,9 @@ void CryptoMinisatSolver::init() CryptoMinisatSolver::~CryptoMinisatSolver() {} ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, - bool rhs, - bool removable) { + bool rhs, + bool removable) +{ Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n"; if (!d_okay) { @@ -97,7 +96,7 @@ ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, } ++(d_statistics.d_xorClausesAdded); - + // ensure all sat literals have positive polarity by pushing // the negation on the result std::vector<CMSatVar> xor_clause; @@ -119,36 +118,19 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ } ++(d_statistics.d_clausesAdded); - + std::vector<CMSat::Lit> internal_clause; toInternalClause(clause, internal_clause); bool nowOkay = d_solver->add_clause(internal_clause); ClauseId freshId; - if (THEORY_PROOF_ON()) - { - freshId = ClauseId(ProofManager::currentPM()->nextId()); - // If this clause results in a conflict, then `nowOkay` may be false, but - // we still need to register this clause as used. Thus, we look at - // `d_okay` instead - if (d_bvp && d_okay) - { - d_bvp->registerUsedClause(freshId, clause); - } - } - else - { - freshId = ClauseIdError; - } + freshId = ClauseIdError; d_okay &= nowOkay; return freshId; } -bool CryptoMinisatSolver::ok() const { - return d_okay; -} - +bool CryptoMinisatSolver::ok() const { return d_okay; } SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ d_solver->new_var(); @@ -208,19 +190,11 @@ SatValue CryptoMinisatSolver::value(SatLiteral l){ return toSatLiteralValue(value); } -SatValue CryptoMinisatSolver::modelValue(SatLiteral l){ - return value(l); -} +SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); } unsigned CryptoMinisatSolver::getAssertionLevel() const { Unreachable() << "No interface to get assertion level in Cryptominisat"; - return -1; -} - -void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp) -{ - d_bvp = bvp; - d_solver->set_drat(&bvp->getDratOstream(), false); + return -1; } // Satistics for CryptoMinisatSolver diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index d60855654..6d3b351b0 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -21,7 +21,6 @@ #ifdef CVC4_USE_CRYPTOMINISAT -#include "proof/clausal_bitvector_proof.h" #include "prop/sat_solver.h" // Cryptominisat has name clashes with the other Minisat implementations since @@ -68,7 +67,6 @@ class CryptoMinisatSolver : public SatSolver SatValue modelValue(SatLiteral l) override; unsigned getAssertionLevel() const override; - void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override; private: class Statistics @@ -97,7 +95,6 @@ class CryptoMinisatSolver : public SatSolver void init(); std::unique_ptr<CMSat::SATSolver> d_solver; - proof::ClausalBitVectorProof* d_bvp; unsigned d_numVariables; bool d_okay; SatVariable d_true; diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp index 0440fcd4e..544a37a3e 100644 --- a/src/prop/kissat.cpp +++ b/src/prop/kissat.cpp @@ -19,7 +19,6 @@ #ifdef CVC4_USE_KISSAT #include "base/check.h" -#include "proof/sat_proof.h" namespace CVC4 { namespace prop { diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index f56f6a447..311224a03 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -30,6 +30,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "options/prop_options.h" #include "options/smt_options.h" #include "proof/clause_id.h" +#include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" #include "proof/sat_proof_implementation.h" @@ -217,7 +218,10 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, propagation_budget(-1), asynch_interrupt(false) { - PROOF(ProofManager::currentPM()->initSatProof(this);) + if (options::unsatCores()) + { + ProofManager::currentPM()->initSatProof(this); + } // Create the constant variables varTrue = newVar(true, false, false); @@ -227,11 +231,11 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); // FIXME: these should be axioms I believe - PROOF - ( - ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false)); - ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true)); - ); + if (options::unsatCores()) + { + ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false)); + ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true)); + } } @@ -390,15 +394,20 @@ CRef Solver::reason(Var x) { // FIXME: at some point will need more information about where this explanation // came from (ie. the theory/sharing) Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; - PROOF(ClauseId id = ProofManager::getSatProof()->registerClause( - real_reason, THEORY_LEMMA); - ProofManager::getCnfProof()->registerConvertedClause(id, true); - // explainPropagation() pushes the explanation on the assertion stack - // in CnfProof, so we need to pop it here. This is important because - // reason() may be called indirectly while adding a clause, which can - // lead to a wrong assertion being associated with the clause being - // added (see issue #2137). - ProofManager::getCnfProof()->popCurrentAssertion();); + if (options::unsatCores()) + { + ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, + THEORY_LEMMA); + // map id to assertion, which may be required if looking for + // lemmas in unsat core + ProofManager::getCnfProof()->registerConvertedClause(id); + // explainPropagation() pushes the explanation on the assertion stack + // in CnfProof, so we need to pop it here. This is important because + // reason() may be called indirectly while adding a clause, which can + // lead to a wrong assertion being associated with the clause being + // added (see issue #2137). + ProofManager::getCnfProof()->popCurrentAssertion(); + } vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -441,9 +450,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } // If a literal is false at 0 level (both sat and user level) we also ignore it if (value(ps[i]) == l_False) { - if (!PROOF_ON() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { + if (!options::unsatCores() && level(var(ps[i])) == 0 + && user_level(var(ps[i])) == 0) + { continue; - } else { + } + else + { // If we decide to keep it, we count it into the false literals falseLiteralsCount ++; } @@ -467,34 +480,46 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); - 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); + if (options::unsatCores()) + { + // Store the expression being converted to CNF until + // the clause is actually created + lemmas_cnf_assertion.push_back( + ProofManager::getCnfProof()->getCurrentAssertion()); + id = ClauseIdUndef; + } } else { assert(decisionLevel() == 0); // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { - if(PROOF_ON()) { + if (options::unsatCores()) + { // Take care of false units here; otherwise, we need to // construct the clause below to give to the proof manager // as the final conflict. if(falseLiteralsCount == 1) { - PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); ) - PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); ) + if (options::unsatCores()) + { + ClauseKind ck = + ProofManager::getCnfProof()->getCurrentAssertionKind() + ? INPUT + : THEORY_LEMMA; + id = ProofManager::getSatProof()->storeUnitConflict(ps[0], ck); + // map id to assertion, which may be required if looking for + // lemmas in unsat core + if (ck == THEORY_LEMMA) + { + ProofManager::getCnfProof()->registerConvertedClause(id); + } + ProofManager::getSatProof()->finalizeProof( + CVC4::Minisat::CRef_Lazy); + } return ok = false; } - } else { + } + else + { return ok = false; } } @@ -509,14 +534,23 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); - attachClause(cr); - - if(PROOF_ON()) { - PROOF( - id = ProofManager::getSatProof()->registerClause(cr, INPUT); - ) - if(ps.size() == falseLiteralsCount) { - PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) + attachClause(cr); + + if (options::unsatCores()) + { + ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind() + ? INPUT + : THEORY_LEMMA; + id = ProofManager::getSatProof()->registerClause(cr, ck); + // map id to assertion, which may be required if looking for + // lemmas in unsat core + if (ck == THEORY_LEMMA) + { + ProofManager::getCnfProof()->registerConvertedClause(id); + } + if (ps.size() == falseLiteralsCount) + { + ProofManager::getSatProof()->finalizeProof(cr); return ok = false; } } @@ -527,15 +561,25 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& 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" << std::endl; - PROOF( - if(ps.size() == 1) { - id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); - } - ); + Debug("cores") << "i'm registering a unit clause, maybe input" + << std::endl; + if (options::unsatCores() && ps.size() == 1) + { + ClauseKind ck = + ProofManager::getCnfProof()->getCurrentAssertionKind() + ? INPUT + : THEORY_LEMMA; + id = ProofManager::getSatProof()->registerUnitClause(ps[0], ck); + // map id to assertion, which may be required if looking for + // lemmas in unsat core + if (ck == THEORY_LEMMA) + { + ProofManager::getCnfProof()->registerConvertedClause(id); + } + } CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { - if (PROOF_ON()) + if (options::unsatCores()) { if (ca[confl].size() == 1) { @@ -552,7 +596,10 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) } return ok; } else { - PROOF(id = ClauseIdUndef;); + if (options::unsatCores()) + { + id = ClauseIdUndef; + } return ok; } } @@ -575,7 +622,10 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; - PROOF( ProofManager::getSatProof()->markDeleted(cr); ); + if (options::unsatCores()) + { + ProofManager::getSatProof()->markDeleted(cr); + } Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); @@ -826,7 +876,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) int max_resolution_level = 0; // Maximal level of the resolved clauses - PROOF( ProofManager::getSatProof()->startResChain(confl); ) + if (options::unsatCores()) + { + ProofManager::getSatProof()->startResChain(confl); + } do{ assert(confl != CRef_Undef); // (otherwise should be UIP) @@ -867,9 +920,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) } // FIXME: can we do it lazily if we actually need the proof? - if (level(var(q)) == 0) + if (options::unsatCores() && level(var(q)) == 0) { - PROOF(ProofManager::getSatProof()->resolveOutUnit(q);) + ProofManager::getSatProof()->resolveOutUnit(q); } } } @@ -881,8 +934,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) seen[var(p)] = 0; pathC--; - if ( pathC > 0 && confl != CRef_Undef ) { - PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); ) + if (options::unsatCores() && pathC > 0 && confl != CRef_Undef) + { + ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); } }while (pathC > 0); @@ -905,7 +959,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) // Literal is not redundant out_learnt[j++] = out_learnt[i]; } else { - PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); ) + if (options::unsatCores()) + { + ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); + } // Literal is redundant, to be safe, mark the level as current assertion level // TODO: maybe optimize max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i]))); @@ -1169,7 +1226,10 @@ void Solver::propagateTheory() { addClause(explanation, true, id); // explainPropagation() pushes the explanation on the assertion // stack in CnfProof, so we need to pop it here. - PROOF(ProofManager::getCnfProof()->popCurrentAssertion();) + if (options::unsatCores()) + { + ProofManager::getCnfProof()->popCurrentAssertion(); + } } } } @@ -1310,9 +1370,10 @@ void Solver::removeSatisfied(vec<CRef>& cs) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (satisfied(c)) { - if (locked(c)) { + if (options::unsatCores() && locked(c)) + { // store a resolution of the literal c propagated - PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); ) + ProofManager::getSatProof()->storeUnitResolution(c[0]); } removeClause(cs[i]); } @@ -1412,8 +1473,11 @@ lbool Solver::search(int nof_conflicts) conflicts++; conflictC++; if (decisionLevel() == 0) { - PROOF( ProofManager::getSatProof()->finalizeProof(confl); ) - return l_False; + if (options::unsatCores()) + { + ProofManager::getSatProof()->finalizeProof(confl); + } + return l_False; } // Analyze the conflict @@ -1425,8 +1489,10 @@ lbool Solver::search(int nof_conflicts) if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause[0]); - PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); ) - + if (options::unsatCores()) + { + ProofManager::getSatProof()->endResChain(learnt_clause[0]); + } } else { CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, @@ -1436,15 +1502,12 @@ lbool Solver::search(int nof_conflicts) attachClause(cr); claBumpActivity(ca[cr]); uncheckedEnqueue(learnt_clause[0], cr); - PROOF(ClauseId id = - ProofManager::getSatProof()->registerClause(cr, LEARNT); - PSTATS(std::unordered_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);); + if (options::unsatCores()) + { + ClauseId id = + ProofManager::getSatProof()->registerClause(cr, LEARNT); + ProofManager::getSatProof()->endResChain(id); + } } varDecayActivity(); @@ -1469,25 +1532,33 @@ lbool Solver::search(int nof_conflicts) } } else { - - // If this was a final check, we are satisfiable - if (check_type == CHECK_FINAL) { - bool decisionEngineDone = d_proxy->isDecisionEngineDone(); - // Unless a lemma has added more stuff to the queues - if (!decisionEngineDone && - (!order_heap.empty() || qhead < trail.size()) ) { - check_type = CHECK_WITH_THEORY; - continue; - } else if (recheck) { - // There some additional stuff added, so we go for another full-check - continue; - } else { - // Yes, we're truly satisfiable - return l_True; - } - } else if (check_type == CHECK_FINAL_FAKE) { + // If this was a final check, we are satisfiable + if (check_type == CHECK_FINAL) + { + bool decisionEngineDone = d_proxy->isDecisionEngineDone(); + // Unless a lemma has added more stuff to the queues + if (!decisionEngineDone + && (!order_heap.empty() || qhead < trail.size())) + { check_type = CHECK_WITH_THEORY; + continue; + } + else if (recheck) + { + // There some additional stuff added, so we go for another + // full-check + continue; } + else + { + // Yes, we're truly satisfiable + return l_True; + } + } + else if (check_type == CHECK_FINAL_FAKE) + { + check_type = CHECK_WITH_THEORY; + } if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget(ResourceManager::Resource::SatConflictStep)) @@ -1744,7 +1815,10 @@ 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, NULLPROOF(ProofManager::getSatProof())); + ca.reloc(ws[j].cref, + to, + CVC4::options::unsatCores() ? ProofManager::getSatProof() + : nullptr); } // All reasons: @@ -1753,22 +1827,31 @@ void Solver::relocAll(ClauseAllocator& to) Var v = var(trail[i]); if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) - ca.reloc( - vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof())); + ca.reloc(vardata[v].d_reason, + to, + CVC4::options::unsatCores() ? ProofManager::getSatProof() + : nullptr); } // All learnt: // for (int i = 0; i < clauses_removable.size(); i++) ca.reloc( - clauses_removable[i], to, NULLPROOF(ProofManager::getSatProof())); + clauses_removable[i], + to, + CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr); // All original: // for (int i = 0; i < clauses_persistent.size(); i++) ca.reloc( - clauses_persistent[i], to, NULLPROOF(ProofManager::getSatProof())); + clauses_persistent[i], + to, + CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr); - PROOF(ProofManager::getSatProof()->finishUpdateCRef();) + if (options::unsatCores()) + { + ProofManager::getSatProof()->finishUpdateCRef(); + } } @@ -1874,7 +1957,7 @@ CRef Solver::updateLemmas() { // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { - Assert(!PROOF_ON()); + Assert(!options::unsatCores()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -1904,7 +1987,8 @@ CRef Solver::updateLemmas() { // Last index in the trail int backtrack_index = trail.size(); - PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size());); + Assert(!options::unsatCores() + || lemmas.size() == (int)lemmas_cnf_assertion.size()); // Attach all the clauses and enqueue all the propagations for (int j = 0; j < lemmas.size(); ++j) @@ -1928,15 +2012,16 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first; - TNode cnf_def = lemmas_cnf_assertion[j].second; - - Debug("pf::sat") - << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerClause( - lemma_ref, THEORY_LEMMA); - ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); - ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);); + if (options::unsatCores()) + { + TNode cnf_assertion = lemmas_cnf_assertion[j]; + + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" + << std::endl; + ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, + THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + } if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1948,17 +2033,15 @@ CRef Solver::updateLemmas() { // If the lemma is propagating enqueue its literal (or set the conflict) if (conflict == CRef_Undef && value(lemma[0]) != l_True) { if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) { - if (PROOF_ON() && lemma.size() == 1) + if (options::unsatCores() && lemma.size() == 1) { - Node cnf_assertion = lemmas_cnf_assertion[j].first; - Node cnf_def = lemmas_cnf_assertion[j].second; + Node cnf_assertion = lemmas_cnf_assertion[j]; Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) " << cnf_assertion << value(lemma[0]) << std::endl; ClauseId id = ProofManager::getSatProof()->registerUnitClause( lemma[0], THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); - ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); } if (value(lemma[0]) == l_False) { @@ -1969,7 +2052,10 @@ 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); ); + if (options::unsatCores()) + { + ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); + } } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; @@ -1979,7 +2065,8 @@ CRef Solver::updateLemmas() { } } - PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size());); + Assert(!options::unsatCores() + || lemmas.size() == (int)lemmas_cnf_assertion.size()); // Clear the lemmas lemmas.clear(); lemmas_cnf_assertion.clear(); diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 508947456..a5f3664e8 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -63,7 +63,7 @@ public: typedef Var TVar; typedef Lit TLit; - typedef Clause TClause; + typedef Clause TClause; typedef CRef TCRef; typedef vec<Lit> TLitVec; @@ -98,7 +98,7 @@ public: vec<bool> lemmas_removable; /** Nodes being converted to CNF */ - std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion; + std::vector<CVC4::Node> lemmas_cnf_assertion; /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -203,7 +203,7 @@ public: lbool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state - void toDimacs (); + void toDimacs(); void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec<Lit>& assumps); void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max); diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index bbd6e17a2..b30d97aee 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -73,9 +73,14 @@ inline bool sign (Lit p) { return p.x & 1; } inline int var (Lit p) { return p.x >> 1; } // Mapping Literals to and from compact integers suitable for array indexing: -inline int toInt (Var v) { return v; } -inline int toInt (Lit p) { return p.x; } -inline Lit toLit (int i) { Lit p; p.x = i; return p; } +inline int toInt(Var v) { return v; } +inline int toInt(Lit p) { return p.x; } +inline Lit toLit(int i) +{ + Lit p; + p.x = i; + return p; +} //const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants. //const Lit lit_Error = mkLit(var_Undef, true ); // } @@ -83,20 +88,19 @@ inline Lit toLit (int i) { Lit p; p.x = i; return p; } const Lit lit_Undef = { -2 }; // }- Useful special constants. const Lit lit_Error = { -1 }; // } - //================================================================================================= // Lifted booleans: // -// NOTE: this implementation is optimized for the case when comparisons between values are mostly -// between one variable and one constant. Some care had to be taken to make sure that gcc -// does enough constant propagation to produce sensible code, and this appears to be somewhat -// fragile unfortunately. +// NOTE: this implementation is optimized for the case when comparisons between +// values are mostly +// between one variable and one constant. Some care had to be taken to +// make sure that gcc does enough constant propagation to produce sensible +// code, and this appears to be somewhat fragile unfortunately. /* - This is to avoid multiple definitions of l_True, l_False and l_Undef if using multiple copies of - Minisat. - IMPORTANT: if we you change the value of the constants so that it is not the same in all copies - of Minisat this breaks! + This is to avoid multiple definitions of l_True, l_False and l_Undef if using + multiple copies of Minisat. IMPORTANT: if we you change the value of the + constants so that it is not the same in all copies of Minisat this breaks! */ #ifndef l_True @@ -124,10 +128,12 @@ public: bool operator != (lbool b) const { return !(*this == b); } lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); } - lbool operator && (lbool b) const { - uint8_t sel = (this->value << 1) | (b.value << 3); - uint8_t v = (0xF7F755F4 >> sel) & 3; - return lbool(v); } + lbool operator&&(lbool b) const + { + uint8_t sel = (this->value << 1) | (b.value << 3); + uint8_t v = (0xF7F755F4 >> sel) & 3; + return lbool(v); + } lbool operator || (lbool b) const { uint8_t sel = (this->value << 1) | (b.value << 3); @@ -163,7 +169,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>& } inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) { - std::string val_str; + std::string val_str; if( val == l_False ) { val_str = "0"; } else if (val == l_True ) { @@ -208,14 +214,14 @@ class Clause { header.size = ps.size(); header.level = level; - for (int i = 0; i < ps.size(); i++) - data[i].lit = ps[i]; + for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i]; if (header.has_extra){ if (header.removable) - data[header.size].act = 0; - else - calcAbstraction(); } + data[header.size].act = 0; + else + calcAbstraction(); + } } public: @@ -321,7 +327,7 @@ class OccLists public: OccLists(const Deleted& d) : deleted(d) {} - + void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); } void resizeTo (const Idx& idx); // Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; } @@ -394,13 +400,12 @@ class CMap typedef Map<CRef, T, CRefHash> HashTable; HashTable map; - + public: // Size-operations: void clear () { map.clear(); } int size () const { return map.elems(); } - // Insert/Remove/Test mapping: void insert (CRef cr, const T& t){ map.insert(cr, t); } void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility @@ -423,15 +428,14 @@ class CMap printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); } }; - /*_________________________________________________________________________________________________ | | subsumes : (other : const Clause&) -> Lit -| +| | Description: -| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' -| by subsumption resolution. -| +| Checks if clause subsumes 'other', and at the same time, if it can be +used to simplify 'other' | by subsumption resolution. +| | Result: | lit_Error - No subsumption or simplification | lit_Undef - Clause subsumes 'other' diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index a4d2dce8a..25353e416 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -154,7 +154,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { return ClauseIdUndef; } d_minisat->addClause(minisat_clause, removable, clause_id); - PROOF(Assert(clause_id != ClauseIdError);); + Assert(!CVC4::options::unsatCores() || clause_id != ClauseIdError); return clause_id; } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 23f97b5d5..0ec8981ca 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/simp/SimpSolver.h" #include "options/prop_options.h" +#include "options/smt_options.h" #include "proof/clause_id.h" -#include "proof/proof.h" #include "prop/minisat/mtl/Sort.h" #include "prop/minisat/utils/System.h" @@ -47,25 +47,30 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: - -SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) : - Solver(proxy, context, enableIncremental) - , grow (opt_grow) - , clause_lim (opt_clause_lim) - , subsumption_lim (opt_subsumption_lim) - , simp_garbage_frac (opt_simp_garbage_frac) - , use_asymm (opt_use_asymm) - , use_rcheck (opt_use_rcheck) - , use_elim (options::minisatUseElim() && !enableIncremental) - , merges (0) - , asymm_lits (0) - , eliminated_vars (0) - , elimorder (1) - , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially - , occurs (ClauseDeleted(ca)) - , elim_heap (ElimLt(n_occ)) - , bwdsub_assigns (0) - , n_touched (0) +SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, + CVC4::context::Context* context, + bool enableIncremental) + : Solver(proxy, context, enableIncremental), + grow(opt_grow), + clause_lim(opt_clause_lim), + subsumption_lim(opt_subsumption_lim), + simp_garbage_frac(opt_simp_garbage_frac), + use_asymm(opt_use_asymm), + use_rcheck(opt_use_rcheck), + use_elim(options::minisatUseElim() && !enableIncremental), + merges(0), + asymm_lits(0), + eliminated_vars(0), + elimorder(1), + use_simplification( + !enableIncremental + && !options::unsatCores()) // TODO: turn off simplifications if + // proofs are on initially + , + occurs(ClauseDeleted(ca)), + elim_heap(ElimLt(n_occ)), + bwdsub_assigns(0), + n_touched(0) { if(options::minisatUseElim() && options::minisatUseElim.wasSetByUser() && @@ -117,8 +122,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { if (options::minisatDumpDimacs()) { - toDimacs(); - return l_Undef; + toDimacs(); + return l_Undef; } assert(decisionLevel() == 0); @@ -533,9 +538,10 @@ bool SimpSolver::eliminateVar(Var v) 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, clause_size) && - (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim))) - return true; + if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) + && (++cnt > cls.size() + grow + || (clause_lim != -1 && clause_size > clause_lim))) + return true; // Delete and store old clauses: eliminated[v] = true; @@ -552,10 +558,9 @@ bool SimpSolver::eliminateVar(Var v) mkElimClause(elimclauses, ~mkLit(v)); } - for (int i = 0; i < cls.size(); i++) - removeClause(cls[i]); + for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); - ClauseId id = ClauseIdUndef; + ClauseId id = ClauseIdUndef; // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) @@ -569,7 +574,7 @@ bool SimpSolver::eliminateVar(Var v) // Free occurs list for this variable: occurs[v].clear(true); - + // Free watchers lists for this variable, if possible: if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true); if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true); @@ -589,7 +594,7 @@ bool SimpSolver::substitute(Var v, Lit x) eliminated[v] = true; setDecisionVar(v, false); const vec<CRef>& cls = occurs.lookup(v); - + vec<Lit>& subst_clause = add_tmp; for (int i = 0; i < cls.size(); i++){ Clause& c = ca[cls[i]]; @@ -641,9 +646,12 @@ bool SimpSolver::eliminate(bool turn_off_elim) gatherTouchedClauses(); // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns); - if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && - !backwardSubsumptionCheck(true)){ - ok = false; goto cleanup; } + if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) + && !backwardSubsumptionCheck(true)) + { + ok = false; + goto cleanup; + } // Empty elim_heap and return immediately on user-interrupt: if (asynch_interrupt){ @@ -656,7 +664,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size()); for (int cnt = 0; !elim_heap.empty(); cnt++){ Var elim = elim_heap.removeMin(); - + if (asynch_interrupt) break; if (isEliminated(elim) || value(elim) != l_Undef) continue; @@ -706,8 +714,10 @@ bool SimpSolver::eliminate(bool turn_off_elim) } if (verbosity >= 1 && elimclauses.size() > 0) - printf("| Eliminated clauses: %10.2f Mb |\n", - double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + printf( + "| Eliminated clauses: %10.2f Mb " + " |\n", + double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024)); return ok; } @@ -744,11 +754,11 @@ void SimpSolver::relocAll(ClauseAllocator& to) // for (int i = 0; i < subsumption_queue.size(); i++) ca.reloc(subsumption_queue[i], to); - // TODO reloc now takes the proof form the core solver + // TODO reloc now takes the proof form the core solver // Temporary clause: // ca.reloc(bwdsub_tmpunit, to); - // TODO reloc now takes the proof form the core solver + // TODO reloc now takes the proof form the core solver } @@ -756,15 +766,17 @@ void SimpSolver::garbageCollect() { // Initialize the next region to a size corresponding to the estimated utilization degree. This // is not precise but should avoid some unnecessary reallocations for the new region: - ClauseAllocator to(ca.size() - ca.wasted()); + ClauseAllocator to(ca.size() - ca.wasted()); cleanUpClauses(); to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields. relocAll(to); Solver::relocAll(to); if (verbosity >= 2) - printf("| Garbage collection: %12d bytes => %12d bytes |\n", - ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + printf( + "| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size() * ClauseAllocator::Unit_Size, + to.size() * ClauseAllocator::Unit_Size); to.moveTo(ca); - // TODO: proof.finalizeUpdateId(); + // TODO: proof.finalizeUpdateId(); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f74e52509..e71e681e5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -99,17 +99,17 @@ PropEngine::PropEngine(TheoryEngine* te, d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); - PROOF ( - ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); - ); + if (options::unsatCores()) + { + ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext); + } } void PropEngine::finishInit() { NodeManager* nm = NodeManager::currentNM(); - d_cnfStream->convertAndAssert(nm->mkConst(true), false, false, RULE_GIVEN); - d_cnfStream->convertAndAssert( - nm->mkConst(false).notNode(), false, false, RULE_GIVEN); + d_cnfStream->convertAndAssert(nm->mkConst(true), false, false); + d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false); } PropEngine::~PropEngine() { @@ -126,18 +126,15 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN); + d_cnfStream->convertAndAssert(node, false, false, true); } -void PropEngine::assertLemma(TNode node, bool negated, - bool removable, - ProofRule rule, - TNode from) { - //Assert(d_inCheckSat, "Sat solver should be in solve()!"); +void PropEngine::assertLemma(TNode node, bool negated, bool removable) +{ Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as (possibly) removable - d_cnfStream->convertAndAssert(node, removable, negated, rule, from); + d_cnfStream->convertAndAssert(node, removable, negated); } void PropEngine::addAssertionsToDecisionEngine( diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 9a2daee49..1df862568 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -103,11 +103,7 @@ class PropEngine * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, - bool negated, - bool removable, - ProofRule rule, - TNode from = TNode::null()); + void assertLemma(TNode node, bool negated, bool removable); /** * Pass a list of assertions from an AssertionPipeline to the decision engine. diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index d4b08ab71..1526e91b9 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -33,11 +33,6 @@ namespace CVC4 { -namespace proof { -class ClausalBitVectorProof; -class ResolutionBitVectorProof; -} // namespace proof - namespace prop { class TheoryProxy; @@ -58,7 +53,7 @@ public: /** Add a clause corresponding to rhs = l1 xor .. xor ln */ virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0; - + /** * Create a new boolean variable in the solver. * @param isTheoryAtom is this a theory atom that needs to be asserted to theory @@ -84,6 +79,7 @@ public: virtual SatValue solve(const std::vector<SatLiteral>& assumptions) { Unimplemented() << "Solving under assumptions not implemented"; + return SAT_VALUE_UNKNOWN; }; /** Interrupt the solver */ @@ -101,10 +97,6 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {} - - virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {} - };/* class SatSolver */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 41da4546e..d0ba4ca71 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -76,22 +76,12 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - LemmaProofRecipe* proofRecipe = NULL; - PROOF(proofRecipe = new LemmaProofRecipe;); + Node theoryExplanation = d_theoryEngine->getExplanation(lNode); - Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe); - - PROOF({ - ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); - ProofManager::getCnfProof()->setProofRecipe(proofRecipe); - - Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: " - << std::endl; - proofRecipe->dump("pf::sat"); - - delete proofRecipe; - proofRecipe = NULL; - }); + if (options::unsatCores()) + { + ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); + } Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl; if (theoryExplanation.getKind() == kind::AND) { |