summaryrefslogtreecommitdiff
path: root/src/prop/minisat/minisat.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
-rw-r--r--src/prop/minisat/minisat.cpp16
1 files changed, 7 insertions, 9 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index bfbf9da6f..ff726e299 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,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause&
}
} /* namespace CVC4 */
-
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback