diff options
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
-rw-r--r-- | src/prop/minisat/minisat.cpp | 41 |
1 files changed, 31 insertions, 10 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ce5c1eb92..739d9087a 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -23,6 +23,7 @@ #include "options/prop_options.h" #include "options/smt_options.h" #include "prop/minisat/simp/SimpSolver.h" +#include "proof/sat_proof.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -94,14 +95,6 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, - SatClause& sat_clause) { - for (int i = 0; i < clause.size(); ++i) { - sat_clause.push_back(toSatLiteral(clause[i])); - } - Assert((unsigned)clause.size() == sat_clause.size()); -} - void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { @@ -149,10 +142,18 @@ void MinisatSatSolver::setupOptions() { d_minisat->restart_inc = options::satRestartInc(); } -void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { +ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { Minisat::vec<Minisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable, proof_id); + ClauseId clause_id = ClauseIdError; + // FIXME: This relies on the invariant that when ok() is false + // the SAT solver does not add the clause (which is what Minisat currently does) + if (!ok()) { + return ClauseIdUndef; + } + d_minisat->addClause(minisat_clause, removable, clause_id); + PROOF( Assert (clause_id != ClauseIdError);); + return clause_id; } SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { @@ -182,6 +183,9 @@ SatValue MinisatSatSolver::solve() { return toSatLiteralValue(d_minisat->solve()); } +bool MinisatSatSolver::ok() const { + return d_minisat->okay(); +} void MinisatSatSolver::interrupt() { d_minisat->interrupt(); @@ -280,3 +284,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ } /* namespace CVC4::prop */ } /* namespace CVC4 */ + + +namespace CVC4 { +template<> +prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) { + return prop::MinisatSatSolver::toSatLiteral(lit); +} + +template<> +void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl, + prop::SatClause& sat_cl) { + prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl); +} + +} /* namespace CVC4 */ + + |