diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-09 19:18:58 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-09 19:18:58 +0000 |
| commit | ca6647503475fb36827e960d9e01c3f8a04c4ed3 (patch) | |
| tree | b951d83522c8d82709abfcd2707298b3a4916d07 /src/theory/theory_engine.cpp | |
| parent | 63e4a6775daa1b7a986cc9dec0bd178b7e023c47 (diff) | |
Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a952c9ee6..a76ad41cc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -30,6 +30,8 @@ #include "theory/rewriter.h" #include "theory/theory_traits.h" +#include "smt/logic_exception.h" + #include "util/node_visitor.h" #include "util/ite_removal.h" @@ -684,7 +686,7 @@ void TheoryEngine::shutdown() { theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { // Reset the interrupt flag - d_interrupted = false; + d_interrupted = false; TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; @@ -695,7 +697,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa ss << "The logic was specified as " << d_logicInfo.getLogicString() << ", which doesn't include " << Theory::theoryOf(atom) << ", but got an asserted fact to that theory"; - throw Exception(ss.str()); + throw LogicException(ss.str()); } Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut); @@ -793,7 +795,7 @@ Node TheoryEngine::preprocess(TNode assertion) { ss << "The logic was specified as " << d_logicInfo.getLogicString() << ", which doesn't include " << Theory::theoryOf(current) << ", but got an asserted fact to that theory"; - throw Exception(ss.str()); + throw LogicException(ss.str()); } // If this is an atom, we preprocess its terms with the theory ppRewriter @@ -883,7 +885,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, ss << "The logic was specified as " << d_logicInfo.getLogicString() << ", which doesn't include " << toTheoryId << ", but got an asserted fact to that theory"; - throw Exception(ss.str()); + throw LogicException(ss.str()); } if (d_inConflict) { |