From: Tim King <taking@cs.nyu.edu>
Date: Tue, 24 Jun 2014 20:46:09 +0000 (-0400)
Subject: Fixing a soundness bug in arithmetic and a roubustness problem in rings.
X-Git-Tag: cvc5-1.0.0~6700^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c67780be0eaa32207025d5e9f867cab731353693;p=cvc5.git

Fixing a soundness bug in arithmetic and a roubustness problem in rings.
---

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index d5dcae726..d3702ccd8 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -308,6 +308,9 @@ void ArithIteUtils::addImplications(Node x, Node y){
   // (=> (not x) y)
   // (=> (not y) x)
 
+  x = Rewriter::rewrite(x);
+  y = Rewriter::rewrite(y);
+
   Node xneg = x.negate();
   Node yneg = y.negate();
   d_implies[xneg].insert(y);
@@ -369,9 +372,21 @@ bool ArithIteUtils::solveBinOr(TNode binor){
   Assert(binor[0].getKind() ==  kind::EQUAL);
   Assert(binor[1].getKind() ==  kind::EQUAL);
 
+  //Node n = 
   Node n = applySubstitutions(binor);
+  if(n != binor){
+    n = Rewriter::rewrite(n);
+
+    if(!(n.getKind() == kind::OR &&
+	 n.getNumChildren() == 2 &&
+	 n[0].getKind() ==  kind::EQUAL &&
+	 n[1].getKind() ==  kind::EQUAL)){
+      return false;
+    }
+  }
+
   Assert(n.getKind() == kind::OR);
-  Assert(binor.getNumChildren() == 2);
+  Assert(n.getNumChildren() == 2);
   TNode l = n[0];
   TNode r = n[1];
 
@@ -416,7 +431,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){
 
         NodeManager* nm = NodeManager::currentNM();
 
-        Node cnd = findIteCnd(binor[0], binor[1]);
+        Node cnd = findIteCnd(l, r);
 
         Node sk = nm->mkSkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f3bdca7c7..f6ac951bc 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2964,6 +2964,19 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
         if(mipRes == MipClosed){
           d_likelyIntegerInfeasible = true;
           replayLog(approx);
+
+	  if(!anyConflict()){
+	    //start up simplex
+	    d_partialModel.stopQueueingBoundCounts();
+	    UpdateTrackingCallback utcb(&d_linEq);
+	    d_partialModel.processBoundsQueue(utcb);
+	    d_linEq.startTrackingBoundCounts();
+	    //call simplex
+	    solveRelaxationOrPanic(effortLevel);
+	    // shutdown simplex
+	    d_linEq.stopTrackingBoundCounts();
+	    d_partialModel.startQueueingBoundCounts();
+	  }
         }
         if(!(anyConflict() || !d_approxCuts.empty())){
           turnOffApproxFor(options::replayNumericFailurePenalty());