From: Gereon Kremer Date: Fri, 14 Jan 2022 21:05:03 +0000 (-0800) Subject: Preprare central model building for RANs (#7951) X-Git-Tag: cvc5-1.0.0~541 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ff195a3d5cc9d60547160d9de68e09d3f8a570a;p=cvc5.git Preprare central model building for RANs (#7951) This PR uses a new utility isEvaluationResult() instead of isConst() within the core model building. This prepares model building for model values that are not constants (in the sense of isConst()) but still constant-lilke values, like real algebraic numbers. --- diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 97774a739..ef25d7819 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1019,10 +1019,10 @@ Node SolverEngine::getValue(const Node& ex) const || resultNode.getType().isSubtypeOf(expectedType)) << "Run with -t smt for details."; - // Ensure it's a constant, or a lambda (for uninterpreted functions). This - // assertion only holds for models that do not have approximate values. - Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA - || resultNode.isConst()); + // 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. + Assert(m->hasApproximations() || TheoryModel::isValue(resultNode)); if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray()) { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 6a083b7e3..6a0d50ac0 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -803,5 +803,11 @@ std::string TheoryModel::debugPrintModelEqc() const return ss.str(); } +bool TheoryModel::isValue(TNode node) +{ + return node.isConst() || node.getKind() == Kind::REAL_ALGEBRAIC_NUMBER + || node.getKind() == Kind::LAMBDA; +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 6d900b39e..c1f7c880f 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -357,6 +357,12 @@ 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. + */ + static bool isValue(TNode node); + protected: /** Unique name of this model */ std::string d_name; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 4aea1ad9d..193a55294 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 (normalized.isConst()) + if (TheoryModel::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 (er.isConst()) + if (TheoryModel::isValue(er)) { // already processed continue; @@ -125,11 +125,6 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a) return true; } -bool TheoryEngineModelBuilder::isValue(TNode n) -{ - return n.getKind() == kind::LAMBDA || n.isConst(); -} - bool TheoryEngineModelBuilder::isAssignable(TNode n) { if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL @@ -508,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 (isValue(n)) + if (TheoryModel::isValue(n)) { Assert(constRep.isNull()); constRep = n; @@ -737,7 +732,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } if (!normalized.isNull()) { - Assert(normalized.isConst()); + Assert(TheoryModel::isValue(normalized)); typeConstSet.add(tb, normalized); assignConstantRep(tm, *i2, normalized); Trace("model-builder") << " Eval: Setting constant rep of " @@ -776,7 +771,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl; - if (normalized.isConst()) + if (TheoryModel::isValue(normalized)) { changed = true; typeConstSet.add(tb, normalized); @@ -1208,7 +1203,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly) { ri = normalize(m, ri, evalOnly); } - if (!ri.isConst()) + if (!TheoryModel::isValue(ri)) { childrenConst = false; } @@ -1255,7 +1250,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) Node rc = m->getRepresentative(un[j]); Trace("model-builder-debug2") << " get rep : " << un[j] << " returned " << rc << std::endl; - Assert(rc.isConst()); + Assert(TheoryModel::isValue(rc)); children.push_back(rc); } Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children); diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index b716ad7d8..fb6204b69 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -126,11 +126,6 @@ class TheoryEngineModelBuilder : protected EnvObj * state of the model m. */ Node evaluateEqc(TheoryModel* m, TNode r); - /** - * Is the node n a "value"? This is true if n is constant, or if n is a - * lambda. - */ - static bool isValue(TNode n); /** is n an assignable expression? * * A term n is an assignable expression if its value is unconstrained by a