From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Feb 2022 21:14:36 +0000 (-0600)
Subject: Fix unsoundness in IAND solver (#8053)
X-Git-Tag: cvc5-1.0.0~443
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=328eeb2a34d333b05b60a7177a2eedffb4d17455;p=cvc5.git

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 dc6b9c9d7..27bb70fe0 100644
--- 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 6545ef923..a4864c4e4 100644
--- 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 bd91d8ec9..40414a89c 100644
--- 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
index 000000000..aed8cb89f
--- /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)