summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.h
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-05-14 02:58:36 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-05-14 02:58:36 +0000
commit5d9b6c30ad2336979cbf3ab5107afb5b31143d90 (patch)
tree54924b1bd08b4afa66217392f374b3e7d67860d9 /src/prop/cnf_stream.h
parent8394cecaf2b1a261b44af54501ef1a433cdbadc2 (diff)
Virtualizing interface between CnfStream and SatSolver
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r--src/prop/cnf_stream.h6
1 files changed, 3 insertions, 3 deletions
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback