From f7675b2df9f72ddb7b52dc5d8f3776112a27531b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Feb 2022 15:34:07 -0600 Subject: [PATCH] Further relax what is considered a value in the model (#8095) Fixes #8094. This makes it so that "value-like" terms can appear as subterms in other terms that are then subsequently also considered values. For example (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is now considered a value. This also changes the default option for when to use witness terms for strings in models, based on some user feedback. --- src/options/strings_options.toml | 3 +- src/smt/solver_engine.cpp | 2 +- src/theory/theory_engine.cpp | 17 ++- src/theory/theory_model.cpp | 111 +++++++++++++++++- src/theory/theory_model.h | 18 ++- src/theory/theory_model_builder.cpp | 12 +- test/regress/CMakeLists.txt | 3 + test/regress/regress0/arith/exp-in-model.smt2 | 2 +- .../regress0/arith/issue7984-quant-trans.smt2 | 1 + .../nl/transcedental_model_simple.smt2 | 7 ++ .../strings/issue8094-witness-model.smt2 | 10 ++ .../regress1/strings/witness-model.smt2 | 9 ++ 12 files changed, 173 insertions(+), 22 deletions(-) create mode 100644 test/regress/regress1/nl/transcedental_model_simple.smt2 create mode 100644 test/regress/regress1/strings/issue8094-witness-model.smt2 create mode 100644 test/regress/regress1/strings/witness-model.smt2 diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 610a1089f..66753fc0b 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -247,6 +247,5 @@ name = "Strings Theory" category = "regular" long = "strings-model-max-len=N" type = "uint64_t" - default = "1000" - maximum = "65536" + default = "65536" help = "The maximum size of string values in models" diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 83d4a903f..39ee661a0 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1005,7 +1005,7 @@ Node SolverEngine::getValue(const Node& ex) const // Ensure it's a value (constant or const-ish like real algebraic // numbers), or a lambda (for uninterpreted functions). This assertion only // holds for models that do not have approximate values. - if (!TheoryModel::isValue(resultNode)) + if (!m->isValue(resultNode)) { d_env->warning() << "Could not evaluate " << resultNode << " in getValue." << std::endl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3092664cd..173a93566 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1796,8 +1796,10 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { bool hasRelevantAssertions = false; if (d_relManager != nullptr) { + d_relManager->beginRound(); relevantAssertions = d_relManager->getRelevantAssertions(hasRelevantAssertions); + d_relManager->endRound(); } for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; @@ -1817,10 +1819,17 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { if (val != d_true) { std::stringstream ss; - ss << " " << theoryId - << " has an asserted fact that the model doesn't satisfy." << endl - << "The fact: " << assertion << endl - << "Model value: " << val << endl; + ss << " " << theoryId << " has an asserted fact that"; + if (val == d_false) + { + ss << " the model doesn't satisfy." << std::endl; + } + else + { + ss << " the model may not satisfy." << std::endl; + } + ss << "The fact: " << assertion << std::endl + << "Model value: " << val << std::endl; if (hardFailure) { if (val == d_false) diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index eb0945ce5..36502101b 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -14,6 +14,7 @@ */ #include "theory/theory_model.h" +#include "expr/attribute.h" #include "expr/cardinality_constraint.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" @@ -803,15 +804,115 @@ std::string TheoryModel::debugPrintModelEqc() const return ss.str(); } -bool TheoryModel::isValue(TNode node) +struct IsModelValueTag { - if (node.isConst()) +}; +struct IsModelValueComputedTag +{ +}; +/** Attribute true for expressions that are quasi-values */ +using IsModelValueAttr = expr::Attribute; +using IsModelValueComputedAttr = expr::Attribute; + +bool TheoryModel::isBaseModelValue(TNode n) const +{ + if (n.isConst()) { return true; } - Kind k = node.getKind(); - return k == kind::REAL_ALGEBRAIC_NUMBER || k == kind::LAMBDA - || k == kind::WITNESS; + Kind k = n.getKind(); + if (k == kind::REAL_ALGEBRAIC_NUMBER || k == kind::LAMBDA + || k == kind::WITNESS) + { + // we are a value if we are one of the above kinds + return true; + } + return false; +} + +bool TheoryModel::isValue(TNode n) const +{ + IsModelValueAttr imva; + IsModelValueComputedAttr imvca; + // The list of nodes we are processing, and the current child index of that + // node we are inspecting. This vector always specifies a single path in the + // original term n. Notice this index accounts for operators, where the + // operator of a term is treated as the first child, and subsequently all + // other children are shifted up by one. + std::vector> visit; + // the last computed value of whether a node was a value + bool currentReturn = false; + visit.emplace_back(n, 0); + std::pair v; + while (!visit.empty()) + { + v = visit.back(); + TNode cur = v.first; + bool finishedComputing = false; + // if we just pushed to the stack, do initial checks + if (v.second == 0) + { + if (cur.getAttribute(imvca)) + { + // already cached + visit.pop_back(); + currentReturn = cur.getAttribute(imva); + continue; + } + if (isBaseModelValue(cur)) + { + finishedComputing = true; + currentReturn = true; + } + else if (cur.getNumChildren() == 0 || rewrite(cur) != cur) + { + finishedComputing = true; + currentReturn = false; + } + } + else if (!currentReturn) + { + // if the last child was not a value, we are not a value + finishedComputing = true; + } + if (!finishedComputing) + { + bool hasOperator = cur.hasOperator(); + size_t nextChildIndex = v.second; + if (hasOperator && nextChildIndex > 0) + { + // if have an operator, we shift the child index we are looking at + nextChildIndex--; + } + if (nextChildIndex == cur.getNumChildren()) + { + // finished, we are a value + currentReturn = true; + } + else + { + visit.back().second++; + if (hasOperator && v.second == 0) + { + // if we have an operator, process it as the first child + visit.emplace_back(cur.getOperator(), 0); + } + else + { + Assert(nextChildIndex < cur.getNumChildren()); + // process the next child, which may be shifted from v.second to + // account for the operator + visit.emplace_back(cur[nextChildIndex], 0); + } + continue; + } + } + visit.pop_back(); + cur.setAttribute(imva, currentReturn); + cur.setAttribute(imvca, true); + } + Assert(n.getAttribute(imvca)); + return currentReturn; } } // namespace theory diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index ada7619e2..b476ddfef 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -358,10 +358,16 @@ class TheoryModel : protected EnvObj std::string debugPrintModelEqc() const; /** - * Is the node n a "value"? This is true if n is constant, a constant-like - * value (e.g. a real algebraic number) or if n is a lambda. + * Is the node n a "value"? This is true if n is a "base value", where + * a base value is one where isConst() returns true, a constant-like + * value (e.g. a real algebraic number) or if n is a lambda or witness + * term. + * + * We also return true for rewritten nodes whose leafs are base values. + * For example, (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is + * a value. */ - static bool isValue(TNode node); + bool isValue(TNode node) const; protected: /** Unique name of this model */ @@ -416,6 +422,12 @@ class TheoryModel : protected EnvObj * a model builder constructs this model. */ virtual void addTermInternal(TNode n); + /** + * Is base model value? This is a helper method for isValue, returns true + * if n is a base model value. + */ + bool isBaseModelValue(TNode n) const; + private: /** cache for getModelValue */ mutable std::unordered_map d_modelCache; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 75c18076a..03cdaa786 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -79,7 +79,7 @@ Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r) { Trace("model-builder-debug") << "...try to normalize" << std::endl; Node normalized = normalize(m, n, true); - if (TheoryModel::isValue(normalized)) + if (m->isValue(normalized)) { return normalized; } @@ -101,7 +101,7 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a) // Members of exclusion set must have values, otherwise we are not yet // assignable. Node er = eset[i]; - if (TheoryModel::isValue(er)) + if (tm->isValue(er)) { // already processed continue; @@ -503,7 +503,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // 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 (TheoryModel::isValue(n)) + if (tm->isValue(n)) { Assert(constRep.isNull()); constRep = n; @@ -732,7 +732,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } if (!normalized.isNull()) { - Assert(TheoryModel::isValue(normalized)); + Assert(tm->isValue(normalized)); typeConstSet.add(tb, normalized); assignConstantRep(tm, *i2, normalized); Trace("model-builder") << " Eval: Setting constant rep of " @@ -771,7 +771,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl; - if (TheoryModel::isValue(normalized)) + if (tm->isValue(normalized)) { changed = true; typeConstSet.add(tb, normalized); @@ -1203,7 +1203,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly) { ri = normalize(m, ri, evalOnly); } - if (!TheoryModel::isValue(ri)) + if (!m->isValue(ri)) { childrenConst = false; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b8a060cfa..2e53419e4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1931,6 +1931,7 @@ set(regress_1_tests regress1/nl/sugar-ident-3.smt2 regress1/nl/sugar-ident.smt2 regress1/nl/tan-rewrite2.smt2 + regress1/nl/transcedental_model_simple.smt2 regress1/nl/zero-subset.smt2 regress1/non-fatal-errors.smt2 regress1/proj-issue175.smt2 @@ -2425,6 +2426,7 @@ set(regress_1_tests regress1/strings/issue6973-dup-lemma-conc.smt2 regress1/strings/issue7677-test-const-rv.smt2 regress1/strings/issue7918-learned-rewrite.smt2 + regress1/strings/issue8094-witness-model.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 @@ -2509,6 +2511,7 @@ set(regress_1_tests regress1/strings/update-ex1.smt2 regress1/strings/update-ex2.smt2 regress1/strings/username_checker_min.smt2 + regress1/strings/witness-model.smt2 regress1/sygus/VC22_a.sy regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy diff --git a/test/regress/regress0/arith/exp-in-model.smt2 b/test/regress/regress0/arith/exp-in-model.smt2 index e63b24e26..3274ca2f5 100644 --- a/test/regress/regress0/arith/exp-in-model.smt2 +++ b/test/regress/regress0/arith/exp-in-model.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_UFNRAT) -(set-option :produce-models true) +(set-info :status sat) (declare-fun b (Real) Real) (declare-fun v () Real) (assert (distinct 0 (* v v))) diff --git a/test/regress/regress0/arith/issue7984-quant-trans.smt2 b/test/regress/regress0/arith/issue7984-quant-trans.smt2 index 7252e11cf..9a36d87a6 100644 --- a/test/regress/regress0/arith/issue7984-quant-trans.smt2 +++ b/test/regress/regress0/arith/issue7984-quant-trans.smt2 @@ -1,6 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_NRAT) +(set-info :status sat) (set-option :re-elim-agg true) (declare-fun r6 () Real) (assert (= 0.0 (cos r6))) diff --git a/test/regress/regress1/nl/transcedental_model_simple.smt2 b/test/regress/regress1/nl/transcedental_model_simple.smt2 new file mode 100644 index 000000000..473ac25bf --- /dev/null +++ b/test/regress/regress1/nl/transcedental_model_simple.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-rlv=always -q +; EXPECT: sat +(set-logic QF_NRAT) +(set-info :status sat) +(declare-fun x () Real) +(assert (or (= x (sin 0.1)) (= x (sin 1.1)))) +(check-sat) diff --git a/test/regress/regress1/strings/issue8094-witness-model.smt2 b/test/regress/regress1/strings/issue8094-witness-model.smt2 new file mode 100644 index 000000000..44da3d501 --- /dev/null +++ b/test/regress/regress1/strings/issue8094-witness-model.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun v () String) +(declare-fun r () Bool) +(declare-fun w () String) +(declare-fun q () String) +(assert (forall ((V String)) (or r (exists ((V String)) (str.in_re (str.++ "z" v) (re.* (str.to_re (str.from_code (str.len v))))))))) +(check-sat) diff --git a/test/regress/regress1/strings/witness-model.smt2 b/test/regress/regress1/strings/witness-model.smt2 new file mode 100644 index 000000000..22e7aa7f4 --- /dev/null +++ b/test/regress/regress1/strings/witness-model.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun w () String) +(declare-fun q () String) +(assert (= (str.len q) 99999999999999999999999999999999999999)) +(assert (= w (str.++ q "A"))) +(check-sat) -- 2.30.2