diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:04:43 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:04:43 +0000 |
commit | 426abc52a0f1631f2adee0eef845e3f8946c5088 (patch) | |
tree | 66bc00874b2b4bd6cd22d3e0dca507cf8729de8d /src/prop/theory_proxy.h | |
parent | 19266a39605baad33543539b0045fc940a0d650f (diff) |
sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r-- | src/prop/theory_proxy.h | 163 |
1 files changed, 163 insertions, 0 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h new file mode 100644 index 000000000..85dcae68b --- /dev/null +++ b/src/prop/theory_proxy.h @@ -0,0 +1,163 @@ +/********************* */ +/*! \file sat.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: taking, cconway, dejan + ** Minor contributors (to current version): barrett + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** SAT Solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__SAT_H +#define __CVC4__PROP__SAT_H + +// Just defining this for now, since there's no other SAT solver bindings. +// Optional blocks below will be unconditionally included +#define __CVC4_USE_MINISAT + +#include "theory/theory.h" +#include "util/options.h" +#include "util/stats.h" + +#include "prop/sat_module.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace prop { + +class PropEngine; +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 theory engine we are using */ + TheoryEngine* d_theoryEngine; + + /** Context we will be using to synchronzie the sat solver */ + context::Context* d_context; + + /** + * 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; + +public: + TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + CnfStream* cnfStream); + + ~TheoryProxy(); + + + void theoryCheck(theory::Theory::Effort effort); + + void explainPropagation(SatLiteral l, SatClause& explanation); + + void theoryPropagate(SatClause& output); + + void enqueueTheoryLiteral(const SatLiteral& l); + + SatLiteral getNextDecisionRequest(); + + bool theoryNeedCheck() const; + + void removeClausesAboveLevel(int level); + + /** + * Notifies of a new variable at a decision level. + */ + void variableNotify(SatVariable var); + + void unregisterVar(SatLiteral lit); + + void renewVar(SatLiteral lit, int level = -1); + + TNode getNode(SatLiteral lit); + + void notifyRestart(); + + void notifyNewLemma(SatClause& lemma); + + SatLiteral getNextReplayDecision(); + + void logDecision(SatLiteral lit); + + void checkTime(); + +};/* class SatSolver */ + +/* Functions that delegate to the concrete SAT solver. */ + +inline TheoryProxy::TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + CnfStream* cnfStream) : + d_propEngine(propEngine), + d_cnfStream(cnfStream), + d_theoryEngine(theoryEngine), + d_context(context) +{} + +}/* CVC4::prop namespace */ + +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { + out << lit.toString(); + return out; +} + +inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { + out << "clause:"; + for(unsigned i = 0; i < clause.size(); ++i) { + out << " " << clause[i]; + } + out << ";"; + return out; +} + +inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { + std::string str; + switch(val) { + case prop::SatValUnknown: + str = "_"; + break; + case prop::SatValTrue: + str = "1"; + break; + case prop::SatValFalse: + str = "0"; + break; + default: + str = "Error"; + break; + } + + out << str; + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__PROP__SAT_H */ |