projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Adding checks to avoid further processing on UNSAT Problems
[satune.git]
/
src
/
Backend
/
satencoder.cc
diff --git
a/src/Backend/satencoder.cc
b/src/Backend/satencoder.cc
index b6e8da1f515741a35d7bd4302ceb11ec70212609..618b8c17c22114177393754313dda6a3c1d8aa5c 100644
(file)
--- a/
src/Backend/satencoder.cc
+++ b/
src/Backend/satencoder.cc
@@
-11,11
+11,12
@@
#include "order.h"
#include "predicate.h"
#include "set.h"
#include "order.h"
#include "predicate.h"
#include "set.h"
+#include "tunable.h"
SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
solver(_solver),
SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
solver(_solver),
- vector(allocDefVectorEdge()) {
+
vector(allocDefVectorEdge()) {
}
SATEncoder::~SATEncoder() {
}
SATEncoder::~SATEncoder() {
@@
-28,11
+29,15
@@
void SATEncoder::resetSATEncoder() {
booledgeMap.reset();
}
booledgeMap.reset();
}
-int SATEncoder::solve() {
+int SATEncoder::solve(long timeout) {
+ cnf->solver->timeout = timeout;
return solveCNF(cnf);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
return solveCNF(cnf);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+ if(csolver->isUnSAT()){
+ return;
+ }
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
@@
-64,13
+69,19
@@
Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
case PREDICATEOP:
result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
break;
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);
}
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();
Edge e = getNewVarSATEncoder();
- generateProxy(cnf, result, e,
constraint->polarity
);
+ generateProxy(cnf, result, e,
p
);
booledgeMap.put(constraint, e.node_ptr);
result = e;
}
booledgeMap.put(constraint, e.node_ptr);
result = e;
}