From: Hamed Date: Wed, 28 Jun 2017 02:08:44 +0000 (-0700) Subject: Fix some bugs, Moving backend codes to SATEncoder X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=4b6277a81c50609abbe7b19a49e641a2d189060a;p=satune.git Fix some bugs, Moving backend codes to SATEncoder --- diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 411af26..297c383 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -51,4 +51,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize); void deleteBoolean(Boolean * This); +inline FunctionEncoding* getPredicateFunctionEncoding(BooleanPredicate* func){ + return &func->encoding; +} + #endif diff --git a/src/AST/element.c b/src/AST/element.c index f219072..5b9d847 100644 --- a/src/AST/element.c +++ b/src/AST/element.c @@ -44,16 +44,17 @@ Constraint * getElementValueConstraint(Element* This, uint64_t value) { switch(GETELEMENTTYPE(This)){ case ELEMSET: ; //Statement is needed for a label and This is a NOPE - ElementSet* elemSet= ((ElementSet*)This); - uint size = getSetSize(elemSet->set); + uint size = getSetSize(((ElementSet*)This)->set); + //FIXME for(uint i=0; iencodingArray[i]==value){ - return generateBinaryConstraint(getElementEncoding(elemSet)->numVars, - getElementEncoding(elemSet)->variables, i); + if( getElementEncoding(This)->encodingArray[i]==value){ + return generateBinaryConstraint(getElementEncoding(This)->numVars, + getElementEncoding(This)->variables, i); } } break; case ELEMFUNCRETURN: + ASSERT(0); break; default: ASSERT(0); diff --git a/src/AST/element.h b/src/AST/element.h index c0eeaf5..3f9693a 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -47,6 +47,11 @@ inline ElementEncoding* getElementEncoding(Element* This){ return NULL; } + +inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func){ + return &func->functionencoding; +} + uint getElementSize(Element* This); Constraint * getElementValueConstraint(Element* This, uint64_t value); #endif diff --git a/src/AST/table.c b/src/AST/table.c index a8af588..a0b1e6f 100644 --- a/src/AST/table.c +++ b/src/AST/table.c @@ -6,9 +6,9 @@ #include "mutableset.h" -Table * allocTable(Element **domains, uint numDomain, Element * range){ +Table * allocTable(Set **domains, uint numDomain, Set * range){ Table* table = (Table*) ourmalloc(sizeof(Table)); - allocInlineArrayInitElement(&table->domains, domains, numDomain); + allocInlineArrayInitSet(&table->domains, domains, numDomain); allocInlineDefVectorTableEntry(&table->entries); table->range =range; return table; @@ -20,7 +20,7 @@ void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t r } void deleteTable(Table* table){ - deleteInlineArrayElement(&table->domains); + deleteInlineArraySet(&table->domains); uint size = getSizeVectorTableEntry(&table->entries); for(uint i=0; ientries, i)); diff --git a/src/AST/table.h b/src/AST/table.h index fa83b06..90f5001 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -5,12 +5,12 @@ #include "structs.h" struct Table { - ArrayElement domains; - Element * range; + ArraySet domains; + Set * range; VectorTableEntry entries; }; -Table * allocTable(Element **domains, uint numDomain, Element * range); +Table * allocTable(Set **domains, uint numDomain, Set * range); void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result); void deleteTable(Table* table); #endif diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index 37d3bc7..325b614 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -4,9 +4,16 @@ #include "boolean.h" #include "constraint.h" #include "common.h" +#include "element.h" +#include "function.h" +#include "tableentry.h" +#include "table.h" + SATEncoder * allocSATEncoder() { SATEncoder *This=ourmalloc(sizeof (SATEncoder)); + allocInlineDefVectorConstraint(getSATEncoderAllConstraints(This)); + allocInlineDefVectorConstraint(getSATEncoderVars(This)); This->varcount=1; return This; } @@ -22,6 +29,20 @@ void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) { Boolean *constraint=getVectorBoolean(constraints, i); encodeConstraintSATEncoder(This, constraint); } + + size = getSizeVectorElement(csolver->allElements); + for(uint i=0; iallElements, i); + switch(GETELEMENTTYPE(element)){ + case ELEMFUNCRETURN: + encodeFunctionElementSATEncoder(This, (ElementFunction*) element); + break; + default: + continue; + //ElementSets that aren't used in any constraints/functions + //will be eliminated. + } + } } Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { @@ -40,11 +61,17 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) { } } +void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) { + for(uint i=0;ivarcount); Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++); setNegConstraint(var, varneg); setNegConstraint(varneg, var); + pushVectorConstraint(getSATEncoderVars(This), var); return var; } @@ -92,5 +119,56 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { //TO IMPLEMENT + + return NULL; +} + +Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){ + switch(GETFUNCTIONTYPE(This->function)){ + case TABLEFUNC: + return encodeTableElementFunctionSATEncoder(encoder, This); + case OPERATORFUNC: + return encodeOperatorElementFunctionSATEncoder(encoder, This); + default: + ASSERT(0); + } + //FIXME + return NULL; +} + +Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ + switch(getElementFunctionEncoding(This)->type){ + case ENUMERATEIMPLICATIONS: + return encodeEnumTableElemFunctionSATEncoder(encoder, This); + break; + default: + ASSERT(0); + } + //FIXME return NULL; } + +Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This){ + return NULL; +} + +Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){ + ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC); + ArrayElement* elements= &This->inputs; + Table* table = ((FunctionTable*) (This->function))->table; + uint size = getSizeVectorTableEntry(&table->entries); + for(uint i=0; ientries, i); + uint inputNum =getSizeArrayElement(elements); + Element* el= getArrayElement(elements, i); + Constraint* carray[inputNum]; + for(uint j=0; jinputs[j]); + } + Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), + getElementValueConstraint((Element*)This, entry->output)); + pushVectorConstraint( getSATEncoderAllConstraints(encoder), row); + } + //FIXME + return NULL; +} \ No newline at end of file diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 5382bc5..dcc6546 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -2,18 +2,34 @@ #define SATENCODER_H #include "classlist.h" +#include "structs.h" struct SATEncoder { uint varcount; + //regarding managing memory + VectorConstraint vars; + VectorConstraint allConstraints; }; +inline VectorConstraint* getSATEncoderVars(SATEncoder* ne){ + return &ne->vars; +} +inline VectorConstraint* getSATEncoderAllConstraints(SATEncoder* ne){ + return &ne->allConstraints; +} SATEncoder * allocSATEncoder(); void deleteSATEncoder(SATEncoder *This); void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver); Constraint * getNewVarSATEncoder(SATEncoder *This); +void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray); Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); + +Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This); +Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); +Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); +Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This); #endif diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c index fc76a4a..7b3ebdd 100644 --- a/src/Encoders/elementencoding.c +++ b/src/Encoders/elementencoding.c @@ -2,6 +2,7 @@ #include "common.h" #include "naiveencoder.h" #include "element.h" +#include "satencoder.h" void initElementEncoding(ElementEncoding * This, Element *element) { This->element=element; @@ -38,14 +39,14 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){ This->type = type; } -void generateBinaryIndexEncodingVars(NaiveEncoder* encoder, ElementEncoding* This){ +void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This){ ASSERT(This->type==BINARYINDEX); uint size = getElementSize(This->element); allocElementConstraintVariables(This, NUMBITS(size-1)); - getArrayNewVars(encoder, This->numVars, This->variables); + getArrayNewVarsSATEncoder(encoder, This->numVars, This->variables); } -void generateElementEncodingVariables(NaiveEncoder* encoder, ElementEncoding* This){ +void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){ ASSERT(This->type!=ELEM_UNASSIGNED); ASSERT(This->variables==NULL); switch(This->type){ diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index ffdb0d0..f04ba7e 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -33,7 +33,7 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) { This->inUseArray[(offset>>6)] |= 1 << (offset & 63); } -void generateBinaryIndexEncodingVars(NaiveEncoder* encode, ElementEncoding* This); -void generateElementEncodingVariables(NaiveEncoder* encoder, ElementEncoding* This); +void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This); +void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This); #endif diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h index 60690e3..a352139 100644 --- a/src/Encoders/functionencoding.h +++ b/src/Encoders/functionencoding.h @@ -21,18 +21,6 @@ struct FunctionEncoding { ElementPredicate op; }; -inline FunctionEncoding* getFunctionEncoding(ASTNode func){ - switch(GETASTNODETYPE(func)){ - case ELEMFUNCRETURN: - return &((ElementFunction*)func)->functionencoding; - case PREDICATEOP: - return &((BooleanPredicate*)func)->encoding; - default: - ASSERT(0); - } - return NULL; -} - void initFunctionEncoding(FunctionEncoding *encoding, Element *function); void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate); void setFunctionEncodingType(FunctionEncoding* encoding, FunctionEncodingType type); diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c index a4f46a5..1ea5857 100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@ -10,30 +10,24 @@ #include "boolean.h" #include "table.h" #include "tableentry.h" -//THIS FILE SHOULD HAVE NOTHING TO DO WITH CONSTRAINTS... -//#include "constraint.h" #include -NaiveEncoder* allocNaiveEncoder(){ - NaiveEncoder* encoder = (NaiveEncoder*) ourmalloc(sizeof(NaiveEncoder)); - allocInlineDefVectorConstraint(GETNAIVEENCODERALLCONSTRAINTS(encoder)); - allocInlineDefVectorConstraint(GETNAIVEENCODERVARS(encoder)); - encoder->varindex=0; - return encoder; -} -void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){ +void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){ uint size = getSizeVectorElement(csolver->allElements); for(uint i=0; iallElements, i); switch(GETELEMENTTYPE(element)){ case ELEMSET: setElementEncodingType(getElementEncoding(element), BINARYINDEX); + //FIXME:Should be moved to SATEncoder baseBinaryIndexElementAssign(getElementEncoding(element)); generateElementEncodingVariables(encoder,getElementEncoding(element)); + // break; case ELEMFUNCRETURN: - setFunctionEncodingType(getFunctionEncoding(element), ENUMERATEIMPLICATIONS); + setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element), + ENUMERATEIMPLICATIONS); break; default: ASSERT(0); @@ -45,7 +39,8 @@ void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){ Boolean* predicate = getVectorBoolean(csolver->allBooleans, i); switch(GETBOOLEANTYPE(predicate)){ case PREDICATEOP: - setFunctionEncodingType(getFunctionEncoding(predicate), ENUMERATEIMPLICATIONS); + setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)predicate), + ENUMERATEIMPLICATIONS); break; default: continue; @@ -53,28 +48,6 @@ void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){ } } - -// THIS SHOULD NOT BE HERE -/* -void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray) { - for(uint i=0;ivarindex); - Constraint* notVar = allocVarConstraint(NOTVAR, encoder->varindex); - setNegConstraint(var, notVar); - setNegConstraint(notVar, var); - pushVectorConstraint(GETNAIVEENCODERVARS(encoder), var); - encoder->varindex++; - return var; -} -*/ - void baseBinaryIndexElementAssign(ElementEncoding *This) { Element * element=This->element; ASSERT(element->type == ELEMSET); @@ -96,98 +69,3 @@ void baseBinaryIndexElementAssign(ElementEncoding *This) { } -void encode(CSolver* csolver){ - NaiveEncoder* encoder = allocNaiveEncoder(); - naiveEncodingDecision( csolver, encoder); - uint size = getSizeVectorElement(csolver->allElements); - for(uint i=0; iallElements, i); - switch(GETELEMENTTYPE(element)){ - case ELEMFUNCRETURN: - naiveEncodeFunctionPredicate(encoder, getFunctionEncoding(element)); - break; - default: - continue; - } - } - - size = getSizeVectorBoolean(csolver->allBooleans); - for(uint i=0; iallBooleans, i); - switch(GETBOOLEANTYPE(predicate)){ - case PREDICATEOP: - naiveEncodeFunctionPredicate(encoder, getFunctionEncoding(predicate)); - break; - default: - continue; - } - } -} - -void naiveEncodeFunctionPredicate(NaiveEncoder* encoder, FunctionEncoding *This){ - if(This->isFunction) { - ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN); - switch(This->type){ - case ENUMERATEIMPLICATIONS: - naiveEncodeEnumeratedFunction(encoder, This); - break; - case CIRCUIT: - naiveEncodeCircuitFunction(encoder, This); - break; - default: - ASSERT(0); - } - }else { - ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP); - BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate; - //FIXME - - } -} - -void naiveEncodeEnumeratedFunction(NaiveEncoder* encoder, FunctionEncoding* This){ - ElementFunction* ef =(ElementFunction*)This->op.function; - switch(GETFUNCTIONTYPE(ef->function)){ - case TABLEFUNC: - naiveEncodeEnumTableFunc(encoder, ef); - break; - case OPERATORFUNC: - naiveEncodeEnumOperatingFunc(encoder, ef); - break; - default: - ASSERT(0); - } -} - -void naiveEncodeEnumTableFunc(NaiveEncoder* encoder, ElementFunction* This){ - ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC); - ArrayElement* elements= &This->inputs; - Table* table = ((FunctionTable*) (This->function))->table; - uint size = getSizeVectorTableEntry(&table->entries); - for(uint i=0; ientries, i); - uint inputNum =getSizeArrayElement(elements); - Element* el= getArrayElement(elements, i); - Constraint* carray[inputNum]; - for(uint j=0; jinputs[j]); - } - Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), - getElementValueConstraint(table->range, entry->output)); - pushVectorConstraint( GETNAIVEENCODERALLCONSTRAINTS(encoder), row); - } - -} - -void naiveEncodeEnumOperatingFunc(NaiveEncoder* encoder, ElementFunction* This){ - -} - - -void naiveEncodeCircuitFunction(NaiveEncoder* encoder, FunctionEncoding* This){ - -} - -void deleteNaiveEncoder(NaiveEncoder* encoder){ - deleteVectorArrayConstraint(&encoder->vars); -} diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h index d3c409c..800860c 100644 --- a/src/Encoders/naiveencoder.h +++ b/src/Encoders/naiveencoder.h @@ -3,28 +3,15 @@ #include "classlist.h" #include "structs.h" -#define GETNAIVEENCODERVARS(ne) (&((NaiveEncoder*)ne)->vars) -#define GETNAIVEENCODERALLCONSTRAINTS(ne) (&((NaiveEncoder*)ne)->allConstraints) -struct NaiveEncoder{ - uint varindex; - VectorConstraint vars; - VectorConstraint allConstraints; -}; -NaiveEncoder* allocNaiveEncoder(); -Constraint* getNewVar(NaiveEncoder* encoder); -void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray); -//For now, This function just simply goes through elements/functions and -//assigns a predefined Encoding to each of them -void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder); -void encode(CSolver* csolver); +/** + *For now, This function just simply goes through elements/functions and + *assigns a predefined Encoding to each of them + * @param csolver + * @param encoder + */ +void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder); void baseBinaryIndexElementAssign(ElementEncoding *This); -void naiveEncodeFunctionPredicate(NaiveEncoder* encoder, FunctionEncoding *This); -void naiveEncodeCircuitFunction(NaiveEncoder* encoder, FunctionEncoding* This); -void naiveEncodeEnumeratedFunction(NaiveEncoder* encoder, FunctionEncoding* This); -void naiveEncodeEnumTableFunc(NaiveEncoder* encoder, ElementFunction* This); -void naiveEncodeEnumOperatingFunc(NaiveEncoder* encoder, ElementFunction* This); -void deleteNaiveEncoder(NaiveEncoder* encoder); #endif diff --git a/src/classlist.h b/src/classlist.h index a707845..3c7d071 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -82,8 +82,6 @@ typedef struct OrderEncoding OrderEncoding; struct TableEntry; typedef struct TableEntry TableEntry; -struct NaiveEncoder; -typedef struct NaiveEncoder NaiveEncoder; typedef unsigned int uint; typedef uint64_t VarType; #endif diff --git a/src/csolver.c b/src/csolver.c index ccb19f0..5f330fd 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -122,7 +122,7 @@ Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, u return predicate; } -Table * createTable(CSolver *solver, Element **domains, uint numDomain, Element * range) { +Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range) { Table* table= allocTable(domains,numDomain,range); pushVectorTable(solver->allTables, table); return table; diff --git a/src/csolver.h b/src/csolver.h index 0bd2088..495d386 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -79,7 +79,7 @@ Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, u /** This function creates an empty instance table.*/ -Table * createTable(CSolver *solver, Element **domains, uint numDomain, Element * range); +Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range); /** This function adds an input output relation to a table. */