From c7e68b150858560656ee2fd557cd8358842b03c9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 24 Feb 2022 17:33:23 -0600 Subject: [PATCH] Make model builder robust to multiple value-like terms in the same equivalence class (#8150) This changes our policy on handling when two value-like terms are in the same equivalence class. We now give preference to the "base" model value, and either warn or throw a debug exception. After f7675b2, we can have the situation where e.g. (seq.nth seq.empty 1) is in the same equivalence class as a constant, where (seq.nth seq.empty 1) is considered value-like, despite being unevaluatable. We now ensure that the constant is taken as the representative of the equivalence class, and not this term. It also removes assignable terms from consideration when assigning values to equivalence classes. In particular, (seq.nth seq.empty 1) is skipped, so a warning is not even given when the above occurs. Fixes #8148. --- src/theory/theory_model_builder.cpp | 91 +++++++++++++------ test/regress/CMakeLists.txt | 2 + .../regress1/seq/issue8148-2-const-mv.smt2 | 6 ++ .../regress1/seq/issue8148-const-mv.smt2 | 9 ++ 4 files changed, 79 insertions(+), 29 deletions(-) create mode 100644 test/regress/regress1/seq/issue8148-2-const-mv.smt2 create mode 100644 test/regress/regress1/seq/issue8148-const-mv.smt2 diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 03cdaa786..fc1d5ee9e 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -458,6 +458,8 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // The assigned represenative and constant representative Node rep, constRep; + // is constant rep a "base model value" (see TheoryModel::isBaseModelValue) + bool constRepBaseModelValue = false; // A flag set to true if the current equivalence class is assignable (see // assignableEqc). bool assignable = false; @@ -499,38 +501,69 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // model-specific processing of the term tm->addTermInternal(n); - // (2) Record constant representative or assign representative, if - // applicable. We check if n is a value here, e.g. a term for which - // isConst returns true, or a lambda. The latter is required only for - // higher-order. - if (tm->isValue(n)) + // compute whether n is assignable + if (!isAssignable(n)) { - Assert(constRep.isNull()); - constRep = n; - Trace("model-builder") - << " ..ConstRep( " << eqc << " ) = " << constRep << std::endl; - // if we have a constant representative, nothing else matters - continue; - } + // (2) Record constant representative or assign representative, if + // applicable. We check if n is a value here, e.g. a term for which + // isConst returns true, or a lambda. The latter is required only for + // 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. + bool assignConstRep = false; + bool isBaseValue = tm->isBaseModelValue(n); + if (constRep.isNull()) + { + assignConstRep = true; + } + else + { + warning() << "Model values in the same equivalence class " + << constRep << " " << n << std::endl; + if (!constRepBaseModelValue) + { + assignConstRep = isBaseValue; + } + else if (isBaseValue) + { + Assert(false) + << "Base model values in the same equivalence class " + << constRep << " " << n << std::endl; + } + } + if (assignConstRep) + { + constRep = n; + Trace("model-builder") << " ..ConstRep( " << eqc + << " ) = " << constRep << std::endl; + constRepBaseModelValue = isBaseValue; + } + // if we have a constant representative, nothing else matters + continue; + } - // If we don't have a constant rep, check if this is an assigned rep. - itm = tm->d_reps.find(n); - if (itm != tm->d_reps.end()) - { - // Notice that this equivalence class may contain multiple terms that - // were specified as being a representative, since e.g. datatypes may - // assert representative for two constructor terms that are not in the - // care graph and are merged during collectModeInfo due to equality - // information from another theory. We overwrite the value of rep in - // these cases here. - rep = itm->second; - Trace("model-builder") - << " ..Rep( " << eqc << " ) = " << rep << std::endl; - } + // If we don't have a constant rep, check if this is an assigned rep. + itm = tm->d_reps.find(n); + if (itm != tm->d_reps.end()) + { + // Notice that this equivalence class may contain multiple terms that + // were specified as being a representative, since e.g. datatypes may + // assert representative for two constructor terms that are not in the + // care graph and are merged during collectModeInfo due to equality + // information from another theory. We overwrite the value of rep in + // these cases here. + rep = itm->second; + Trace("model-builder") + << " ..Rep( " << eqc << " ) = " << rep << std::endl; + } - // (3) Finally, process assignable information - if (!isAssignable(n)) - { + // (3) Finally, process assignable information evaluable = true; // expressions that are not assignable should not be given assignment // exclusion sets diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5f299152f..b28651d95 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2265,6 +2265,8 @@ set(regress_1_tests regress1/sep/wand-simp-sat.smt2 regress1/sep/wand-simp-sat2.smt2 regress1/sep/wand-simp-unsat.smt2 + regress1/seq/issue8148-2-const-mv.smt2 + regress1/seq/issue8148-const-mv.smt2 regress1/sets/choose.cvc.smt2 regress1/sets/choose1.smt2 regress1/sets/choose2.smt2 diff --git a/test/regress/regress1/seq/issue8148-2-const-mv.smt2 b/test/regress/regress1/seq/issue8148-2-const-mv.smt2 new file mode 100644 index 000000000..7ef7f93db --- /dev/null +++ b/test/regress/regress1/seq/issue8148-2-const-mv.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(assert (forall ((V Int)) (= 0 (seq.nth (seq.unit 0) 1)))) +(check-sat) diff --git a/test/regress/regress1/seq/issue8148-const-mv.smt2 b/test/regress/regress1/seq/issue8148-const-mv.smt2 new file mode 100644 index 000000000..01f7aefe0 --- /dev/null +++ b/test/regress/regress1/seq/issue8148-const-mv.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(set-option :re-elim-agg true) +(declare-fun e!0 () (Seq Bool)) +(assert (= e!0 seq.empty)) +(assert (seq.nth e!0 0)) +(check-sat) -- 2.30.2