From: Andrew Reynolds Date: Mon, 15 Mar 2021 19:08:03 +0000 (-0500) Subject: Make nonlinear extension account for relevant term set (#6147) X-Git-Tag: cvc5-1.0.0~2077 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=216f3c9fb07a08909942b91a2a4739cd178f5a72;p=cvc5.git Make nonlinear extension account for relevant term set (#6147) This fixes a subtle issue with non-linear and theory combination. It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination. In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF. Fixes #5662. --- diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 671c3f44a..25aebf6d4 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -301,7 +301,7 @@ void NonlinearExtension::check(Theory::Effort e) } } -bool NonlinearExtension::modelBasedRefinement() +bool NonlinearExtension::modelBasedRefinement(const std::set& termSet) { ++(d_stats.d_mbrRuns); d_checkCounter++; @@ -317,8 +317,18 @@ bool NonlinearExtension::modelBasedRefinement() Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl; // get the extended terms belonging to this theory + std::vector xtsAll; + d_extTheory.getTerms(xtsAll); + // only consider those that are currently relevant based on the current + // assertions, i.e. those contained in termSet std::vector xts; - d_extTheory.getTerms(xts); + for (const Node& x : xtsAll) + { + if (termSet.find(x) != termSet.end()) + { + xts.push_back(x); + } + } if (Trace.isOn("nl-ext-debug")) { @@ -496,7 +506,8 @@ bool NonlinearExtension::modelBasedRefinement() return false; } -void NonlinearExtension::interceptModel(std::map& arithModel) +void NonlinearExtension::interceptModel(std::map& arithModel, + const std::set& termSet) { if (!needsCheckLastEffort()) { @@ -509,7 +520,7 @@ void NonlinearExtension::interceptModel(std::map& arithModel) if (!d_builtModel.get()) { Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; - modelBasedRefinement(); + modelBasedRefinement(termSet); } if (d_builtModel.get()) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index baa0f886c..09e3a8370 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -128,7 +128,8 @@ class NonlinearExtension * arithModel so that it satisfies certain nonlinear constraints. This may * involve e.g. solving for variables in nonlinear equations. */ - void interceptModel(std::map& arithModel); + void interceptModel(std::map& arithModel, + const std::set& termSet); /** Does this class need a call to check(...) at last call effort? */ bool needsCheckLastEffort() const { return d_needsLastCall; } /** presolve @@ -158,7 +159,7 @@ class NonlinearExtension * may have information regarding how to construct a model, in the case that * we determined the problem is satisfiable. */ - bool modelBasedRefinement(); + bool modelBasedRefinement(const std::set& termSet); /** get assertions * diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 83337dd90..36b2d3eb8 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -248,7 +248,7 @@ bool TheoryArith::collectModelValues(TheoryModel* m, { // Non-linear may repair values to satisfy non-linear constraints (see // documentation for NonlinearExtension::interceptModel). - d_nonlinearExtension->interceptModel(arithModel); + d_nonlinearExtension->interceptModel(arithModel, termSet); } // We are now ready to assert the model. for (const std::pair& p : arithModel) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 30cdf43d9..5c28a34cc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1596,6 +1596,8 @@ set(regress_1_tests regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 + regress1/nl/issue5662-nl-tc.smt2 + regress1/nl/issue5662-nl-tc-min.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 regress1/nl/metitarski_3_4_2e.smt2 diff --git a/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 new file mode 100644 index 000000000..0e7279ef9 --- /dev/null +++ b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 @@ -0,0 +1,16 @@ +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun j () Real) +(declare-fun k () Real) +(declare-fun h () Real) +(assert (< 0 k)) +(assert (= 1 (* k j))) +(assert + (or + (= h 0) + (= 0.0 (* a k)) + ) +) +(assert (distinct a h)) +(check-sat) diff --git a/test/regress/regress1/nl/issue5662-nl-tc.smt2 b/test/regress/regress1/nl/issue5662-nl-tc.smt2 new file mode 100644 index 000000000..d805b721d --- /dev/null +++ b/test/regress/regress1/nl/issue5662-nl-tc.smt2 @@ -0,0 +1,17 @@ +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) +(declare-fun j () Real) +(declare-fun e () Real) +(declare-fun f () Real) +(declare-fun k () Real) +(declare-fun g () Real) +(declare-fun h () Real) +(assert (forall ((i Real)) (xor (and (or (and (or (and (or (and (or + (and (> 0.0 (* a e) (* c e)) (>= 0 k)) (<= g 0)) (= (* b j) + 2.0))))) (> f k)) (>= 0.0 k))) (>= 0 k)))) +(assert (distinct a (* d h))) +(check-sat)