LogicInfo locking implemented, and some initialization-order issues in SmtEngine...

ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers.  In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 67d873a483517b940a7838b76c849bee482ed070..52d98435eb71ef3a87a005451b6eeb43f5c24276 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -270,6 +270,10 @@ void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
   }
 }
 
+void AntlrInput::warning(const std::string& message) {
+  Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl;
+}
+
 void AntlrInput::parseError(const std::string& message)
   throw (ParserException, AssertionException) {
   Debug("parser") << "Throwing exception: "

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index bdf5fe59ee0e97df9892ddb36a72f4ef99779fee..84b5099fb4c99e74d00def19bd823bbe54d09d10 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -196,6 +196,11 @@ protected:
    * <code>setLexer()</code>. */
   pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
 
+  /**
+   * Issue a non-fatal warning to the user with file, line, and column info.
+   */
+  void warning(const std::string& msg);
+
   /**
    * Throws a <code>ParserException</code> with the given message.
    */

diff --git a/src/parser/input.h b/src/parser/input.h
index 8fa51a0957f089b18044b851efc1a437fc01fcfa..92b039edabfa487d51e665fcfc8c32a65f6bbee4 100644 (file)
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -166,6 +166,11 @@ protected:
   virtual Command* parseCommand()
     throw (ParserException, TypeCheckingException, AssertionException) = 0;
 
+  /**
+   * Issue a warning to the user, with source file, line, and column info.
+   */
+  virtual void warning(const std::string& msg) = 0;
+
   /**
    * Throws a <code>ParserException</code> with the given message.
    */

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 405e397b83dc3b044b3b1e8021b64d9b1729170e..a3ddba0138c65e1db7c3fe667cabe6540973d15f 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -457,6 +457,11 @@ public:
   /** Parse and return the next expression. */
   Expr nextExpression() throw(ParserException);
 
+  /** Issue a warning to the user. */
+  inline void warning(const std::string& msg) {
+    d_input->warning(msg);
+  }
+
   /** Raise a parse error with the given message. */
   inline void parseError(const std::string& msg) throw(ParserException) {
     d_input->parseError(msg);

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index b9db8daced356e52401736428969b212565bb263..c3b81655c7207fa6925905f999cf566176e945c6 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -54,6 +54,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
+  logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
   return logicMap;
 }
 
@@ -248,6 +250,16 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_REALS);
     break;
 
+  case ALL_SUPPORTED:
+    /* fall through */
+  case QF_ALL_SUPPORTED:
+    addTheory(THEORY_ARRAYS_EX);
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case AUFLIA:
   case AUFLIRA:
   case AUFNIRA:

diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 34ec624bc28a497c7fc5c9dc8c7a3205bce19f2b..d77808930f619fa8f90712909bd3bfce036b0640 100644 (file)
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -65,7 +65,9 @@ public:
     QF_UFNIRA, // nonstandard
     QF_UFNRA,
     UFLRA,
