diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2010-07-07 02:18:42 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2010-07-07 02:18:42 +0000 |
commit | daf3b024547deaf1cf53b66ed046fbb15584b9d3 (patch) | |
tree | 91a2b7ebfe804041ad531ae897a037bdde61a4a7 /test/unit | |
parent | 34ef50c2fcfa4d6aa8337c3096defa56d7dc0093 (diff) |
Added shared term manager. Basic mechanism for identifying shared terms is
working. Still need to implement theory-specific shared term propagation.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_uf_white.h | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index d8c41bf3a..ea1ee698f 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -70,7 +70,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_arith = new TheoryArith(d_ctxt, d_outputChannel); + d_arith = new TheoryArith(0, d_ctxt, d_outputChannel); preregistered = new std::set<Node>(); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 967a53462..0c6a38d0b 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -95,7 +95,7 @@ public: vector<Node> d_getSequence; DummyTheory(Context* ctxt, OutputChannel& out) : - Theory(ctxt, out) { + Theory(0, ctxt, out) { } void registerTerm(TNode n) { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index addf15af3..570fa74a4 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -80,7 +80,7 @@ class FakeTheory : public Theory { public: FakeTheory(context::Context* ctxt, OutputChannel& out, std::string id) : - Theory(ctxt, out), + Theory(0, ctxt, out), d_id(id) { } diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index a959d01ba..8e72c428f 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -59,7 +59,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_euf = new TheoryUF(d_ctxt, d_outputChannel); + d_euf = new TheoryUF(0, d_ctxt, d_outputChannel); d_booleanType = new TypeNode(d_nm->booleanType()); } |