diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-28 11:03:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-28 11:03:33 -0500 |
commit | c38f35164adc5ab255803765a568ef820fa8f3b2 (patch) | |
tree | 6cbd4b21e8e9ff364b5b2f14467cd986ea69acf2 /src/theory/output_channel.h | |
parent | b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42 (diff) |
Use lemma property enum for OutputChannel::lemma (#4755)
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r-- | src/theory/output_channel.h | 75 |
1 files changed, 48 insertions, 27 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index ff13d1b6b..d65d4fc53 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -32,6 +32,42 @@ namespace CVC4 { namespace theory { +/** Properties of lemmas */ +enum class LemmaProperty : uint32_t +{ + // default + NONE = 0, + // whether the lemma is removable + REMOVABLE = 1, + // whether the lemma needs preprocessing + PREPROCESS = 2, + // whether the processing of the lemma should send atoms to the caller + SEND_ATOMS = 4 +}; +/** Define operator lhs | rhs */ +LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs); +/** Define operator lhs |= rhs */ +LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs); +/** Define operator lhs & rhs */ +LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs); +/** Define operator lhs &= rhs */ +LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs); +/** is the removable bit set on p? */ +bool isLemmaPropertyRemovable(LemmaProperty p); +/** is the preprocess bit set on p? */ +bool isLemmaPropertyPreprocess(LemmaProperty p); +/** is the send atoms bit set on p? */ +bool isLemmaPropertySendAtoms(LemmaProperty p); + +/** + * Writes an lemma property name to a stream. + * + * @param out The stream to write to + * @param p The lemma property to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, LemmaProperty p); + class Theory; /** @@ -41,17 +77,17 @@ class Theory; */ class LemmaStatus { public: - LemmaStatus(TNode rewrittenLemma, unsigned level) - : d_rewrittenLemma(rewrittenLemma), d_level(level) {} + LemmaStatus(TNode rewrittenLemma, unsigned level); /** Get the T-rewritten form of the lemma. */ - TNode getRewrittenLemma() const { return d_rewrittenLemma; } + TNode getRewrittenLemma() const; /** * Get the user-level at which the lemma resides. After this user level * is popped, the lemma is un-asserted from the SAT layer. This level * will be 0 if the lemma didn't reach the SAT layer at all. */ - unsigned getLevel() const { return d_level; } + unsigned getLevel() const; + private: Node d_rewrittenLemma; unsigned d_level; @@ -114,23 +150,18 @@ class OutputChannel { * * @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 + * @param p The properties of the lemma * @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, ProofRule rule, bool removable = false, - bool preprocess = false, - bool sendAtoms = false) = 0; + virtual LemmaStatus lemma(TNode n, + ProofRule rule, + LemmaProperty p = LemmaProperty::NONE) = 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) { - return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); - } + virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE); /** * Request a split on a new theory atom. This is equivalent to @@ -138,7 +169,7 @@ class OutputChannel { * * @param n - a theory atom; must be of Boolean type */ - LemmaStatus split(TNode n) { return splitLemma(n.orNode(n.notNode())); } + LemmaStatus split(TNode n); virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0; @@ -197,11 +228,7 @@ class OutputChannel { * by the generator pfg. Apart from pfg, the interface for this method is * the same as OutputChannel. */ - virtual void trustedConflict(TrustNode pconf) - { - Unreachable() << "OutputChannel::trustedConflict: no implementation" - << std::endl; - } + virtual void trustedConflict(TrustNode pconf); /** * Let plem be the pair (Node lem, ProofGenerator * pfg). * Send lem on the output channel of this class whose proof can be generated @@ -209,13 +236,7 @@ class OutputChannel { * the same as OutputChannel. */ virtual LemmaStatus trustedLemma(TrustNode lem, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) - { - Unreachable() << "OutputChannel::trustedLemma: no implementation" - << std::endl; - } + LemmaProperty p = LemmaProperty::NONE); //---------------------------- end new proof }; /* class OutputChannel */ |