diff options
Diffstat (limited to 'src/theory/theory_test_utils.h')
| -rw-r--r-- | src/theory/theory_test_utils.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 96bd02b5a..aaf47425b 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -41,6 +41,7 @@ namespace theory { enum OutputChannelCallType { CONFLICT, PROPAGATE, + PROPAGATE_AS_DECISION, AUG_LEMMA, LEMMA, EXPLANATION @@ -52,6 +53,7 @@ inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType switch(type) { case theory::CONFLICT: return out << "CONFLICT"; case theory::PROPAGATE: return out << "PROPAGATE"; + case theory::PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION"; case theory::AUG_LEMMA: return out << "AUG_LEMMA"; case theory::LEMMA: return out << "LEMMA"; case theory::EXPLANATION: return out << "EXPLANATION"; @@ -81,6 +83,11 @@ public: push(PROPAGATE, n); } + void propagateAsDecision(TNode n) + throw(AssertionException) { + push(PROPAGATE_AS_DECISION, n); + } + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); return LemmaStatus(Node::null(), 0); |