Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

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 {