diff options
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r-- | src/prop/theory_proxy.h | 98 |
1 files changed, 51 insertions, 47 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 413b4941d..59bc859cb 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -23,9 +23,15 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT +#include <iosfwd> + #include "context/cdqueue.h" +#include "expr/node.h" #include "expr/statistics_registry.h" #include "prop/sat_solver.h" +#include "smt/smt_globals.h" +#include "smt_util/lemma_output_channel.h" +#include "smt_util/lemma_input_channel.h" #include "theory/theory.h" namespace CVC4 { @@ -42,40 +48,13 @@ class CnfStream; * The proxy class that allows the SatSolver to communicate with the theories */ class TheoryProxy { - - /** The prop engine we are using */ - PropEngine* d_propEngine; - - /** The CNF engine we are using */ - CnfStream* d_cnfStream; - - /** The decision engine we are using */ - DecisionEngine* d_decisionEngine; - - /** The theory engine we are using */ - TheoryEngine* d_theoryEngine; - - /** Queue of asserted facts */ - context::CDQueue<TNode> d_queue; - - /** - * Set of all lemmas that have been "shared" in the portfolio---i.e., - * all imported and exported lemmas. - */ - std::hash_set<Node, NodeHashFunction> d_shared; - - /** - * Statistic: the number of replayed decisions (via --replay). - */ - KEEP_STATISTIC(IntStat, d_replayedDecisions, - "prop::theoryproxy::replayedDecisions", 0); - public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream); + CnfStream* cnfStream, + SmtGlobals* globals); ~TheoryProxy(); @@ -117,25 +96,50 @@ public: SatValue getDecisionPolarity(SatVariable var); -};/* class SatSolver */ + private: + /** The prop engine we are using. */ + PropEngine* d_propEngine; -/* Functions that delegate to the concrete SAT solver. */ - -inline TheoryProxy::TheoryProxy(PropEngine* propEngine, - TheoryEngine* theoryEngine, - DecisionEngine* decisionEngine, - context::Context* context, - CnfStream* cnfStream) : - d_propEngine(propEngine), - d_cnfStream(cnfStream), - d_decisionEngine(decisionEngine), - d_theoryEngine(theoryEngine), - d_queue(context) -{} - -inline TheoryProxy::~TheoryProxy() { - /* nothing to do for now */ -} + /** The CNF engine we are using. */ + CnfStream* d_cnfStream; + + /** The decision engine we are using. */ + DecisionEngine* d_decisionEngine; + + /** The theory engine we are using. */ + TheoryEngine* d_theoryEngine; + + + /** + * Container for inputChannel, outputChannel, replayLog, and + * replayStream. + */ + SmtGlobals* d_globals; + + /** The lemma input channel we are using. */ + LemmaInputChannel* inputChannel(); + + /** The lemma output channel we are using. */ + LemmaOutputChannel* outputChannel(); + + std::ostream* replayLog(); + ExprStream* replayStream(); + + /** Queue of asserted facts */ + context::CDQueue<TNode> d_queue; + + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set<Node, NodeHashFunction> d_shared; + + /** + * Statistic: the number of replayed decisions (via --replay). + */ + KEEP_STATISTIC(IntStat, d_replayedDecisions, + "prop::theoryproxy::replayedDecisions", 0); +};/* class SatSolver */ }/* CVC4::prop namespace */ |