Added OutputChannel::propagateAsDecision() functionality, allowing a theory
authorMorgan Deters <mdeters@gmail.com>
Wed, 22 Feb 2012 20:08:57 +0000 (20:08 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 22 Feb 2012 20:08:57 +0000 (20:08 +0000)
commit7719c492e69e22f9bdf0ce84ecc41ba0a4423aee
treebcb5015c6c3d4789088b870105358bad2db5b68d
parent4aecb261e60bf3e2de0d6a59af8d3a55b608c273
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
src/prop/minisat/core/Solver.cc
src/prop/sat.cpp
src/prop/sat.h
src/theory/output_channel.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_test_utils.h
test/unit/theory/theory_black.h
test/unit/theory/theory_engine_white.h