diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 17:08:23 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 19:35:52 -0400 |
commit | f6d24c56905449e68ee23a9cea54985eacd24aa3 (patch) | |
tree | cfaff8f9d3eb9cb97708e2963ae8828a0922a2f4 | |
parent | d4c5c5d06f71958fcca6e561b7eade8fd72f7304 (diff) |
disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)
-rw-r--r-- | src/theory/theory_engine.cpp | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5ee8e5fda..ee37f331e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -192,18 +192,23 @@ void TheoryEngine::preRegister(TNode preprocessed) { // Remove the top theory, if any more that means multiple theories were involved bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories); TheoryId i; - while((i = Theory::setPop(theories)) != THEORY_LAST) { - if(!d_logicInfo.isTheoryEnabled(i)) { - LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy(); - newLogicInfo.enableTheory(i); - newLogicInfo.lock(); - stringstream ss; - ss << "The logic was specified as " << d_logicInfo.getLogicString() - << ", which doesn't include " << i - << ", but found a term in that theory." << endl - << "You might want to extend your logic to " << newLogicInfo - << endl; - throw LogicException(ss.str()); + // These checks don't work with finite model finding, because it + // uses Rational constants to represent cardinality constraints, + // even though arithmetic isn't actually involved. + if(!options::finiteModelFind()) { + while((i = Theory::setPop(theories)) != THEORY_LAST) { + if(!d_logicInfo.isTheoryEnabled(i)) { + LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy(); + newLogicInfo.enableTheory(i); + newLogicInfo.lock(); + stringstream ss; + ss << "The logic was specified as " << d_logicInfo.getLogicString() + << ", which doesn't include " << i + << ", but found a term in that theory." << endl + << "You might want to extend your logic to " + << newLogicInfo.getLogicString() << endl; + throw LogicException(ss.str()); + } } } if (multipleTheories) { |