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