diff options
Diffstat (limited to 'src/prop/prop_engine.h')
| -rw-r--r-- | src/prop/prop_engine.h | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index efbd82947..42b3ce65f 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,7 +28,6 @@ #include "expr/node.h" #include "options/options.h" #include "proof/proof_manager.h" -#include "smt_util/lemma_channels.h" #include "util/resource_manager.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -94,14 +93,16 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); -public: - + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, - context::Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels); + PropEngine(TheoryEngine*, + DecisionEngine*, + context::Context* satContext, + context::Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream); /** * Destructor. @@ -115,7 +116,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { } + void shutdown() {} /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -135,7 +136,11 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); + void assertLemma(TNode node, + bool negated, + bool removable, + ProofRule rule, + TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This @@ -243,8 +248,7 @@ public: */ bool properExplanation(TNode node, TNode expl) const; -};/* class PropEngine */ - +}; /* class PropEngine */ }/* CVC4::prop namespace */ }/* CVC4 namespace */ |