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, 7 insertions, 0 deletions

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index bf1370090..44f009bc0 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -94,6 +94,13 @@ public:
     return LemmaStatus(Node::null(), 0);
   }
 
+  void requirePhase(TNode, bool) throw(Interrupted, AssertionException) {
+  }
+
+  bool flipDecision() throw(Interrupted, AssertionException) {
+    return true;
+  }
+
   void setIncomplete() throw(AssertionException) {}
 
   void clear() {