From 96ce991a4b8593f7ec831c3a9b40b214d2ac3761 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 14 Dec 2010 21:07:46 +0000 Subject: [PATCH] congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk --- src/expr/node_manager.cpp | 3 + src/expr/node_manager.h | 11 ++ src/expr/type_constant.h | 4 +- src/printer/Makefile.am | 3 - src/theory/uf/morgan/theory_uf_morgan.h | 2 +- src/util/congruence_closure.h | 190 ++++++++++++++-------- test/unit/util/congruence_closure_white.h | 88 +++++++++- 7 files changed, 218 insertions(+), 83 deletions(-) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 280c55254..9006bf4d9 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -228,6 +228,9 @@ TypeNode NodeManager::computeType(TNode n, bool check) // Infer the type switch(n.getKind()) { + case kind::BUILTIN: + typeNode = builtinOperatorType(); + break; case kind::SORT_TYPE: typeNode = kindType(); break; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 206cf35d5..04de81b1c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -471,6 +471,12 @@ public: /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); + /** + * Get the (singleton) type for builtin operators (that is, the type + * of the Node returned from Node::getOperator() when the operator + * is built-in, like EQUAL). */ + inline TypeNode builtinOperatorType(); + /** * Make a function type from domain to range. * @@ -680,6 +686,11 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst(KIND_TYPE)); } +/** Get the (singleton) type for builtin operators. */ +inline TypeNode NodeManager::builtinOperatorType() { + return TypeNode(mkTypeConst(BUILTIN_OPERATOR_TYPE)); +} + /** Make a function type from domain to range. */ inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { std::vector sorts; diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h index 3001d4513..23c23cc9f 100644 --- a/src/expr/type_constant.h +++ b/src/expr/type_constant.h @@ -36,7 +36,9 @@ enum TypeConstant { /** The real type */ REAL_TYPE, /** The kind type (type of types) */ - KIND_TYPE + KIND_TYPE, + /** The builtin operator type (type of non-PARAMETERIZED operators) */ + BUILTIN_OPERATOR_TYPE };/* enum TypeConstant */ /** diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am index 8fd50d823..ca3cbacf1 100644 --- a/src/printer/Makefile.am +++ b/src/printer/Makefile.am @@ -16,6 +16,3 @@ libprinter_la_SOURCES = \ smt2/smt2_printer.cpp \ cvc/cvc_printer.h \ cvc/cvc_printer.cpp - -libprinter_la_LIBADD = \ - @builddir@/../lib/libreplacements.la diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 99e6f5fbc..cbc5f1eab 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -74,7 +74,7 @@ private: /** * Instance of the congruence closure module. */ - CongruenceClosure d_cc; + CongruenceClosure > d_cc; /** * Our union find for equalities. diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 8a13e3587..0968b39ed 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -39,12 +39,12 @@ namespace CVC4 { -template +template class CongruenceClosure; -template +template std::ostream& operator<<(std::ostream& out, - const CongruenceClosure& cc); + const CongruenceClosure& cc); /** * A CongruenceClosureException is thrown by @@ -59,6 +59,36 @@ public: Exception(std::string("Congruence closure exception: ") + msg) {} };/* class CongruenceClosureException */ +struct EndOfCongruenceOpList; +template +struct CongruenceOperator { + enum { kind = kind_ }; + typedef Tail_ Tail; +};/* class CongruenceOperator<> */ + +#define CONGRUENCE_OPERATORS_1(kind1) CongruenceOperator +#define CONGRUENCE_OPERATORS_2(kind1, kind2) CongruenceOperator +#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) CongruenceOperator +#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) CongruenceOperator +#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) CongruenceOperator + +/** + * Returns true if the kind k is registered as a congruence operator + * for this CongruenceClosure. (That is, if it's in the + * CongruenceOperatorList template parameter.) False otherwise. + */ +template +inline bool isInCongruenceOperatorList(Kind k) { + typedef typename CongruenceOperatorList::Tail Tail; + return k == Kind(CongruenceOperatorList::kind) || + isInCongruenceOperatorList(k); +} + +// specialization for empty list +template <> +inline bool isInCongruenceOperatorList(Kind k) { + return false; +} /** * Congruence closure module for CVC4. @@ -95,8 +125,12 @@ public: * // interrupt you. * } * }; + * + * CongruenceOperatorList is a typelist of congruence Kinds, + * e.g., CONGRUENCE_OPERATORS_1(kind::APPLY_UF) + * or CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE) */ -template +template class CongruenceClosure { /** The context */ context::Context* d_context; @@ -147,6 +181,10 @@ class CongruenceClosure { AverageStat d_explanationLength;/*! average explanation length */ IntStat d_newSkolemVars;/*! new vars created */ + static inline bool isCongruenceOperator(Kind k) { + return isInCongruenceOperatorList(k); + } + public: /** Construct a congruence closure module instance */ CongruenceClosure(context::Context* ctxt, OutputChannel* out) @@ -187,8 +225,8 @@ public: Assert(inputEq.getKind() == kind::EQUAL || inputEq.getKind() == kind::IFF); NodeBuilder<> eqb(inputEq.getKind()); - if(inputEq[1].getKind() == kind::APPLY_UF && - inputEq[0].getKind() != kind::APPLY_UF) { + if(isCongruenceOperator(inputEq[1].getKind()) && + !isCongruenceOperator(inputEq[0].getKind())) { eqb << flatten(inputEq[1]) << inputEq[0]; } else { eqb << flatten(inputEq[0]) << replace(flatten(inputEq[1])); @@ -199,11 +237,13 @@ public: void addEq(TNode eq, TNode inputEq); Node flatten(TNode t) { - if(t.getKind() == kind::APPLY_UF) { - NodeBuilder<> appb(kind::APPLY_UF); + if(isCongruenceOperator(t.getKind())) { + NodeBuilder<> appb(t.getKind()); Assert(replace(flatten(t.getOperator())) == t.getOperator(), "CongruenceClosure:: bad state: higher-order term ??"); - appb << t.getOperator(); + if(t.getMetaKind() == kind::metakind::PARAMETERIZED) { + appb << t.getOperator(); + } for(TNode::iterator i = t.begin(); i != t.end(); ++i) { appb << replace(flatten(*i)); } @@ -214,7 +254,7 @@ public: } Node replace(TNode t) { - if(t.getKind() == kind::APPLY_UF) { + if(isCongruenceOperator(t.getKind())) { EqMap::iterator i = d_eqMap.find(t); if(i == d_eqMap.end()) { ++d_newSkolemVars; @@ -315,7 +355,7 @@ public: private: friend std::ostream& operator<< <>(std::ostream& out, - const CongruenceClosure& cc); + const CongruenceClosure& cc); /** * Internal propagation of information. Propagation tends to @@ -414,8 +454,8 @@ public: };/* class CongruenceClosure */ -template -void CongruenceClosure::addTerm(TNode t) { +template +void CongruenceClosure::addTerm(TNode t) { Node trm = replace(flatten(t)); Node trmp = find(trm); @@ -445,8 +485,8 @@ void CongruenceClosure::addTerm(TNode t) { } -template -void CongruenceClosure::addEq(TNode eq, TNode inputEq) { +template +void CongruenceClosure::addEq(TNode eq, TNode inputEq) { Assert(!eq[0].getType().isFunction() && !eq[1].getType().isFunction(), "CongruenceClosure:: equality between function symbols not allowed"); @@ -457,7 +497,7 @@ void CongruenceClosure::addEq(TNode eq, TNode inputEq) { } Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); - Assert(eq[1].getKind() != kind::APPLY_UF); + Assert(!isCongruenceOperator(eq[1].getKind())); if(areCongruent(eq[0], eq[1])) { Trace("cc") << "CC -- redundant, ignoring...\n"; return; @@ -472,7 +512,7 @@ void CongruenceClosure::addEq(TNode eq, TNode inputEq) { // change from paper: do this whether or not s, t are applications Trace("cc:detail") << "CC propagating the eq" << std::endl; - if(s.getKind() != kind::APPLY_UF) { + if(!isCongruenceOperator(s.getKind())) { // s, t are constants propagate(eq); } else { @@ -500,16 +540,18 @@ void CongruenceClosure::addEq(TNode eq, TNode inputEq) { }/* addEq() */ -template -Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, +template +Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, Kind kindToBuild) throw(AssertionException) { - Assert(apply.getKind() == kind::APPLY_UF); + Assert(isCongruenceOperator(apply.getKind())); NodeBuilder<> argspb(kindToBuild); - // FIXME probably don't have to do find() of operator Assert(find(apply.getOperator()) == apply.getOperator(), - "CongruenceClosure:: bad state: function symbol merged with another"); - argspb << apply.getOperator(); + "CongruenceClosure:: bad state: " + "function symbol (or other congruence operator) merged with another"); + if(apply.getMetaKind() == kind::metakind::PARAMETERIZED) { + argspb << apply.getOperator(); + } for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) { argspb << find(*i); } @@ -517,8 +559,8 @@ Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, }/* buildRepresentativesOfApply() */ -template -void CongruenceClosure::propagate(TNode seed) { +template +void CongruenceClosure::propagate(TNode seed) { Trace("cc:detail") << "=== doing a round of propagation ===" << std::endl << "the \"seed\" propagation is: " << seed << std::endl; @@ -559,8 +601,8 @@ void CongruenceClosure::propagate(TNode seed) { a = e[0][1]; b = e[1][1]; - Assert(a.getKind() != kind::APPLY_UF); - Assert(b.getKind() != kind::APPLY_UF); + Assert(!isCongruenceOperator(a.getKind())); + Assert(!isCongruenceOperator(b.getKind())); Trace("cc") << " ( " << a << " , " << b << " )" << std::endl; } @@ -631,7 +673,7 @@ void CongruenceClosure::propagate(TNode seed) { Trace("cc:detail") << "calling merge2 " << c << bp << std::endl; merge(c, bp); // move c from classList(ap) to classlist(bp); - //i = cl.erase(i);// FIXME do we need to? + //i = cl.erase(i);// difference from paper: don't need to erase Trace("cc") << " adding c to class list of " << bp << std::endl; cl_bp->push_back(c); } @@ -658,10 +700,11 @@ void CongruenceClosure::propagate(TNode seed) { eq.getKind() == kind::IFF); // change from paper // use list elts can have form (apply c..) = x OR x = (apply c..) - Assert(eq[0].getKind() == kind::APPLY_UF || eq[1].getKind() == kind::APPLY_UF); + Assert(isCongruenceOperator(eq[0].getKind()) || + isCongruenceOperator(eq[1].getKind())); // do for each side that is an application for(int side = 0; side <= 1; ++side) { - if(eq[side].getKind() != kind::APPLY_UF) { + if(!isCongruenceOperator(eq[side].getKind())) { continue; } @@ -681,14 +724,14 @@ void CongruenceClosure::propagate(TNode seed) { // remove f(c1,c2)=c from UseList(ap) Trace("cc:detail") << "supposed to remove " << eq << std::endl << " from UseList of " << ap << std::endl; - //i = ul.erase(i);// FIXME do we need to? + //i = ul.erase(i);// difference from paper: don't need to erase } else { Trace("cc") << "CC -- lookup(c') is null" << std::endl; Trace("cc") << "CC -- setlookup(c') to " << eq << std::endl; // set lookup(c1',c2') to f(c1,c2)=c setLookup(cp, eq); // move f(c1,c2)=c from UseList(ap) to UseList(b') - //i = ul.erase(i);// FIXME do we need to remove from UseList(ap) ? + //i = ul.erase(i);// difference from paper: don't need to erase appendToUseList(bp, eq); } } @@ -713,8 +756,8 @@ void CongruenceClosure::propagate(TNode seed) { }/* propagate() */ -template -void CongruenceClosure::merge(TNode ec1, TNode ec2) { +template +void CongruenceClosure::merge(TNode ec1, TNode ec2) { /* if(Debug.isOn("cc:detail")) { Debug("cc:detail") << " -- merging " << ec1 @@ -730,8 +773,8 @@ void CongruenceClosure::merge(TNode ec1, TNode ec2) { Trace("cc") << "CC to " << ec2 << std::endl; /* can now be applications - Assert(ec1.getKind() != kind::APPLY_UF); - Assert(ec2.getKind() != kind::APPLY_UF); + Assert(!isCongruenceOperator(ec1.getKind())); + Assert(!isCongruenceOperator(ec2.getKind())); */ Assert(find(ec1) != ec2); @@ -747,8 +790,8 @@ void CongruenceClosure::merge(TNode ec1, TNode ec2) { }/* merge() */ -template -void CongruenceClosure::mergeProof(TNode a, TNode b, TNode e) { +template +void CongruenceClosure::mergeProof(TNode a, TNode b, TNode e) { Trace("cc") << " -- merge-proofing " << a << "\n" << " and " << b << "\n" << " with " << e << "\n"; @@ -786,26 +829,29 @@ void CongruenceClosure::mergeProof(TNode a, TNode b, TNode e) { }/* mergeProof() */ -template -Node CongruenceClosure::normalize(TNode t) const +template +Node CongruenceClosure::normalize(TNode t) const throw(AssertionException) { Trace("cc:detail") << "normalize " << t << std::endl; - if(t.getKind() != kind::APPLY_UF) {// t is a constant + if(!isCongruenceOperator(t.getKind())) {// t is a constant t = find(t); Trace("cc:detail") << " find " << t << std::endl; return t; } else {// t is an apply NodeBuilder<> apb(kind::TUPLE); Assert(normalize(t.getOperator()) == t.getOperator(), - "CongruenceClosure:: bad state: function symbol merged with another"); - apb << t.getOperator(); + "CongruenceClosure:: bad state: " + "function symbol merged with another"); + if(t.getMetaKind() == kind::metakind::PARAMETERIZED) { + apb << t.getOperator(); + } Node n; - bool allConstants = (n.getKind() != kind::APPLY_UF); + bool allConstants = (!isCongruenceOperator(n.getKind())); for(TNode::iterator i = t.begin(); i != t.end(); ++i) { TNode c = *i; n = normalize(c); apb << n; - allConstants = (allConstants && n.getKind() != kind::APPLY_UF); + allConstants = (allConstants && !isCongruenceOperator(n.getKind())); } Node ap = apb; @@ -815,15 +861,15 @@ Node CongruenceClosure::normalize(TNode t) const if(allConstants && !theLookup.isNull()) { Assert(theLookup.getKind() == kind::EQUAL || theLookup.getKind() == kind::IFF); - Assert(theLookup[0].getKind() == kind::APPLY_UF); - Assert(theLookup[1].getKind() != kind::APPLY_UF); + Assert(isCongruenceOperator(theLookup[0].getKind())); + Assert(!isCongruenceOperator(theLookup[1].getKind())); return find(theLookup[1]); } else { - NodeBuilder<> fa(kind::APPLY_UF); + NodeBuilder<> fa(t.getKind()); for(Node::iterator i = ap.begin(); i != ap.end(); ++i) { fa << *i; } - // ensure a hard Node link exists during the call + // ensure a hard Node link exists for the return Node n = fa; return n; } @@ -834,8 +880,8 @@ Node CongruenceClosure::normalize(TNode t) const // This is the find() operation for the auxiliary union-find. This // union-find is not context-dependent, as it's used only during // explain(). It does path compression. -template -Node CongruenceClosure::highestNode(TNode a, UnionFind_t& unionFind) const +template +Node CongruenceClosure::highestNode(TNode a, UnionFind_t& unionFind) const throw(AssertionException) { UnionFind_t::iterator i = unionFind.find(a); if(i == unionFind.end()) { @@ -846,8 +892,8 @@ Node CongruenceClosure::highestNode(TNode a, UnionFind_t& unionFi }/* highestNode() */ -template -void CongruenceClosure::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list& pf) +template +void CongruenceClosure::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list& pf) throw(AssertionException) { a = highestNode(a, unionFind); @@ -863,10 +909,10 @@ void CongruenceClosure::explainAlongPath(TNode a, TNode c, Pendin Assert(e.getKind() == kind::TUPLE); pf.push_back(e[0]); pf.push_back(e[1]); - Assert(e[0][0].getKind() == kind::APPLY_UF); - Assert(e[0][1].getKind() != kind::APPLY_UF); - Assert(e[1][0].getKind() == kind::APPLY_UF); - Assert(e[1][1].getKind() != kind::APPLY_UF); + Assert(isCongruenceOperator(e[0][0].getKind())); + Assert(!isCongruenceOperator(e[0][1].getKind())); + Assert(isCongruenceOperator(e[1][0].getKind())); + Assert(!isCongruenceOperator(e[1][1].getKind())); Assert(e[0][0].getNumChildren() == e[1][0].getNumChildren()); Assert(e[0][0].getOperator() == e[1][0].getOperator(), "CongruenceClosure:: bad state: function symbols should be equal"); @@ -882,8 +928,8 @@ void CongruenceClosure::explainAlongPath(TNode a, TNode c, Pendin }/* explainAlongPath() */ -template -Node CongruenceClosure::nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind) +template +Node CongruenceClosure::nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind) throw(AssertionException) { SeenSet_t seen; @@ -907,8 +953,8 @@ Node CongruenceClosure::nearestCommonAncestor(TNode a, TNode b, U }/* nearestCommonAncestor() */ -template -Node CongruenceClosure::explain(Node a, Node b) +template +Node CongruenceClosure::explain(Node a, Node b) throw(CongruenceClosureException, AssertionException) { Assert(a != b); @@ -918,10 +964,10 @@ Node CongruenceClosure::explain(Node a, Node b) "that aren't congruent"); } - if(a.getKind() == kind::APPLY_UF) { + if(isCongruenceOperator(a.getKind())) { a = replace(flatten(a)); } - if(b.getKind() == kind::APPLY_UF) { + if(isCongruenceOperator(b.getKind())) { b = replace(flatten(b)); } @@ -976,44 +1022,44 @@ Node CongruenceClosure::explain(Node a, Node b) }/* explain() */ -template +template std::ostream& operator<<(std::ostream& out, - const CongruenceClosure& cc) { + const CongruenceClosure& cc) { out << "==============================================" << std::endl; /*out << "Representatives:" << std::endl; - for(typename CongruenceClosure::RepresentativeMap::const_iterator i = cc.d_representative.begin(); i != cc.d_representative.end(); ++i) { + for(typename CongruenceClosure::RepresentativeMap::const_iterator i = cc.d_representative.begin(); i != cc.d_representative.end(); ++i) { out << " " << (*i).first << " => " << (*i).second << std::endl; }*/ out << "ClassLists:" << std::endl; - for(typename CongruenceClosure::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) { + for(typename CongruenceClosure::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) { if(cc.find((*i).first) == (*i).first) { out << " " << (*i).first << " =>" << std::endl; - for(typename CongruenceClosure::ClassList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) { + for(typename CongruenceClosure::ClassList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) { out << " " << *j << std::endl; } } } out << "UseLists:" << std::endl; - for(typename CongruenceClosure::UseLists::const_iterator i = cc.d_useList.begin(); i != cc.d_useList.end(); ++i) { + for(typename CongruenceClosure::UseLists::const_iterator i = cc.d_useList.begin(); i != cc.d_useList.end(); ++i) { if(cc.find((*i).first) == (*i).first) { out << " " << (*i).first << " =>" << std::endl; - for(typename CongruenceClosure::UseList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) { + for(typename CongruenceClosure::UseList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) { out << " " << *j << std::endl; } } } out << "Lookup:" << std::endl; - for(typename CongruenceClosure::LookupMap::const_iterator i = cc.d_lookup.begin(); i != cc.d_lookup.end(); ++i) { + for(typename CongruenceClosure::LookupMap::const_iterator i = cc.d_lookup.begin(); i != cc.d_lookup.end(); ++i) { TNode n = (*i).second; out << " " << (*i).first << " => " << n << std::endl; } out << "Care set:" << std::endl; - for(typename CongruenceClosure::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) { + for(typename CongruenceClosure::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) { out << " " << *i << std::endl; } diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index 29a104a8e..a12cb79ea 100644 --- a/test/unit/util/congruence_closure_white.h +++ b/test/unit/util/congruence_closure_white.h @@ -92,13 +92,18 @@ class CongruenceClosureWhite : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; MyOutputChannel* d_out; - CongruenceClosure* d_cc; + CongruenceClosure >* d_cc; + CongruenceClosure* d_ccArray; TypeNode U; Node a, f, fa, ffa, fffa, ffffa, b, fb, ffb, fffb, ffffb; Node g, gab, gba, gfafb, gfbfa, gfaa, gbfb; Node h, hab, hba, hfaa; Node a_eq_b, fa_eq_b, a_eq_fb, fa_eq_fb, h_eq_g; + + Node ar, ar_a, ar_b; + Node arar, arar_a, arar_b; + public: void setUp() { @@ -106,7 +111,8 @@ public: d_nm = new NodeManager(d_context); d_scope = new NodeManagerScope(d_nm); d_out = new MyOutputChannel(d_context, d_nm); - d_cc = new CongruenceClosure(d_context, d_out); + d_cc = new CongruenceClosure >(d_context, d_out); + d_ccArray = new CongruenceClosure(d_context, d_out); U = d_nm->mkSort("U"); @@ -140,10 +146,22 @@ public: fa_eq_fb = d_nm->mkNode(kind::EQUAL, fa, fb); h_eq_g = d_nm->mkNode(kind::EQUAL, h, g); + + // arrays + ar = d_nm->mkVar("ar", d_nm->mkArrayType(U, U)); + ar_a = d_nm->mkNode(kind::SELECT, ar, a); + ar_b = d_nm->mkNode(kind::SELECT, ar, b); + + arar = d_nm->mkVar("arar", d_nm->mkArrayType(U, d_nm->mkArrayType(U, U))); + arar_a = d_nm->mkNode(kind::SELECT, arar, a); + arar_b = d_nm->mkNode(kind::SELECT, arar, b); } void tearDown() { try { + arar = arar_a = arar_b = Node::null(); + ar = ar_a = ar_b = Node::null(); + f = a = fa = ffa = fffa = ffffa = Node::null(); b = fb = ffb = fffb = ffffb = Node::null(); g = gab = gba = gfafb = gfbfa = gfaa = gbfb = Node::null(); @@ -151,14 +169,14 @@ public: a_eq_b = fa_eq_b = a_eq_fb = fa_eq_fb = h_eq_g = Node::null(); U = TypeNode::null(); + delete d_ccArray; delete d_cc; delete d_out; delete d_scope; delete d_nm; delete d_context; - } catch(Exception& e) { - Warning() << std::endl << e << std::endl; + cout << "\n\n" << e << "\n\n"; throw; } } @@ -382,7 +400,7 @@ public: TS_ASSERT(d_out->areCongruent(gfaa, gba)); TS_ASSERT(d_cc->areCongruent(gfaa, gba)); - } catch(Exception e) { + } catch(Exception& e) { cout << "\n\n" << e << "\n\n"; throw; } @@ -430,7 +448,10 @@ public: d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_0),c_1)); d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_0)); d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0)); - }catch(Exception &e) { cout << e << "\n"; throw e; } + } catch(Exception& e) { + cout << "\n\n" << e << "\n\n"; + throw e; + } } void testUF2() { @@ -450,4 +471,59 @@ public: d_cc->addEquality(ffffx_eq_z); } + void testSimpleArray() { + //Debug.on("cc"); + // add terms, then add equalities + try { + d_ccArray->addTerm(ar_a); + d_ccArray->addTerm(ar_b); + + d_ccArray->addEquality(a_eq_b); + + TS_ASSERT(d_out->areCongruent(ar_a, ar_b)); + TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b)); + + TS_ASSERT(!d_out->areCongruent(a, b)); + TS_ASSERT(d_ccArray->areCongruent(a, b)); + } catch(Exception& e) { + cout << "\n\n" << e << "\n\n"; + throw; + } + } + + void testSimpleReverseArray() { + // add equalities, then add terms; should get the same as + // testSimple() + + d_ccArray->addEquality(a_eq_b); + + d_ccArray->addTerm(ar_a); + d_ccArray->addTerm(ar_b); + + TS_ASSERT(d_out->areCongruent(ar_a, ar_b)); + TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b)); + + TS_ASSERT(!d_out->areCongruent(a, b)); + TS_ASSERT(d_ccArray->areCongruent(a, b)); + } + + void testArray() { + Node ar_eq_arar_a = d_nm->mkNode(kind::EQUAL, ar, arar_a); + Node ar2 = d_nm->mkVar("ar2", d_nm->mkArrayType(U, U)); + Node store_arar_b_ar2 = d_nm->mkNode(kind::STORE, arar, b, ar2); + Node select__store_arar_b_ar2__a = + d_nm->mkNode(kind::SELECT, store_arar_b_ar2, a); + Node select__store_arar_b_ar2__a__eq__arar_a = + d_nm->mkNode(kind::EQUAL, select__store_arar_b_ar2__a, arar_a); + + d_ccArray->addTerm(ar); + d_ccArray->addTerm(select__store_arar_b_ar2__a); + + d_ccArray->addEquality(ar_eq_arar_a); + d_ccArray->addEquality(select__store_arar_b_ar2__a__eq__arar_a); + + TS_ASSERT(d_ccArray->areCongruent(ar, select__store_arar_b_ar2__a)); + TS_ASSERT(d_out->areCongruent(ar, select__store_arar_b_ar2__a)); + } + };/* class CongruenceClosureWhite */ -- 2.30.2