diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-17 01:02:06 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-17 01:02:06 +0000 |
commit | 4713dd0a7fcf73a73909cc35e9e1d615022c8975 (patch) | |
tree | 36df381464b1fa8c7163f202fb1fa4cf6d2b1e20 /src/theory/arith/arith_utilities.h | |
parent | 6bfdda562cc4d838f9b1e90b7c7107162bf5200e (diff) |
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.
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 89 |
1 files changed, 36 insertions, 53 deletions
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<Rational>(); + const Rational& c2 = rh2.getConst<Rational>(); + int cmpRes = c1.cmp(c2); + return cmpRes < 0; + } +}; + }; /* namesapce arith */ }; /* namespace theory */ }; /* namespace CVC4 */ |