diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /src/theory/output_channel.h | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2491aef3a..d5c12457a 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -22,6 +22,7 @@ #include "base/cvc4_assert.h" #include "smt/logic_exception.h" #include "theory/interrupted.h" +#include "proof/proof_manager.h" #include "util/resource_manager.h" namespace CVC4 { @@ -99,8 +100,10 @@ public: * assigned false), or else a literal by itself (in the case of a * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. + * @param pf - a proof of the conflict. This is only non-null if proofs + * are enabled. */ - virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; + virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0; /** * Propagate a theory literal. @@ -115,16 +118,31 @@ public: * been detected. (This requests a split.) * * @param n - a theory lemma valid at decision level 0 + * @param rule - the proof rule for this lemma * @param removable - whether the lemma can be removed at any point * @param preprocess - whether to apply more aggressive preprocessing * @param sendAtoms - whether to ensure atoms are sent to the theory * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ - virtual LemmaStatus lemma(TNode n, bool removable = false, - bool preprocess = false, bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0; + virtual LemmaStatus lemma(TNode n, ProofRule rule, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + + /** + * Variant of the lemma function that does not require providing a proof rule. + */ + virtual LemmaStatus lemma(TNode n, + bool removable = false, + bool preprocess = false, + bool sendAtoms = false) + throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); + } + /** * Request a split on a new theory atom. This is equivalent to * calling lemma({OR n (NOT n)}). |