Some bug fixes in the SAT for lemmas, and an experiment with a more complete (wr propagation) splitter in arithmetic.

1 files changed, 11 insertions, 1 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7b768d9af..7cedbcd20 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -416,7 +416,17 @@ void TheoryArith::check(Effort effortLevel){
           Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
           Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
           Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
-          d_out->lemma(lemma);
+
+          // < => !>
+          Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode();
+          // < => !=
+          Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode();
+          // > => !=
+          Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode();
+          // All the implication
+          Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3;
+
+          d_out->lemma(lemma.andNode(impClosure));
         }
       }
     }