From 019be6360c21a4899debbcc4e2615be2fbe08974 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 31 Mar 2022 01:44:49 +0200 Subject: [PATCH] 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. --- src/theory/theory_model_builder.cpp | 30 +++++++++++++------ test/regress/cli/CMakeLists.txt | 1 + .../regress0/nl/issue8414-ran-rational.smt2 | 12 ++++++++ 3 files changed, 34 insertions(+), 9 deletions(-) create mode 100644 test/regress/cli/regress0/nl/issue8414-ran-rational.smt2 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()) + { + 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) -- 2.30.2