SATEncoder * allocSATEncoder() {
SATEncoder *This=ourmalloc(sizeof (SATEncoder));
This->varcount=1;
- This->satSolver = allocIncrementalSolver();
+ This->cnf=createCNF();
return This;
}
void deleteSATEncoder(SATEncoder *This) {
- deleteIncrementalSolver(This->satSolver);
+ deleteCNF(This->cnf);
ourfree(This);
}
-Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64_t value) {
- generateElementEncodingVariables(encoder, getElementEncoding(This));
- switch(getElementEncoding(This)->type){
+Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
+ generateElementEncodingVariables(This, getElementEncoding(elem));
+ switch(getElementEncoding(elem)->type){
case ONEHOT:
//FIXME
ASSERT(0);
ASSERT(0);
break;
case BINARYINDEX:
- return getElementValueBinaryIndexConstraint(This, value);
+ return getElementValueBinaryIndexConstraint(This, elem, value);
break;
case ONEHOTBINARY:
ASSERT(0);
ASSERT(0);
break;
}
- return NULL;
+ return E_BOGUS;
}
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
- ASTNodeType type = GETELEMENTTYPE(This);
+
+Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
+ ASTNodeType type = GETELEMENTTYPE(elem);
ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
- ElementEncoding* elemEnc = getElementEncoding(This);
+ ElementEncoding* elemEnc = getElementEncoding(elem);
for(uint i=0; i<elemEnc->encArraySize; i++){
if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
- return generateBinaryConstraint(elemEnc->numVars,
- elemEnc->variables, i);
+ return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
}
}
- return NULL;
-}
-
-void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver) {
- VectorConstraint* simplified = simplifyConstraint(c);
- uint size = getSizeVectorConstraint(simplified);
- for(uint i=0; i<size; i++) {
- Constraint *simp=getVectorConstraint(simplified, i);
- if (simp->type==TRUE)
- continue;
- ASSERT(simp->type!=FALSE);
- dumpConstraint(simp, satSolver);
- freerecConstraint(simp);
- }
- deleteVectorConstraint(simplified);
+ return E_BOGUS;
}
void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
uint size=getSizeVectorBoolean(constraints);
for(uint i=0;i<size;i++) {
Boolean *constraint=getVectorBoolean(constraints, i);
- Constraint* c= encodeConstraintSATEncoder(This, constraint);
- printConstraint(c);
- model_print("\n\n");
- addConstraintToSATSolver(c, This->satSolver);
- //FIXME: When do we want to delete constraints? Should we keep an array of them
- // and delete them later, or it would be better to just delete them right away?
+ Edge c= encodeConstraintSATEncoder(This, constraint);
+ printCNF(c);
+ printf("\n");
+ addConstraint(This->cnf, c);
}
}
-Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
switch(GETBOOLEANTYPE(constraint)) {
case ORDERCONST:
return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
}
}
-void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
+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) {
+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)];
+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) {
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( getSizeArrayBoolean(&constraint->inputs)==1);
- return negateConstraint(array[0]);
- case L_XOR: {
+ return constraintNegate(array[0]);
+ case L_XOR:
ASSERT( getSizeArrayBoolean(&constraint->inputs)==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]));
- }
+ return constraintXOR(This->cnf, array[0], array[1]);
case L_IMPLIES:
ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
- return allocConstraint(IMPLIES, array[0], array[1]);
+ 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) {
+Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
switch( constraint->order->type){
case PARTIAL:
return encodePartialOrderSATEncoder(This, constraint);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
bool negate = false;
OrderPair flipped;
if (pair->first > pair->second) {
flipped.second=pair->first;
pair = &flipped; //FIXME: accessing a local variable from outside of the function?
}
- Constraint * constraint;
+ Edge constraint;
if (!containsBoolConst(table, pair)) {
constraint = getNewVarSATEncoder(This);
OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
} else
constraint = getBoolConst(table, pair)->constraint;
if (negate)
- return negateConstraint(constraint);
+ return constraintNegate(constraint);
else
return constraint;
}
-Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
+Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
ASSERT(boolOrder->order->type == TOTAL);
if(boolOrder->order->boolsToConstraints == NULL){
initializeOrderHashTable(boolOrder->order);
- return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+ createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
}
HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
- OrderPair pair={boolOrder->first, boolOrder->second, NULL};
- Constraint *constraint = getPairConstraint(This, boolToConsts, & pair);
+ OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
+ Edge constraint = getPairConstraint(This, boolToConsts, & pair);
return constraint;
}
-Constraint* createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
+void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
ASSERT(order->type == TOTAL);
VectorInt* mems = order->set->members;
HashTableBoolConst* table = order->boolsToConstraints;
uint size = getSizeVectorInt(mems);
- Constraint* constraints [size*size];
uint csize =0;
for(uint i=0; i<size; i++){
uint64_t valueI = getVectorInt(mems, i);
for(uint j=i+1; j<size;j++){
uint64_t valueJ = getVectorInt(mems, j);
OrderPair pairIJ = {valueI, valueJ};
- Constraint* constIJ=getPairConstraint(This, table, & pairIJ);
+ Edge constIJ=getPairConstraint(This, table, & pairIJ);
for(uint k=j+1; k<size; k++){
uint64_t valueK = getVectorInt(mems, k);
OrderPair pairJK = {valueJ, valueK};
OrderPair pairIK = {valueI, valueK};
- Constraint* constIK = getPairConstraint(This, table, & pairIK);
- Constraint* constJK = getPairConstraint(This, table, & pairJK);
- constraints[csize++] = generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK);
- ASSERT(csize < size*size);
+ Edge constIK = getPairConstraint(This, table, & pairIK);
+ Edge constJK = getPairConstraint(This, table, & pairJK);
+ addConstraint(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
}
}
}
- return allocArrayConstraint(AND, csize, constraints);
}
-Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
ASSERT(pair->first!= pair->second);
- Constraint* constraint= getBoolConst(table, pair)->constraint;
+ Edge constraint = getBoolConst(table, pair)->constraint;
if(pair->first > pair->second)
return constraint;
else
- return negateConstraint(constraint);
+ return constraintNegate(constraint);
}
-Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
- //FIXME: first we should add the the constraint to the satsolver!
- ASSERT(constIJ!= NULL && constJK != NULL && constIK != NULL);
- Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
- Constraint * loop1= allocArrayConstraint(OR, 3, carray);
- Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
- Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
- return allocConstraint(AND, loop1, loop2);
+Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
+ Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
+ Edge loop1= constraintOR(This->cnf, 3, carray);
+ Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
+ Edge loop2= constraintOR(This->cnf, 3, carray2 );
+ return constraintAND2(This->cnf, loop1, loop2);
}
-Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
+Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
// FIXME: we can have this implementation for partial order. Basically,
// we compute the transitivity between two order constraints specified by the client! (also can be used
// when client specify sparse constraints for the total order!)
if( containsBoolConst(boolToConsts, boolOrder) ){
return getBoolConst(boolToConsts, boolOrder);
} else {
- Constraint* constraint = getNewVarSATEncoder(This);
+ Edge constraint = getNewVarSATEncoder(This);
putBoolConst(boolToConsts,boolOrder, constraint);
VectorBoolean* orderConstrs = &boolOrder->order->constraints;
uint size= getSizeVectorBoolean(orderConstrs);
ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
BooleanOrder* newBool;
- Constraint* first, *second;
+ Edge first, second;
if(tmp->second==boolOrder->first){
newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
first = encodeTotalOrderSATEncoder(This, tmp);
second = encodeTotalOrderSATEncoder(This, tmp);
}else
continue;
- Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
+ Edge transConstr= encodeTotalOrderSATEncoder(This, newBool);
generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
}
return constraint;
}
*/
- return NULL;
+ return E_BOGUS;
}
-Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
+Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
switch(GETPREDICATETYPE(constraint->predicate) ){
case TABLEPRED:
return encodeTablePredicateSATEncoder(This, constraint);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
switch(constraint->encoding.type){
case ENUMERATEIMPLICATIONS:
case ENUMERATEIMPLICATIONSNEGATE:
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
FunctionEncodingType encType = constraint->encoding.type;
uint size = getSizeVectorTableEntry(entries);
- Constraint* constraints[size];
+ Edge constraints[size];
for(uint i=0; i<size; i++){
TableEntry* entry = getVectorTableEntry(entries, i);
if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
continue;
ArrayElement* inputs = &constraint->inputs;
uint inputNum =getSizeArrayElement(inputs);
- Constraint* carray[inputNum];
+ Edge carray[inputNum];
for(uint j=0; j<inputNum; j++){
Element* el = getArrayElement(inputs, j);
- Constraint* tmpc = getElementValueConstraint(This,el, entry->inputs[j]);
- ASSERT(tmpc!= NULL);
+ Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]);
if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
- Constraint* func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
- ASSERT(func!=NULL);
- carray[j] = allocConstraint(AND, func, tmpc);
+ Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
+ carray[j] = constraintAND2(This->cnf, func, tmpc);
} else {
carray[j] = tmpc;
}
- ASSERT(carray[j]!= NULL);
}
- constraints[i]=allocArrayConstraint(AND, inputNum, carray);
+ constraints[i]=constraintAND(This->cnf, inputNum, carray);
}
- Constraint* result= allocArrayConstraint(OR, size, constraints);
+ Edge result=constraintOR(This->cnf, size, constraints);
//FIXME: if it didn't match with any entry
- return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
+ return encType==ENUMERATEIMPLICATIONS? result: constraintNegate(result);
}
-Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
switch(constraint->encoding.type){
case ENUMERATEIMPLICATIONS:
return encodeEnumOperatorPredicateSATEncoder(This, constraint);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
ASSERT(predicate->op == EQUALS); //For now, we just only support equals
uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
uint64_t commonElements [size];
getEqualitySetIntersection(predicate, &size, commonElements);
- Constraint* carray[size];
+ Edge carray[size];
Element* elem1 = getArrayElement( &constraint->inputs, 0);
- Constraint *elemc1 = NULL, *elemc2 = NULL;
+ Edge elemc1 = E_NULL, elemc2 = E_NULL;
if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
Element* elem2 = getArrayElement( &constraint->inputs, 1);
if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
for(uint i=0; i<size; i++){
- Constraint* arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
- ASSERT(arg1!=NULL);
- Constraint* arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
- ASSERT(arg2 != NULL);
- carray[i] = allocConstraint(AND, arg1, arg2);
+ Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
+ Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
+ carray[i] = constraintAND2(This->cnf, arg1, arg2);
}
//FIXME: the case when there is no intersection ....
- Constraint* result = allocArrayConstraint(OR, size, carray);
- ASSERT(result!= NULL);
- if(elemc1!= NULL)
- result = allocConstraint(AND, result, elemc1);
- if(elemc2 != NULL)
- result = allocConstraint (AND, result, elemc2);
+ Edge result = constraintOR(This->cnf, size, carray);
+ if (!edgeIsNull(elemc1))
+ result = constraintAND2(This->cnf, result, elemc1);
+ if (!edgeIsNull(elemc2))
+ result = constraintAND2(This->cnf, result, elemc2);
return result;
}
-Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
+Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
switch(GETFUNCTIONTYPE(This->function)){
case TABLEFUNC:
return encodeTableElementFunctionSATEncoder(encoder, This);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
switch(getElementFunctionEncoding(This)->type){
case ENUMERATEIMPLICATIONS:
return encodeEnumTableElemFunctionSATEncoder(encoder, This);
default:
ASSERT(0);
}
- return NULL;
+ return E_BOGUS;
}
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
ASSERT(getSizeArrayElement(&This->inputs)==2 );
ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
- Constraint* carray[elem1->encArraySize*elem2->encArraySize];
+ Edge carray[elem1->encArraySize*elem2->encArraySize];
uint size=0;
- Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
+ Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
for(uint i=0; i<elem1->encArraySize; i++){
if(isinUseElement(elem1, i)){
for( uint j=0; j<elem2->encArraySize; j++){
elem2->encodingArray[j], &isInRange);
//FIXME: instead of getElementValueConstraint, it might be useful to have another function
// that doesn't iterate over encodingArray and treats more efficient ...
- Constraint* valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
- ASSERT(valConstrIn1 != NULL);
- Constraint* valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
- ASSERT(valConstrIn2 != NULL);
- Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
- if(valConstrOut == NULL)
+ Edge valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
+ Edge valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
+ Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
+ if(edgeIsNull(valConstrOut))
continue; //FIXME:Should talk to brian about it!
- Constraint* OpConstraint = allocConstraint(IMPLIES,
- allocConstraint(AND, valConstrIn1, valConstrIn2) , valConstrOut);
+ Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
switch( ((FunctionOperator*)This->function)->overflowbehavior ){
case IGNORE:
if(isInRange){
break;
case FLAGFORCESOVERFLOW:
if(isInRange){
- Constraint* const1 = allocConstraint(IMPLIES,
- allocConstraint(AND, valConstrIn1, valConstrIn2),
- negateConstraint(overFlowConstraint));
- carray[size++] = allocConstraint(AND, const1, OpConstraint);
+ Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
+ carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
}
break;
case OVERFLOWSETSFLAG:
if(isInRange){
carray[size++] = OpConstraint;
} else{
- carray[size++] = allocConstraint(IMPLIES,
- allocConstraint(AND, valConstrIn1, valConstrIn2),
- overFlowConstraint);
+ carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
}
break;
case FLAGIFFOVERFLOW:
if(isInRange){
- Constraint* const1 = allocConstraint(IMPLIES,
- allocConstraint(AND, valConstrIn1, valConstrIn2),
- negateConstraint(overFlowConstraint));
- carray[size++] = allocConstraint(AND, const1, OpConstraint);
- }else{
- carray[size++] = allocConstraint(IMPLIES,
- allocConstraint(AND, valConstrIn1, valConstrIn2),
- overFlowConstraint);
+ Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
+ carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
+ } else {
+ carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
}
break;
case NOOVERFLOW:
}
}
}
- return allocArrayConstraint(AND, size, carray);
+ return constraintAND(encoder->cnf, size, carray);
}
-Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+Edge 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++){
+ Edge 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);
- Constraint* carray[inputNum];
+ uint inputNum = getSizeArrayElement(elements);
+ Edge carray[inputNum];
for(uint j=0; j<inputNum; j++){
Element* el= getArrayElement(elements, j);
carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
- ASSERT(carray[j]!= NULL);
}
- Constraint* output = getElementValueConstraint(encoder, (Element*)This, entry->output);
- ASSERT(output!= NULL);
- Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), output);
+ Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output);
+ Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output);
constraints[i]=row;
}
- Constraint* result = allocArrayConstraint(OR, size, constraints);
+ Edge result = constraintOR(encoder->cnf, size, constraints);
return result;
}
+
projects / satune.git / blobdiff