diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-26 00:08:20 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 00:08:20 -0800 |
commit | 50c31e61ab240ccd551a0aea732f8b9a88d7fb32 (patch) | |
tree | 30531d1f4813ed399209d198ca1eb75ac6f9dc30 /src/prop/prop_engine.h | |
parent | b28ff31b6713791f27b4860f439aaa3f63aab9d7 (diff) |
Remove portfolio leftovers (#3821)
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
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 */ |