New LogicInfo functionality.

src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps
track of which theories are active (which should remain constant throughout
the life of an SmtEngine) and other details (like integers, reals,
linear/nonlinear, etc.).

This class has a default constructor which is the most all-inclusive logic.
Alternatively, this class can be constructed from an SMT-LIB logic string
(the empty string gives the same as "QF_SAT").  Once constructed, theories
can be enabled or disabled, quantifiers flipped on and off, integers flipped
on and off, etc.  At any point an SMT-LIB-like logic string can be extracted.  

The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine
(and, in turn, the theories) only a const reference to it.  This ensures that
the logic info doesn't mutate over the course of the run.

As part of this commit, the TheoryEngine's old notion of "active theories"
has been completely removed.  As a result, SMT benchmarks that are incorrectly
tagged with a logic will assert-fail or worse.  (We should probably fail
more gracefully in this case.)  One such example was bug303.smt2,
which used UF reasoning but was tagged QF_LIA.  This has been fixed.

5 files changed, 394 insertions, 3 deletions

diff --git a/test/regress/regress0/bug303.smt2 b/test/regress/regress0/bug303.smt2
index bf603bc62..611147e6e 100644
--- a/test/regress/regress0/bug303.smt2
+++ b/test/regress/regress0/bug303.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_LIA)
+(set-logic QF_UFLIA)
 (set-info :status unsat)
 
 ;; don't use a datatypes for currently focusing in uf
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index bb0b5ea08..9dbb12ae3 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,5 +1,6 @@
 # All unit tests
 UNIT_TESTS = \
+	theory/logic_info_white \
 	theory/theory_engine_white \
 	theory/theory_black \
 	theory/theory_arith_white \
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 5c20b534d..63ba95b57 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -110,6 +110,9 @@ class CnfStreamBlack : public CxxTest::TestSuite {
   /** The SAT solver proxy */
   FakeSatSolver* d_satSolver;
 
+  /** The logic info */
+  LogicInfo* d_logicInfo;
+
   /** The theory engine */
   TheoryEngine* d_theoryEngine;
 
@@ -134,7 +137,8 @@ class CnfStreamBlack : public CxxTest::TestSuite {
     d_nodeManager = new NodeManager(d_context, NULL);
     NodeManagerScope nms(d_nodeManager);
     d_satSolver = new FakeSatSolver();
-    d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+    d_logicInfo = new LogicInfo();
+    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);
     d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
@@ -146,6 +150,7 @@ class CnfStreamBlack : public CxxTest::TestSuite {
     delete d_cnfStream;
     d_theoryEngine->shutdown();
     delete d_theoryEngine;
+    delete d_logicInfo;
     delete d_satSolver;
     delete d_nodeManager;
     delete d_userContext;
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
new file mode 100644
index 000000000..77d18bd72
--- /dev/null
+++ b/test/unit/theory/logic_info_white.h
@@ -0,0 +1,382 @@
+/*********************                                                        */
+/*! \file logic_info_white.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Unit testing for CVC4::LogicInfo class
+ **
+ ** Unit testing for CVC4::LogicInfo class.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/kind.h"
+#include "theory/logic_info.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+
+using namespace std;
+
+class LogicInfoWhite : public CxxTest::TestSuite {
+
+public:
+
+  void testSmtlibLogics() {
+    LogicInfo info("QF_SAT");
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( !info.isQuantified() );
+
+    info.setLogicString("AUFLIA");
+    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_BOOL ) );
+    TS_ASSERT( info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( !info.areRealsUsed() );
+
+    info.setLogicString("AUFLIRA");
+    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_BOOL ) );
+    TS_ASSERT( info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areRealsUsed() );
+
+    info.setLogicString("AUFNIRA");
+    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_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areRealsUsed() );
+
+    info.setLogicString("LRA");
+    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.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+    info.setLogicString("QF_AUFBV");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+    info.setLogicString("QF_AUFLIA");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+    info.setLogicString("QF_BV");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+    info.setLogicString("QF_IDL");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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_NIA");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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_NRA");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( !info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( info.isPure( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+    info.setLogicString("QF_UFBV");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+    info.setLogicString("QF_UFIDL");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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_UFNRA");
+    TS_ASSERT( !info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    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");
+    TS_ASSERT( info.isQuantified() );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( !info.isDifferenceLogic() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( !info.areRealsUsed() );
+  }
+
+  void testDefaultLogic() {
+    LogicInfo info;
+    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTNIRA" );
+    TS_ASSERT( info.isSharingEnabled() );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_QUANTIFIERS ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_REWRITERULES ) );
+    TS_ASSERT( ! info.isPure( THEORY_BUILTIN ) );
+    TS_ASSERT( ! info.isPure( THEORY_BOOL ) );
+    TS_ASSERT( ! info.isPure( THEORY_UF ) );
+    TS_ASSERT( ! info.isPure( THEORY_ARITH ) );
+    TS_ASSERT( ! info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( ! info.isPure( THEORY_BV ) );
+    TS_ASSERT( ! info.isPure( THEORY_DATATYPES ) );
+    TS_ASSERT( ! info.isPure( THEORY_QUANTIFIERS ) );
+    TS_ASSERT( ! info.isPure( THEORY_REWRITERULES ) );
+    TS_ASSERT( info.isQuantified() );
+    TS_ASSERT( info.areIntegersUsed() );
+    TS_ASSERT( info.areRealsUsed() );
+    TS_ASSERT( ! info.isLinear() );
+
+    info.arithOnlyLinear();
+    info.disableIntegers();
+    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" );
+    info.disableQuantifiers();
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" );
+    info.disableTheory(THEORY_BV);
+    info.disableTheory(THEORY_DATATYPES);
+    info.enableIntegers();
+    info.disableReals();
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" );
+    info.disableTheory(THEORY_ARITH);
+    info.disableTheory(THEORY_UF);
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
+    TS_ASSERT( info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( ! info.isQuantified() );
+  }
+
+};/* class LogicInfoWhite */
+
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 8d7bc9c72..6bca0c873 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -231,6 +231,7 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
   NodeManagerScope* d_scope;
   FakeOutputChannel *d_nullChannel;
   TheoryEngine* d_theoryEngine;
+  LogicInfo* d_logicInfo;
 
 public:
 
@@ -244,7 +245,8 @@ public:
     d_nullChannel = new FakeOutputChannel();
 
     // create the TheoryEngine
-    d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt);
+    d_logicInfo = new LogicInfo();
+    d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt, *d_logicInfo);
 
     d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
     d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
@@ -259,6 +261,7 @@ public:
   void tearDown() {
     d_theoryEngine->shutdown();
     delete d_theoryEngine;
+    delete d_logicInfo;
 
     delete d_nullChannel;