#include "tableentry.h"
#include "table.h"
#include "order.h"
+#include "predicate.h"
+#include "set.h"
+#include "satfuncopencoder.h"
+//TODO: Should handle sharing of AST Nodes without recoding them a second time
-SATEncoder * allocSATEncoder() {
- SATEncoder *This=ourmalloc(sizeof (SATEncoder));
- This->varcount=1;
+SATEncoder *allocSATEncoder() {
+ SATEncoder *This = ourmalloc(sizeof (SATEncoder));
+ This->varcount = 1;
+ This->cnf = createCNF();
return This;
}
void deleteSATEncoder(SATEncoder *This) {
+ deleteCNF(This->cnf);
ourfree(This);
}
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
- /** We really should not walk the free list to generate constraint
- variables...walk the constraint tree instead. Or even better
- yet, just do this as you need to during the encodeAllSATEncoder
- walk. */
-
-// FIXME!!!!(); // Make sure Hamed sees comment above
-
- uint size = getSizeVectorElement(csolver->allElements);
- for(uint i=0; i<size; i++){
- Element* element = getVectorElement(csolver->allElements, i);
- generateElementEncodingVariables(This,getElementEncoding(element));
+void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
+ VectorBoolean *constraints = csolver->constraints;
+ uint size = getSizeVectorBoolean(constraints);
+ for (uint i = 0; i < size; i++) {
+ model_print("Encoding All ...\n\n");
+ Boolean *constraint = getVectorBoolean(constraints, i);
+ Edge c = encodeConstraintSATEncoder(This, constraint);
+ model_print("Returned Constraint in EncodingAll:\n");
+ addConstraintCNF(This->cnf, c);
}
}
-
-Constraint * getElementValueConstraint(Element* This, uint64_t value) {
- switch(getElementEncoding(This)->type){
- case ONEHOT:
- ASSERT(0);
- break;
- case UNARY:
- ASSERT(0);
- break;
- case BINARYINDEX:
- ASSERT(0);
- break;
- case ONEHOTBINARY:
- return getElementValueBinaryIndexConstraint(This, value);
- break;
- case BINARYVAL:
- ASSERT(0);
- break;
- default:
- ASSERT(0);
- break;
- }
- return NULL;
-}
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
- ASTNodeType type = GETELEMENTTYPE(This);
- ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
- ElementEncoding* elemEnc = getElementEncoding(This);
- for(uint i=0; i<elemEnc->encArraySize; i++){
- if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
- return generateBinaryConstraint(elemEnc->numVars,
- elemEnc->variables, i);
- }
- }
- ASSERT(0);
- return NULL;
-}
-
-void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
- VectorBoolean *constraints=csolver->constraints;
- uint size=getSizeVectorBoolean(constraints);
- for(uint i=0;i<size;i++) {
- 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) {
- switch(GETBOOLEANTYPE(constraint)) {
+Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+ switch (GETBOOLEANTYPE(constraint)) {
case ORDERCONST:
return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
case BOOLEANVAR:
}
}
-void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
- for(uint i=0;i<num;i++)
- carray[i]=getNewVarSATEncoder(encoder);
+void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *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);
- return var;
+Edge getNewVarSATEncoder(SATEncoder *This) {
+ return constraintNewVar(This->cnf);
}
-Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
- if (constraint->var == NULL) {
- constraint->var=getNewVarSATEncoder(This);
+Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
+ if (edgeIsNull(constraint->var)) {
+ constraint->var = getNewVarSATEncoder(This);
}
return constraint->var;
}
-Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
- Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
- for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
- array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
+Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
+ Edge array[getSizeArrayBoolean(&constraint->inputs)];
+ for (uint i = 0; i < getSizeArrayBoolean(&constraint->inputs); i++)
+ array[i] = encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
- switch(constraint->op) {
+ switch (constraint->op) {
case L_AND:
- return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
+ return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
case L_OR:
- return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
+ return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
case L_NOT:
- ASSERT(constraint->numArray==1);
- return negateConstraint(array[0]);
- case L_XOR: {
- ASSERT(constraint->numArray==2);
- Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
- Constraint * nright=negateConstraint(cloneConstraint(array[1]));
- return allocConstraint(OR,
- allocConstraint(AND, array[0], nright),
- allocConstraint(AND, nleft, array[1]));
- }
+ ASSERT( getSizeArrayBoolean(&constraint->inputs) == 1);
+ return constraintNegate(array[0]);
+ case L_XOR:
+ ASSERT( getSizeArrayBoolean(&constraint->inputs) == 2);
+ return constraintXOR(This->cnf, array[0], array[1]);
case L_IMPLIES:
- ASSERT(constraint->numArray==2);
- return allocConstraint(IMPLIES, array[0], array[1]);
+ ASSERT( getSizeArrayBoolean( &constraint->inputs) == 2);
+ return constraintIMPLIES(This->cnf, array[0], array[1]);
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
exit(-1);
}
}
-Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
- if(constraint->var== NULL){
- constraint->var = getNewVarSATEncoder(This);
+Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+ switch (GETPREDICATETYPE(constraint->predicate) ) {
+ case TABLEPRED:
+ return encodeTablePredicateSATEncoder(This, constraint);
+ case OPERATORPRED:
+ return encodeOperatorPredicateSATEncoder(This, constraint);
+ default:
+ ASSERT(0);
}
- return constraint->var;
+ return E_BOGUS;
}
-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);
+Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+ switch (constraint->encoding.type) {
+ case ENUMERATEIMPLICATIONS:
+ case ENUMERATEIMPLICATIONSNEGATE:
+ return encodeEnumTablePredicateSATEncoder(This, constraint);
+ case CIRCUIT:
+ ASSERT(0);
+ break;
+ default:
+ ASSERT(0);
}
- return NULL;
-}
-
-Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
- switch(getElementFunctionEncoding(This)->type){
- case ENUMERATEIMPLICATIONS:
- return encodeEnumTableElemFunctionSATEncoder(encoder, This);
- break;
- case CIRCUIT:
- ASSERT(0);
- break;
- default:
- ASSERT(0);
+ return E_BOGUS;
+}
+
+void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
+ switch ( GETELEMENTTYPE(This) ) {
+ case ELEMFUNCRETURN:
+ generateElementEncoding(encoder, This);
+ encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
+ break;
+ case ELEMSET:
+ generateElementEncoding(encoder, This);
+ return;
+ case ELEMCONST:
+ return;
+ default:
+ ASSERT(0);
}
- return NULL;
}
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
- //FIXME: for now it just adds/substracts inputs exhustively
- return NULL;
+void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
+ switch (GETFUNCTIONTYPE(This->function)) {
+ case TABLEFUNC:
+ encodeTableElementFunctionSATEncoder(encoder, This);
+ break;
+ case OPERATORFUNC:
+ encodeOperatorElementFunctionSATEncoder(encoder, This);
+ break;
+ default:
+ ASSERT(0);
+ }
}
-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);
- Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any 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),
- getElementValueBinaryIndexConstraint((Element*)This, entry->output));
- constraints[i]=row;
+void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
+ switch (getElementFunctionEncoding(This)->type) {
+ case ENUMERATEIMPLICATIONS:
+ encodeEnumTableElemFunctionSATEncoder(encoder, This);
+ break;
+ case CIRCUIT:
+ ASSERT(0);
+ break;
+ default:
+ ASSERT(0);
}
- Constraint* result = allocArrayConstraint(OR, size, constraints);
- return result;
}
projects / satune.git / blobdiff