From: bdemsky <bdemsky@uci.edu>
Date: Wed, 12 Jul 2017 03:22:29 +0000 (-0700)
Subject: Add CIRCUIT Encoding for Equals
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f8f96c5249608261ceb234c1331ac22badb3cc8e;p=satune.git

Add CIRCUIT Encoding for Equals
---

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 801d4ff..8938824 100644
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -56,6 +56,35 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 	return E_BOGUS;
 }
 
+Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
+	PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
+	
+	switch(predicate->op) {
+	case EQUALS: {
+		return encodeCircuitEquals(This, constraint);
+	}
+	default:
+		ASSERT(0);
+	}
+	exit(-1);
+}
+
+Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
+	PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
+	ASSERT(getSizeArraySet(&predicate->domains) == 2);
+	Element *elem0 = getArrayElement( &constraint->inputs, 0);
+	Element *elem1 = getArrayElement( &constraint->inputs, 1);
+	ElementEncoding *ee0=getElementEncoding(elem0);
+	ElementEncoding *ee1=getElementEncoding(elem1);
+	ASSERT(ee0->numVars==ee1->numVars);
+	uint numVars=ee0->numVars;
+	Edge carray[numVars];
+	for (uint i=0; i<numVars; i++) {
+		carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
+	}
+	return constraintAND(This->cnf, numVars, carray);
+}
+
 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 	PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
 	uint numDomains=getSizeArraySet(&predicate->domains);
diff --git a/src/Backend/satfuncencoder.h b/src/Backend/satfuncencoder.h
index b24fc1f..02dc858 100644
--- a/src/Backend/satfuncencoder.h
+++ b/src/Backend/satfuncencoder.h
@@ -6,5 +6,7 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 void encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint);
+Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint);
 
 #endif
diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 385f5c2..72cae3d 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -28,6 +28,7 @@ void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
 void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
 void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
+static inline uint numEncodingVars(ElementEncoding *This) {return This->numVars;}
 
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {
 	return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;