diff options
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); + } } } } |