91 lines
3.1 KiB
Diff
91 lines
3.1 KiB
Diff
--- ./undertaker/SatChecker.h.orig 2011-08-24 09:05:15.000000000 -0600
|
|
+++ ./undertaker/SatChecker.h 2013-07-31 16:34:25.000000000 -0600
|
|
@@ -48,7 +48,7 @@ namespace Picosat {
|
|
|
|
/* Include the Limmat library header as C */
|
|
extern "C" {
|
|
-#include <picosat/picosat.h>
|
|
+#include <picosat.h>
|
|
}
|
|
};
|
|
|
|
@@ -202,6 +202,8 @@ private:
|
|
const std::string _sat;
|
|
clock_t _runtime;
|
|
|
|
+ Picosat::PicoSAT *picosat_inst;
|
|
+
|
|
int stringToSymbol(const std::string &key);
|
|
int newSymbol(void);
|
|
void addClause(int *clause);
|
|
--- ./undertaker/SatChecker.cpp.orig 2011-08-24 09:05:15.000000000 -0600
|
|
+++ ./undertaker/SatChecker.cpp 2013-07-31 16:32:06.000000000 -0600
|
|
@@ -70,13 +70,13 @@ int SatChecker::stringToSymbol(const std
|
|
}
|
|
|
|
int SatChecker::newSymbol(void) {
|
|
- return Picosat::picosat_inc_max_var();
|
|
+ return Picosat::picosat_inc_max_var(picosat_inst);
|
|
}
|
|
|
|
void SatChecker::addClause(int *clause) {
|
|
for (int *x = clause; *x; x++)
|
|
- Picosat::picosat_add(*x);
|
|
- Picosat::picosat_add(0);
|
|
+ Picosat::picosat_add(picosat_inst, *x);
|
|
+ Picosat::picosat_add(picosat_inst, 0);
|
|
}
|
|
|
|
int SatChecker::notClause(int inner_clause) {
|
|
@@ -299,7 +299,8 @@ void SatChecker::fillSatChecker(std::str
|
|
std::cout << std::string(expression.begin(), expression.begin()
|
|
+ info.length) << endl;
|
|
*/
|
|
- Picosat::picosat_reset();
|
|
+ Picosat::picosat_reset(picosat_inst);
|
|
+ picosat_inst = NULL;
|
|
throw SatCheckerError("SatChecker: Couldn't parse: " + expression);
|
|
}
|
|
}
|
|
@@ -308,7 +309,7 @@ void SatChecker::fillSatChecker(tree_par
|
|
iter_t expression = info.trees.begin()->children.begin();
|
|
int top_clause = transform_bool_rec(expression);
|
|
/* This adds the last clause */
|
|
- Picosat::picosat_assume(top_clause);
|
|
+ Picosat::picosat_assume(picosat_inst, top_clause);
|
|
}
|
|
|
|
SatChecker::SatChecker(const char *sat, int debug)
|
|
@@ -325,26 +326,26 @@ bool SatChecker::operator()() throw (Sat
|
|
debug_parser_indent = 0;
|
|
|
|
try {
|
|
- Picosat::picosat_init();
|
|
+ picosat_inst = Picosat::picosat_init();
|
|
// try to enable as many features as possible
|
|
- Picosat::picosat_set_global_default_phase(1);
|
|
+ Picosat::picosat_set_global_default_phase(picosat_inst, 1);
|
|
|
|
fillSatChecker(_sat);
|
|
|
|
- int res = Picosat::picosat_sat(-1);
|
|
+ int res = Picosat::picosat_sat(picosat_inst, -1);
|
|
|
|
if (res == PICOSAT_SATISFIABLE) {
|
|
/* Let's get the assigment out of picosat, because we have to
|
|
reset the sat solver afterwards */
|
|
std::map<std::string, int>::const_iterator it;
|
|
for (it = symbolTable.begin(); it != symbolTable.end(); ++it) {
|
|
- bool selected = Picosat::picosat_deref(it->second) == 1;
|
|
+ bool selected = Picosat::picosat_deref(picosat_inst, it->second) == 1;
|
|
assignmentTable.insert(std::make_pair(it->first, selected));
|
|
}
|
|
}
|
|
|
|
- Picosat::picosat_reset();
|
|
-
|
|
+ Picosat::picosat_reset(picosat_inst);
|
|
+ picosat_inst = NULL;
|
|
|
|
if (res == PICOSAT_UNSATISFIABLE)
|
|
return false;
|