From cca221de7d29e86fd770af3aca0efc0d877dff26 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 19 Feb 2014 15:50:07 -0500
Subject: [PATCH] Stopping non-linear terms from entering the dio solver. Fixes
 bug 547.

---
 src/theory/arith/dio_solver.cpp           |  4 ++++
 src/theory/arith/dio_solver.h             |  2 ++
 src/theory/arith/normal_form.cpp          | 11 +++++++++++
 src/theory/arith/normal_form.h            | 12 ++++++++++++
 test/regress/regress0/arith/Makefile.am   |  4 +++-
 test/regress/regress0/arith/bug547.1.smt2 |  8 ++++++++
 test/regress/regress0/arith/bug547.2.smt2 |  9 +++++++++
 7 files changed, 49 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/arith/bug547.1.smt2
 create mode 100644 test/regress/regress0/arith/bug547.2.smt2

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 92cd50864..39c2d859b 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -141,6 +141,10 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
   Assert(eq.getNode().getKind() == kind::EQUAL);
 
   SumPair sp = eq.toSumPair();
+  if(sp.isNonlinear()){
+    return;
+  }
+
   uint32_t length = sp.maxLength();
   if(length > d_maxInputCoefficientLength){
     d_maxInputCoefficientLength = length;
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index f19291c98..5039f826c 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -191,6 +191,8 @@ public:
    * orig can either be of the form (= p c) or (and ub lb).
    * where ub is either (leq p c) or (not (> p [- c 1])), and
    * where lb is either (geq p c) or (not (< p [+ c 1]))
+   *
+   * If eq cannot be used, this constraint is dropped.
    */
   void pushInputConstraint(const Comparison& eq, Node reason);
 
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 7cd202e53..4edc55cca 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -1084,6 +1084,17 @@ Node Polynomial::makeAbsCondition(Variable v, Polynomial p){
   return absCnd;
 }
 
+bool Polynomial::isNonlinear() const {
+
+  for(iterator i=begin(), iend =end(); i != iend; ++i){
+    Monomial m = *i;
+    if(m.isNonlinear()){
+      return true;
+    }
+  }
+  return false;
+}
+
 } //namespace arith
 } //namespace theory
 } //namespace CVC4
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 1dddb5a5b..cd5f047b5 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -708,6 +708,11 @@ public:
     return integralCoefficient() && integralVariables();
   }
 
+  /** Returns true if the VarList is a product of at least 2 Variables.*/
+  bool isNonlinear() const {
+    return getVarList().size() >= 2;
+  }
+
   /**
    * Given a sorted list of monomials, this function transforms this
    * into a strictly sorted list of monomials that does not contain zero.
@@ -933,6 +938,9 @@ public:
     return true;
   }
 
+  /** Returns true if the polynomial contains a non-linear monomial.*/
+  bool isNonlinear() const;
+
   /**
    * Selects a minimal monomial in the polynomial by the absolute value of
    * the coefficient.
@@ -1165,6 +1173,10 @@ public:
     return getConstant().isZero() && isConstant();
   }
 
+  bool isNonlinear() const{
+    return getPolynomial().isNonlinear();
+  }
+
   /**
    * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
    * The SumPair must be integral.
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 6897ee3c4..b67be1263 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -45,7 +45,9 @@ TESTS =	\
 	miplib2.cvc \
 	miplib3.cvc \
 	miplib4.cvc \
-	miplibtrick.smt
+	miplibtrick.smt \
+	bug547.1.smt2 \
+	bug547.2.smt2
 #	problem__003.smt2
 
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/arith/bug547.1.smt2 b/test/regress/regress0/arith/bug547.1.smt2
new file mode 100644
index 000000000..4b7cf9780
--- /dev/null
+++ b/test/regress/regress0/arith/bug547.1.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --rewrite-divk
+; EXPECT: unknown
+(set-logic QF_NIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (= 1 (mod (* x y) 3)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/arith/bug547.2.smt2 b/test/regress/regress0/arith/bug547.2.smt2
new file mode 100644
index 000000000..f39262c08
--- /dev/null
+++ b/test/regress/regress0/arith/bug547.2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --rewrite-divk
+; EXPECT: unknown
+(set-logic QF_NIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(assert (= (+ (* z 2) 1) (* x y)))
+(check-sat)
+(exit)
-- 
2.30.2