X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.cc;h=618b8c17c22114177393754313dda6a3c1d8aa5c;hp=b6e8da1f515741a35d7bd4302ceb11ec70212609;hb=cbd921ee35b6a29934fd7cecccde7f160228af17;hpb=91c9fc86e8649796d0750572954054ab95432137

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index b6e8da1..618b8c1 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -11,11 +11,12 @@
 #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() {
@@ -28,11 +29,15 @@ void SATEncoder::resetSATEncoder() {
 	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();
@@ -64,13 +69,19 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
 	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;
 	}