diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/prop/minisat/minisat.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
-rw-r--r-- | src/prop/minisat/minisat.cpp | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ff726e299..bfbf9da6f 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { // 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; + return ClauseIdUndef; } d_minisat->addClause(minisat_clause, removable, clause_id); PROOF( Assert (clause_id != ClauseIdError);); @@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() { } bool MinisatSatSolver::ok() const { - return d_minisat->okay(); + return d_minisat->okay(); } void MinisatSatSolver::interrupt() { @@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const return true; } -void MinisatSatSolver::requirePhase(SatLiteral lit) { +void MinisatSatSolver::requirePhase(SatLiteral lit) { Assert(!d_minisat->rnd_pol); Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl; SatVariable v = lit.getSatVariable(); d_minisat->freezePolarity(v, lit.isNegated()); } -bool MinisatSatSolver::flipDecision() { +bool MinisatSatSolver::flipDecision() { Debug("minisat") << "flipDecision()" << std::endl; return d_minisat->flipDecision(); } -bool MinisatSatSolver::isDecision(SatVariable decn) const { - return d_minisat->isDecision( decn ); +bool MinisatSatSolver::isDecision(SatVariable decn) const { + return d_minisat->isDecision( decn ); } /** Incremental interface */ @@ -291,7 +291,7 @@ 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, @@ -300,3 +300,5 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& } } /* namespace CVC4 */ + + |