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.

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 193a55294d38164c9e11c1f250eae14ddfd2bf24..75c18076ab79dcda4643257ec7ab0768a0880b49 100644 (file)
--- 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 1b10d47f20fd7b854de62a38caa4edc6a37bf413..bd91d8ec9559229c275ce3f2ce6b79116bd6e8af 100644 (file)
--- 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 (file)
index 0000000..e6185da
--- /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)