cleanup, documentation, SMT-LIBv2 compliance

7 files changed, 55 insertions, 19 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 60b48542b..b17e98b38 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -20,11 +20,13 @@
 #include <vector>
 #include <utility>
 #include <iterator>
+#include <sstream>
 
 #include "expr/command.h"
 #include "smt/smt_engine.h"
 #include "smt/bad_option_exception.h"
 #include "util/output.h"
+#include "util/sexpr.h"
 
 using namespace std;
 
@@ -337,7 +339,18 @@ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
 }
 
 void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
-  // FIXME: TODO: something to be done with the status
+  stringstream ss;
+  ss << d_status;
+  SExpr status = ss.str();
+  try {
+    smtEngine->setInfo(":status", status);
+    //d_result = "success";
+  } catch(ModalException& m) {
+    d_result = "error";
+  } catch(BadOptionException& bo) {
+    // should not happen
+    d_result = "error";
+  }
 }
 
 void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
@@ -351,7 +364,12 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
 }
 
 void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
-  // FIXME: TODO: something to be done with the logic
+  try {
+    smtEngine->setLogic(d_logic);
+    //d_result = "success";
+  } catch(ModalException& m) {
+    d_result = "error";
+  }
 }
 
 void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
@@ -369,6 +387,8 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     //d_result = "success";
+  } catch(ModalException& m) {
+    d_result = "error";
   } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
@@ -429,6 +449,8 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     //d_result = "success";
+  } catch(ModalException& m) {
+    d_result = "error";
   } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
diff --git a/src/expr/command.h b/src/expr/command.h
index 172ddea86..fbb48b6b0 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -196,6 +196,7 @@ public:
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 protected:
+  std::string d_result;
   BenchmarkStatus d_status;
 public:
   SetBenchmarkStatusCommand(BenchmarkStatus status);
@@ -205,6 +206,7 @@ public:
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 protected:
+  std::string d_result;
   std::string d_logic;
 public:
   SetBenchmarkLogicCommand(std::string logic);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index e307732f4..96d1925de 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -72,7 +72,7 @@ protected:
   /**
    * Asserts the given clause to the sat solver.
    * @param node the node giving rise to this clause
-   * @param clause the clasue to assert
+   * @param clause the clause to assert
    */
   void assertClause(TNode node, SatClause& clause);
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5fc846a6c..296abe0e1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -151,7 +151,6 @@ void SmtEngine::init(const Options& opts) throw() {
   d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion;
   d_produceModels = opts.produceModels;
   d_produceAssignments = opts.produceAssignments;
-
 }
 
 void SmtEngine::shutdown() {
@@ -180,8 +179,15 @@ SmtEngine::~SmtEngine() {
   delete d_decisionEngine;
 }
 
+void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+  if(d_logic != "") {
+    throw ModalException("logic already set");
+  }
+  d_logic = s;
+}
+
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
-  throw(BadOptionException) {
+  throw(BadOptionException, ModalException) {
   Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(key == ":name" ||
      key == ":source" ||
@@ -245,8 +251,11 @@ SExpr SmtEngine::getInfo(const std::string& key) const
 }
 
 void SmtEngine::setOption(const std::string& key, const SExpr& value)
-  throw(BadOptionException) {
+  throw(BadOptionException, ModalException) {
   Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
+  if(d_logic != "") {
+    throw ModalException("logic already set; cannot set options");
+  }
   if(key == ":print-success") {
     throw BadOptionException();
   } else if(key == ":expand-definitions") {
@@ -490,13 +499,6 @@ Expr SmtEngine::getValue(const Expr& e)
   Assert(e.getExprManager() == d_exprManager);
   Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point
   Debug("smt") << "SMT getValue(" << e << ")" << endl;
-  /* FIXME - for SMT-LIBv2 compliance, we need to check this ?!
-  if(!d_interactive) {
-    const char* msg =
-      "Cannot get value when not in interactive mode.";
-    throw ModalException(msg);
-  }
-  */
   if(!d_produceModels) {
     const char* msg =
       "Cannot get value when produce-models options is off.";
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a73dbdad9..854399bd7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -119,6 +119,11 @@ class CVC4_PUBLIC SmtEngine {
   AssignmentSet* d_assignments;
 
   /**
+   * The logic we're in.
+   */
+  std::string d_logic;
+
+  /**
    * Whether or not we have added any
    * assertions/declarations/definitions since the last checkSat/query
    * (and therefore we're not responsible for an assignment).
@@ -205,10 +210,15 @@ public:
   ~SmtEngine();
 
   /**
+   * Set the logic of the script.
+   */
+  void setLogic(const std::string& logic) throw(ModalException);
+
+  /**
    * Set information about the script executing.
    */
   void setInfo(const std::string& key, const SExpr& value)
-    throw(BadOptionException);
+    throw(BadOptionException, ModalException);
 
   /**
    * Query information about the SMT environment.
@@ -220,7 +230,7 @@ public:
    * Set an aspect of the current SMT execution environment.
    */
   void setOption(const std::string& key, const SExpr& value)
-    throw(BadOptionException);
+    throw(BadOptionException, ModalException);
 
   /**
    * Get an aspect of the current SMT execution environment.
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 1d2e4ed8b..6d3a06b4b 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -351,6 +351,7 @@ throw(OptionException) {
       break;
 
     case LAZY_TYPE_CHECKING:
+      typeChecking = true;
       earlyTypeChecking = false;
       break;
 
diff --git a/src/util/options.h b/src/util/options.h
index 350c031c7..8cf0b8446 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -29,9 +29,9 @@
 
 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else
+#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif
+#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 
 #include <iostream>
 #include <string>
@@ -178,10 +178,9 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
- 
-
 }/* CVC4 namespace */
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 
 #endif /* __CVC4__OPTIONS_H */