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 7ca737fa8ae7e4b733c424c9ddbb432075259109..01a2d87eb658f57bfb85142a7959e1f9540265b2 100644 (file)
--- 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 a4179b203f85c61804693d0afbb22a237ddc6d28..327a815c6153c6986fc73201d39ca95cfe786c9d 100644 (file)
--- 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 (file)
index 0000000..b8164f9
--- /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)