From f051883afa31d9dbe14a5d1ae1c9700cffded3b1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Feb 2022 16:48:12 -0600 Subject: [PATCH] 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. --- src/theory/theory_model.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/nta/proj-issue460-pi-value.smt2 | 7 +++++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/nl/nta/proj-issue460-pi-value.smt2 diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 58bd32995..c8af6abcb 100644 --- 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 e2b234950..35fec0387 100644 --- 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 index 000000000..6b7c10165 --- /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)))))) -- 2.30.2