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;