Fix unsoundness in IAND solver (#8053)

Fixes #5461, fixes #8063. The initial lemma schema was assuming arguments were in bounds.

This also modifies the solver so that we throw logic exceptions when encountering iand or transcendentals.

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index dc6b9c9d77b09c9d9580e118519324a4f07fd3c4..27bb70fe0208f450f4abeab2886e1864bbdc0c17 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -93,6 +93,10 @@ void IAndSolver::checkInitialRefine()
       }
       d_initRefine.insert(i);
       Node op = i.getOperator();
+      size_t bsize = op.getConst<IntAnd>().d_size;
+      Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
+      Node arg0Mod = nm->mkNode(kind::INTS_MODULUS, i[0], twok);
+      Node arg1Mod = nm->mkNode(kind::INTS_MODULUS, i[1], twok);
       // initial refinement lemmas
       std::vector<Node> conj;
       // iand(x,y)=iand(y,x) is guaranteed by rewriting
@@ -101,12 +105,12 @@ void IAndSolver::checkInitialRefine()
       // 0 <= iand(x,y) < 2^k
       conj.push_back(nm->mkNode(LEQ, d_zero, i));
       conj.push_back(nm->mkNode(LT, i, rewrite(d_iandUtils.twoToK(k))));
-      // iand(x,y)<=x
-      conj.push_back(nm->mkNode(LEQ, i, i[0]));
-      // iand(x,y)<=y
-      conj.push_back(nm->mkNode(LEQ, i, i[1]));
-      // x=y => iand(x,y)=x
-      conj.push_back(nm->mkNode(IMPLIES, i[0].eqNode(i[1]), i.eqNode(i[0])));
+      // iand(x,y)<=mod(x, 2^k)
+      conj.push_back(nm->mkNode(LEQ, i, arg0Mod));
+      // iand(x,y)<=mod(y, 2^k)
+      conj.push_back(nm->mkNode(LEQ, i, arg1Mod));
+      // x=y => iand(x,y)=mod(x, 2^k)
+      conj.push_back(nm->mkNode(IMPLIES, i[0].eqNode(i[1]), i.eqNode(arg0Mod)));
       Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
       Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
                           << std::endl;

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 6545ef923e3b56601db4957f12baaf0ca5cd292e..a4864c4e43575b16511abc552c4665a1a82c6d18 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1254,11 +1254,13 @@ void TheoryArithPrivate::releaseArithVar(ArithVar v){
 
 ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool aux, bool internal){
   //TODO : The VarList trick is good enough?
-  Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == ADD || internal);
-  if (logicInfo().isLinear() && Variable::isDivMember(x))
+  Kind xk = x.getKind();
+  Assert(isLeaf(x) || VarList::isMember(x) || xk == ADD || internal);
+  if (logicInfo().isLinear()
+      && (Variable::isDivMember(x) || xk == IAND || isTranscendentalKind(xk)))
   {
     stringstream ss;
-    ss << "A non-linear fact (involving div/mod/divisibility) was asserted to "
+    ss << "A non-linear fact was asserted to "
           "arithmetic in a linear logic: "
        << x << std::endl;
     throw LogicException(ss.str());

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bd91d8ec9559229c275ce3f2ce6b79116bd6e8af..40414a89c2cc18f3d8490018b004ae9bdbee8b8a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1878,6 +1878,7 @@ set(regress_1_tests
   regress1/nl/issue3966-conf-coeff.smt2
   regress1/nl/issue4791-llr.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
+  regress1/nl/issue5461-iand-init-refine.smt2
   regress1/nl/issue5660-mb-success.smt2
   regress1/nl/issue5662-nl-tc.smt2
   regress1/nl/issue5662-nl-tc-min.smt2

diff --git a/test/regress/regress1/nl/issue5461-iand-init-refine.smt2 b/test/regress/regress1/nl/issue5461-iand-init-refine.smt2
new file mode 100644 (file)
index 0000000..aed8cb8
--- /dev/null
+++ b/test/regress/regress1/nl/issue5461-iand-init-refine.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --nl-ext-tplanes
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (< x 0))
+(assert (= (* x x) 16))
+(assert (= x y))
+(assert (> ((_ iand 4) x y) 0))
+(check-sat)