From 4713dd0a7fcf73a73909cc35e9e1d615022c8975 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 17 Feb 2011 01:02:06 +0000 Subject: [PATCH] Updates based on the group code review of arithmetic on 2011-02-15. The only substantive change is that UnatePropagator no longer uses attributes. The rest is comments and other beatification. --- src/theory/arith/Makefile.am | 2 - src/theory/arith/arith_utilities.h | 89 +++++------- src/theory/arith/ordered_set.h | 15 +- src/theory/arith/unate_propagator.cpp | 189 +++++++++++++------------- src/theory/arith/unate_propagator.h | 48 ++++--- 5 files changed, 168 insertions(+), 175 deletions(-) diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 31867c4cf..139a53350 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -17,9 +17,7 @@ libarith_la_SOURCES = \ delta_rational.cpp \ partial_model.h \ partial_model.cpp \ - ordered_bounds_list.h \ ordered_set.h \ - arithvar_dense_set.h \ arithvar_set.h \ tableau.h \ tableau.cpp \ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 452d54fae..c8532f1a2 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -119,16 +119,22 @@ inline bool isRelationOperator(Kind k){ } } -/** is k \in {LT, LEQ, EQ, GEQ, GT} */ +/** + * Given a relational kind, k, return the kind k' s.t. + * swapping the lefthand and righthand side is equivalent. + * + * The following equivalence should hold, + * (k l r) <=> (k' r l) + */ inline Kind reverseRelationKind(Kind k){ using namespace kind; switch(k){ - case LT: return GT; - case LEQ: return GEQ; + case LT: return GT; + case LEQ: return GEQ; case EQUAL: return EQUAL; - case GEQ: return LEQ; - case GT: return LT; + case GEQ: return LEQ; + case GT: return LT; default: Unreachable(); @@ -150,56 +156,13 @@ inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Ration } } - - -inline Node pushInNegation(Node assertion){ - using namespace CVC4::kind; - Assert(assertion.getKind() == NOT); - - Node p = assertion[0]; - - Kind k; - - switch(p.getKind()){ - case EQUAL: - return assertion; - case GT: - k = LEQ; - break; - case GEQ: - k = LT; - break; - case LEQ: - k = GT; - break; - case LT: - k = GEQ; - break; - default: - Unreachable(); - } - - return NodeManager::currentNM()->mkNode(k, p[0],p[1]); -} - /** - * Validates that a node constraint has the following form: - * constraint: x |><| c - * where |><| is either <, <=, ==, >=, LT, - * x is of metakind a variabale, - * and c is a constant rational. + * Returns the appropraite coefficient for the infinitesimal given the kind + * for an arithmetic atom inorder to represent strict inequalities as inequalities. + * x < c becomes x <= c + (-1) * \delta + * x > c becomes x >= x + ( 1) * \delta + * Non-strict inequalities have a coefficient of zero. */ -inline bool validateConstraint(TNode constraint){ - using namespace CVC4::kind; - switch(constraint.getKind()){ - case LT:case LEQ: case EQUAL: case GEQ: case GT: break; - default: return false; - } - - if(constraint[0].getMetaKind() != metakind::VARIABLE) return false; - return constraint[1].getKind() == CONST_RATIONAL; -} - inline int deltaCoeff(Kind k){ switch(k){ case kind::LT: @@ -256,6 +219,26 @@ inline int deltaCoeff(Kind k){ } } + /** + * Takes two nodes with exactly 2 children, + * the second child of both are of kind CONST_RATIONAL, + * and compares value of the two children. + * This is for comparing inequality nodes. + * RightHandRationalLT((<= x 50), (< x 75)) == true + */ +struct RightHandRationalLT +{ + bool operator()(TNode s1, TNode s2) const + { + TNode rh1 = s1[1]; + TNode rh2 = s2[1]; + const Rational& c1 = rh1.getConst(); + const Rational& c2 = rh2.getConst(); + int cmpRes = c1.cmp(c2); + return cmpRes < 0; + } +}; + }; /* namesapce arith */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index fa606188a..68c5e18c9 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -2,26 +2,15 @@ #include "expr/kind.h" #include "expr/node.h" #include "util/Assert.h" +#include "theory/arith/arith_utilities.h" namespace CVC4 { namespace theory { namespace arith { -struct RightHandRationalLT -{ - bool operator()(TNode s1, TNode s2) const - { - TNode rh1 = s1[1]; - TNode rh2 = s2[1]; - const Rational& c1 = rh1.getConst(); - const Rational& c2 = rh2.getConst(); - int cmpRes = c1.cmp(c2); - return cmpRes < 0; - } -}; -typedef std::set OrderedSet; +typedef std::set OrderedSet; struct SetCleanupStrategy{ static void cleanup(OrderedSet* l){ diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp index e042e2320..069f4f0f3 100644 --- a/src/theory/arith/unate_propagator.cpp +++ b/src/theory/arith/unate_propagator.cpp @@ -30,28 +30,37 @@ using namespace CVC4::kind; using namespace std; -struct PropagatorLeqSetID {}; -typedef expr::Attribute PropagatorLeqSet; - -struct PropagatorEqSetID {}; -typedef expr::Attribute PropagatorEqSet; - -struct PropagatorGeqSetID {}; -typedef expr::Attribute PropagatorGeqSet; - ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) : - d_arithOut(out) + d_arithOut(out), d_orderedListMap() { } bool ArithUnatePropagator::leftIsSetup(TNode left){ - return left.hasAttribute(PropagatorEqSet()); + return d_orderedListMap.find(left) != d_orderedListMap.end(); +} + +ArithUnatePropagator::OrderedSetTriple& ArithUnatePropagator::getOrderedSetTriple(TNode left){ + Assert(leftIsSetup(left)); + return d_orderedListMap[left]; +} + +OrderedSet& ArithUnatePropagator::getEqSet(TNode left){ + Assert(leftIsSetup(left)); + return getOrderedSetTriple(left).d_eqSet; +} +OrderedSet& ArithUnatePropagator::getLeqSet(TNode left){ + Assert(leftIsSetup(left)); + return getOrderedSetTriple(left).d_leqSet; +} +OrderedSet& ArithUnatePropagator::getGeqSet(TNode left){ + Assert(leftIsSetup(left)); + return getOrderedSetTriple(left).d_geqSet; } bool ArithUnatePropagator::hasAnyAtoms(TNode v){ Assert(!leftIsSetup(v) - || !v.getAttribute(PropagatorEqSet())->empty() - || !v.getAttribute(PropagatorLeqSet())->empty() - || !v.getAttribute(PropagatorGeqSet())->empty()); + || !(getEqSet(v)).empty() + || !(getLeqSet(v)).empty() + || !(getGeqSet(v)).empty()); return leftIsSetup(v); } @@ -59,13 +68,7 @@ bool ArithUnatePropagator::hasAnyAtoms(TNode v){ void ArithUnatePropagator::setupLefthand(TNode left){ Assert(!leftIsSetup(left)); - OrderedSet* eqList = new OrderedSet(); - OrderedSet* leqList = new OrderedSet(); - OrderedSet* geqList = new OrderedSet(); - - left.setAttribute(PropagatorEqSet(), eqList); - left.setAttribute(PropagatorLeqSet(), geqList); - left.setAttribute(PropagatorGeqSet(), leqList); + d_orderedListMap[left] = OrderedSetTriple(); } void ArithUnatePropagator::addAtom(TNode atom){ @@ -76,38 +79,38 @@ void ArithUnatePropagator::addAtom(TNode atom){ setupLefthand(left); } - OrderedSet* eqSet = left.getAttribute(PropagatorEqSet()); - OrderedSet* leqSet = left.getAttribute(PropagatorLeqSet()); - OrderedSet* geqSet = left.getAttribute(PropagatorGeqSet()); + OrderedSet& eqSet = getEqSet(left); + OrderedSet& leqSet = getLeqSet(left); + OrderedSet& geqSet = getGeqSet(left); switch(atom.getKind()){ case EQUAL: { - pair res = eqSet->insert(atom); + pair res = eqSet.insert(atom); Assert(res.second); - addEqualityToEqualities(atom, eqSet, res.first); - addEqualityToLeqs(atom, leqSet); - addEqualityToGeqs(atom, geqSet); + addImplicationsUsingEqualityAndEqualityList(atom, eqSet); + addImplicationsUsingEqualityAndLeqList(atom, leqSet); + addImplicationsUsingEqualityAndGeqList(atom, geqSet); break; } case LEQ: { - pair res = leqSet->insert(atom); + pair res = leqSet.insert(atom); Assert(res.second); - addLeqToLeqs(atom, leqSet, res.first); - addLeqToEqualities(atom, eqSet); - addLeqToGeqs(atom, geqSet); + addImplicationsUsingLeqAndEqualityList(atom, eqSet); + addImplicationsUsingLeqAndLeqList(atom, leqSet); + addImplicationsUsingLeqAndGeqList(atom, geqSet); break; } case GEQ: { - pair res = geqSet->insert(atom); + pair res = geqSet.insert(atom); Assert(res.second); - addGeqToGeqs(atom, geqSet, res.first); - addGeqToEqualities(atom, eqSet); - addGeqToLeqs(atom, leqSet); + addImplicationsUsingGeqAndEqualityList(atom, eqSet); + addImplicationsUsingGeqAndLeqList(atom, leqSet); + addImplicationsUsingGeqAndGeqList(atom, geqSet); break; } @@ -125,23 +128,24 @@ bool rightHandRationalIsEqual(TNode a, TNode b){ return qA == qB; } -bool rightHandRationalIsLT(TNode a, TNode b){ - TNode secondA = a[1]; - TNode secondB = b[1]; - const Rational& qA = secondA.getConst(); - const Rational& qB = secondB.getConst(); - return qA < qB; +bool rightHandRationalIsLT(TNode a, TNode b){ + //This version is sticking around because it is easier to read! + return RightHandRationalLT()(a,b); } -void ArithUnatePropagator::addEqualityToEqualities(TNode atom, - OrderedSet* eqSet, - OrderedSet::iterator eqPos){ +//void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet* eqSet); + +void ArithUnatePropagator::addImplicationsUsingEqualityAndEqualityList(TNode atom, OrderedSet& eqSet){ Assert(atom.getKind() == EQUAL); + OrderedSet::iterator eqPos = eqSet.find(atom); + Assert(eqPos != eqSet.end()); + Assert(*eqPos == atom); + Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - for(OrderedSet::iterator eqIter = eqSet->begin(); - eqIter != eqSet->end(); ++eqIter){ + for(OrderedSet::iterator eqIter = eqSet.begin(); + eqIter != eqSet.end(); ++eqIter){ if(eqIter == eqPos) continue; TNode eq = *eqIter; Assert(!rightHandRationalIsEqual(eq, atom)); @@ -149,17 +153,17 @@ void ArithUnatePropagator::addEqualityToEqualities(TNode atom, } } -void ArithUnatePropagator::addEqualityToLeqs(TNode atom, OrderedSet* leqSet) -{ +void ArithUnatePropagator::addImplicationsUsingEqualityAndLeqList(TNode atom, OrderedSet& leqSet){ + Assert(atom.getKind() == EQUAL); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator leqIter = leqSet->lower_bound(atom); - if(leqIter != leqSet->end()){ + OrderedSet::iterator leqIter = leqSet.lower_bound(atom); + if(leqIter != leqSet.end()){ TNode lowerBound = *leqIter; if(rightHandRationalIsEqual(atom, lowerBound)){ addImplication(atom, lowerBound); // x=b /\ b = b' => x <= b' - if(leqIter != leqSet->begin()){ + if(leqIter != leqSet.begin()){ --leqIter; Assert(rightHandRationalIsLT(*leqIter, atom)); addImplication(*leqIter, negation); // x=b /\ b > b' => x > b' @@ -169,34 +173,34 @@ void ArithUnatePropagator::addEqualityToLeqs(TNode atom, OrderedSet* leqSet) Assert(rightHandRationalIsLT(atom, lowerBound)); addImplication(atom, lowerBound);// x=b /\ b < b' => x <= b' - if(leqIter != leqSet->begin()){ + if(leqIter != leqSet.begin()){ --leqIter; Assert(rightHandRationalIsLT(*leqIter, atom)); addImplication(*leqIter, negation);// x=b /\ b > b' => x > b' } } - }else if(leqIter != leqSet->begin()){ + }else if(leqIter != leqSet.begin()){ --leqIter; TNode strictlyLessThan = *leqIter; Assert(rightHandRationalIsLT(strictlyLessThan, atom)); addImplication(*leqIter, negation); // x=b /\ b < b' => x <= b' }else{ - Assert(leqSet->empty()); + Assert(leqSet.empty()); } } -void ArithUnatePropagator::addEqualityToGeqs(TNode atom, OrderedSet* geqSet){ +void ArithUnatePropagator::addImplicationsUsingEqualityAndGeqList(TNode atom, OrderedSet& geqSet){ Assert(atom.getKind() == EQUAL); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator geqIter = geqSet->lower_bound(atom); - if(geqIter != geqSet->end()){ + OrderedSet::iterator geqIter = geqSet.lower_bound(atom); + if(geqIter != geqSet.end()){ TNode lowerBound = *geqIter; if(rightHandRationalIsEqual(atom, lowerBound)){ addImplication(atom, lowerBound); // x=b /\ b = b' => x >= b' ++geqIter; - if(geqIter != geqSet->end()){ // x=b /\ b < b' => x < b' + if(geqIter != geqSet.end()){ // x=b /\ b < b' => x < b' TNode strictlyGt = *geqIter; Assert(rightHandRationalIsLT( atom, strictlyGt )); addImplication(strictlyGt, negation); @@ -204,32 +208,33 @@ void ArithUnatePropagator::addEqualityToGeqs(TNode atom, OrderedSet* geqSet){ }else{ Assert(rightHandRationalIsLT(atom, lowerBound)); addImplication(lowerBound, negation);// x=b /\ b < b' => x < b' - if(geqIter != geqSet->begin()){ + if(geqIter != geqSet.begin()){ --geqIter; TNode strictlyLessThan = *geqIter; Assert(rightHandRationalIsLT(strictlyLessThan, atom)); addImplication(atom, strictlyLessThan);// x=b /\ b > b' => x >= b' } } - }else if(geqIter != geqSet->begin()){ + }else if(geqIter != geqSet.begin()){ --geqIter; TNode strictlyLT = *geqIter; Assert(rightHandRationalIsLT(strictlyLT, atom)); addImplication(atom, strictlyLT);// x=b /\ b > b' => x >= b' }else{ - Assert(geqSet->empty()); + Assert(geqSet.empty()); } } -void ArithUnatePropagator::addLeqToLeqs -(TNode atom, - OrderedSet* leqSet, - OrderedSet::iterator atomPos) +void ArithUnatePropagator::addImplicationsUsingLeqAndLeqList(TNode atom, OrderedSet& leqSet) { Assert(atom.getKind() == LEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - if(atomPos != leqSet->begin()){ + OrderedSet::iterator atomPos = leqSet.find(atom); + Assert(atomPos != leqSet.end()); + Assert(*atomPos == atom); + + if(atomPos != leqSet.begin()){ --atomPos; TNode beforeLeq = *atomPos; Assert(rightHandRationalIsLT(beforeLeq, atom)); @@ -237,25 +242,25 @@ void ArithUnatePropagator::addLeqToLeqs ++atomPos; } ++atomPos; - if(atomPos != leqSet->end()){ + if(atomPos != leqSet.end()){ TNode afterLeq = *atomPos; Assert(rightHandRationalIsLT(atom, afterLeq)); addImplication(atom, afterLeq);// x<=b /\ b < b' => x <= b' } } -void ArithUnatePropagator::addLeqToGeqs(TNode atom, OrderedSet* geqSet) { +void ArithUnatePropagator::addImplicationsUsingLeqAndGeqList(TNode atom, OrderedSet& geqSet) { Assert(atom.getKind() == LEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator geqIter = geqSet->lower_bound(atom); - if(geqIter != geqSet->end()){ + OrderedSet::iterator geqIter = geqSet.lower_bound(atom); + if(geqIter != geqSet.end()){ TNode lowerBound = *geqIter; if(rightHandRationalIsEqual(atom, lowerBound)){ Assert(rightHandRationalIsEqual(atom, lowerBound)); addImplication(negation, lowerBound);// (x > b) => (x >= b) ++geqIter; - if(geqIter != geqSet->end()){ + if(geqIter != geqSet.end()){ TNode next = *geqIter; Assert(rightHandRationalIsLT(atom, next)); addImplication(next, negation);// x>=b' /\ b' > b => x > b @@ -263,29 +268,29 @@ void ArithUnatePropagator::addLeqToGeqs(TNode atom, OrderedSet* geqSet) { }else{ Assert(rightHandRationalIsLT(atom, lowerBound)); addImplication(lowerBound, negation);// x>=b' /\ b' > b => x > b - if(geqIter != geqSet->begin()){ + if(geqIter != geqSet.begin()){ --geqIter; TNode prev = *geqIter; Assert(rightHandRationalIsLT(prev, atom)); addImplication(negation, prev);// (x>b /\ b > b') => x >= b' } } - }else if(geqIter != geqSet->begin()){ + }else if(geqIter != geqSet.begin()){ --geqIter; TNode strictlyLT = *geqIter; Assert(rightHandRationalIsLT(strictlyLT, atom)); addImplication(negation, strictlyLT);// (x>b /\ b > b') => x >= b' }else{ - Assert(geqSet->empty()); + Assert(geqSet.empty()); } } -void ArithUnatePropagator::addLeqToEqualities(TNode atom, OrderedSet* eqSet) { +void ArithUnatePropagator::addImplicationsUsingLeqAndEqualityList(TNode atom, OrderedSet& eqSet) { Assert(atom.getKind() == LEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); //TODO Improve this later - for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){ + for(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){ TNode eq = *eqIter; if(rightHandRationalIsEqual(atom, eq)){ // (x = b' /\ b = b') => x <= b @@ -301,13 +306,15 @@ void ArithUnatePropagator::addLeqToEqualities(TNode atom, OrderedSet* eqSet) { } -void ArithUnatePropagator::addGeqToGeqs -(TNode atom, OrderedSet* geqSet, OrderedSet::iterator atomPos) -{ +void ArithUnatePropagator::addImplicationsUsingGeqAndGeqList(TNode atom, OrderedSet& geqSet){ Assert(atom.getKind() == GEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - if(atomPos != geqSet->begin()){ + OrderedSet::iterator atomPos = geqSet.find(atom); + Assert(atomPos != geqSet.end()); + Assert(*atomPos == atom); + + if(atomPos != geqSet.begin()){ --atomPos; TNode beforeGeq = *atomPos; Assert(rightHandRationalIsLT(beforeGeq, atom)); @@ -315,26 +322,26 @@ void ArithUnatePropagator::addGeqToGeqs ++atomPos; } ++atomPos; - if(atomPos != geqSet->end()){ + if(atomPos != geqSet.end()){ TNode afterGeq = *atomPos; Assert(rightHandRationalIsLT(atom, afterGeq)); addImplication(afterGeq, atom);// x>=b' /\ b' > b => x >= b } } -void ArithUnatePropagator::addGeqToLeqs(TNode atom, OrderedSet* leqSet){ +void ArithUnatePropagator::addImplicationsUsingGeqAndLeqList(TNode atom, OrderedSet& leqSet){ Assert(atom.getKind() == GEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); - OrderedSet::iterator leqIter = leqSet->lower_bound(atom); - if(leqIter != leqSet->end()){ + OrderedSet::iterator leqIter = leqSet.lower_bound(atom); + if(leqIter != leqSet.end()){ TNode lowerBound = *leqIter; if(rightHandRationalIsEqual(atom, lowerBound)){ Assert(rightHandRationalIsEqual(atom, lowerBound)); addImplication(negation, lowerBound);// (x < b) => (x <= b) - if(leqIter != leqSet->begin()){ + if(leqIter != leqSet.begin()){ --leqIter; TNode prev = *leqIter; Assert(rightHandRationalIsLT(prev, atom)); @@ -344,28 +351,28 @@ void ArithUnatePropagator::addGeqToLeqs(TNode atom, OrderedSet* leqSet){ Assert(rightHandRationalIsLT(atom, lowerBound)); addImplication(negation, lowerBound);// (x < b /\ b < b') => x <= b' ++leqIter; - if(leqIter != leqSet->end()){ + if(leqIter != leqSet.end()){ TNode next = *leqIter; Assert(rightHandRationalIsLT(atom, next)); addImplication(negation, next);// (x < b /\ b < b') => x <= b' } } - }else if(leqIter != leqSet->begin()){ + }else if(leqIter != leqSet.begin()){ --leqIter; TNode strictlyLT = *leqIter; Assert(rightHandRationalIsLT(strictlyLT, atom)); addImplication(strictlyLT, negation);// (x <= b' /\ b' < b) => x < b }else{ - Assert(leqSet->empty()); + Assert(leqSet.empty()); } } -void ArithUnatePropagator::addGeqToEqualities(TNode atom, OrderedSet* eqSet){ +void ArithUnatePropagator::addImplicationsUsingGeqAndEqualityList(TNode atom, OrderedSet& eqSet){ Assert(atom.getKind() == GEQ); Node negation = NodeManager::currentNM()->mkNode(NOT, atom); //TODO Improve this later - for(OrderedSet::iterator eqIter = eqSet->begin(); eqIter != eqSet->end(); ++eqIter){ + for(OrderedSet::iterator eqIter = eqSet.begin(); eqIter != eqSet.end(); ++eqIter){ TNode eq = *eqIter; if(rightHandRationalIsEqual(atom, eq)){ // (x = b' /\ b = b') => x >= b diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index ca2135cf3..383b9f8e8 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -49,13 +49,13 @@ #define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H #include "expr/node.h" -#include "context/cdlist.h" #include "context/context.h" -#include "context/cdo.h" #include "theory/output_channel.h" #include "theory/arith/ordered_set.h" +#include + namespace CVC4 { namespace theory { namespace arith { @@ -68,6 +68,16 @@ private: */ OutputChannel& d_arithOut; + struct OrderedSetTriple { + OrderedSet d_leqSet; + OrderedSet d_eqSet; + OrderedSet d_geqSet; + }; + + /** TODO: justify making this a TNode. */ + typedef __gnu_cxx::hash_map NodeToOrderedSetMap; + NodeToOrderedSetMap d_orderedListMap; + public: ArithUnatePropagator(context::Context* cxt, OutputChannel& arith); @@ -81,6 +91,12 @@ public: bool hasAnyAtoms(TNode v); private: + OrderedSetTriple& getOrderedSetTriple(TNode left); + OrderedSet& getEqSet(TNode left); + OrderedSet& getLeqSet(TNode left); + OrderedSet& getGeqSet(TNode left); + + /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */ void addImplication(TNode a, TNode b); @@ -92,32 +108,32 @@ private: /** - * The addKtoJs(...) functions are the work horses of ArithUnatePropagator. + * The addImplicationsUsingKAndJList(...) + * functions are the work horses of ArithUnatePropagator. * These take an atom of the kind K that has just been added - * to its associated list, and the list of Js associated with the lhs, + * to its associated list, and the ordered list of Js associated with the lhs, * and uses these to deduce unate implications. * (K and J vary over EQUAL, LEQ, and GEQ.) * * Input: - * atom - the atom being inserted - * Kset - the list of atoms of kind K associated with the lhs. - * atomPos - the atoms Position in its own list after being inserted. + * atom - the atom being inserted of kind K + * Jset - the list of atoms of kind J associated with the lhs. * * Unfortunately, these tend to be an absolute bear to read because * of all of the special casing and C++ iterator manipulation required. */ - void addEqualityToEqualities(TNode eq, OrderedSet* eqSet, OrderedSet::iterator eqPos); - void addEqualityToLeqs(TNode eq, OrderedSet* leqSet); - void addEqualityToGeqs(TNode eq, OrderedSet* geqSet); + void addImplicationsUsingEqualityAndEqualityList(TNode eq, OrderedSet& eqSet); + void addImplicationsUsingEqualityAndLeqList(TNode eq, OrderedSet& leqSet); + void addImplicationsUsingEqualityAndGeqList(TNode eq, OrderedSet& geqSet); - void addLeqToLeqs(TNode leq, OrderedSet* leqSet, OrderedSet::iterator leqPos); - void addLeqToGeqs(TNode leq, OrderedSet* geqSet); - void addLeqToEqualities(TNode leq, OrderedSet* eqSet); + void addImplicationsUsingLeqAndEqualityList(TNode leq, OrderedSet& eqSet); + void addImplicationsUsingLeqAndLeqList(TNode leq, OrderedSet& leqSet); + void addImplicationsUsingLeqAndGeqList(TNode leq, OrderedSet& geqSet); - void addGeqToGeqs(TNode geq, OrderedSet* geqSet, OrderedSet::iterator geqPos); - void addGeqToLeqs(TNode geq, OrderedSet* leqSet); - void addGeqToEqualities(TNode geq, OrderedSet* eqSet); + void addImplicationsUsingGeqAndEqualityList(TNode geq, OrderedSet& eqSet); + void addImplicationsUsingGeqAndLeqList(TNode geq, OrderedSet& leqSet); + void addImplicationsUsingGeqAndGeqList(TNode geq, OrderedSet& geqSet); }; -- 2.30.2