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 f2a4aa2e3ef6170c4b5405281fbc07a7ffbf15f7..48d974bce1e545337d04a9d26038e0137affde09 100644 (file)
--- 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 c8af6abcbcc36405266def0c9bfbe80896533fd2..37ceccbc2bf8df60e9ab20e76f554a6a5436ab44 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::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 0d646392fbda78b2378b70ac8d8216c76e817839..9119708712ddb78fe7c2ccf23fa01fedb7995d51 100644 (file)
--- 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 (file)
index 0000000..40fa615
--- /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)