valuerecord.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 "valuerecord.h"
  11 #include "mymemory.h"
  12 #include "constraint.h"
  13 #include "constgen.h"
  14 #include "mcutil.h"
  15
  16 ValueRecord::ValueRecord(IntHashSet *_set) : set(_set)
  17 {
  18         uint numvalue=set->getSize();
  19         numvars=NUMBITS(numvalue-1);
  20 }
  21
  22 ValueRecord::~ValueRecord() {
  23 }
  24
  25 uint64_t ValueRecord::getValue(Constraint **vars, bool *satsolution) {
  26         uint value=0;
  27         for(int j=numvars-1;j>=0;j--) {
  28                 value=value<<1;
  29                 if (satsolution[vars[j]->getVar()])
  30                         value|=1;
  31         }
  32         uint i=0;
  33         IntIterator * it=set->iterator();
  34         while(it->hasNext()) {
  35                 uint64_t val=it->next();
  36                 if (numvars==0) {
  37                         delete it;
  38                         return val;
  39                 }
  40                 if (i==value) {
  41                         delete it;
  42                         return val;
  43                 }
  44                 i++;
  45         }
  46         delete it;
  47         return 111111111;
  48 }
  49
  50 Constraint * ValueRecord::getValueEncoding(Constraint **vars, uint64_t value) {
  51         uint i=0;
  52         IntIterator * it=set->iterator();
  53         while(it->hasNext()) {
  54                 if (it->next()==value) {
  55                         delete it;
  56                         if (numvars==0) {
  57                                 return &ctrue;
  58                         }
  59                         return generateConstraint(numvars, vars, i);
  60                 }
  61                 i++;
  62         }
  63         delete it;
  64
  65
  66         return NULL;
  67 }