diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-27 09:30:06 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-27 09:30:06 +0200 |
commit | 65c2e1688d83dfeb913b689c10d9b43c5dc89cc0 (patch) | |
tree | f552414624cd7259e638b6edc0c7a710a4215138 /src/theory/theory_model.cpp | |
parent | e4cff69e3b565e928dbf04960249477ce2c9ef6b (diff) |
Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 52b018234..05d0c896a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -478,6 +478,14 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac cache.insert(n); } +void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) { + constantReps[eqc] = const_rep; + Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl; + if( !fullModel ){ + tm->d_rep_set.d_values_to_terms[const_rep] = eqc; + } +} + void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) { @@ -551,7 +559,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (!const_rep.isNull()) { // Theories should not specify a rep if there is already a constant in the EC Assert(rep.isNull() || rep == const_rep); - constantReps[eqc] = const_rep; + assignConstantRep( tm, constantReps, eqc, const_rep, fullModel ); typeConstSet.add(eqct.getBaseType(), const_rep); } else if (!rep.isNull()) { @@ -615,7 +623,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Node normalized = normalize(tm, n, constantReps, true); if (normalized.isConst()) { typeConstSet.add(tb, normalized); - constantReps[*i2] = normalized; + assignConstantRep( tm, constantReps, *i2, normalized, fullModel ); Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; changed = true; evaluated = true; @@ -648,7 +656,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (normalized.isConst()) { changed = true; typeConstSet.add(tb, normalized); - constantReps[*i] = normalized; + assignConstantRep( tm, constantReps, *i, normalized, fullModel ); assertedReps.erase(*i); i2 = i; ++i; @@ -727,11 +735,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) n = *te; } Assert(!n.isNull()); - constantReps[*i2] = n; - Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; - if( !fullModel ){ - tm->d_rep_set.d_values_to_terms[n] = (*i2); - } + assignConstantRep( tm, constantReps, *i2, n, fullModel ); changed = true; noRepSet.erase(i2); if (assignOne) { |