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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 72ce3804d..ebec37031 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -281,6 +281,32 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_SELECTOR:
     break;
 
+    // quantifiers
+  case kind::FORALL: out << "forall "; break;
+  case kind::EXISTS: out << "exists "; break;
+  case kind::BOUND_VAR_LIST:
+    out << '(';
+    for(TNode::iterator i = n.begin(),
+          iend = n.end();
+        i != iend; ) {
+      out << '(';
+      (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                    types, language::output::LANG_SMTLIB_V2);
+      out << ' ';
+      (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                              false, language::output::LANG_SMTLIB_V2);
+      out << ')';
+      if(++i != iend) {
+        out << ' ';
+      }
+    }
+    out << ')';
+    return;
+  case kind::INST_PATTERN:
+  case kind::INST_PATTERN_LIST:
+    // TODO user patterns
+    break;
+
   default:
     // fall back on however the kind prints itself; this probably
     // won't be SMT-LIB v2 compliant, but it will be clear from the