X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.cc;h=00219efe24ece732c6aeb57ed3ba450ded890dee;hb=dd394251eb1578f17507f5da84791113e1e9cef7;hp=1fe98ce398af1bf4e54b854b410448b72552914d;hpb=cb887a9e8e6cc23c2e09638a1f7bceed4ce1868a;p=satune.git

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
old mode 100644
new mode 100755
index 1fe98ce..00219ef
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -11,21 +11,33 @@
 #include "order.h"
 #include "predicate.h"
 #include "set.h"
+#include "tunable.h"
 
 SATEncoder::SATEncoder(CSolver *_solver) :
 	cnf(createCNF()),
-	solver(_solver) {
+	solver(_solver),
+	vector(allocDefVectorEdge()) {
 }
 
 SATEncoder::~SATEncoder() {
 	deleteCNF(cnf);
+	deleteVectorEdge(vector);
 }
 
-int SATEncoder::solve() {
+void SATEncoder::resetSATEncoder() {
+	resetCNF(cnf);
+	booledgeMap.reset();
+}
+
+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();
@@ -37,7 +49,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
 
 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
 	Edge result;
-	Boolean * constraint = c.getBoolean();
+	Boolean *constraint = c.getBoolean();
 
 	if (booledgeMap.contains(constraint)) {
 		Edge e = {(Node *) booledgeMap.get(constraint)};
@@ -57,11 +69,23 @@ 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);
 	}
-	booledgeMap.put(constraint, result.node_ptr);
+	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, p);
+		booledgeMap.put(constraint, e.node_ptr);
+		result = e;
+	}
+
 	return c.isNegated() ? constraintNegate(result) : result;
 }
 
@@ -92,11 +116,12 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
 	case SATC_NOT:
 		return constraintNegate(array[0]);
 	case SATC_IFF:
+		ASSERT(constraint->inputs.getSize() == 2);
 		return constraintIFF(cnf, array[0], array[1]);
 	case SATC_OR:
 	case SATC_XOR:
 	case SATC_IMPLIES:
-		//Don't handle, translate these away...
+	//Don't handle, translate these away...
 	default:
 		model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 		exit(-1);
@@ -131,7 +156,7 @@ Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 
 void SATEncoder::encodeElementSATEncoder(Element *element) {
 	/* Check to see if we have already encoded this element. */
-	if (getElementEncoding(element)->variables != NULL)
+	if (element->getElementEncoding()->variables != NULL)
 		return;
 
 	/* Need to encode. */
@@ -164,7 +189,7 @@ void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
-	switch (getElementFunctionEncoding(function)->type) {
+	switch (function->getElementFunctionEncoding()->type) {
 	case ENUMERATEIMPLICATIONS:
 		encodeEnumTableElemFunctionSATEncoder(function);
 		break;