-    UFNIA
+    UFNIA,
+    QF_ALL_SUPPORTED, // nonstandard
+    ALL_SUPPORTED // nonstandard
   };
 
   enum Theory {

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 19f77ac87842dcc92050e616d103713558824c92..d711ddab53761aa7a8eb37fae830bf17c94e55bd 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -191,6 +191,7 @@ command returns [CVC4::Command* cmd = NULL]
     DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
     { Debug("parser") << "declare sort: '" << name
                       << "' arity=" << n << std::endl;
+      PARSER_STATE->checkThatLogicIsSet();
       unsigned arity = AntlrInput::tokenToUnsigned(n);
       if(arity == 0) {
         Type type = PARSER_STATE->mkSort(name);
@@ -204,6 +205,7 @@ command returns [CVC4::Command* cmd = NULL]
     DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
     {
+      PARSER_STATE->checkThatLogicIsSet();
       PARSER_STATE->pushScope();
       for(std::vector<std::string>::const_iterator i = names.begin(),
             iend = names.end();
@@ -224,6 +226,7 @@ command returns [CVC4::Command* cmd = NULL]
     LPAREN_TOK sortList[sorts] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
+      PARSER_STATE->checkThatLogicIsSet();
       if( sorts.size() > 0 ) {
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
@@ -235,6 +238,7 @@ command returns [CVC4::Command* cmd = NULL]
     sortSymbol[t,CHECK_DECLARED]
     { /* add variables to parser state before parsing term */
       Debug("parser") << "define fun: '" << name << "'" << std::endl;
+      PARSER_STATE->checkThatLogicIsSet();
       if( sortedVarNames.size() > 0 ) {
         std::vector<CVC4::Type> sorts;
         sorts.reserve(sortedVarNames.size());
@@ -263,13 +267,9 @@ command returns [CVC4::Command* cmd = NULL]
       $cmd = new DefineFunctionCommand(name, func, terms, expr);
     }
   | /* value query */
-    ( GET_VALUE_TOK
-      { if(PARSER_STATE->strictModeEnabled()) {
-          PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\".  Maybe you want (get-value...)?");
-        }
-      } )
-    LPAREN_TOK termList[terms,expr] RPAREN_TOK
-    { if(terms.size() == 1) {
+    GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
+    { PARSER_STATE->checkThatLogicIsSet();
+      if(terms.size() == 1) {
         $cmd = new GetValueCommand(terms[0]);
       } else {
         CommandSequence* seq = new CommandSequence();
@@ -284,24 +284,31 @@ command returns [CVC4::Command* cmd = NULL]
     }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK
-    { cmd = new GetAssignmentCommand; }
+    { PARSER_STATE->checkThatLogicIsSet();
+      cmd = new GetAssignmentCommand; }
   | /* assertion */
     ASSERT_TOK term[expr]
-    { cmd = new AssertCommand(expr); }
+    { PARSER_STATE->checkThatLogicIsSet();
+      cmd = new AssertCommand(expr); }
   | /* checksat */
     CHECKSAT_TOK
-    { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
+    { PARSER_STATE->checkThatLogicIsSet();
+      cmd = new CheckSatCommand(MK_CONST(bool(true))); }
   | /* get-assertions */
     GET_ASSERTIONS_TOK
-    { cmd = new GetAssertionsCommand; }
+    { PARSER_STATE->checkThatLogicIsSet();
+      cmd = new GetAssertionsCommand; }
   | /* get-proof */
     GET_PROOF_TOK
-    { cmd = new GetProofCommand; }
+    { PARSER_STATE->checkThatLogicIsSet();
+      cmd = new GetProofCommand; }
   | /* get-unsat-core */
     GET_UNSAT_CORE_TOK
-    { UNSUPPORTED("unsat cores not yet supported"); }
+    { PARSER_STATE->checkThatLogicIsSet();
+      UNSUPPORTED("unsat cores not yet supported"); }
   | /* push */
     PUSH_TOK
+    { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
       { unsigned n = AntlrInput::tokenToUnsigned(k);
         if(n == 0) {
@@ -323,6 +330,7 @@ command returns [CVC4::Command* cmd = NULL]
         }
       } )
   | POP_TOK
+    { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
       { unsigned n = AntlrInput::tokenToUnsigned(k);
         if(n == 0) {
@@ -348,7 +356,8 @@ command returns [CVC4::Command* cmd = NULL]
 
     /* CVC4-extended SMT-LIBv2 commands */
   | extendedCommand[cmd]
-    { if(PARSER_STATE->strictModeEnabled()) {
+    { PARSER_STATE->checkThatLogicIsSet();
+      if(PARSER_STATE->strictModeEnabled()) {
         PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
       }
     }

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3fa00baaecf82d469dacb2ba4ec4adae9ca33327..709ba087f5ce1e6120e5d00ba65c07f5b1f3fa9c 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -17,6 +17,7 @@
  **/
 
 #include "expr/type.h"
+#include "expr/command.h"
 #include "parser/parser.h"
 #include "parser/smt/smt.h"
 #include "parser/smt2/smt2.h"
@@ -193,6 +194,16 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_REALS);
     break;
 
+  case Smt::ALL_SUPPORTED:
+    /* fall through */
+  case Smt::QF_ALL_SUPPORTED:
+    addTheory(THEORY_ARRAYS);
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case Smt::AUFLIA:
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
@@ -211,5 +222,22 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
 }
 
+void Smt2::checkThatLogicIsSet() {
+  if( ! logicIsSet() ) {
+    if( strictModeEnabled() ) {
+      parseError("set-logic must appear before this point.");
+    } else {
+      warning("No set-logic command was given before this point.");
+      warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
+      warning("Consider setting a stricter logic for (likely) better performance.");
+      warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
+
+      setLogic("ALL_SUPPORTED");
+
+      preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+    }
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index e9363b9701eff0ffb96443cd62f127a2d44d66bc..b71f635581bb5036f921f2992e13dc6ad13c9cc9 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -72,6 +72,8 @@ public:
 
   void setOption(const std::string& flag, const SExpr& sexpr);
 
+  void checkThatLogicIsSet();
+
 private:
 
   void addArithmeticOperators();

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5b71e5ec581eca4a05f572d902880426a1711f2f..58270b4d0a186c46fcc745a22533f0ee4444c03f 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -247,6 +247,10 @@ void PropEngine::pop() {
   Debug("prop") << "pop()" << endl;
 }
 
+unsigned PropEngine::getAssertionLevel() const {
+  return d_satSolver->getAssertionLevel();
+}
+
 bool PropEngine::isRunning() const {
   return d_inCheckSat;
 }

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 9e49cf3f10b8fb580d61f485882d877b8ec44491..603cdb0e6df118ee2aad07ba84df2fd94fc4922a 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -245,6 +245,11 @@ public:
    */
   void pop();
 
+  /**
+   * Get the assertion level of the SAT solver.
+   */
+  unsigned getAssertionLevel() const;
+
   /**
    * Return true if we are currently searching (either in this or
    * another thread).

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8b3e6b7424b3b32e01c2308917a71a04303bfac7..ed28c23a3a3ee7ca6434d88ec58bc76b129e061b 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -242,7 +242,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_assertionList(NULL),
   d_assignments(NULL),
   d_logic(),
-  d_logicIsSet(false),
+  d_fullyInited(false),
   d_problemExtended(false),
   d_queryMade(false),
   d_needPostsolve(false),
@@ -328,6 +328,19 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   if(Options::current()->cumulativeMillisecondLimit != 0) {
     setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
   }
+}
+
+void SmtEngine::finalOptionsAreSet() {
+  if(d_fullyInited) {
+    return;
+  }
+
+  AlwaysAssert( d_propEngine->getAssertionLevel() == 0,
+                "The PropEngine has pushed but the SmtEngine "
+                "hasn't finished initializing!" );
+
+  d_fullyInited = true;
+  d_logic.lock();
 
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
@@ -401,15 +414,12 @@ SmtEngine::~SmtEngine() throw() {
 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   NodeManagerScope nms(d_nodeManager);
 
-  if(d_logicIsSet) {
-    throw ModalException("logic already set");
-  }
-
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
   }
 
-  setLogicInternal(logic);
+  d_logic = logic;
+  setLogicInternal();
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
@@ -418,57 +428,63 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
   setLogic(LogicInfo(s));
 }
 
-void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
-  d_logic = logic;
+// This function is called when d_logic has just been changed.
+// The LogicInfo isn't passed in explicitly, because that might
+// tempt people in the code to use the (potentially unlocked)
+// version that's passed in, leading to assert-fails in certain
+// uses of the CVC4 library.
+void SmtEngine::setLogicInternal() throw(AssertionException) {
+  Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run");
+
+  d_logic.lock();
 
   // by default, symmetry breaker is on only for QF_UF
   if(! Options::current()->ufSymmetryBreakerSetByUser) {
-    bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified();
+    bool qf_uf = d_logic.isPure(theory::THEORY_UF) && !d_logic.isQuantified();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
     NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
   }
   // by default, nonclausal simplification is off for QF_SAT
   if(! Options::current()->simplificationModeSetByUser) {
-    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
-    Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
+    bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified();
+    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << std::endl;
     NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
   }
 
   // If in arrays, set the UF handler to arrays
-  if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) {
+  if(d_logic.isPure(theory::THEORY_ARRAY) && !d_logic.isQuantified()) {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
   } else {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
   }
   // Turn on ite simplification for QF_LIA and QF_AUFBV
   if(! Options::current()->doITESimpSetByUser) {
-    bool iteSimp = !logic.isQuantified() &&
-      ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() &&  !logic.areRealsUsed()) ||
-       (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)));
+    bool iteSimp = !d_logic.isQuantified() &&
+      ((d_logic.isPure(theory::THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areRealsUsed()) ||
+       (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV)));
     Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
     NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! Options::current()->repeatSimpSetByUser) {
-    bool repeatSimp = !logic.isQuantified() &&
-      (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV));
+    bool repeatSimp = !d_logic.isQuantified() &&
+      (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV));
     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
     NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
   }
   // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
   if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
-    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+    bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified();
     bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
     NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
   }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! Options::current()->arithRewriteEqSetByUser) {
-    bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
+    bool arithRewriteEq = d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified();
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
     NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
   }
-
 }
 
 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
@@ -496,7 +512,8 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
           throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
         }
         NodeManagerScope nms(d_nodeManager);
-        setLogicInternal(value.getValue());
+        d_logic = value.getValue();
+        setLogicInternal();
         return;
       }
     }
@@ -592,7 +609,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
   } else {
     // The following options can only be set at the beginning; we throw
     // a ModalException if someone tries.
-    if(d_logicIsSet) {
+    if(d_logic.isLocked()) {
       throw ModalException("logic already set; cannot set options");
     }
 
@@ -761,8 +778,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHas
   }
 }
 
-
 void SmtEnginePrivate::removeITEs() {
+  d_smt.finalOptionsAreSet();
+
   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 
   // Remove all of the ITE occurrences and normalize
@@ -774,6 +792,7 @@ void SmtEnginePrivate::removeITEs() {
 }
 
 void SmtEnginePrivate::staticLearning() {
+  d_smt.finalOptionsAreSet();
 
   TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime);
 
@@ -793,6 +812,7 @@ void SmtEnginePrivate::staticLearning() {
 }
 
 void SmtEnginePrivate::nonClausalSimplify() {
+  d_smt.finalOptionsAreSet();
 
   TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime);
 
@@ -1072,6 +1092,8 @@ void SmtEnginePrivate::simplifyAssertions()
 }
 
 Result SmtEngine::check() {
+  Assert(d_fullyInited);
+
   Trace("smt") << "SmtEngine::check()" << endl;
 
   // Make sure the prop layer has all of the assertions
@@ -1124,11 +1146,13 @@ Result SmtEngine::check() {
 }
 
 Result SmtEngine::quickCheck() {
+  Assert(d_fullyInited);
   Trace("smt") << "SMT quickCheck()" << endl;
   return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 }
 
 void SmtEnginePrivate::processAssertions() {
+  Assert(d_smt.d_fullyInited);
 
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
@@ -1252,6 +1276,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
   NodeManagerScope nms(d_nodeManager);
 
+  finalOptionsAreSet();
+
   Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
 
   if(d_queryMade && !Options::current()->incrementalSolving) {
@@ -1313,6 +1339,8 @@ Result SmtEngine::query(const BoolExpr& e) {
 
   NodeManagerScope nms(d_nodeManager);
 
+  finalOptionsAreSet();
+
   Trace("smt") << "SMT query(" << e << ")" << endl;
 
   if(d_queryMade && !Options::current()->incrementalSolving) {
@@ -1366,6 +1394,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
   ensureBoolean(e);
   if(d_assertionList != NULL) {
@@ -1378,6 +1407,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) {
 Expr SmtEngine::simplify(const Expr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   if( Options::current()->typeChecking ) {
     e.getType(true);// ensure expr is type-checked at this point
   }
@@ -1435,6 +1465,7 @@ Expr SmtEngine::getValue(const Expr& e)
 
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Type type = e.getType(Options::current()->typeChecking);
   // must be Boolean
   CheckArgument( type.isBoolean(), e,
@@ -1463,6 +1494,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getAssignment()" << endl;
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssignmentCommand();
   }
@@ -1519,6 +1551,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getProof()" << endl;
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetProofCommand();
   }
@@ -1566,6 +1599,7 @@ size_t SmtEngine::getStackLevel() const {
 
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Trace("smt") << "SMT push()" << endl;
   d_private->processAssertions();
   if(Dump.isOn("benchmark")) {
@@ -1589,6 +1623,7 @@ void SmtEngine::push() {
 
 void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
+  finalOptionsAreSet();
   Trace("smt") << "SMT pop()" << endl;
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PopCommand();
@@ -1624,6 +1659,7 @@ void SmtEngine::pop() {
 }
 
 void SmtEngine::internalPush() {
+  Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPush()" << endl;
   if(Options::current()->incrementalSolving) {
     d_private->processAssertions();
@@ -1634,6 +1670,7 @@ void SmtEngine::internalPush() {
 }
 
 void SmtEngine::internalPop() {
+  Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPop()" << endl;
   if(Options::current()->incrementalSolving) {
     d_propEngine->pop();

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f07815e2e73331376b51c871125629701939c720..4c0fed74cfd65374434178ea4a34da144def802f 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -135,9 +135,12 @@ class CVC4_PUBLIC SmtEngine {
   LogicInfo d_logic;
 
   /**
-   * Whether the logic has been set yet.
+   * Whether or not this SmtEngine has been fully initialized (that is,
+   * the ).  This post-construction initialization is automatically
+   * triggered by the use of the SmtEngine; e.g. when setLogic() is
+   * called, or the first assertion is made, etc.
    */
-  bool d_logicIsSet;
+  bool d_fullyInited;
 
   /**
    * Whether or not we have added any assertions/declarations/definitions
@@ -184,6 +187,14 @@ class CVC4_PUBLIC SmtEngine {
    */
   smt::SmtEnginePrivate* d_private;
 
+  /**
+   * This is something of an "init" procedure, but is idempotent; call
+   * as often as you like.  Should be called whenever the final options
+   * and logic for the problem are set (at least, those options that are
+   * not permitted to change after assertions and queries are made).
+   */
+  void finalOptionsAreSet();
+
   /**
    * This is called by the destructor, just before destroying the
    * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
@@ -216,9 +227,10 @@ class CVC4_PUBLIC SmtEngine {
   void internalPop();
 
   /**
-   * Internally handle the setting of a logic.
+   * Internally handle the setting of a logic.  This function should always
+   * be called when d_logic is updated.
    */
-  void setLogicInternal(const LogicInfo& logic) throw();
+  void setLogicInternal() throw(AssertionException);
 
   friend class ::CVC4::smt::SmtEnginePrivate;
 

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index ba7119071bb1fe924898265ef2555c0ac5127c0e..d0c1e4b6a8ada5a8e0b66f422fc769cf5c02e72c 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -37,7 +37,9 @@ LogicInfo::LogicInfo() :
   d_sharingTheories(0),
   d_integers(true),
   d_reals(true),
-  d_linear(false) {
+  d_linear(false),
+  d_differenceLogic(false),
+  d_locked(false) {
 
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
     d_theories[id] = false;// ensure it's cleared
@@ -51,11 +53,16 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
   d_sharingTheories(0),
   d_integers(false),
   d_reals(false),
-  d_linear(false) {
+  d_linear(false),
+  d_differenceLogic(false),
+  d_locked(false) {
+
   setLogicString(logicString);
+  lock();
 }
 
 std::string LogicInfo::getLogicString() const {
+  Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
   if(d_logicString == "") {
     size_t seen = 0; // make sure we support all the active theories
 
@@ -108,6 +115,7 @@ std::string LogicInfo::getLogicString() const {
 }
 
 void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
     d_theories[id] = false;// ensure it's cleared
   }
@@ -124,6 +132,16 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
   if(!strcmp(p, "QF_SAT") || *p == '\0') {
     // propositional logic only; we're done.
     p += 6;
+  } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
+    // the "all theories included" logic, no quantifiers
+    enableEverything();
+    disableQuantifiers();
+    p += 16;
+  } else if(!strcmp(p, "ALL_SUPPORTED")) {
+    // the "all theories included" logic, with quantifiers
+    enableEverything();
+    enableQuantifiers();
+    p += 13;
   } else {
     if(!strncmp(p, "QF_", 3)) {
       disableQuantifiers();
@@ -211,7 +229,18 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
   d_logicString = logicString;
 }
 
+void LogicInfo::enableEverything() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  *this = LogicInfo();
+}
+
+void LogicInfo::disableEverything() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
+  *this = LogicInfo("");
+}
+
 void LogicInfo::enableTheory(theory::TheoryId theory) {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   if(!d_theories[theory]) {
     if(isTrueTheory(theory)) {
       ++d_sharingTheories;
@@ -222,6 +251,7 @@ void LogicInfo::enableTheory(theory::TheoryId theory) {
 }
 
 void LogicInfo::disableTheory(theory::TheoryId theory) {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   if(d_theories[theory]) {
     if(isTrueTheory(theory)) {
       Assert(d_sharingTheories > 0);
@@ -237,12 +267,14 @@ void LogicInfo::disableTheory(theory::TheoryId theory) {
 }
 
 void LogicInfo::enableIntegers() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   enableTheory(THEORY_ARITH);
   d_integers = true;
 }
 
 void LogicInfo::disableIntegers() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_integers = false;
   if(!d_reals) {
@@ -251,12 +283,14 @@ void LogicInfo::disableIntegers() {
 }
 
 void LogicInfo::enableReals() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   enableTheory(THEORY_ARITH);
   d_reals = true;
 }
 
 void LogicInfo::disableReals() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_reals = false;
   if(!d_integers) {
@@ -265,21 +299,34 @@ void LogicInfo::disableReals() {
 }
 
 void LogicInfo::arithOnlyDifference() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = true;
 }
 
 void LogicInfo::arithOnlyLinear() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = true;
   d_differenceLogic = false;
 }
 
 void LogicInfo::arithNonLinear() {
+  Assert(!d_locked, "This LogicInfo is locked, and cannot be modified");
   d_logicString = "";
   d_linear = false;
   d_differenceLogic = false;
 }
 
+LogicInfo LogicInfo::getUnlockedCopy() const {
+  if(d_locked) {
+    LogicInfo info = *this;
+    info.d_locked = false;
+    return info;
+  } else {
+    return *this;
+  }
+}
+
 }/* CVC4 namespace */

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index d5b8be58d2913691b39d96a8fbd1f79b459f649e..33a059bb98f57ac4f915e025a8edd52ad68f5480 100644 (file)
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -54,6 +54,8 @@ class LogicInfo {
   bool d_linear; /**< linear-only arithmetic in this logic? */
   bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
 
+  bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
+
   /**
    * Returns true iff this is a "true" theory (one that must be worried
    * about for sharing
@@ -95,12 +97,19 @@ public:
   std::string getLogicString() const;
 
   /** Is sharing enabled for this logic? */
-  bool isSharingEnabled() const { return d_sharingTheories > 1; }
+  bool isSharingEnabled() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    return d_sharingTheories > 1;
+  }
   /** Is the given theory module active in this logic? */
-  bool isTheoryEnabled(theory::TheoryId theory) const { return d_theories[theory]; }
+  bool isTheoryEnabled(theory::TheoryId theory) const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    return d_theories[theory];
+  }
 
   /** Is this a quantified logic? */
   bool isQuantified() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
     return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
   }
 
@@ -110,6 +119,7 @@ public:
    * use "isPure(theory) && !isQuantified()".
    */
   bool isPure(theory::TheoryId theory) const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
     // the third and fourth conjucts are really just to rule out the misleading
     // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
     return isTheoryEnabled(theory) && !isSharingEnabled() &&
@@ -120,13 +130,25 @@ public:
   // these are for arithmetic
 
   /** Are integers in this logic? */
-  bool areIntegersUsed() const { return d_integers; }
+  bool areIntegersUsed() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    return d_integers;
+  }
   /** Are reals in this logic? */
-  bool areRealsUsed() const { return d_reals; }
+  bool areRealsUsed() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    return d_reals;
+  }
   /** Does this logic only linear arithmetic? */
-  bool isLinear() const { return d_linear || d_differenceLogic; }
+  bool isLinear() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    return d_linear || d_differenceLogic;
+  }
   /** Does this logic only permit difference reasoning? (implies linear) */
-  bool isDifferenceLogic() const { return d_differenceLogic; }
+  bool isDifferenceLogic() const {
+    Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
+    return d_differenceLogic;
+  }
 
   // MUTATORS
 
@@ -137,6 +159,18 @@ public:
    */
   void setLogicString(std::string logicString) throw(IllegalArgumentException);
 
+  /**
+   * Enable all functionality.  All theories, plus quantifiers, will be
+   * enabled.
+   */
+  void enableEverything();
+
+  /**
+   * Disable all functionality.  The result will be a LogicInfo with
+   * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
+   */
+  void disableEverything();
+
   /**
    * Enable the given theory module.
    */
@@ -181,6 +215,15 @@ public:
   /** Permit nonlinear arithmetic in this logic. */
   void arithNonLinear();
 
+  // LOCKING FUNCTIONALITY
+
+  /** Lock this LogicInfo, disabling further mutation and allowing queries */
+  void lock() { d_locked = true; }
+  /** Check whether this LogicInfo is locked, disallowing further mutation */
+  bool isLocked() const { return d_locked; }
+  /** Get a copy of this LogicInfo that is identical, but unlocked */
+  LogicInfo getUnlockedCopy() const;
+
 };/* class LogicInfo */
 
 }/* CVC4 namespace */

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index c24104acc582eff0eb53fd64a7737e2002c2a3a9..de05105826aab5fb16a91b2b147ef5874160dba2 100644 (file)
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -146,6 +146,7 @@ class CnfStreamBlack : public CxxTest::TestSuite {
     NodeManagerScope nms(d_nodeManager);
     d_satSolver = new FakeSatSolver();
     d_logicInfo = new LogicInfo();
+    d_logicInfo->lock();
     d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
     d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
     d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
@@ -200,9 +201,15 @@ public:
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
+  void testTrue() {
+    NodeManagerScope nms(d_nodeManager);
+    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
+    TS_ASSERT( d_satSolver->addClauseCalled() );
+  }
+
   void testFalse() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert(  d_nodeManager->mkConst(false), false, false );
+    d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
@@ -255,12 +262,6 @@ public:
     TS_ASSERT( d_satSolver->addClauseCalled() );
   }
 
-  void testTrue() {
-    NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert(  d_nodeManager->mkConst(true), false, false );
-    TS_ASSERT( d_satSolver->addClauseCalled() );
-  }
-
   void testVar() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 8bb3b52df0d0e891c9b24cadaf8eb0d5b209073b..70ebdc7f8508fb1d62edba2a477c04509039c80c 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -32,11 +32,12 @@ public:
 
   void testSmtlibLogics() {
     LogicInfo info("QF_SAT");
+    TS_ASSERT( info.isLocked() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
 
-    info.setLogicString("AUFLIA");
+    info = LogicInfo("AUFLIA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
@@ -44,13 +45,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("AUFLIRA");
+    info = LogicInfo("AUFLIRA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
@@ -58,13 +60,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("AUFNIRA");
+    info = LogicInfo("AUFNIRA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
@@ -72,13 +75,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( !info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("LRA");
+    info = LogicInfo("LRA");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
@@ -87,13 +91,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("QF_ABV");
+    info = LogicInfo("QF_ABV");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
@@ -102,9 +107,10 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
 
-    info.setLogicString("QF_AUFBV");
+    info = LogicInfo("QF_AUFBV");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -112,9 +118,10 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
 
-    info.setLogicString("QF_AUFLIA");
+    info = LogicInfo("QF_AUFLIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -122,13 +129,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("QF_AX");
+    info = LogicInfo("QF_AX");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -136,9 +144,10 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARRAY ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
 
-    info.setLogicString("QF_BV");
+    info = LogicInfo("QF_BV");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -146,9 +155,10 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
 
-    info.setLogicString("QF_IDL");
+    info = LogicInfo("QF_IDL");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -156,13 +166,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("QF_LIA");
+    info = LogicInfo("QF_LIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -170,13 +181,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("QF_LRA");
+    info = LogicInfo("QF_LRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -185,12 +197,13 @@ public:
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("QF_NIA");
+    info = LogicInfo("QF_NIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -199,12 +212,13 @@ public:
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( !info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("QF_NRA");
+    info = LogicInfo("QF_NRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -212,13 +226,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( !info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("QF_RDL");
+    info = LogicInfo("QF_RDL");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -226,13 +241,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("QF_UF");
+    info = LogicInfo("QF_UF");
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
@@ -244,7 +260,7 @@ public:
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
 
-    info.setLogicString("QF_UFBV");
+    info = LogicInfo("QF_UFBV");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -253,9 +269,10 @@ public:
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
 
-    info.setLogicString("QF_UFIDL");
+    info = LogicInfo("QF_UFIDL");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -263,13 +280,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("QF_UFLIA");
+    info = LogicInfo("QF_UFLIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -277,13 +295,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
 
-    info.setLogicString("QF_UFLRA");
+    info = LogicInfo("QF_UFLRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -297,7 +316,7 @@ public:
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("QF_UFNRA");
+    info = LogicInfo("QF_UFNRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -305,13 +324,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( !info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("UFLRA");
+    info = LogicInfo("UFLRA");
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -319,13 +339,14 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( !info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
 
-    info.setLogicString("UFNIA");
+    info = LogicInfo("UFNIA");
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
@@ -333,15 +354,78 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( !info.isLinear() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.areRealsUsed() );
+
+    info = LogicInfo("QF_ALL_SUPPORTED");
+    TS_ASSERT( info.isLocked() );
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areRealsUsed() );
+
+    info = LogicInfo("ALL_SUPPORTED");
+    TS_ASSERT( info.isLocked() );
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isQuantified() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areRealsUsed() );
   }
 
   void testDefaultLogic() {
     LogicInfo info;
+    TS_ASSERT( !info.isLocked() );
+
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException );
+#endif /* CVC4_ASSERTIONS */
+
+    info.lock();
+    TS_ASSERT( info.isLocked() );
     TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTNIRA" );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) );
@@ -367,21 +451,126 @@ public:
     TS_ASSERT( info.areRealsUsed() );
     TS_ASSERT( ! info.isLinear() );
 
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException );
+    TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException );
+#endif /* CVC4_ASSERTIONS */
+
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
     info.arithOnlyLinear();
     info.disableIntegers();
+    info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" );
+
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
     info.disableQuantifiers();
+    info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" );
+
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_BV);
     info.disableTheory(THEORY_DATATYPES);
     info.enableIntegers();
     info.disableReals();
+    info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" );
+
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_ARITH);
     info.disableTheory(THEORY_UF);
+    info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
     TS_ASSERT( info.isPure( THEORY_ARRAY ) );
     TS_ASSERT( ! info.isQuantified() );
+
+    // check all-excluded logic
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
+    info.disableEverything();
+    info.lock();
+    TS_ASSERT( info.isLocked() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( !info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( !info.areRealsUsed() );
+
+    // check copy is unchanged
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
+    info.lock();
+    TS_ASSERT( info.isLocked() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( !info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( !info.areRealsUsed() );
+
+    // check all-included logic
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
+    info.enableEverything();
+    info.lock();
+    TS_ASSERT( info.isLocked() );
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isQuantified() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areRealsUsed() );
+
+    // check copy is unchanged
+    info = info.getUnlockedCopy();
+    TS_ASSERT( !info.isLocked() );
+    info.lock();
+    TS_ASSERT( info.isLocked() );
+    TS_ASSERT( !info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isQuantified() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areRealsUsed() );
   }
 
 };/* class LogicInfoWhite */