summaryrefslogtreecommitdiff
path: root/test/unit/theory
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/theory')
-rw-r--r--test/unit/theory/logic_info_white.h382
-rw-r--r--test/unit/theory/theory_engine_white.h5
2 files changed, 386 insertions, 1 deletions
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