From 2ba4f51d43406c9475116abbab7f3ebea94679af Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 30 Apr 2013 13:42:50 -0400 Subject: added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma --- src/prop/bvminisat/bvminisat.cpp | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) (limited to 'src/prop') diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ab25fa6cb..fa5f53113 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -101,6 +101,7 @@ void BVMinisatSatSolver::interrupt(){ } SatValue BVMinisatSatSolver::solve(){ + ++d_statistics.d_statCallsToSolve; return toSatLiteralValue(d_minisat->solve()); } @@ -121,30 +122,6 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } -// SatValue BVMinisatSatSolver::solve(const context::CDList & assumptions, bool only_bcp){ -// ++d_solveCount; -// ++d_statistics.d_statCallsToSolve; - -// Debug("sat::minisat") << "Solve with assumptions "; -// context::CDList::const_iterator it = assumptions.begin(); -// BVMinisat::vec assump; -// for(; it!= assumptions.end(); ++it) { -// SatLiteral lit = *it; -// Debug("sat::minisat") << lit <<" "; -// assump.push(toMinisatLit(lit)); -// } -// Debug("sat::minisat") <<"\n"; - -// clock_t begin, end; -// begin = clock(); -// d_minisat->setOnlyBCP(only_bcp); -// SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); -// end = clock(); -// d_statistics.d_statSolveTime = d_statistics.d_statSolveTime.getData() + (end - begin)/(double)CLOCKS_PER_SEC; -// return result; -// } - - void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { // TODO add assertion to check the call was after an unsat call for (int i = 0; i < d_minisat->conflict.size(); ++i) { -- cgit v1.2.3