command-line flag to disable theory registration, also SMT-LIBv2 compliance (per...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 296abe0e133aaef4a6771d3c62467e2002c6c495..151f7237b241d66b5c80b8300199845548b232df 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -253,23 +253,13 @@ SExpr SmtEngine::getInfo(const std::string& key) const
 void SmtEngine::setOption(const std::string& key, const SExpr& value)
   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") {
     throw BadOptionException();
   } else if(key == ":interactive-mode") {
     throw BadOptionException();
-  } else if(key == ":produce-proofs") {
-    throw BadOptionException();
-  } else if(key == ":produce-unsat-cores") {
-    throw BadOptionException();
-  } else if(key == ":produce-models") {
-    throw BadOptionException();
-  } else if(key == ":produce-assignments") {
-    throw BadOptionException();
   } else if(key == ":regular-output-channel") {
     throw BadOptionException();
   } else if(key == ":diagnostic-output-channel") {
@@ -279,7 +269,23 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
   } else if(key == ":verbosity") {
     throw BadOptionException();
   } else {
-    throw BadOptionException();
+    // The following options can only be set at the beginning; we throw
+    // a ModalException if someone tries.
+    if(d_logic != "") {
+      throw ModalException("logic already set; cannot set options");
+    }
+
+    if(key == ":produce-proofs") {
+      throw BadOptionException();
+    } else if(key == ":produce-unsat-cores") {
+      throw BadOptionException();
+    } else if(key == ":produce-models") {
+      throw BadOptionException();
+    } else if(key == ":produce-assignments") {
+      throw BadOptionException();
+    } else {
+      throw BadOptionException();
+    }
   }
 }
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 40debc7c7ac6786309215a278e637b84850467ba..eb4c1816178fff14023b6af4fed69295cd757701 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -65,7 +65,8 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
     // Automatically track all asserted equalities in the shared term manager
     d_engine->getSharedTermManager()->addEq(fact);
   }
-  if(! fact.getAttribute(RegisteredAttr())) {
+
+  if(d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
     list<TNode> toReg;
     toReg.push_back(fact);
 
@@ -123,12 +124,13 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
         d_engine->theoryOf(n)->registerTerm(n);
       }
     }
-  }
+  }/* d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
 }
 
 TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
   d_propEngine(NULL),
   d_theoryOut(this, ctxt),
+  d_theoryRegistration(opts.theoryRegistration),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
   d_statistics() {

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7e08a29d5a859d1d1eb0f4f71d99fc98ae4f71ed..b2f0478247699a922caa3d8c7b45978abb9d37db 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -135,6 +135,12 @@ class TheoryEngine {
   theory::Theory* d_arrays;
   theory::Theory* d_bv;
 
+  /**
+   * Whether or not theory registration is on.  May not be safe to
+   * turn off with some theories.
+   */
+  bool d_theoryRegistration;
+
   /**
    * Debugging flag to ensure that shutdown() is called before the
    * destructor.

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 6d3a06b4b88d669e0a2dd52037cee5cb93aa0581..dbfed887d13fff85fff4e6eb323ff290d6274efd 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -52,6 +52,7 @@ static const string optionsDescription = "\
    --eager-type-checking  type check expressions immediately on creation\n\
    --no-type-checking     never type check expressions\n\
    --no-checking          disable ALL semantic checks, including type checks \n\
+   --no-theory-registration disable theory reg (not safe for some theories)\n\
    --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
    --verbose | -v         increase verbosity (repeatable)\n\
    --quiet | -q           decrease verbosity (repeatable)\n\
@@ -103,6 +104,7 @@ enum OptionValue {
   SEGV_NOSPIN,
   PARSE_ONLY,
   NO_CHECKING,
+  NO_THEORY_REGISTRATION,
   USE_MMAP,
   SHOW_CONFIG,
   STRICT_PARSING,
@@ -151,6 +153,7 @@ static struct option cmdlineOptions[] = {
   { "trace"      , required_argument, NULL, 't'         },
   { "stats"      , no_argument      , NULL, STATS       },
   { "no-checking", no_argument      , NULL, NO_CHECKING },
+  { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
   { "show-config", no_argument      , NULL, SHOW_CONFIG },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
   { "help"       , no_argument      , NULL, 'h'         },
@@ -268,6 +271,10 @@ throw(OptionException) {
       parseOnly = true;
       break;
 
+    case NO_THEORY_REGISTRATION:
+      theoryRegistration = false;
+      break;
+
     case NO_CHECKING:
       semanticChecks = false;
       typeChecking = false;

diff --git a/src/util/options.h b/src/util/options.h
index 8cf0b84461364d2a4c8c240e7eba6ea1c42bb778..60c8f2a1a3d8045cb2c2e2e51272ac9c7e8ee18f 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -90,6 +90,9 @@ struct CVC4_PUBLIC Options {
   /** Should the parser do semantic checks? */
   bool semanticChecks;
 
+  /** Should the TheoryEngine do theory registration? */
+  bool theoryRegistration;
+
   /** Should the parser memory-map file input? */
   bool memoryMap;
 
@@ -134,6 +137,7 @@ struct CVC4_PUBLIC Options {
     uf_implementation(MORGAN),
     parseOnly(false),
     semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
+    theoryRegistration(true),
     memoryMap(false),
     strictParsing(false),
     lazyDefinitionExpansion(false),