From f8f96c5249608261ceb234c1331ac22badb3cc8e Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 20:22:29 -0700 Subject: [PATCH] Add CIRCUIT Encoding for Equals --- src/Backend/satfuncencoder.c | 29 +++++++++++++++++++++++++++++ src/Backend/satfuncencoder.h | 2 ++ src/Encoders/elementencoding.h | 1 + 3 files changed, 32 insertions(+) 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; icnf, 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; -- 2.34.1