summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/prop/cnf_stream_black.h7
-rw-r--r--test/unit/theory/logic_info_white.h382
-rw-r--r--test/unit/theory/theory_engine_white.h5
4 files changed, 393 insertions, 2 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback