additional stuff for sharing,

6 files changed, 31 insertions, 192 deletions

diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 86a6b031c..5199f2b62 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -6,15 +6,15 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 
 # Regression tests for SMT inputs
-SMT_TESTS = \
-	pb_real_10_0100_10_10.smt \
-	pb_real_10_0100_10_11.smt \
-	pb_real_10_0100_10_15.smt \
-	pb_real_10_0100_10_16.smt \
-	pb_real_10_0100_10_19.smt \
-	pb_real_10_0200_10_22.smt \
-	pb_real_10_0200_10_26.smt \
-	pb_real_10_0200_10_29.smt
+#SMT_TESTS = \
+#	pb_real_10_0100_10_10.smt \
+#	pb_real_10_0100_10_11.smt \
+#	pb_real_10_0100_10_15.smt \
+#	pb_real_10_0100_10_16.smt \
+#	pb_real_10_0100_10_19.smt \
+#	pb_real_10_0200_10_22.smt \
+#	pb_real_10_0200_10_26.smt \
+#	pb_real_10_0200_10_29.smt
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 608d6335b..b8e4c1679 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,12 +1,11 @@
 # All unit tests
 UNIT_TESTS = \
-	theory/shared_term_manager_black \
 	theory/theory_engine_white \
 	theory/theory_black \
 	theory/theory_arith_white \
 	theory/union_find_black \
 	expr/expr_public \
