diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-22 20:08:57 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-22 20:08:57 +0000 |
commit | 7719c492e69e22f9bdf0ce84ecc41ba0a4423aee (patch) | |
tree | bcb5015c6c3d4789088b870105358bad2db5b68d /test/unit | |
parent | 4aecb261e60bf3e2de0d6a59af8d3a55b608c273 (diff) |
Added OutputChannel::propagateAsDecision() functionality, allowing a theory
to request a decision on a literal. All these theory requests are kept in a
context-dependent queue and serviced in order when the SAT solver goes to make a
decision. Requests that don't have a SAT literal give an assert-fail. Requests
for literals that already have an assignment are silently ignored.
Since the queue is CD, requests can actually be serviced more than once (e.g., if
a request is made at DL 5, but not serviced until DL 10, and later, a conflict
backtracks to level 7, the request may be serviced again).
Performance impact: none to negligible for theories that don't use it
See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/theory_black.h | 5 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 3 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 60e090d16..76385219d 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -62,6 +62,11 @@ public: push(PROPAGATE, n); } + void propagateAsDecision(TNode n) + throw(AssertionException) { + // ignore + } + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 2363e4906..8d7bc9c72 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -54,6 +54,9 @@ class FakeOutputChannel : public OutputChannel { void propagate(TNode n) throw(AssertionException) { Unimplemented(); } + void propagateAsDecision(TNode n) throw(AssertionException) { + Unimplemented(); + } LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { Unimplemented(); } |