From ead6d41a4cbfd0d99a80201cd1197943c63428ee Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 May 2022 13:52:59 -0500 Subject: [PATCH] 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. --- src/options/smt_options.toml | 2 +- src/theory/arith/nl/iand_solver.cpp | 22 ++++++++++++++----- src/theory/arith/nl/nl_model.cpp | 2 +- test/regress/cli/CMakeLists.txt | 2 ++ .../regress0/nl/dd.iand-wrong-0513-pp.smt2 | 8 +++++++ .../cli/regress1/bv/dd.iand-wrong-0513.smt2 | 15 +++++++++++++ 6 files changed, 44 insertions(+), 7 deletions(-) create mode 100644 test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2 create mode 100644 test/regress/cli/regress1/bv/dd.iand-wrong-0513.smt2 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index b24e48644..36d0e6d11 100644 --- 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 ddc0199a6..4ded5b024 100644 --- 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& assertions, } size_t bsize = a.getOperator().getConst().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().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 55f327b3a..1fbbabaab 100644 --- 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& 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 727508583..f9264e14b 100644 --- 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 index 000000000..77b1f7ff3 --- /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 index 000000000..907745453 --- /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) -- 2.30.2