diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/prop/bvminisat/bvminisat.cpp | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/prop/bvminisat/bvminisat.cpp')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 45 |
1 files changed, 28 insertions, 17 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index fa5f53113..46b521e6b 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -22,14 +22,15 @@ using namespace CVC4; using namespace prop; -BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext) +BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name) : context::ContextNotifyObj(mainSatContext, false), d_minisat(new BVMinisat::SimpSolver(mainSatContext)), d_minisatNotify(0), d_solveCount(0), d_assertionsCount(0), d_assertionsRealCount(mainSatContext, 0), - d_lastPropagation(mainSatContext, 0) + d_lastPropagation(mainSatContext, 0), + d_statistics(name) { d_statistics.init(d_minisat); } @@ -61,6 +62,7 @@ SatValue BVMinisatSatSolver::propagate() { void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) { d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit))); + markUnremovable(lit); } void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) { @@ -113,9 +115,9 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ } else { d_minisat->setConfBudget(resource); } - BVMinisat::vec<BVMinisat::Lit> empty; + // BVMinisat::vec<BVMinisat::Lit> empty; unsigned long conflictsBefore = d_minisat->conflicts; - SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + SatValue result = toSatLiteralValue(d_minisat->solveLimited()); d_minisat->clearInterrupt(); resource = d_minisat->conflicts - conflictsBefore; Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl; @@ -211,20 +213,24 @@ void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, // Satistics for BVMinisatSatSolver -BVMinisatSatSolver::Statistics::Statistics() : - d_statStarts("theory::bv::bvminisat::starts"), - d_statDecisions("theory::bv::bvminisat::decisions"), - d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), - d_statPropagations("theory::bv::bvminisat::propagations"), - d_statConflicts("theory::bv::bvminisat::conflicts"), - d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), - d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), - d_statMaxLiterals("theory::bv::bvminisat::max_literals"), - d_statTotLiterals("theory::bv::bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars"), - d_statCallsToSolve("theory::bv::bvminisat::calls_to_solve", 0), - d_statSolveTime("theory::bv::bvminisat::solve_time", 0) +BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) : + d_statStarts("theory::bv::"+prefix+"bvminisat::starts"), + d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"), + d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"), + d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"), + d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"), + d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0), + d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0), + d_registerStats(!prefix.empty()) { + if (!d_registerStats) + return; + StatisticsRegistry::registerStat(&d_statStarts); StatisticsRegistry::registerStat(&d_statDecisions); StatisticsRegistry::registerStat(&d_statRndDecisions); @@ -240,6 +246,8 @@ BVMinisatSatSolver::Statistics::Statistics() : } BVMinisatSatSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; StatisticsRegistry::unregisterStat(&d_statStarts); StatisticsRegistry::unregisterStat(&d_statDecisions); StatisticsRegistry::unregisterStat(&d_statRndDecisions); @@ -255,6 +263,9 @@ BVMinisatSatSolver::Statistics::~Statistics() { } void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ + if (!d_registerStats) + return; + d_statStarts.setData(minisat->starts); d_statDecisions.setData(minisat->decisions); d_statRndDecisions.setData(minisat->rnd_decisions); |