Fixes and improvement for IAND solver (#8771)

This fixes a model soundness bug in the non-linear solver for IAND, which was caused by the core NL model solving for an IAND term. This adds 2 delta debugged variants of a benchmark from an application.

It also improves the value-based refinement scheme for IAND significantly by ensuring we take the modulus of model values. This should make it terminating.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index b24e48644f66ee7839d1bcc67ae0c4a0007e1701..36d0e6d1166919882998c57fd10453d76ca97706 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -353,7 +353,7 @@ name   = "SMT Layer"
   help = "Do not translate bit-vectors to integers"
 [[option.mode.SUM]]
   name = "sum"
-  help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity"
+  help = "Generate a sum expression for each bvand instance, based on the value in --solve-bv-as-int-granularity"
 [[option.mode.IAND]]
   name = "iand"
   help = "Translate bvand to the iand operator (experimental)"

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index ddc0199a620f406e0a543037037c84fe05361df3..4ded5b02418e4fd5b382a42363c420656d4e3ca6 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -71,9 +71,8 @@ void IAndSolver::initLastCall(const std::vector<Node>& assertions,
     }
     size_t bsize = a.getOperator().getConst<IntAnd>().d_size;
     d_iands[bsize].push_back(a);
+    Trace("iand-mv") << "- " << a << std::endl;
   }
-
-  Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl;
 }
 
 void IAndSolver::checkInitialRefine()
@@ -231,19 +230,32 @@ Node IAndSolver::mkINot(unsigned k, Node x) const
 
 Node IAndSolver::valueBasedLemma(Node i)
 {
+  NodeManager* nm = NodeManager::currentNM();
   Assert(i.getKind() == IAND);
   Node x = i[0];
   Node y = i[1];
 
+  size_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
+  Node twok = nm->mkConstInt(Rational(Integer(2).pow(bvsize)));
   Node valX = d_model.computeConcreteModelValue(x);
   Node valY = d_model.computeConcreteModelValue(y);
+  valX = nm->mkNode(kind::INTS_MODULUS, valX, twok);
+  valY = nm->mkNode(kind::INTS_MODULUS, valY, twok);
 
-  NodeManager* nm = NodeManager::currentNM();
   Node valC = nm->mkNode(IAND, i.getOperator(), valX, valY);
   valC = rewrite(valC);
 
-  Node lem = nm->mkNode(
-      IMPLIES, nm->mkNode(AND, x.eqNode(valX), y.eqNode(valY)), i.eqNode(valC));
+  Node xm = nm->mkNode(kind::INTS_MODULUS, x, twok);
+  Node ym = nm->mkNode(kind::INTS_MODULUS, y, twok);
+
+  // (=>
+  //   (and (= (mod x 2^n) (mod c1 2^n)) (= (mod y 2^n) (mod c2 2^n)))
+  //   (= ((_ iand n) x y) rewrite(((_ iand n) (mod c1 2^n) (mod c2 2^n))))
+  // Note we use mod above since it ensures the the set of possible literals
+  // introduced is finite, since there are finitely many values mod 2^n.
+  Node lem = nm->mkNode(IMPLIES,
+                        nm->mkNode(AND, xm.eqNode(valX), ym.eqNode(valY)),
+                        i.eqNode(valC));
   return lem;
 }
 

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 55f327b3a3c0cb856c8de8b3084773383d28687e..1fbbabaab0f2c857036528c84430a091f26d649a 100644 (file)
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -212,7 +212,7 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
         {
           Kind k = cur.getKind();
           if (k != MULT && k != ADD && k != NONLINEAR_MULT
-              && !isTranscendentalKind(k))
+              && !isTranscendentalKind(k) && k != IAND && k != POW2)
           {
             // if we have not set an approximate bound for it
             if (!hasAssignment(cur))

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 7275085834eb9cd32611ae70ae610f7aa863bd80..f9264e14b4f7eb4be9601436f0d823bbaf9d8ebd 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -781,6 +781,7 @@ set(regress_0_tests
   regress0/nl/coeff-sat.smt2
   regress0/nl/combined-uf.smt2
   regress0/nl/dd.fuzz01.smtv1-to-real-idem.smt2
+  regress0/nl/dd.iand-wrong-0513-pp.smt2
   regress0/nl/iand-no-init.smt2
   regress0/nl/issue3003.smt2
   regress0/nl/issue3407.smt2
@@ -1839,6 +1840,7 @@ set(regress_1_tests
   regress1/bv/bv2nat-simp-range-sat.smt2
   regress1/bv/bv2nat-types.smt2
   regress1/bv/cmu-rdk-3.smt2
+  regress1/bv/dd.iand-wrong-0513.smt2
   regress1/bv/decision-weight00.smt2
   regress1/bv/divtest.smt2
   regress1/bv/fuzz18.smtv1.smt2

diff --git a/test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2 b/test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2
new file mode 100644 (file)
index 0000000..77b1f7f
--- /dev/null
+++ b/test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2
@@ -0,0 +1,8 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () Int)
+(declare-fun i () Int)
+(assert (= (+ 1 (- i x)) ((_ iand 2) 1 i)))
+(assert (< x 4))
+(assert (= 0 ((_ iand 2) 1 x)))
+(check-sat)

diff --git a/test/regress/cli/regress1/bv/dd.iand-wrong-0513.smt2 b/test/regress/cli/regress1/bv/dd.iand-wrong-0513.smt2
new file mode 100644 (file)
index 0000000..9077454
--- /dev/null
+++ b/test/regress/cli/regress1/bv/dd.iand-wrong-0513.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=bitwise --nl-ext-tplanes
+; EXPECT: sat
+(set-logic ALL)
+(declare-const a (_ BitVec 2))
+(declare-const R (_ BitVec 2))
+(declare-const t (_ BitVec 2))
+(declare-const x Bool)
+(assert 
+(or 
+(and (= (_ bv1 6) ((_ zero_extend 4) t)) (= ((_ zero_extend 4) a) (bvor ((_ zero_extend 4) t) ((_ zero_extend 4) R)))) 
+x))
+(assert 
+(= (_ bv0 6) (bvand ((_ zero_extend 4) a) ((_ zero_extend 4) t)))
+)
+(check-sat)