Stopping non-linear terms from entering the dio solver. Fixes bug 547.

4 files changed, 29 insertions, 0 deletions

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.