From 8fe459b1fb3843ebdbda86f24a414c46b986aa90 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 15:35:13 -0500 Subject: [PATCH] Fix issue related to sanity checking integer models (#7363) We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat". This also changes an assertion to warning, to allow the regression to pass. Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks). As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252. --- src/theory/arith/theory_arith.cpp | 23 +++++++++++-------- test/regress/CMakeLists.txt | 3 +++ .../arith/issue6774-sanity-int-model.smt2 | 21 +++++++++++++++++ .../arith/issue7252-arith-sanity.smt2 | 14 +++++++++++ .../cores/issue6988-arith-sanity.smt2 | 18 +++++++++++++++ 5 files changed, 69 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress1/arith/issue6774-sanity-int-model.smt2 create mode 100644 test/regress/regress1/arith/issue7252-arith-sanity.smt2 create mode 100644 test/regress/regress1/cores/issue6988-arith-sanity.smt2 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 76a0c363d..cf2373b9f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level) if (Theory::fullEffort(level)) { d_arithModelCache.clear(); + std::set termSet; if (d_nonlinearExtension != nullptr) { - std::set termSet; updateModelCache(termSet); d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet); } @@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level) // set incomplete d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED); } + // If we won't be doing a last call effort check (which implies that + // models will be computed), we must sanity check the integer model + // from the linear solver now. We also must update the model cache + // if we did not do so above. + if (d_nonlinearExtension == nullptr) + { + updateModelCache(termSet); + } + sanityCheckIntegerModel(); } } @@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m, updateModelCache(termSet); - if (sanityCheckIntegerModel()) - { - // We added a lemma - return false; - } - // We are now ready to assert the model. for (const std::pair& p : d_arithModelCache) { @@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel() Trace("arith-check") << p.first << " -> " << p.second << std::endl; if (p.first.getType().isInteger() && !p.second.getType().isInteger()) { - Assert(false) << "TheoryArithPrivate generated a bad model value for " - "integer variable " - << p.first << " : " << p.second; + Warning() << "TheoryArithPrivate generated a bad model value for " + "integer variable " + << p.first << " : " << p.second; // must branch and bound TrustNode lem = d_bab.branchIntegerVariable(p.first, p.second.getConst()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b1d776b21..84f0ef408 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1505,6 +1505,8 @@ set(regress_1_tests regress1/arith/issue3952-rew-eq.smt2 regress1/arith/issue4985-model-success.smt2 regress1/arith/issue4985b-model-success.smt2 + regress1/arith/issue6774-sanity-int-model.smt2 + regress1/arith/issue7252-arith-sanity.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc.smt2 regress1/arith/mod.02.smt2 @@ -1576,6 +1578,7 @@ set(regress_1_tests regress1/constarr3.cvc.smt2 regress1/constarr3.smt2 regress1/cores/issue5604.smt2 + regress1/cores/issue6988-arith-sanity.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 diff --git a/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 new file mode 100644 index 000000000..732b709f9 --- /dev/null +++ b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic ALIRA) +(declare-const x Real) +(declare-fun i () Int) +(declare-fun i1 () Int) +(push) +(assert (< 1 (- i))) +(check-sat) +(pop) +(push) +(assert (or (>= i1 (* 5 (- i))))) +(check-sat) +(pop) +(assert (or (> i1 1) (= x (to_real i)))) +(check-sat) +(assert (not (is_int x))) +(check-sat) diff --git a/test/regress/regress1/arith/issue7252-arith-sanity.smt2 b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 new file mode 100644 index 000000000..dd7a1fa2e --- /dev/null +++ b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(declare-fun e () Int) +(declare-fun f () Int) +(declare-fun g () Int) +(assert (> 0 (* a (mod 0 b)))) +(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0))) +(check-sat) diff --git a/test/regress/regress1/cores/issue6988-arith-sanity.smt2 b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 new file mode 100644 index 000000000..622d64375 --- /dev/null +++ b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +(set-logic ANIA) +(declare-const x Bool) +(set-option :produce-unsat-cores true) +(declare-fun i () Int) +(declare-fun i5 () Int) +(declare-fun i8 () Int) +(assert (or x (< i5 0))) +(push) +(assert (and (= i8 1) (= i5 (+ 1 i)) (= i8 (+ 1 i)))) +(push) +(check-sat) +(pop) +(pop) +(assert (= i8 (* i8 3 (+ i8 1)))) +(check-sat) -- 2.30.2