diff options
Diffstat (limited to 'src/prop/cryptominisat.cpp')
| -rw-r--r-- | src/prop/cryptominisat.cpp | 29 |
1 files changed, 22 insertions, 7 deletions
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index df5a20791..c04fb8b56 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -62,10 +62,11 @@ void toInternalClause(SatClause& clause, CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, const std::string& name) -: d_solver(new CMSat::SATSolver()) -, d_numVariables(0) -, d_okay(true) -, d_statistics(registry, name) + : d_solver(new CMSat::SATSolver()), + d_bvp(nullptr), + d_numVariables(0), + d_okay(true), + d_statistics(registry, name) { d_true = newVar(); d_false = newVar(); @@ -117,9 +118,17 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ std::vector<CMSat::Lit> internal_clause; toInternalClause(clause, internal_clause); - bool res = d_solver->add_clause(internal_clause); - d_okay &= res; - return ClauseIdError; + bool nowOkay = d_solver->add_clause(internal_clause); + ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId()); + + THEORY_PROOF( + // 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); }) + + d_okay &= nowOkay; + return freshId; } bool CryptoMinisatSolver::ok() const { @@ -193,6 +202,12 @@ unsigned CryptoMinisatSolver::getAssertionLevel() const { return -1; } +void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp) +{ + d_bvp = bvp; + d_solver->set_drat(&bvp->getDratOstream(), false); +} + // Satistics for CryptoMinisatSolver CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry, |