-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);
-}