functionrecord.cc

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #include "functionrecord.h"
  11 #include "constraint.h"
  12 #include "constgen.h"
  13 #include "eprecord.h"
  14
  15 FunctionRecord::FunctionRecord(ConstGen *cg, EPRecord *func) : function(func) {
  16         if (function->getPhi()) {
  17                 uint numvals=function->getSet(VC_BASEINDEX)->getSize();
  18                 numvars=NUMBITS(numvals-1);
  19                 vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
  20                 cg->getArrayNewVars(numvars, vars);
  21         } else {
  22                 uint numvals=function->getSet(VC_FUNCOUTINDEX)->getSize();
  23                 numvals++;                                              //allow for new combinations in sat formulas
  24                 numvars=NUMBITS(numvals-1);
  25                 vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
  26                 cg->getArrayNewVars(numvars, vars);
  27         }
  28 }
  29
  30 FunctionRecord::~FunctionRecord() {
  31         model_free(vars);
  32 }
  33
  34 Constraint * FunctionRecord::getValueEncoding(uint64_t val) {
  35         int index=-1;
  36         if (function->getPhi()) {
  37                 IntIterator *it=function->getSet(VC_BASEINDEX)->iterator();
  38                 int count=0;
  39                 while(it->hasNext()) {
  40                         if (it->next()==val) {
  41                                 index=count;
  42                                 break;
  43                         }
  44                         count++;
  45                 }
  46                 delete it;
  47         } else {
  48                 IntIterator *it=function->getSet(VC_FUNCOUTINDEX)->iterator();
  49                 int count=0;
  50                 while(it->hasNext()) {
  51                         if (it->next()==val) {
  52                                 index=count;
  53                                 break;
  54                         }
  55                         count++;
  56                 }
  57                 delete it;
  58         }
  59         if (index==-1)
  60                 return NULL;
  61         return generateConstraint(numvars, vars, (uint)index);
  62 }
  63
  64 Constraint * FunctionRecord::getNoValueEncoding() {
  65         return new Constraint(AND, numvars, vars);
  66 }