From b8b52b5cfa2fbfcb6d3450b9e03b2fa680af605d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Feb 2022 17:56:33 -0600 Subject: [PATCH] Ensure variables are constrained in model when equal to transcendental function apps (#8153) Fixes #8147. --- src/smt/check_models.cpp | 7 ----- .../transcendental/transcendental_solver.cpp | 28 +++++++++++-------- .../nl/transcendental/transcendental_solver.h | 11 ++++++-- test/regress/CMakeLists.txt | 1 + .../regress0/nl/nta/issue8147-unc-model.smt2 | 8 ++++++ 5 files changed, 35 insertions(+), 20 deletions(-) create mode 100644 test/regress/regress0/nl/nta/issue8147-unc-model.smt2 diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index f3393caae..5a410ba2d 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -41,13 +41,6 @@ void CheckModels::checkModel(TheoryModel* m, // If this function is running, the user gave --check-model (or equivalent), // and if verbose(1) is on, the user gave --verbose (or equivalent). - // check-model is not guaranteed to succeed if approximate values were used. - // Thus, we intentionally abort here. - if (m->hasApproximations()) - { - throw RecoverableModalException( - "Cannot run check-model on a model with approximate values."); - } Node sepHeap, sepNeq; if (m->getHeapModel(sepHeap, sepNeq)) { diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 6a254fc54..c394512d1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -455,13 +455,15 @@ void TranscendentalSolver::postProcessModel(std::map& arithModel, const std::set& termSet) { Trace("nl-ext") << "TranscendentalSolver::postProcessModel" << std::endl; - std::unordered_set trReps; + // map from equivalence classes to a transcendental function application, + // if it exists. + std::unordered_map trReps; for (const Node& n : termSet) { if (isTranscendentalKind(n.getKind())) { Node r = d_astate.getRepresentative(n); - trReps.insert(r); + trReps[r] = n; } } if (trReps.empty()) @@ -469,25 +471,29 @@ void TranscendentalSolver::postProcessModel(std::map& arithModel, Trace("nl-ext") << "...no transcendental functions" << std::endl; return; } - std::vector rmFromModel; + std::unordered_map::iterator it; for (auto& am : arithModel) { + // skip integer variables + if (am.first.getType().isInteger()) + { + continue; + } Node r = d_astate.getRepresentative(am.first); - if (trReps.find(r) != trReps.end()) + it = trReps.find(r); + // if it is in the same equivalence class as a trancendental function + // application, we replace its value in the model with that application + if (it != trReps.end()) { - Trace("nl-ext") << "...erase value for " << am.first - << ", since approximate" << std::endl; - rmFromModel.push_back(am.first); + Trace("nl-ext") << "...abstract value for " << am.first << " to " + << it->second << std::endl; + am.second = it->second; } else { Trace("nl-ext") << "...keep model value for " << am.first << std::endl; } } - for (const Node& n : rmFromModel) - { - arithModel.erase(n); - } } } // namespace transcendental diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index f8c7b8c9b..413d4535f 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -153,9 +153,16 @@ class TranscendentalSolver : protected EnvObj void checkTranscendentalTangentPlanes(); /** - * Post-process model. This ensures that the domain of arithModel does not - * contain terms that are equal to any transcendental function applications, + * Post-process model. This ensures that for all terms t in the domain of + * arithModel, if t is in the same equivalence class as a transcendental + * function application, then arithModel[t] maps to one such application. + * + * This is to ensure that the linear model is ignored for such terms, * as their values cannot be properly represented in the model. + * + * It is important to map such terms t to a transcendental function + * application, or otherwise they would be unconstrained, leading to + * spurious models. */ void postProcessModel(std::map& arithModel, const std::set& termSet); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b28651d95..71219634b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -789,6 +789,7 @@ set(regress_0_tests regress0/nl/nta/exp-n0.5-ub.smt2 regress0/nl/nta/exp-neg2-unsat-unsound.smt2 regress0/nl/nta/exp1-ub.smt2 + regress0/nl/nta/issue8147-unc-model.smt2 regress0/nl/nta/real-pi.smt2 regress0/nl/nta/sin-sym.smt2 regress0/nl/nta/sqrt-simple.smt2 diff --git a/test/regress/regress0/nl/nta/issue8147-unc-model.smt2 b/test/regress/regress0/nl/nta/issue8147-unc-model.smt2 new file mode 100644 index 000000000..1acdab13b --- /dev/null +++ b/test/regress/regress0/nl/nta/issue8147-unc-model.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-const x Bool) +(declare-fun a () Real) +(declare-fun r () Real) +(declare-fun v () Real) +(assert (and (xor (= a 1.0) x) (= 1 (- v (exp (* r v)))))) +(check-sat) -- 2.30.2