diff options
Diffstat (limited to 'src/prop/bvminisat')
| -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 |
6 files changed, 191 insertions, 409 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); } |