src/AST/function.cc

   1 #include "function.h"
   2 #include "table.h"
   3 #include "set.h"
   4 #include "csolver.h"
   5
   6 FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) :
   7         Function(OPERATORFUNC),
   8         op(_op),
   9         domains(domain, numDomain),
  10         range(_range),
  11         overflowbehavior(_overflowbehavior) {
  12 }
  13
  14 FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) :
  15         Function(TABLEFUNC),
  16         table(_table),
  17         undefBehavior(_undefBehavior) {
  18 }
  19
  20 uint64_t FunctionOperator::applyFunctionOperator(uint numVals, uint64_t *values) {
  21         ASSERT(numVals == 2);
  22         switch (op) {
  23         case SATC_ADD:
  24                 return values[0] + values[1];
  25                 break;
  26         case SATC_SUB:
  27                 return values[0] - values[1];
  28                 break;
  29         default:
  30                 ASSERT(0);
  31         }
  32 }
  33
  34 bool FunctionOperator::isInRangeFunction(uint64_t val) {
  35         return range->exists(val);
  36 }
  37
  38 Function *FunctionOperator::clone(CSolver *solver, CloneMap *map) {
  39         Function *f = (Function *) map->get(this);
  40         if (f != NULL)
  41                 return f;
  42
  43         Set *array[domains.getSize()];
  44         for (uint i = 0; i < domains.getSize(); i++) {
  45                 array[i] = domains.get(i)->clone(solver, map);
  46         }
  47         Set *rcopy = range->clone(solver, map);
  48         f = solver->createFunctionOperator(op, array, domains.getSize(), rcopy, overflowbehavior);
  49         map->put(this, f);
  50         return f;
  51 }
  52
  53 Function *FunctionTable::clone(CSolver *solver, CloneMap *map) {
  54         Function *f = (Function *) map->get(this);
  55         if (f != NULL)
  56                 return f;
  57
  58         Table *tcopy = table->clone(solver, map);
  59         f = solver->completeTable(tcopy, undefBehavior);
  60         map->put(this, f);
  61         return f;
  62 }