diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-07 12:54:55 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-07 12:54:55 +0200 |
commit | d3af3aab6827bd898cc7f62776febef79150e250 (patch) | |
tree | f32f789fe7b960c0872178e44e1c07b1ddc3ef24 /src/theory/theory_model.cpp | |
parent | 6343fbb0c9b238aeb1addca6449f95a01071c1ac (diff) |
Minor improvements, add endpoint eq inference to strings.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 92f834bff..cde3aef1c 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -119,11 +119,12 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // no good. Instead, return the quantifier itself. If we're in // checkModel(), and the quantifier actually matters, we'll get an // assert-fail since the quantifier isn't a constant. - if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) { + Node nr = Rewriter::rewrite(n); + if(!d_equalityEngine->hasTerm(nr)) { d_modelCache[n] = ret; return ret; } else { - ret = Rewriter::rewrite(n); + ret = nr; } } else { if(n.getKind() == kind::LAMBDA) { @@ -193,8 +194,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator()); } if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ - //FIXME - ret = NodeManager::currentNM()->mkConst(false); + //do nothing } d_modelCache[n] = ret; return ret; |