summaryrefslogtreecommitdiff
path: root/src/prop/sat_solver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/sat_solver.h')
-rw-r--r--src/prop/sat_solver.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 960881844..1c1dae410 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -24,9 +24,10 @@
#include <string>
#include "context/cdlist.h"
+#include "context/context.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
@@ -101,7 +102,7 @@ public:
virtual void notify(SatClause& clause) = 0;
virtual void spendResource(unsigned ammount) = 0;
virtual void safePoint(unsigned ammount) = 0;
-
+
};/* class BVSatSolverInterface::Notify */
virtual void setNotify(Notify* notify) = 0;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback