From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 30 Mar 2022 23:44:49 +0000 (+0200)
Subject: Allow for multiple (equal) base model values (#8467)
X-Git-Tag: cvc5-1.0.0~113
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=019be6360c21a4899debbcc4e2615be2fbe08974;p=cvc5.git

Allow for multiple (equal) base model values (#8467)

This PR weakens an assertion about multiple model values in the same equivalence class. We now accept multiple base model values in the same equivalence class, as long as they compare equal. This allows to gracefully handle cases where real algebraic numbers fail to realize that they are rational.
Fixes #8414.
---

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 7ca737fa8..01a2d87eb 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -513,12 +513,16 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
         // higher-order.
         if (tm->isValue(n))
         {
-          // In rare cases, it could be that multiple terms in the same
-          // equivalence class are considered values. We prefer the one that is
-          // a "base" model value (e.g. a constant) here. We throw a warning
-          // if there are 2 model values in the same equivalence class, and
-          // a debug failure if there are 2 base values in the same equivalence
-          // class.
+          // In some cases, there can be multiple terms in the same equivalence
+          // class are considered values, e.g., when real algebraic numbers did
+          // not simplify to rational values or real.pi was used as a model
+          // value. We distinguish three kinds of model values: constants,
+          // non-constant base values and non-base values, and we use them in
+          // this order of preference.
+          // We print a trace message if there is more than one model value in
+          // the same equivalence class. We throw a debug failure if there are
+          // at least two base model values in the same equivalence class that
+          // do not compare equal.
           bool assignConstRep = false;
           bool isBaseValue = tm->isBaseModelValue(n);
           if (constRep.isNull())
@@ -538,9 +542,17 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             }
             else if (isBaseValue)
             {
-              Assert(false)
-                  << "Base model values in the same equivalence class "
-                  << constRep << " " << n << std::endl;
+              Node isEqual = rewrite(constRep.eqNode(n));
+              if (isEqual.isConst() && isEqual.getConst<bool>())
+              {
+                assignConstRep = n.isConst();
+              }
+              else
+              {
+                Assert(false) << "Distinct base model values in the same "
+                                 "equivalence class "
+                              << constRep << " " << n << std::endl;
+              }
             }
           }
           if (assignConstRep)
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index a4179b203..327a815c6 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -795,6 +795,7 @@ set(regress_0_tests
   regress0/nl/issue8135-icp-candidates.smt2
   regress0/nl/issue8161-var-elim.smt2
   regress0/nl/issue8226-ran-refinement.smt2
+  regress0/nl/issue8414-ran-rational.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
diff --git a/test/regress/cli/regress0/nl/issue8414-ran-rational.smt2 b/test/regress/cli/regress0/nl/issue8414-ran-rational.smt2
new file mode 100644
index 000000000..b8164f969
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8414-ran-rational.smt2
@@ -0,0 +1,12 @@
+; EXPECT: sat
+;; only triggers with UFNRA (instead of QF_UFNRA)
+(set-logic UFNRA)
+(declare-fun r2 () Real)
+(declare-fun r5 () Real)
+(declare-fun r () Real)
+(declare-fun b (Bool) Real)
+(declare-fun u (Real) Real)
+(declare-fun r9 () Real)
+(assert (= r2 (u (+ 0.2 r2))))
+(assert (= (= 0.0 (+ r2 3.2 r)) (= 1.0 (+ (u r5) (- r9 (b (= (* r r5) (+ 3 r))))))))
+(check-sat)