Shared term manager tested and working

It is currently tracking all asserted equalities for simplicity.
Might want to check if this is a performance hit

3 files changed, 160 insertions, 4 deletions

diff --git a/test/regress/regress0/arr2.smt b/test/regress/regress0/arr2.smt
new file mode 100644
index 000000000..213660c0a
--- /dev/null
+++ b/test/regress/regress0/arr2.smt
@@ -0,0 +1,7 @@
+(benchmark simple_arr
+  :logic QF_AX
+  :status unsat
+  :extrafuns ((a Array))
+  :extrafuns ((i1 Index) (i2 Index) (i3 Index))
+  :formula (not (implies (and (= i1 i2) (= i2 i3)) (= (select a i1) (select a i3))))
+)
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index c96fbccb6..7d6f6ff50 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,5 +1,10 @@
 # All unit tests
 UNIT_TESTS = \
+	theory/shared_term_manager_black \
+	theory/theory_engine_white \
+	theory/theory_black \
+	theory/theory_uf_white \
+	theory/theory_arith_white \
 	expr/expr_public \
         expr/expr_manager_public \
 	expr/node_white \
@@ -21,10 +26,6 @@ UNIT_TESTS = \
 	context/cdlist_black \
 	context/cdmap_black \
 	context/cdmap_white \
-	theory/theory_engine_white \
-	theory/theory_black \
-	theory/theory_uf_white \
-	theory/theory_arith_white \
 	util/assert_white \
 	util/bitvector_black \
 	util/configuration_black \
diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
new file mode 100644
index 000000000..4393d99cd
--- /dev/null
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -0,0 +1,148 @@
+/*********************                                                        */
+/*! \file shared_term_manager_black.h
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 "theory/theoryof_table.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/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);
+    d_scope = new NodeManagerScope(d_nm);
+
+    d_theoryEngine = new TheoryEngine(d_ctxt);
+
+  }
+
+  void tearDown() {
+    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();
+  }
+
+};