Add CIRCUIT Encoding for Equals

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 801d4ffd7b925290e6d0c5e490ef1bef4f5c470c..89388249af184347248df967f4cf6236ef9e20e8 100644 (file)
--- 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 b24fc1f3c2b8889e71d2dcd46b0c7f8fcfc17254..02dc85878392fec8ce9a37cefd76def7bb310911 100644 (file)
--- 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 385f5c27d1fe66a4408987cc13a1995f2479119b..72cae3d21d70ff2f9b73f5a540bf3468ce421ba6 100644 (file)
--- 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;