diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-10-03 19:41:45 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-10-03 19:41:45 +0000 |
commit | 83722fdc9072c8bee19c2123176d77bef50bbe0d (patch) | |
tree | 540ca6db2838024addb26396f46ddcf123ebac7f /src/theory/theory_engine.h | |
parent | 98db56a7b94d62a1fb0aa3be555fb09b0f98449f (diff) |
added support for interrupting TheoryBV
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5ec0d9776..8f534a62c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -36,11 +36,13 @@ #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" +#include "theory/interrupted.h" #include "options/options.h" #include "smt/options.h" #include "util/statistics_registry.h" #include "util/hash.h" #include "util/cache.h" +#include "util/cvc4_assert.h" #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" #include "theory/model.h" @@ -230,6 +232,11 @@ class TheoryEngine { { } + void safePoint() throw(theory::Interrupted, AssertionException) { + if (d_engine->d_interrupted) + throw theory::Interrupted(); + } + void conflict(TNode conflictNode) throw(AssertionException) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; ++ d_statistics.conflicts; @@ -386,6 +393,9 @@ class TheoryEngine { Node d_true; Node d_false; + /** Whether we were just interrupted (or not) */ + bool d_interrupted; + public: /** Constructs a theory engine */ @@ -394,6 +404,8 @@ public: /** Destroys a theory engine */ ~TheoryEngine(); + void interrupt() throw(ModalException); + /** * Adds a theory. Only one theory per TheoryId can be present, so if * there is another theory it will be deleted. |