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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/output_channel.cpp | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp new file mode 100644 index 000000000..9fe973569 --- /dev/null +++ b/src/theory/output_channel.cpp @@ -0,0 +1,111 @@ +/********************* */ +/*! \file output_channel.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The theory output channel interface + **/ + +#include "theory/output_channel.h" + +namespace CVC4 { +namespace theory { + +LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs) +{ + return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs) + | static_cast<uint32_t>(rhs)); +} +LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs) +{ + lhs = lhs | rhs; + return lhs; +} +LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs) +{ + return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs) + & static_cast<uint32_t>(rhs)); +} +LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs) +{ + lhs = lhs & rhs; + return lhs; +} +bool isLemmaPropertyRemovable(LemmaProperty p) +{ + return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE; +} +bool isLemmaPropertyPreprocess(LemmaProperty p) +{ + return (p & LemmaProperty::PREPROCESS) != LemmaProperty::NONE; +} +bool isLemmaPropertySendAtoms(LemmaProperty p) +{ + return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE; +} + +std::ostream& operator<<(std::ostream& out, LemmaProperty p) +{ + if (p == LemmaProperty::NONE) + { + out << "NONE"; + } + else + { + out << "{"; + if (isLemmaPropertyRemovable(p)) + { + out << " REMOVABLE"; + } + if (isLemmaPropertyPreprocess(p)) + { + out << " PREPROCESS"; + } + if (isLemmaPropertySendAtoms(p)) + { + out << " SEND_ATOMS"; + } + out << " }"; + } + return out; +} + +LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level) + : d_rewrittenLemma(rewrittenLemma), d_level(level) +{ +} + +TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; } + +unsigned LemmaStatus::getLevel() const { return d_level; } + +LemmaStatus OutputChannel::lemma(TNode n, LemmaProperty p) +{ + return lemma(n, RULE_INVALID, p); +} + +LemmaStatus OutputChannel::split(TNode n) +{ + return splitLemma(n.orNode(n.notNode())); +} + +void OutputChannel::trustedConflict(TrustNode pconf) +{ + Unreachable() << "OutputChannel::trustedConflict: no implementation" + << std::endl; +} + +LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p) +{ + Unreachable() << "OutputChannel::trustedLemma: no implementation" + << std::endl; +} + +} // namespace theory +} // namespace CVC4 |