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 /src/theory/theory_engine.cpp | |
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 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 75c64654d..c4a8dc591 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -55,6 +55,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_logic(""), d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), + d_decisionRequests(context), + d_decisionRequestsIndex(context, 0), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms) { @@ -665,13 +667,22 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { } } +void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) { + Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl; + + d_propEngine->checkTime(); + + Assert(d_propEngine->isSatLiteral(literal.getKind() == kind::NOT ? literal[0] : literal), "OutputChannel::propagateAsDecision() requires a SAT literal (or negation of one)"); + + d_decisionRequests.push_back(literal); +} + theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType() == b.getType()); return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } -Node TheoryEngine::getExplanation(TNode node) -{ +Node TheoryEngine::getExplanation(TNode node) { Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; TNode atom = node.getKind() == kind::NOT ? node[0] : node; |