diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-08 15:49:14 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-08 15:50:20 -0600 |
| commit | 2dd6292b73e4e19be2e261c7fe5664bd2b0149bd (patch) | |
| tree | 0f4956ec068972da8c8d1c708df7c8b2f7a07f3a /src/theory/theory_model.cpp | |
| parent | 3c4c4420ebae4d27d53084453591363942eb4d2e (diff) | |
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a61df11d8..d024e0270 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -114,7 +114,8 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || + ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). // However, if the Decision Engine stops us early, there might be a // quantifier that isn't assigned. In conjunction with miniscoping, this @@ -570,6 +571,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; d_te->collectModelInfo(tm, fullModel); + // model-builder specific initialization + preProcessBuildModel(tm, fullModel); + + // Loop through all terms and make sure that assignable sub-terms are in the equality engine // Also, record #eqc per type (for finite model finding) std::map< TypeNode, unsigned > eqc_usort_count; @@ -830,6 +835,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (t.getCardinality().isInfinite()) { bool success; do{ + Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl; n = typeConstSet.nextTypeEnum(t, true); //--- AJR: this code checks whether n is a legal value Assert( !n.isNull() ); @@ -1016,6 +1022,9 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node return retNode; } +void TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) { + +} void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) { |