cleanup, documentation, SMT-LIBv2 compliance

2 files changed, 24 insertions, 12 deletions

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.