Improved compatibility layer, now supports quantifiers. Also incorporates

numerous bugfixes, and the cvc3 system test is enabled.

4 files changed, 27 insertions, 23 deletions

diff --git a/src/smt/options b/src/smt/options
index 13b3b51f3..fea609bb5 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -21,7 +21,7 @@ common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-
 expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
  expand define-funs/LAMBDAs lazily
 
-option simplificationMode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
+option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
  choose simplification mode, see --simplification=help
 alias --no-simplification = --simplification=none
  turn off all simplification (same as --simplification=none)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bcd7cc6d2..d450319b1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -310,6 +310,16 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_context->push();
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+}
+
+void SmtEngine::finishInit() {
+  d_decisionEngine = new DecisionEngine(d_context, d_userContext);
+  d_decisionEngine->init();   // enable appropriate strategies
+
+  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
+
+  d_theoryEngine->setPropEngine(d_propEngine);
+  d_theoryEngine->setDecisionEngine(d_decisionEngine);
 
   // [MGD 10/20/2011] keep around in incremental mode, due to a
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
@@ -336,16 +346,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   }
 }
 
-void SmtEngine::finishInit() {
-  d_decisionEngine = new DecisionEngine(d_context, d_userContext);
-  d_decisionEngine->init();   // enable appropriate strategies
-
-  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
-
-  d_theoryEngine->setPropEngine(d_propEngine);
-  d_theoryEngine->setDecisionEngine(d_decisionEngine);
-}
-
 void SmtEngine::finalOptionsAreSet() {
   if(d_fullyInited) {
     return;
@@ -1534,7 +1534,7 @@ void SmtEnginePrivate::addFormula(TNode n)
   }
 }
 
-void SmtEngine::ensureBoolean(const BoolExpr& e) {
+void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) {
   Type type = e.getType(options::typeChecking());
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
@@ -1546,7 +1546,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) {
   }
 }
 
-Result SmtEngine::checkSat(const BoolExpr& e) {
+Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
 
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
@@ -1608,7 +1608,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   return r;
 }
 
-Result SmtEngine::query(const BoolExpr& e) {
+Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
 
   Assert(!e.isNull());
   Assert(e.getExprManager() == d_exprManager);
@@ -1667,7 +1667,7 @@ Result SmtEngine::query(const BoolExpr& e) {
   return r;
 }
 
-Result SmtEngine::assertFormula(const BoolExpr& e) {
+Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -1680,7 +1680,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
   return quickCheck().asValidityResult();
 }
 
-Expr SmtEngine::simplify(const Expr& e) {
+Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -1691,6 +1691,9 @@ Expr SmtEngine::simplify(const Expr& e) {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SimplifyCommand(e);
   }
+  // Make sure we've done simple preprocessing, unit detection, etc.
+  Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
+  d_private->processAssertions();
   return d_private->applySubstitutions(e).toExpr();
 }
 
@@ -1912,6 +1915,7 @@ vector<Expr> SmtEngine::getAssertions()
     throw ModalException(msg);
   }
   Assert(d_assertionList != NULL);
+  // copy the result out
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 43a7ee58d..25800f5b3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -234,7 +234,7 @@ class CVC4_PUBLIC SmtEngine {
    * Fully type-check the argument, and also type-check that it's
    * actually Boolean.
    */
-  void ensureBoolean(const BoolExpr& e);
+  void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException);
 
   void internalPush();
 
@@ -337,20 +337,20 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(const BoolExpr& e);
+  Result assertFormula(const BoolExpr& e) throw(TypeCheckingException);
 
   /**
    * Check validity of an expression with respect to the current set
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const BoolExpr& e);
+  Result query(const BoolExpr& e) throw(TypeCheckingException);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const BoolExpr& e = BoolExpr());
+  Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException);
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -361,7 +361,7 @@ public:
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
    */
-  Expr simplify(const Expr& e);
+  Expr simplify(const Expr& e) throw(TypeCheckingException);
 
   /**
    * Get the assigned value of an expr (only if immediately preceded
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index b254a3b30..1af029f17 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -52,7 +52,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 
 #line 54 "${template}"
 
-  throw UnrecognizedOptionException();
+  throw UnrecognizedOptionException(key);
 }
 
 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
@@ -69,7 +69,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 
 #line 71 "${template}"
 
-  throw UnrecognizedOptionException();
+  throw UnrecognizedOptionException(key);
 }
 
 }/* CVC4 namespace */