diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 7 | ||||
-rw-r--r-- | test/unit/theory/logic_info_white.h | 382 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 5 |
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; |