From 5eb347630fcccf038a8fae15946e35600bcc91ae Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 7 Feb 2022 12:56:34 -0800 Subject: [PATCH] Allow non-value model values (#8076) We previously required model values to be "values", i.e., constants or constant-like stuff like real algebraic numbers or lambdas. This is an inherent problem for, e.g, transcendental models: the simplest model for a transcendental problem may legitimately be 3 * PI or PI + exp(3). This PR removes this restriction, only requiring that values are rewritten. --- src/theory/theory_model_builder.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/arith/exp-in-model.smt2 | 10 ++++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/arith/exp-in-model.smt2 diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 193a55294..75c18076a 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1250,7 +1250,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) Node rc = m->getRepresentative(un[j]); Trace("model-builder-debug2") << " get rep : " << un[j] << " returned " << rc << std::endl; - Assert(TheoryModel::isValue(rc)); + Assert(rewrite(rc) == rc); children.push_back(rc); } Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1b10d47f2..bd91d8ec9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -37,6 +37,7 @@ set(regress_0_tests regress0/arith/div.04.smt2 regress0/arith/div.05.smt2 regress0/arith/div.07.smt2 + regress0/arith/exp-in-model.smt2 regress0/arith/fuzz_3-eq.smtv1.smt2 regress0/arith/incorrect1.smtv1.smt2 regress0/arith/integers/ackermann1.smt2 diff --git a/test/regress/regress0/arith/exp-in-model.smt2 b/test/regress/regress0/arith/exp-in-model.smt2 new file mode 100644 index 000000000..e6185da09 --- /dev/null +++ b/test/regress/regress0/arith/exp-in-model.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --check-model +; EXPECT: (error "Cannot run check-model on a model with approximate values.") +; EXIT: 1 +(set-logic QF_UFNRAT) +(set-option :produce-models true) +(declare-fun b (Real) Real) +(declare-fun v () Real) +(assert (distinct 0 (* v v))) +(assert (= 0.0 (b (exp 1.0)))) +(check-sat) -- 2.30.2