summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r--src/prop/cnf_stream.h7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9d152a915..929cae346 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -29,6 +29,7 @@
#include "expr/node.h"
#include "prop/sat.h"
+#include "theory/registrar.h"
#include <ext/hash_map>
@@ -70,6 +71,8 @@ private:
protected:
+ theory::Registrar d_registrar;
+
/** Top level nodes that we translated */
std::vector<TNode> d_translationTrail;
@@ -177,7 +180,7 @@ public:
* set of clauses and sends them to the given sat solver.
* @param satSolver the sat solver to use
*/
- CnfStream(SatInputInterface* satSolver);
+ CnfStream(SatInputInterface* satSolver, theory::Registrar r);
/**
* Destructs a CnfStream. This implementation does nothing, but we
@@ -252,7 +255,7 @@ public:
* Constructs the stream to use the given sat solver.
* @param satSolver the sat solver to use
*/
- TseitinCnfStream(SatInputInterface* satSolver);
+ TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar reg);
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback