diff options
author | lianah <lianahady@gmail.com> | 2013-04-30 13:42:50 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | 2ba4f51d43406c9475116abbab7f3ebea94679af (patch) | |
tree | 389e05d0b432bdc44d9d797f9ffbb84d811bd994 /src/prop/bvminisat/bvminisat.cpp | |
parent | 94dc66d4cb4061a80bffe1ec72d2ab98e44dd626 (diff) |
added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma
Diffstat (limited to 'src/prop/bvminisat/bvminisat.cpp')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 25 |
1 files changed, 1 insertions, 24 deletions
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<SatLiteral> & assumptions, bool only_bcp){ -// ++d_solveCount; -// ++d_statistics.d_statCallsToSolve; - -// Debug("sat::minisat") << "Solve with assumptions "; -// context::CDList<SatLiteral>::const_iterator it = assumptions.begin(); -// BVMinisat::vec<BVMinisat::Lit> 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) { |