Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
void deleteBoolean(Boolean * This);
+inline FunctionEncoding* getPredicateFunctionEncoding(BooleanPredicate* func){
+ return &func->encoding;
+}
+
#endif
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; i<size; i++){
- if( getElementEncoding(elemSet)->encodingArray[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);
return NULL;
}
+
+inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func){
+ return &func->functionencoding;
+}
+
uint getElementSize(Element* This);
Constraint * getElementValueConstraint(Element* This, uint64_t value);
#endif
#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;
}
void deleteTable(Table* table){
- deleteInlineArrayElement(&table->domains);
+ deleteInlineArraySet(&table->domains);
uint size = getSizeVectorTableEntry(&table->entries);
for(uint i=0; i<size; i++){
deleteTableEntry(getVectorTableEntry(&table->entries, i));
#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
#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;
}
Boolean *constraint=getVectorBoolean(constraints, i);
encodeConstraintSATEncoder(This, constraint);
}
+
+ size = getSizeVectorElement(csolver->allElements);
+ for(uint i=0; i<size; i++){
+ Element* element = getVectorElement(csolver->allElements, 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) {
}
}
+void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
+ for(uint i=0;i<num;i++)
+ carray[i]=getNewVarSATEncoder(encoder);
+}
+
Constraint * getNewVarSATEncoder(SATEncoder *This) {
Constraint * var=allocVarConstraint(VAR, This->varcount);
Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
setNegConstraint(var, varneg);
setNegConstraint(varneg, var);
+ pushVectorConstraint(getSATEncoderVars(This), var);
return var;
}
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; i<size; i++){
+ TableEntry* entry = getVectorTableEntry(&table->entries, i);
+ uint inputNum =getSizeArrayElement(elements);
+ Element* el= getArrayElement(elements, i);
+ Constraint* carray[inputNum];
+ for(uint j=0; j<inputNum; j++){
+ carray[inputNum] = getElementValueConstraint(el, entry->inputs[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
#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
#include "common.h"
#include "naiveencoder.h"
#include "element.h"
+#include "satencoder.h"
void initElementEncoding(ElementEncoding * This, Element *element) {
This->element=element;
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){
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
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);
#include "boolean.h"
#include "table.h"
#include "tableentry.h"
-//THIS FILE SHOULD HAVE NOTHING TO DO WITH CONSTRAINTS...
-//#include "constraint.h"
#include <strings.h>
-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; i<size; i++){
Element* element = getVectorElement(csolver->allElements, 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);
Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
switch(GETBOOLEANTYPE(predicate)){
case PREDICATEOP:
- setFunctionEncodingType(getFunctionEncoding(predicate), ENUMERATEIMPLICATIONS);
+ setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)predicate),
+ ENUMERATEIMPLICATIONS);
break;
default:
continue;
}
}
-
-// THIS SHOULD NOT BE HERE
-/*
-void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray) {
- for(uint i=0;i<num;i++)
- carray[i]=getNewVar(encoder);
-}
-*/
-
-// THIS SHOULD NOT BE HERE
-/*
-Constraint * getNewVar(NaiveEncoder* encoder) {
- Constraint* var = allocVarConstraint(VAR, encoder->varindex);
- 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);
}
-void encode(CSolver* csolver){
- NaiveEncoder* encoder = allocNaiveEncoder();
- naiveEncodingDecision( csolver, encoder);
- uint size = getSizeVectorElement(csolver->allElements);
- for(uint i=0; i<size; i++){
- Element* element = getVectorElement(csolver->allElements, i);
- switch(GETELEMENTTYPE(element)){
- case ELEMFUNCRETURN:
- naiveEncodeFunctionPredicate(encoder, getFunctionEncoding(element));
- break;
- default:
- continue;
- }
- }
-
- size = getSizeVectorBoolean(csolver->allBooleans);
- for(uint i=0; i<size; i++){
- Boolean* predicate = getVectorBoolean(csolver->allBooleans, 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; i<size; i++){
- TableEntry* entry = getVectorTableEntry(&table->entries, i);
- uint inputNum =getSizeArrayElement(elements);
- Element* el= getArrayElement(elements, i);
- Constraint* carray[inputNum];
- for(uint j=0; j<inputNum; j++){
- carray[inputNum] = getElementValueConstraint(el, entry->inputs[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);
-}
#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
struct TableEntry;
typedef struct TableEntry TableEntry;
-struct NaiveEncoder;
-typedef struct NaiveEncoder NaiveEncoder;
typedef unsigned int uint;
typedef uint64_t VarType;
#endif
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;
/** 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. */