From 5b4b7727433f06c1788647b08e7da1ee1cc37bc9 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 7 Jul 2010 21:55:11 +0000 Subject: [PATCH] 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 --- src/theory/arrays/theory_arrays.cpp | 4 +- src/theory/arrays/theory_arrays.h | 2 +- src/theory/shared_data.cpp | 18 ++- src/theory/shared_data.h | 28 +++- src/theory/shared_term_manager.cpp | 131 ++++++++++++---- src/theory/shared_term_manager.h | 60 +++++++- src/theory/theory.h | 12 +- src/theory/theory_engine.cpp | 8 + test/regress/regress0/arr2.smt | 7 + test/unit/Makefile.am | 9 +- test/unit/theory/shared_term_manager_black.h | 148 +++++++++++++++++++ 11 files changed, 366 insertions(+), 61 deletions(-) create mode 100644 test/regress/regress0/arr2.smt create mode 100644 test/unit/theory/shared_term_manager_black.h diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index b84b1e507..8b5f7d3e7 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -45,9 +45,9 @@ void TheoryArrays::addSharedTerm(TNode t) { } -void TheoryArrays::notifyEq(TNode eq) { +void TheoryArrays::notifyEq(TNode lhs, TNode rhs) { Debug("arrays") << "TheoryArrays::notifyEq(): " - << eq << endl; + << lhs << " = " << rhs << endl; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 3cb050287..cb738d085 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -49,7 +49,7 @@ public: } void addSharedTerm(TNode t); - void notifyEq(TNode eq); + void notifyEq(TNode lhs, TNode rhs); void check(Effort e); void propagate(Effort e) { } void explain(TNode n, Effort e) { } diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp index 7a8970c29..50e916832 100644 --- a/src/theory/shared_data.cpp +++ b/src/theory/shared_data.cpp @@ -33,6 +33,7 @@ SharedData::SharedData(Context * context, TNode n, uint64_t theories) : d_size(1), d_find(this), d_proofNext(this), + d_edgeReversed(false), d_explainingTheory(NULL), d_rep(n) { } @@ -49,7 +50,7 @@ void SharedData::restore(ContextObj* pContextObj) { d_size = data->d_size; d_find = data->d_find; d_proofNext = data->d_proofNext; - d_equality = data->d_equality; + d_edgeReversed = data->d_edgeReversed; d_explainingTheory = data->d_explainingTheory; d_rep = data->d_rep; } @@ -60,20 +61,23 @@ void SharedData::reverseEdges() { SharedData* parent = this; SharedData* current = d_proofNext; - Node equality = d_equality; + bool reversed = d_edgeReversed; Theory* explainingTheory = d_explainingTheory; makeCurrent(); + + // Make this the proof root d_proofNext = this; - Node tmpNode; + // Reverse the edges from here to the former root + bool tmpReversed; Theory* tmpTheory; SharedData* tmpData; while (!current->isProofRoot()) { - tmpNode = current->getEquality(); - current->setEquality(equality); - equality = tmpNode; + tmpReversed = current->getEdgeReversed(); + current->setEdgeReversed(!reversed); + reversed = tmpReversed; tmpTheory = current->getExplainingTheory(); current->setExplainingTheory(explainingTheory); @@ -84,7 +88,7 @@ void SharedData::reverseEdges() { parent = current; current = tmpData; } - current->setEquality(equality); + current->setEdgeReversed(!reversed); current->setExplainingTheory(explainingTheory); current->setProofNext(parent); } diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h index 64b7f5ab1..0b21eedae 100644 --- a/src/theory/shared_data.h +++ b/src/theory/shared_data.h @@ -72,13 +72,15 @@ private: SharedData* d_proofNext; /** - * The equality that justifies this node being equal to - * the node at d_proofNext. Not valid if this is proof root. + * In order to precisely reconstruct the equality that justifies this node + * being equal to the node at d_proofNext, we need to know whether this edge + * has been switched. Value is meaningless at the proof root. */ - Node d_equality; + bool d_edgeReversed; /** - * The theory that can explain d_equality. Not valid if this is proof root. + * The theory that can explain the equality of this node and the node at + * d_proofNext. Not valid if this is proof root. */ theory::Theory* d_explainingTheory; @@ -157,14 +159,24 @@ public: void setProofNext(SharedData* pData) { makeCurrent(); d_proofNext = pData; } /** - * Get the equality associated with the link in the proof tree. + * Get the edge reversed property of this node */ - Node getEquality() const { return d_equality; } + bool getEdgeReversed() const { return d_edgeReversed; } /** - * Set the equality associated with the link in the proof tree. + * Set the edge reversed flag to value */ - void setEquality(TNode eq) { makeCurrent(); d_equality = eq; } + void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } + + /** + * Get the original equality that created the link from this node to the next + * proof node. + */ + Node getEquality() const { + return d_edgeReversed + ? NodeManager::currentNM()->mkNode(kind::EQUAL, d_proofNext->getRep(), d_rep) + : NodeManager::currentNM()->mkNode(kind::EQUAL, d_rep, d_proofNext->getRep()); + } /** * Get the explaining theory diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp index 55087ecbd..564fb776f 100644 --- a/src/theory/shared_term_manager.cpp +++ b/src/theory/shared_term_manager.cpp @@ -31,11 +31,16 @@ SharedTermManager::SharedTermManager(TheoryEngine* engine, } -SharedData* SharedTermManager::find(SharedData* pData) { +SharedData* SharedTermManager::find(SharedData* pData) const { + // Check if pData is the representative SharedData* next = pData->getFind(); if (next == pData) return pData; + + // Check if its successor is the representative SharedData* nextNext = next->getFind(); if (nextNext == next) return next; + + // Otherwise, recurse and do find path-compression next = find(nextNext); pData->setFind(next); return next; @@ -59,23 +64,49 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { // theory id uint64_t parentTag = (1 << parent->getId()); uint64_t childTag = (1 << child->getId()); - uint64_t newTags = parentTag | childTag; + uint64_t bothTags = parentTag | childTag; + + // Create or update the SharedData for n SharedData* pData; if(n.getAttribute(SharedAttr(), pData)) { // The attribute already exists, just update it if necessary uint64_t tags = pData->getTheories(); - newTags |= tags; + uint64_t newTags = tags | bothTags; if (tags == newTags) return; + + // Get the equivalence class representative -- if this is different from + // the current node, then we will need to notify the theories of that and + // update the theory tags on the representative node + SharedData* pDataFind = find(pData); + + // Notify parent theory if necessary if (!(tags & parentTag)) { parent->addSharedTerm(n); + if (pData != pDataFind) { + parent->notifyEq(n, pDataFind->getRep()); + } } + + // Notify child theory if necessary if (!(tags & childTag)) { child->addSharedTerm(n); + if (pData != pDataFind) { + child->notifyEq(n, pDataFind->getRep()); + } } + + // Update theory tags pData->setTheories(newTags); + if (pData != pDataFind) { + tags = pDataFind->getTheories(); + newTags = tags | bothTags; + if (tags != newTags) { + pDataFind->setTheories(newTags); + } + } } else { // The attribute does not exist, so it is created and set - pData = new (true) SharedData(d_context, n, newTags); + pData = new (true) SharedData(d_context, n, bothTags); n.setAttribute(SharedAttr(), pData); parent->addSharedTerm(n); child->addSharedTerm(n); @@ -83,22 +114,35 @@ void SharedTermManager::addTerm(TNode n, Theory* parent, Theory* child) { } -void SharedTermManager::addEq(Theory* thReason, TNode eq) { - Assert(eq.getKind() == kind::EQUAL && - eq[0].hasAttribute(SharedAttr()) && eq[1].hasAttribute(SharedAttr()), +void SharedTermManager::addEq(TNode eq, Theory* thReason) { + Assert(eq.getKind() == kind::EQUAL, "SharedTermManager::addEq precondition violated"); TNode x = eq[0]; TNode y = eq[1]; - SharedData* pDataX = x.getAttribute(SharedAttr()); - SharedData* pDataY = y.getAttribute(SharedAttr()); + SharedData* pDataX; + SharedData* pDataY; + + // Grab the SharedData for each side of the equality, create if necessary + if(!x.getAttribute(SharedAttr(), pDataX)) { + pDataX = new (true) SharedData(d_context, x, 0); + x.setAttribute(SharedAttr(), pDataX); + } + if(!y.getAttribute(SharedAttr(), pDataY)) { + pDataY = new (true) SharedData(d_context, y, 0); + y.setAttribute(SharedAttr(), pDataY); + } + // Get the representatives SharedData* pDataXX = find(pDataX); SharedData* pDataYY = find(pDataY); + // If already in the same equivalence class, nothing to do if(pDataXX == pDataYY) return; + // Make sure we reverse the edges in the smaller tree + bool switched = false; if(pDataXX->getSize() > pDataYY->getSize()) { SharedData* tmp = pDataXX; pDataXX = pDataYY; @@ -107,17 +151,27 @@ void SharedTermManager::addEq(Theory* thReason, TNode eq) { tmp = pDataX; pDataX = pDataY; pDataY = tmp; + + switched = true; } - pDataX->reverseEdges(); - pDataX->setEquality(eq); + // Reverse the edges in the left proof tree and link the two trees + if(!pDataX->isProofRoot()) { + pDataX->reverseEdges(); + } + pDataX->setEdgeReversed(switched); pDataX->setExplainingTheory(thReason); pDataX->setProofNext(pDataY); + // Set the equivalence class representative for the left node to be the right node pDataXX->setFind(pDataYY); pDataYY->setSize(pDataYY->getSize() + pDataXX->getSize()); + + // Update the theory tags for the new representative uint64_t tags = pDataXX->getTheories(); pDataYY->setTheories(pDataYY->getTheories() | tags); + + // Notify the theories that care about the left node int id = 0; while (tags != 0) { if (tags & 1) { @@ -129,8 +183,29 @@ void SharedTermManager::addEq(Theory* thReason, TNode eq) { } +void SharedTermManager::collectExplanations(SharedData* pData, set& s) const { + Theory* expTh = pData->getExplainingTheory(); + if(expTh == NULL) { + // This equality is directly from SAT, no need to ask a theory for an explanation + s.insert(pData->getEquality()); + } + else { + // This equality was sent by a theory - ask the theory for the explanation + Node n = d_engine->getExplanation(pData->getEquality(), expTh); + if(n.getKind() == kind::AND) { + for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { + s.insert(*it); + } + } + else { + s.insert(n); + } + } +} + + // Explain this equality -Node SharedTermManager::explain(TNode eq) { +Node SharedTermManager::explain(TNode eq) const { Assert(eq.getKind() == kind::EQUAL && eq[0].hasAttribute(SharedAttr()) && eq[1].hasAttribute(SharedAttr()), "SharedTermManager::explain precondition violated"); @@ -138,14 +213,15 @@ Node SharedTermManager::explain(TNode eq) { TNode x = eq[0]; TNode y = eq[1]; + // Get the SharedData for both sides of the equality SharedData* pDataX = x.getAttribute(SharedAttr()); SharedData* pDataY = y.getAttribute(SharedAttr()); Assert(find(pDataX) == find(pDataY), "invalid equality input to SharedTermManager::explain"); + // Find the path between the two nodes and build up the explanation std::set s; - Node n; SharedData* tmp = pDataX; // Check to see if Y is on path from X to root @@ -155,39 +231,27 @@ Node SharedTermManager::explain(TNode eq) { if (tmp == pDataY) { // Y is on path from X to root, just traverse that path while (pDataX != pDataY) { - n = d_engine->getExplanation(pDataX->getEquality(), - pDataX->getExplainingTheory()); - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } + collectExplanations(pDataX, s); pDataX = pDataX->getProofNext(); } } else { // Y is not on path from X to root, so traverse from Y to root instead while (!pDataY->isProofRoot() && pDataX != pDataY) { - n = d_engine->getExplanation(pDataY->getEquality(), - pDataY->getExplainingTheory()); - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } + collectExplanations(pDataY, s); pDataY = pDataY->getProofNext(); } } if (pDataX != pDataY) { // X and Y are on different branches - have to traverse both while (!pDataX->isProofRoot()) { - n = d_engine->getExplanation(pDataX->getEquality(), - pDataX->getExplainingTheory()); - for (Node::iterator it = n.begin(), iend = n.end(); it != iend; ++it) { - s.insert(*it); - } + collectExplanations(pDataX, s); pDataX = pDataX->getProofNext(); } } // Build explanation from s - NodeBuilder nb; + NodeBuilder<> nb(kind::AND); set::iterator it = s.begin(), iend = s.end(); for (; it != iend; ++it) { nb << *it; @@ -196,4 +260,13 @@ Node SharedTermManager::explain(TNode eq) { } +Node SharedTermManager::getRep(TNode n) const { + Assert(n.hasAttribute(SharedAttr()), + "SharedTermManager::getRep precondition violated"); + + SharedData* pData = n.getAttribute(SharedAttr()); + return find(pData)->getRep(); +} + + }/* CVC4 namespace */ diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h index e6a58cdc9..8b5567e4e 100644 --- a/src/theory/shared_term_manager.h +++ b/src/theory/shared_term_manager.h @@ -39,25 +39,77 @@ namespace theory { */ class SharedTermManager { + /** + * Pointer back to theory engine + */ TheoryEngine* d_engine; + /** + * Pointer to context + */ context::Context* d_context; + /** + * List of all theories indexed by theory id (built by calls to registerTheory) + */ std::vector d_theories; - SharedData* find(SharedData* pData); + /** + * Private method to find equivalence class representative in union-find data + * structure. + */ + SharedData* find(SharedData* pData) const; + + /** + * Helper function for explain: add all reasons for equality at pData to set s + */ + void collectExplanations(SharedData* pData, std::set& s) const; public: + /** + * Constructor + */ SharedTermManager(TheoryEngine* engine, context::Context* context); + /** + * Should be called once for each theory at setup time + */ void registerTheory(theory::Theory* th); + /** + * Called by theory engine to indicate that node n is shared by theories + * parent and child. + */ void addTerm(TNode n, theory::Theory* parent, theory::Theory* child); - void addEq(theory::Theory* thReason, TNode eq); - - Node explain(TNode eq); + /** + * Called by theory engine or theories to notify the shared term manager that + * two terms are equal. + * + * @param eq the equality between shared terms + * @param thReason the theory that knows why, NULL means it's a SAT assertion + */ + void addEq(TNode eq, theory::Theory* thReason = NULL); + + /** + * Called by theory engine or theories to notify the shared term manager that + * two terms are disequal. + * + * @param eq the equality between shared terms whose negation now holds + * @param thReason the theory that knows why, NULL means it's a SAT assertion + */ + void addDiseq(TNode eq, theory::Theory* thReason = NULL) { } + + /** + * Get an explanation for an equality known by the SharedTermManager + */ + Node explain(TNode eq) const; + + /** + * Get the representative node in the equivalence class containing n + */ + Node getRep(TNode n) const; };/* class SharedTermManager */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 6da47fbd8..64a3b8f06 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -358,15 +358,15 @@ public: virtual void addSharedTerm(TNode n) { } /** - * This method is called by the shared term manager when a shared term t + * This method is called by the shared term manager when a shared term lhs * which this theory cares about (either because it received a previous - * addSharedTerm call with t or because it received a previous notifyEq call - * with t as the second argument) becomes equal to another shared term u. + * addSharedTerm call with lhs or because it received a previous notifyEq call + * with lhs as the second argument) becomes equal to another shared term rhs. * This call also serves as notice to the theory that the shared term manager - * now considers u the representative for this equivalence class of shared - * terms, so future notifications for this class will be based on u not t. + * now considers rhs the representative for this equivalence class of shared + * terms, so future notifications for this class will be based on rhs not lhs. */ - virtual void notifyEq(TNode t, TNode u) { } + virtual void notifyEq(TNode lhs, TNode rhs) { } /** * Check the current assignment's consistency. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d16d80090..4fae94254 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -46,6 +46,14 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { if (fact.getKind() == kind::NOT) { // No need to register negations - only atoms fact = fact[0]; +// FIXME: In future, might want to track disequalities in shared term manager +// if (fact.getKind() == kind::EQUAL) { +// d_engine->getSharedTermManager()->addDiseq(fact); +// } + } + else if (fact.getKind() == kind::EQUAL) { + // Automatically track all asserted equalities in the shared term manager + d_engine->getSharedTermManager()->addEq(fact); } if(! fact.getAttribute(RegisteredAttr())) { std::list toReg; 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 + +#include +#include +#include + +#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(); + } + +}; -- 2.30.2