summaryrefslogtreecommitdiff
path: root/src/prop/minisat/simp/SimpSolver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.h')
-rw-r--r--src/prop/minisat/simp/SimpSolver.h19
1 files changed, 11 insertions, 8 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 221b4c6e2..f9e9b0387 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -17,23 +17,25 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef CVC4_MiniSat_SimpSolver_h
-#define CVC4_MiniSat_SimpSolver_h
+#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
+#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
#include <cstdio>
+#include <cassert>
-#include "Queue.h"
-#include "Solver.h"
+#include "../mtl/Queue.h"
+#include "../core/Solver.h"
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
SimpSolver();
- ~SimpSolver();
+ CVC4_PUBLIC ~SimpSolver();
// Problem specification:
//
@@ -159,8 +161,9 @@ inline bool SimpSolver::isEliminated (Var v) const { return v < elimtable.size(
inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
inline bool SimpSolver::solve (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
//=================================================================================================
-#endif /* CVC4_MiniSat_SimpSolver_h */
+#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback