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, 16 insertions, 0 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 6b02153c7..6fa698bd0 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -178,6 +178,22 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const
return true;
}
+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() {
+ Debug("minisat") << "flipDecision()" << std::endl;
+ return d_minisat->flipDecision();
+}
+
+bool MinisatSatSolver::isDecision(SatVariable decn) const {
+ return d_minisat->isDecision( decn );
+}
+
/** Incremental interface */
unsigned MinisatSatSolver::getAssertionLevel() const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback