From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 28 Feb 2022 22:37:08 +0000 (-0600)
Subject: Fix special casing for PI in model value (#8189)
X-Git-Tag: cvc5-1.0.0~361
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa9d296d9b11814df62675bf8fa93c5f7e5da90e;p=cvc5.git

Fix special casing for PI in model value (#8189)

PI should be considered a model value but not a "base" model value. This avoid spurious debug assertion failures, which are now treated as warnings. This makes a difference when another theory e.g. UF says that PI is currently equal to a constant value c. Since our lemma schemas are model-based, we may require building a spurious model where PI is c, and refine afterwards.

This also fixes a bug in our extended function rewriting which would mistakenly think that PI was reduced, and hence skip a full effort check if PI was the only extended function in the current context. This was previously causing a final model to be one where PI = 0.0.

Fixes #8183.
---

diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index f2a4aa2e3..48d974bce 100644
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -129,7 +129,7 @@ bool NlExtTheoryCallback::isExtfReduced(
       }
     }
   }
-  return true;
+  return false;
 }
 
 }  // namespace nl
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c8af6abcb..37ceccbc2 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::PI)
+      || k == kind::WITNESS)
   {
     // we are a value if we are one of the above kinds
     return true;
@@ -826,8 +826,17 @@ bool TheoryModel::isValue(TNode n) const
         finishedComputing = true;
         currentReturn = true;
       }
-      else if (cur.getNumChildren() == 0 || rewrite(cur) != cur)
+      else if (cur.getNumChildren() == 0)
       {
+        // PI is a (non-base) value. We require it as a special case here
+        // since nullary operators are represented internal as variables.
+        // All other non-constant terms with zero children are not values.
+        finishedComputing = true;
+        currentReturn = (cur.getKind() == kind::PI);
+      }
+      else if (rewrite(cur) != cur)
+      {
+        // non-rewritten terms are never model values
         finishedComputing = true;
         currentReturn = false;
       }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0d646392f..911970871 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -794,6 +794,7 @@ set(regress_0_tests
   regress0/nl/nta/issue8160-model-purify.smt2
   regress0/nl/nta/issue8182-exact-mv-keep.smt2
   regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
+  regress0/nl/nta/issue8183-tc-pi.smt2
   regress0/nl/nta/proj-issue460-pi-value.smt2
   regress0/nl/nta/real-pi.smt2
   regress0/nl/nta/sin-sym.smt2
diff --git a/test/regress/regress0/nl/nta/issue8183-tc-pi.smt2 b/test/regress/regress0/nl/nta/issue8183-tc-pi.smt2
new file mode 100644
index 000000000..40fa6154f
--- /dev/null
+++ b/test/regress/regress0/nl/nta/issue8183-tc-pi.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun v () Real)
+(declare-fun a () (Array Real Real))
+(assert (exists ((V Real)) (or (and (= 0 (/ 0 v)) (< 0 (/ 0 v))) (= 1.0 (select (store a (/ (+ 0.0 real.pi) 0.0) 0.0) 0.0)))))
+(check-sat)