src/Encoders/naiveencoder.c

   1 #include "naiveencoder.h"
   2 #include "elementencoding.h"
   3 #include "element.h"
   4 #include "functionencoding.h"
   5 #include "function.h"
   6 #include "set.h"
   7 #include "common.h"
   8 #include "structs.h"
   9 #include "csolver.h"
  10 #include "boolean.h"
  11 #include "table.h"
  12 #include "tableentry.h"
  13 //THIS FILE SHOULD HAVE NOTHING TO DO WITH CONSTRAINTS...
  14 //#include "constraint.h"
  15 #include <strings.h>
  16
  17 NaiveEncoder* allocNaiveEncoder(){
  18         NaiveEncoder* encoder = (NaiveEncoder*) ourmalloc(sizeof(NaiveEncoder));
  19         allocInlineDefVectorConstraint(GETNAIVEENCODERALLCONSTRAINTS(encoder));
  20         allocInlineDefVectorConstraint(GETNAIVEENCODERVARS(encoder));
  21         encoder->varindex=0;
  22         return encoder;
  23 }
  24
  25 void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){
  26         uint size = getSizeVectorElement(csolver->allElements);
  27         for(uint i=0; i<size; i++){
  28                 Element* element = getVectorElement(csolver->allElements, i);
  29                 switch(GETELEMENTTYPE(element)){
  30                         case ELEMSET:
  31                                 setElementEncodingType(GETELEMENTENCODING(element), BINARYINDEX);
  32                                 baseBinaryIndexElementAssign(GETELEMENTENCODING(element));
  33                                 generateElementEncodingVariables(encoder,GETELEMENTENCODING(element));
  34                                 break;
  35                         case ELEMFUNCRETURN:
  36                                 setFunctionEncodingType(GETFUNCTIONENCODING(element), ENUMERATEIMPLICATIONS);
  37                                 break;
  38                         default:
  39                                 ASSERT(0);
  40                 }
  41         }
  42
  43         size = getSizeVectorBoolean(csolver->allBooleans);
  44         for(uint i=0; i<size; i++){
  45                 Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
  46                 switch(GETBOOLEANTYPE(predicate)){
  47                         case PREDICATEOP:
  48                                 setFunctionEncodingType(GETFUNCTIONENCODING(predicate), ENUMERATEIMPLICATIONS);
  49                                 break;
  50                         default:
  51                                 continue;
  52                 }
  53         }
  54 }
  55
  56
  57 // THIS SHOULD NOT BE HERE
  58 /*
  59 void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray) {
  60         for(uint i=0;i<num;i++)
  61                 carray[i]=getNewVar(encoder);
  62 }
  63 */
  64
  65 // THIS SHOULD NOT BE HERE
  66 /*
  67 Constraint * getNewVar(NaiveEncoder* encoder) {
  68         Constraint* var = allocVarConstraint(VAR, encoder->varindex);
  69         Constraint* notVar = allocVarConstraint(NOTVAR, encoder->varindex);
  70         setNegConstraint(var, notVar);
  71         setNegConstraint(notVar, var);
  72         pushVectorConstraint(GETNAIVEENCODERVARS(encoder), var);
  73         encoder->varindex++;
  74         return var;
  75 }
  76 */
  77
  78 void baseBinaryIndexElementAssign(ElementEncoding *This) {
  79         Element * element=This->element;
  80         ASSERT(element->type == ELEMSET);
  81         Set * set= ((ElementSet*)element)->set;
  82         ASSERT(set->isRange==false);
  83         uint size=getSizeVectorInt(set->members);
  84         uint encSize=NEXTPOW2(size);
  85         allocEncodingArrayElement(This, encSize);
  86         allocInUseArrayElement(This, encSize);
  87
  88         for(uint i=0;i<size;i++) {
  89                 This->encodingArray[i]=getVectorInt(set->members, i);
  90                 setInUseElement(This, i);
  91         }
  92         This->numVars = NUMBITS(size-1);
  93         This->variables = ourmalloc(sizeof(Constraint*)* This->numVars);
  94
  95
  96 }
  97
  98
  99 void encode(CSolver* csolver){
 100         NaiveEncoder* encoder = allocNaiveEncoder();
 101         naiveEncodingDecision( csolver, encoder);
 102         uint size = getSizeVectorElement(csolver->allElements);
 103         for(uint i=0; i<size; i++){
 104                 Element* element = getVectorElement(csolver->allElements, i);
 105                 switch(GETELEMENTTYPE(element)){
 106                         case ELEMFUNCRETURN:
 107                                 naiveEncodeFunctionPredicate(encoder, GETFUNCTIONENCODING(element));
 108                                 break;
 109                         default:
 110                                 continue;
 111                 }
 112         }
 113
 114         size = getSizeVectorBoolean(csolver->allBooleans);
 115         for(uint i=0; i<size; i++){
 116                 Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
 117                 switch(GETBOOLEANTYPE(predicate)){
 118                         case PREDICATEOP:
 119                                 naiveEncodeFunctionPredicate(encoder, GETFUNCTIONENCODING(predicate));
 120                                 break;
 121                         default:
 122                                 continue;
 123                 }
 124         }
 125 }
 126
 127 void naiveEncodeFunctionPredicate(NaiveEncoder* encoder, FunctionEncoding *This){
 128         if(This->isFunction) {
 129                 ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN);
 130                 switch(This->type){
 131                         case ENUMERATEIMPLICATIONS:
 132                                 naiveEncodeEnumeratedFunction(encoder, This);
 133                                 break;
 134                         case CIRCUIT:
 135                                 naiveEncodeCircuitFunction(encoder, This);
 136                                 break;
 137                         default:
 138                                 ASSERT(0);
 139                 }
 140         }else {
 141                 ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP);
 142                 BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate;
 143                 //FIXME
 144
 145         }
 146 }
 147
 148 void naiveEncodeEnumeratedFunction(NaiveEncoder* encoder, FunctionEncoding* This){
 149         ElementFunction* ef =(ElementFunction*)This->op.function;
 150         switch(GETFUNCTIONTYPE(ef->function)){
 151                 case TABLEFUNC:
 152                         naiveEncodeEnumTableFunc(encoder, ef);
 153                         break;
 154                 case OPERATORFUNC:
 155                         naiveEncodeEnumOperatingFunc(encoder, ef);
 156                         break;
 157                 default:
 158                         ASSERT(0);
 159         }
 160 }
 161
 162 void naiveEncodeEnumTableFunc(NaiveEncoder* encoder, ElementFunction* This){
 163         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 164         ArrayElement* elements= &This->inputs;
 165         Table* table = ((FunctionTable*) (This->function))->table;
 166         uint size = getSizeVectorTableEntry(&table->entries);
 167         for(uint i=0; i<size; i++){
 168                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 169                 uint inputNum =getSizeArrayElement(elements);
 170                 Element* el= getArrayElement(elements, i);
 171                 Constraint* carray[inputNum];
 172                 for(uint j=0; j<inputNum; j++){
 173                          carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
 174                 }
 175                 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 176                         getElementValueConstraint(table->range, entry->output));
 177                 pushVectorConstraint( GETNAIVEENCODERALLCONSTRAINTS(encoder), row);
 178         }
 179
 180 }
 181
 182 void naiveEncodeEnumOperatingFunc(NaiveEncoder* encoder, ElementFunction* This){
 183
 184 }
 185
 186
 187 void naiveEncodeCircuitFunction(NaiveEncoder* encoder, FunctionEncoding* This){
 188
 189 }
 190
 191 void deleteNaiveEncoder(NaiveEncoder* encoder){
 192         deleteVectorArrayConstraint(&encoder->vars);
 193 }