diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
commit | ccd77233892ace44fd4852999e66534d1c2283ea (patch) | |
tree | a856cacd24508a5839fcdbe728583ff055b64e34 /src/theory/arith/arith_utilities.h | |
parent | 9644b6e12fbd3b649daafa43c5400d272e27bfb4 (diff) |
Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
Roughly speaking this means: (= x (+ y z)) is in normal form.
(See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 127 |
1 files changed, 73 insertions, 54 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index a5d94ec40..af32c3f87 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -168,17 +168,17 @@ inline int deltaCoeff(Kind k){ * - (NOT (GT left right)) -> LEQ * If none of these match, it returns UNDEFINED_KIND. */ - inline Kind simplifiedKind(TNode assertion){ - switch(assertion.getKind()){ + inline Kind oldSimplifiedKind(TNode literal){ + switch(literal.getKind()){ case kind::LT: case kind::GT: case kind::LEQ: case kind::GEQ: case kind::EQUAL: - return assertion.getKind(); + return literal.getKind(); case kind::NOT: { - TNode atom = assertion[0]; + TNode atom = literal[0]; switch(atom.getKind()){ case kind::LEQ: //(not (LEQ x c)) <=> (GT x c) return kind::GT; @@ -201,57 +201,58 @@ inline int deltaCoeff(Kind k){ } } -template <bool selectLeft> -inline TNode getSide(TNode assertion, Kind simpleKind){ - switch(simpleKind){ - case kind::LT: - case kind::GT: - case kind::DISTINCT: - return selectLeft ? (assertion[0])[0] : (assertion[0])[1]; - case kind::LEQ: - case kind::GEQ: - case kind::EQUAL: - return selectLeft ? assertion[0] : assertion[1]; - default: - Unreachable(); - return TNode::null(); - } -} - -inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ - TNode right = getSide<false>(assertion, simpleKind); - - Assert(right.getKind() == kind::CONST_RATIONAL); - const Rational& noninf = right.getConst<Rational>(); - Rational inf = Rational(Integer(deltaCoeff(simpleKind))); - return DeltaRational(noninf, inf); -} - -inline DeltaRational asDeltaRational(TNode n){ - Kind simp = simplifiedKind(n); - return determineRightConstant(n, simp); -} - - /** - * 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; - } -}; +// template <bool selectLeft> +// inline TNode getSide(TNode assertion, Kind simpleKind){ +// switch(simpleKind){ +// case kind::LT: +// case kind::GT: +// case kind::DISTINCT: +// return selectLeft ? (assertion[0])[0] : (assertion[0])[1]; +// case kind::LEQ: +// case kind::GEQ: +// case kind::EQUAL: +// return selectLeft ? assertion[0] : assertion[1]; +// default: +// Unreachable(); +// return TNode::null(); +// } +// } + +// inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){ +// TNode right = getSide<false>(assertion, simpleKind); + +// Assert(right.getKind() == kind::CONST_RATIONAL); +// const Rational& noninf = right.getConst<Rational>(); + +// Rational inf = Rational(Integer(deltaCoeff(simpleKind))); +// return DeltaRational(noninf, inf); +// } + +// inline DeltaRational asDeltaRational(TNode n){ +// Kind simp = simplifiedKind(n); +// return determineRightConstant(n, simp); +// } + +// /** +// * 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; +// } +// }; inline Node negateConjunctionAsClause(TNode conjunction){ Assert(conjunction.getKind() == kind::AND); @@ -278,6 +279,24 @@ inline Node maybeUnaryConvert(NodeBuilder<>& builder){ } } +inline void flattenAnd(Node n, std::vector<TNode>& out){ + Assert(n.getKind() == kind::AND); + for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ + Node curr = *i; + if(curr.getKind() == kind::AND){ + flattenAnd(curr, out); + }else{ + out.push_back(curr); + } + } +} + +inline Node flattenAnd(Node n){ + std::vector<TNode> out; + flattenAnd(n, out); + return NodeManager::currentNM()->mkNode(kind::AND, out); +} + }; /* namesapce arith */ }; /* namespace theory */ }; /* namespace CVC4 */ |