case ELEMSET:
return ((ElementSet*)This)->set;
case ELEMFUNCRETURN:
- ;//Nope is needed for label assignment. i.e. next instruction isn't
+ ;//Nope is needed for label assignment. i.e. next instruction isn't a statement
Function* func = ((ElementFunction*)This)->function;
switch(GETFUNCTIONTYPE(func)){
case TABLEFUNC:
return NULL;
}
-FIXME()!!!!
-
-/** This function belongs in the backend...Elements should not touch
- binary constraints nor should they touch their encoders... */
-
-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 deleteElement(Element *This) {
switch(GETELEMENTTYPE(This)) {
case ELEMFUNCRETURN: {
yet, just do this as you need to during the encodeAllSATEncoder
walk. */
- FIXME!!!!(); // Make sure Hamed sees comment above
+// FIXME!!!!(); // Make sure Hamed sees comment above
uint size = getSizeVectorElement(csolver->allElements);
for(uint i=0; i<size; i++){
}
}
+
+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);
Element* el= getArrayElement(elements, i);
Constraint* carray[inputNum];
for(uint j=0; j<inputNum; j++){
- FIXME!!!!();
- //This next line should not assume a particular encoding type for the element... just a generic element encoding function that should choose the appropriate encoding...
-
- carray[inputNum] = getElementValueBinaryIndexConstraint(el, entry->inputs[j]);
+ carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
}
Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
getElementValueBinaryIndexConstraint((Element*)This, entry->output));
Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
+Constraint * getElementValueConstraint(Element* This, uint64_t value);
Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);