diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/output_channel.h | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 5c2cedf5b..b1a5fc60c 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -149,6 +149,64 @@ public: } /** + * If a decision is made on n, it must be in the phase specified. + * Note that this is enforced *globally*, i.e., it is completely + * context-INdependent. If you ever requirePhase() on a literal, + * it is phase-locked forever and ever. If it is to ever have the + * other phase as its assignment, it will be because it has been + * propagated that way (or it's a unit, at decision level 0). + * + * @param n - a theory atom with a SAT literal assigned; must have + * been pre-registered + * @param phase - the phase to decide on n + */ + virtual void requirePhase(TNode n, bool phase) + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + + /** + * Flips the most recent unflipped decision to the other phase and + * returns true. If all decisions have been flipped, the root + * decision is re-flipped and flipDecision() returns false. If no + * decisions (flipped nor unflipped) are on the decision stack, the + * state is not affected and flipDecision() returns false. + * + * For example, if l1, l2, and l3 are all decision literals, and + * have been decided in positive phase, a series of flipDecision() + * calls has the following effects: + * + * l1 l2 l3 <br/> + * l1 l2 ~l3 <br/> + * l1 ~l2 <br/> + * ~l1 <br/> + * l1 (and flipDecision() returns false) + * + * Naturally, flipDecision() might be interleaved with search. For example: + * + * l1 l2 l3 <br/> + * flipDecision() <br/> + * l1 l2 ~l3 <br/> + * flipDecision() <br/> + * l1 ~l2 <br/> + * SAT decides l3 <br/> + * l1 ~l2 l3 <br/> + * flipDecision() <br/> + * l1 ~l2 ~l3 <br/> + * flipDecision() <br/> + * ~l1 <br/> + * SAT decides l2 <br/> + * ~l1 l2 <br/> + * flipDecision() <br/> + * ~l1 ~l2 <br/> + * flipDecision() returns FALSE<br/> + * l1 + * + * @return true if a decision was flipped; false if no decision + * could be flipped, or if the root decision was re-flipped + */ + virtual bool flipDecision() + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; + + /** * Notification from a theory that it realizes it is incomplete at * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. |