From 328eeb2a34d333b05b60a7177a2eedffb4d17455 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 7 Feb 2022 15:14:36 -0600 Subject: [PATCH] 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. --- src/theory/arith/nl/iand_solver.cpp | 16 ++++++++++------ src/theory/arith/theory_arith_private.cpp | 8 +++++--- test/regress/CMakeLists.txt | 1 + .../regress1/nl/issue5461-iand-init-refine.smt2 | 10 ++++++++++ 4 files changed, 26 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress1/nl/issue5461-iand-init-refine.smt2 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().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 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) -- 2.30.2