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

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 92cd50864d3d3b2e20fffab5752ef0329554a05c..39c2d859b28bda2c3629ef65e1a2c2136895dcac 100644 (file)
--- 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 f19291c98eb196b663dafd3970753d8cea176660..5039f826c27287873c633e36349df8783e7a734f 100644 (file)
--- 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 7cd202e53ff8bab6ce30a5066686d3194861d9ae..4edc55cca9013bc69d6a25708418e6f79aa6a7b2 100644 (file)
--- 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 1dddb5a5b1607da3355c0b8c203382c8997a9ea1..cd5f047b5965ee523a8cf34a952e499ebbf7b5c8 100644 (file)
--- 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 6897ee3c4fbf3a18d4501d86bfbb4349569aea65..b67be1263b72a34554bb89b513a1780f6a4cd421 100644 (file)
--- 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 (file)
index 0000000..4b7cf97
--- /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 (file)
index 0000000..f39262c
--- /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)