From c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 26 Nov 2012 17:30:44 +0000
Subject: [PATCH] Removing DioSolver::acceptableOriginalNodes(). This assertion
 was too strong, and was broken by r4620. This commit resolves bug463. Adding
 a previously triggering test case.

---
 src/theory/arith/dio_solver.cpp          | 20 ++---------------
 src/theory/arith/dio_solver.h            |  5 -----
 test/regress/regress0/auflia/Makefile.am |  3 ++-
 test/regress/regress0/auflia/x2.smt      | 28 ++++++++++++++++++++++++
 4 files changed, 32 insertions(+), 24 deletions(-)
 create mode 100644 test/regress/regress0/auflia/x2.smt

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 46ca717bf..4d9d66cec 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -132,27 +132,11 @@ bool DioSolver::debugEqualityInInputEquations(Node eq){
   return false;
 }
 
-bool DioSolver::acceptableOriginalNodes(Node n){
-  Kind k = n.getKind();
-  if(k == kind::EQUAL){
-    return true;
-  }else if(k == kind::AND){
-    Node ub = n[0];
-    Node lb = n[1];
-    Kind kub = Comparison::comparisonKind(ub);
-    Kind klb = Comparison::comparisonKind(lb);
-    Debug("nf::tmp") << n << endl;
-    return (kub == kind::GEQ || kub==kind::LT) && (klb == kind::GEQ || klb == kind::LT);
-  }else{
-    return false;
-  }
-}
 
 void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
   Assert(!debugEqualityInInputEquations(reason));
   Assert(eq.debugIsIntegral());
   Assert(eq.getNode().getKind() == kind::EQUAL);
-  Assert(acceptableOriginalNodes(reason));
 
   SumPair sp = eq.toSumPair();
   uint32_t length = sp.maxLength();
@@ -209,7 +193,6 @@ Node DioSolver::proveIndex(TrailIndex i){
     Variable v = vl.getHead();
 
     Node input = proofVariableToReason(v);
-    Assert(acceptableOriginalNodes(input));
     if(input.getKind() == kind::AND){
       for(Node::iterator input_iter = input.begin(), input_end = input.end(); input_iter != input_end; ++input_iter){
 	Node inputChild = *input_iter;
@@ -689,9 +672,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex(
 
   TrailIndex ci = d_trail.size();
   d_trail.push_back(Constraint(newSI, Polynomial::mkZero()));
+  // no longer reference av safely!
 
   Debug("arith::dio") << "Decompose ci(" << ci <<":" <<  d_trail[ci].d_eq.getNode()
-                      << ") for " << av.getNode() << endl;
+                      << ") for " << d_trail[i].d_minimalMonomial.getNode() << endl;
   Assert(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl) == Constant::mkConstant(-1));
 
   SumPair newFact = r + fresh_a;
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 7d1faed86..bfcd19021 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -237,11 +237,6 @@ private:
    */
   size_t allocateVariableInPool();
 
-  /**
-   * Returns true if the node can be accepted as a reason according to the
-   * kinds.
-   */
-  bool acceptableOriginalNodes(Node n);
 
   /** Empties the unproccessed input constraints into the queue. */
   void enqueueInputConstraints();
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index d12bb0441..cc4a1556f 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -21,7 +21,8 @@ TESTS =	\
 	fuzz04.smt \
 	fuzz05.smt \
 	a17.smt \
-	error72.delta2.smt
+	error72.delta2.smt \
+	x2.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/auflia/x2.smt b/test/regress/regress0/auflia/x2.smt
new file mode 100644
index 000000000..3566d9858
--- /dev/null
+++ b/test/regress/regress0/auflia/x2.smt
@@ -0,0 +1,28 @@
+(benchmark fuzzsmt
+:logic QF_AUFLIA
+:extrafuns ((v4 Array))
+:extrafuns ((f0 Int Int))
+:extrapreds ((p0 Int Int Int))
+:status sat
+:formula
+(let (?n1 0)
+(flet ($n2 (p0 ?n1 ?n1 ?n1))
+(let (?n3 1)
+(let (?n4 (ite $n2 ?n3 ?n1))
+(flet ($n5 (< ?n1 ?n4))
+(flet ($n6 (p0 ?n3 ?n1 ?n1))
+(let (?n7 (ite $n6 ?n3 ?n1))
+(let (?n8 (ite $n5 ?n7 ?n3))
+(flet ($n9 (< ?n1 ?n8))
+(flet ($n10 true)
+(let (?n11 3)
+(let (?n12 (f0 ?n1))
+(let (?n13 (* ?n11 ?n12))
+(let (?n14 (select v4 ?n1))
+(flet ($n15 (> ?n13 ?n14))
+(flet ($n16 (xor $n10 $n15))
+(flet ($n17 false)
+(flet ($n18 (implies $n16 $n17))
+(flet ($n19 (and $n9 $n18))
+$n19
+))))))))))))))))))))
-- 
2.30.2