diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:06:02 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:39:21 -0500 |
commit | 6d71aac1070aa7b1a8575722f4022a04b57d5763 (patch) | |
tree | e51de5c69f3837946b5fad3e8cb9b21ac81d3683 /src/theory | |
parent | 195dffbb7468e814d3dc3226666688869c13ba3d (diff) |
fix --check-model --finite-model-find when used together (related to bug 486)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/model.cpp | 3 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 26 |
2 files changed, 16 insertions, 13 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 2333a4394..713587be2 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -131,6 +131,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const children.push_back(val); } Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children)); + if(val.getKind() == kind::CARDINALITY_CONSTRAINT) { + val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator()); + } Assert(hasBoundVars || val.isConst()); return val; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2ea0e866f..a23480eeb 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1378,19 +1378,19 @@ void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) { d_attr_handle[ str ].push_back( t ); } -void TheoryEngine::checkTheoryAssertionsWithModel() -{ - for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - Theory* theory = d_theoryTable[theoryId]; - if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { - if (theoryId == THEORY_QUANTIFIERS || theoryId == THEORY_REWRITERULES) { - continue; - } - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - Node assertion = (*it).assertion; - Node val = getModel()->getValue(assertion); - Assert(val == d_true); +void TheoryEngine::checkTheoryAssertionsWithModel() { + for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + if(theoryId != THEORY_REWRITERULES) { + Theory* theory = d_theoryTable[theoryId]; + if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { + for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(), + it_end = theory->facts_end(); + it != it_end; + ++it) { + Node assertion = (*it).assertion; + Node val = getModel()->getValue(assertion); + Assert(val == d_true); + } } } } |