diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-14 02:58:36 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-14 02:58:36 +0000 |
commit | 5d9b6c30ad2336979cbf3ab5107afb5b31143d90 (patch) | |
tree | 54924b1bd08b4afa66217392f374b3e7d67860d9 /src/prop | |
parent | 8394cecaf2b1a261b44af54501ef1a433cdbadc2 (diff) |
Virtualizing interface between CnfStream and SatSolver
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 4 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 6 | ||||
-rw-r--r-- | src/prop/sat.h | 16 |
3 files changed, 20 insertions, 6 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 25134b413..9abea4fcd 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -29,11 +29,11 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolver *satSolver) : +CnfStream::CnfStream(SatInputInterface *satSolver) : d_satSolver(satSolver) { } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver) : +TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) : CnfStream(satSolver) { } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9a63c26f9..6e4eaf047 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -43,7 +43,7 @@ class CnfStream { private: /** The SAT solver we will be using */ - SatSolver *d_satSolver; + SatInputInterface *d_satSolver; /** Cache of what literals have been registered to a node. */ typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache; @@ -121,7 +121,7 @@ public: * and sends them to the given sat solver. * @param satSolver the sat solver to use */ - CnfStream(SatSolver* satSolver); + CnfStream(SatInputInterface* satSolver); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -179,7 +179,7 @@ public: * Constructs the stream to use the given sat solver. * @param satSolver the sat solver to use */ - TseitinCnfStream(SatSolver* satSolver); + TseitinCnfStream(SatInputInterface* satSolver); private: diff --git a/src/prop/sat.h b/src/prop/sat.h index d5adedd20..33ab674c9 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -73,12 +73,26 @@ hashSatLiteral(const SatLiteral& literal) { #endif /* __CVC4_USE_MINISAT */ +/** Interface encapsulating the "input" to the solver, e.g., from the + * CNF converter. + * + * TODO: Is it possible to push the typedefs of SatClause and SatVariable + * into here, somehow? + */ +class SatInputInterface { +public: + /** Assert a clause in the solver. */ + virtual void addClause(SatClause& clause) = 0; + /** Create a new boolean variable in the solver. */ + virtual SatVariable newVar(bool theoryAtom = false) = 0; +}; + /** * The proxy class that allows us to modify the internals of the SAT solver. * It's only accessible from the PropEngine, and should be treated with major * care. */ -class SatSolver { +class SatSolver : public SatInputInterface { /** The prop engine we are using */ PropEngine* d_propEngine; |