diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-08 23:57:50 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-08 23:58:02 +0200 |
| commit | e253094f6b4ade626813a3d500d86785e5dde138 (patch) | |
| tree | dd1e2c897249d32f443578bbf73c0e9b637fa620 /src/theory/theory_model.cpp | |
| parent | 477e72b588e8cd6630f0379ac2014a1f738f94fc (diff) | |
Minor improvements to strings. Refactor rewriter. Enable fairness for multiple sorts in UF finite model finding by default.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index cde3aef1c..c62a0dd4a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -104,7 +104,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { // 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 @@ -193,9 +193,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) { ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator()); } - if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ - //do nothing - } d_modelCache[n] = ret; return ret; } |