Consider PI to be a model value (#8176)

Fixes cvc5/cvc5-projects#460.

The special case is necessary due to the node representation of nullary operators, which uses variables internally to represent operators. The other nullary operators are not model values.

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 58bd3299503c6dbc2e47d694040b8ccac7ab6505..c8af6abcbcc36405266def0c9bfbe80896533fd2 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -784,7 +784,7 @@ bool TheoryModel::isBaseModelValue(TNode n) const
   }
   Kind k = n.getKind();
   if (k == kind::REAL_ALGEBRAIC_NUMBER || k == kind::LAMBDA
-      || k == kind::WITNESS)
+      || k == kind::WITNESS || k == kind::PI)
   {
     // we are a value if we are one of the above kinds
     return true;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e2b234950a652605d9783f68fc546353b6f643c3..35fec03874548166bde27c16cbe83bc7e1ed3c10 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -792,6 +792,7 @@ set(regress_0_tests
   regress0/nl/nta/issue7938-tf-model.smt2
   regress0/nl/nta/issue8147-unc-model.smt2
   regress0/nl/nta/issue8160-model-purify.smt2
+  regress0/nl/nta/proj-issue460-pi-value.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/proj-issue460-pi-value.smt2 b/test/regress/regress0/nl/nta/proj-issue460-pi-value.smt2
new file mode 100644 (file)
index 0000000..6b7c101
--- /dev/null
+++ b/test/regress/regress0/nl/nta/proj-issue460-pi-value.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(set-option :global-declarations true)
+(set-option :sets-ext true)
+(check-sat-assuming ( (let ((_let0 real.pi))(set.member (- _let0) (set.complement (set.singleton _let0))))))