diff options
Diffstat (limited to 'src/theory/output_channel.h')
| -rw-r--r-- | src/theory/output_channel.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index d65d4fc53..0fd610c58 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -42,7 +42,9 @@ enum class LemmaProperty : uint32_t // whether the lemma needs preprocessing PREPROCESS = 2, // whether the processing of the lemma should send atoms to the caller - SEND_ATOMS = 4 + SEND_ATOMS = 4, + // whether the lemma is part of the justification for answering "sat" + NEEDS_JUSTIFY = 8 }; /** Define operator lhs | rhs */ LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs); @@ -58,6 +60,8 @@ bool isLemmaPropertyRemovable(LemmaProperty p); bool isLemmaPropertyPreprocess(LemmaProperty p); /** is the send atoms bit set on p? */ bool isLemmaPropertySendAtoms(LemmaProperty p); +/** is the needs justify bit set on p? */ +bool isLemmaPropertyNeedsJustify(LemmaProperty p); /** * Writes an lemma property name to a stream. |