-        expr/expr_manager_public \
+	expr/expr_manager_public \
 	expr/node_white \
 	expr/node_black \
 	expr/kind_black \
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 8fb96c74a..c9a2196a5 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -108,9 +108,9 @@ void setUp() {
   NodeManagerScope nms(d_nodeManager);
   d_satSolver = new FakeSatSolver;
   d_theoryEngine = new TheoryEngine(d_context);
-  d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>();
-  d_theoryEngine->addTheory<theory::booleans::TheoryBool>();
-  d_theoryEngine->addTheory<theory::arith::TheoryArith>();
+  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);
   theory::Registrar registrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
 }
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
deleted file mode 100644
index 1be116517..000000000
--- a/test/unit/theory/shared_term_manager_black.h
+++ /dev/null
@@ -1,148 +0,0 @@
-/*********************                                                        */
-/*! \file shared_term_manager_black.h
- ** \verbatim
- ** Original author: barrett
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  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 Black box testing of CVC4::SharedTermManager.
- **
- ** Black box testing of CVC4::SharedTermManager.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <string>
-#include <deque>
-
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "expr/kind.h"
-#include "context/context.h"
-#include "util/rational.h"
-#include "util/integer.h"
-#include "util/options.h"
-#include "util/Assert.h"
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-using namespace CVC4::kind;
-
-using namespace std;
-
-/**
- * Test the SharedTermManager.
- */
-class SharedTermManagerBlack : public CxxTest::TestSuite {
-  Context* d_ctxt;
-
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-  TheoryEngine* d_theoryEngine;
-
-public:
-
-  void setUp() {
-    d_ctxt = new Context;
-
-    d_nm = new NodeManager(d_ctxt, NULL);
-    d_scope = new NodeManagerScope(d_nm);
-
-    d_theoryEngine = new TheoryEngine(d_ctxt);
-  }
-
-  void tearDown() {
-    d_theoryEngine->shutdown();
-    delete d_theoryEngine;
-
-    delete d_scope;
-    delete d_nm;
-
-    delete d_ctxt;
-  }
-
-  void testExplanation() {
-    // Example from Barcelogic paper
-    SharedTermManager* stm = d_theoryEngine->getSharedTermManager();
-
-    Node x1 = d_nm->mkVar("x1", d_nm->integerType());
-    Node x2 = d_nm->mkVar("x2", d_nm->integerType());
-    Node x3 = d_nm->mkVar("x3", d_nm->integerType());
-    Node x4 = d_nm->mkVar("x4", d_nm->integerType());
-    Node x5 = d_nm->mkVar("x5", d_nm->integerType());
-    Node x6 = d_nm->mkVar("x6", d_nm->integerType());
-    Node x7 = d_nm->mkVar("x7", d_nm->integerType());
-    Node x8 = d_nm->mkVar("x8", d_nm->integerType());
-    Node x9 = d_nm->mkVar("x9", d_nm->integerType());
-    Node x10 = d_nm->mkVar("x10", d_nm->integerType());
-    Node x11 = d_nm->mkVar("x11", d_nm->integerType());
-    Node x12 = d_nm->mkVar("x12", d_nm->integerType());
-    Node x13 = d_nm->mkVar("x13", d_nm->integerType());
-    Node x14 = d_nm->mkVar("x14", d_nm->integerType());
-
-    Node a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12;
-
-    d_ctxt->push();
-
-    stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8));
-    stm->addEq(a2 = d_nm->mkNode(EQUAL, x7, x2));
-    stm->addEq(a3 = d_nm->mkNode(EQUAL, x3, x13));
-    stm->addEq(a4 = d_nm->mkNode(EQUAL, x7, x1));
-    stm->addEq(a5 = d_nm->mkNode(EQUAL, x6, x7));
-    stm->addEq(a6 = d_nm->mkNode(EQUAL, x9, x5));
-    stm->addEq(a7 = d_nm->mkNode(EQUAL, x9, x3));
-    stm->addEq(a8 = d_nm->mkNode(EQUAL, x14, x11));
-    stm->addEq(a9 = d_nm->mkNode(EQUAL, x10, x4));
-    stm->addEq(a10 = d_nm->mkNode(EQUAL, x12, x9));
-    stm->addEq(a11 = d_nm->mkNode(EQUAL, x4, x11));
-    stm->addEq(a12 = d_nm->mkNode(EQUAL, x10, x7));
-
-    Node explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x4));
-
-    TS_ASSERT(explanation.getNumChildren() == 3);
-
-    Node e0 = explanation[0];
-    Node e1 = explanation[1];
-    Node e2 = explanation[2];
-
-    TS_ASSERT(e0 == a4 && e1 == a9 && e2 == a12);
-
-    TS_ASSERT(stm->getRep(x8) == stm->getRep(x14));
-    TS_ASSERT(stm->getRep(x2) != stm->getRep(x12));
-
-    d_ctxt->pop();
-
-    TS_ASSERT(stm->getRep(x8) != stm->getRep(x14));
-
-    d_ctxt->push();
-
-    stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8));
-    stm->addEq(a2 = d_nm->mkNode(EQUAL, x8, x2));
-    stm->addEq(a3 = d_nm->mkNode(EQUAL, x2, x3));
-
-    explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x3));
-    TS_ASSERT(explanation.getNumChildren() == 3);
-
-    e0 = explanation[0];
-    e1 = explanation[1];
-    e2 = explanation[2];
-
-    TS_ASSERT(e0 == a1 && e1 == a2 && e2 == a3);
-
-    TS_ASSERT(stm->getRep(x8) == stm->getRep(x2));
-
-    d_ctxt->pop();
-  }
-
-};
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index ff6b352d0..2c3ff0bb1 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -52,32 +52,23 @@ public:
 
   void safePoint() throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) {
+  void conflict(TNode n)
+    throw(AssertionException) {
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) {
+  void propagate(TNode n)
+    throw(AssertionException) {
     push(PROPAGATE, n);
   }
 
-  void lemma(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) {
+  void lemma(TNode n, bool removable)
+    throw(AssertionException) {
     push(LEMMA, n);
   }
-  void augmentingLemma(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) {
-    Unreachable();
-  }
-
-  void explanation(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) {
-    push(EXPLANATION, n);
-  }
 
   void setIncomplete()
-    throw(Interrupted, AssertionException) {
+    throw(AssertionException) {
     Unreachable();
   }
 
@@ -292,7 +283,7 @@ public:
 
   void testOutputChannel() {
     Node n = atom0.orNode(atom1);
-    d_outputChannel.lemma(n);
+    d_outputChannel.lemma(n, false);
     d_outputChannel.split(atom0);
     Node s = atom0.orNode(atom0.notNode());
     TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index a1b058eeb..e33efb597 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -48,19 +48,16 @@ using namespace CVC4::kind;
 using namespace std;
 
 class FakeOutputChannel : public OutputChannel {
-  void conflict(TNode n, bool safe) throw(AssertionException) {
+  void conflict(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  void propagate(TNode n, bool safe) throw(AssertionException) {
+  void propagate(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  void lemma(TNode n, bool safe) throw(AssertionException) {
+  void lemma(TNode n, bool removable) throw(AssertionException) {
     Unimplemented();
   }
-  void augmentingLemma(TNode n, bool safe) throw(AssertionException) {
-    Unimplemented();
-  }
-  void explanation(TNode n, bool safe) throw(AssertionException) {
+  void explanation(TNode n) throw(AssertionException) {
     Unimplemented();
   }
   void setIncomplete() throw(AssertionException) {
@@ -244,12 +241,12 @@ public:
     // create the TheoryEngine
     d_theoryEngine = new TheoryEngine(d_ctxt);
 
-    d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >();
-    d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >();
-    d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >();
-    d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >();
-    d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >();
-    d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >();
+    d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
+    d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
+    d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF);
+    d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH);
+    d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY);
+    d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV);
 
     //Debug.on("theory-rewrite");
   }