diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 62 | ||||
| -rw-r--r-- | src/theory/theory_model_builder.h | 11 |
2 files changed, 38 insertions, 35 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index f711dfdd1..34659031e 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -218,62 +218,62 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue( Assert(assertedReps.find(*i) != assertedReps.end()); Node rep = assertedReps[*i]; Trace("model-builder-debug") << " Rep : " << rep << std::endl; - // check matching val to rep with eqc as a free variable - Node eqc_m; - if (isCdtValueMatch(val, rep, eqc, eqc_m)) + // check whether it is possible that rep will be assigned the same value + // as val. + if (isCdtValueMatch(val, rep)) { - Trace("model-builder-debug") << " ...matches with " << eqc << " -> " - << eqc_m << std::endl; - if (eqc_m.getKind() == kind::CODATATYPE_BOUND_VARIABLE) - { - Trace("model-builder-debug") << "*** " << val - << " is excluded datatype for " << eqc - << std::endl; - return true; - } + return true; } } return false; } -bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, - Node r, - Node eqc, - Node& eqc_m) +bool TheoryEngineModelBuilder::isCdtValueMatch(Node v, Node r) { if (r == v) { + // values equal match trivially return true; } - else if (r == eqc) + else if (v.isConst() && r.isConst()) { - if (eqc_m.isNull()) + // distinct constant values do not match + return false; + } + else if (r.getKind() == kind::APPLY_CONSTRUCTOR) + { + if (v.getKind() != kind::APPLY_CONSTRUCTOR) { - // only if an uninterpreted constant? - eqc_m = v; + Assert(v.getKind() == kind::CODATATYPE_BOUND_VARIABLE); + // v is the position of a loop. It may be possible to match, we return + // true, which is an over-approximation of when it is unsafe to use v. return true; } - else - { - return v == eqc_m; - } - } - else if (v.getKind() == kind::APPLY_CONSTRUCTOR - && r.getKind() == kind::APPLY_CONSTRUCTOR) - { if (v.getOperator() == r.getOperator()) { - for (unsigned i = 0; i < v.getNumChildren(); i++) + for (size_t i = 0, nchild = v.getNumChildren(); i < nchild; i++) { - if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m)) + if (!isCdtValueMatch(v[i], r[i])) { + // if one child fails to match, we cannot match return false; } } return true; } + // operators do not match + return false; } - return false; + else if (v.getKind() == kind::APPLY_CONSTRUCTOR) + { + // v has a constructor in a position that we have yet to fill in r. + // we are either a finite type in which case this subfield of r can be + // assigned a default value (or otherwise would have been split on). + // otherwise we are an infinite type and the subfield of r will be + // chosen not to clash with the subfield of v. + return false; + } + return true; } bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index a604d0402..fb6204b69 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -292,11 +292,14 @@ class TheoryEngineModelBuilder : protected EnvObj Node eqc); /** is codatatype value match * - * This returns true if v is r{ eqc -> t } for some t. - * If this function returns true, then t above is - * stored in eqc_m. + * Takes as arguments a codatatype value v, and a codatatype term r of the + * same sort. + * + * It returns true if it is possible that the value of r will be forced to + * be equal to v during model construction. A return value of false indicates + * that it is safe to use value v to avoid merging with r. */ - bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m); + static bool isCdtValueMatch(Node v, Node r); //------------------------------------end for codatatypes //---------------------------------for debugging finite model finding |