src/AST/function.cc

   1 #include "function.h"
   2 #include "table.h"
   3 #include "set.h"
   4 #include "csolver.h"
   5 #include "serializer.h"
   6
   7 FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) :
   8         Function(OPERATORFUNC),
   9         op(_op),
  10         domains(domain, numDomain),
  11         range(_range),
  12         overflowbehavior(_overflowbehavior) {
  13 }
  14
  15 FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) :
  16         Function(TABLEFUNC),
  17         table(_table),
  18         undefBehavior(_undefBehavior) {
  19 }
  20
  21 uint64_t FunctionOperator::applyFunctionOperator(uint numVals, uint64_t *values) {
  22         ASSERT(numVals == 2);
  23         switch (op) {
  24         case SATC_ADD:
  25                 return values[0] + values[1];
  26                 break;
  27         case SATC_SUB:
  28                 return values[0] - values[1];
  29                 break;
  30         default:
  31                 ASSERT(0);
  32         }
  33 }
  34
  35 bool FunctionOperator::isInRangeFunction(uint64_t val) {
  36         return range->exists(val);
  37 }
  38
  39 Function *FunctionOperator::clone(CSolver *solver, CloneMap *map) {
  40         Function *f = (Function *) map->get(this);
  41         if (f != NULL)
  42                 return f;
  43
  44         Set *array[domains.getSize()];
  45         for (uint i = 0; i < domains.getSize(); i++) {
  46                 array[i] = domains.get(i)->clone(solver, map);
  47         }
  48         Set *rcopy = range->clone(solver, map);
  49         f = solver->createFunctionOperator(op, array, domains.getSize(), rcopy, overflowbehavior);
  50         map->put(this, f);
  51         return f;
  52 }
  53
  54 Function *FunctionTable::clone(CSolver *solver, CloneMap *map) {
  55         Function *f = (Function *) map->get(this);
  56         if (f != NULL)
  57                 return f;
  58
  59         Table *tcopy = table->clone(solver, map);
  60         f = solver->completeTable(tcopy, undefBehavior);
  61         map->put(this, f);
  62         return f;
  63 }
  64
  65 Set * FunctionTable::getRange() {
  66         return table->getRange();
  67 }
  68
  69 void FunctionTable::serialize(Serializer* serializer){
  70         if(serializer->isSerialized(this))
  71                 return;
  72         serializer->addObject(this);
  73
  74         table->serialize(serializer);
  75
  76         ASTNodeType type = FUNCTABLETYPE;
  77         serializer->mywrite(&type, sizeof(ASTNodeType));
  78         FunctionTable* This = this;
  79         serializer->mywrite(&This, sizeof(FunctionTable*));
  80         serializer->mywrite(&table, sizeof(Table *));
  81         serializer->mywrite(&undefBehavior, sizeof(UndefinedBehavior));
  82
  83 }
  84
  85 void FunctionTable::print(){
  86         model_println("{FunctionTable:");
  87         table->print();
  88         model_println("}\n");
  89
  90 }
  91
  92 void FunctionOperator::serialize(Serializer* serializer){
  93         if(serializer->isSerialized(this))
  94                 return;
  95         serializer->addObject(this);
  96
  97         uint size = domains.getSize();
  98         for(uint i=0; i<size; i++){
  99                 Set* domain = domains.get(i);
 100                 domain->serialize(serializer);
 101         }
 102         range->serialize(serializer);
 103
 104         ASTNodeType nodeType = FUNCOPTYPE;
 105         serializer->mywrite(&nodeType, sizeof(ASTNodeType));
 106         FunctionOperator* This = this;
 107         serializer->mywrite(&This, sizeof(FunctionOperator*));
 108         serializer->mywrite(&op, sizeof(ArithOp));
 109         serializer->mywrite(&size, sizeof(uint));
 110         for(uint i=0; i<size; i++){
 111                 Set *domain = domains.get(i);
 112                 serializer->mywrite(&domain, sizeof(Set *));
 113         }
 114         serializer->mywrite(&range, sizeof(Set *));
 115         serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior));
 116 }
 117
 118 void FunctionOperator::print(){
 119         model_println("{FunctionOperator: %s}", op == SATC_ADD? "ADD": "SUB" );
 120 }