#include "order.h"
#include "predicate.h"
#include "set.h"
+#include "tunable.h"
SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
solver(_solver),
- vector(allocDefVectorEdge()) {
+ vector(allocDefVectorEdge()) {
}
SATEncoder::~SATEncoder() {
booledgeMap.reset();
}
-int SATEncoder::solve() {
+int SATEncoder::solve(long timeout) {
+ cnf->solver->timeout = timeout;
return solveCNF(cnf);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+ if (csolver->isUnSAT()) {
+ return;
+ }
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
case PREDICATEOP:
result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
break;
+ case BOOLCONST:
+ result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
+ break;
default:
model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
exit(-1);
}
- if (constraint->parents.getSize() > 1) {
+ Polarity p = constraint->polarity;
+ uint pSize = constraint->parents.getSize();
+
+ if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
Edge e = getNewVarSATEncoder();
- generateProxy(cnf, result, e, constraint->polarity);
+ generateProxy(cnf, result, e, p);
booledgeMap.put(constraint, e.node_ptr);
result = e;
}