diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-19 17:16:16 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-19 17:16:16 +0000 |
commit | 1f80df98e2766a0202741d9e924bf842ba2225b5 (patch) | |
tree | 8ab2ece58fcf56de4b179cdb24b13df5be770695 /src/theory/arith | |
parent | 913691ef342edf411a33b81ecc071682978af858 (diff) |
Changed the splitting-on-demand lemmas of arithmetic to no longer contain the equality being split on. Instead of issuing 'x != y implies (x < y or x > y)', the lemma is now '(x <= y or x >= y)'. This resolves bug 450.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/constraint.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 792d4b16c..392d04f6c 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -590,10 +590,10 @@ Node ConstraintValue::split(){ TNode lhs = eqNode[0]; TNode rhs = eqNode[1]; - Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; - Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; + Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs; + Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs; - Node lemma = NodeBuilder<3>(OR) << eqNode << ltNode << gtNode; + Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode; eq->d_database->pushSplitWatch(eq); |