1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
10 #include "functionrecord.h"
11 #include "constraint.h"
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);
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);
30 FunctionRecord::~FunctionRecord() {
34 Constraint * FunctionRecord::getValueEncoding(uint64_t val) {
36 if (function->getPhi()) {
37 IntIterator *it=function->getSet(VC_BASEINDEX)->iterator();
39 while(it->hasNext()) {
40 if (it->next()==val) {
48 IntIterator *it=function->getSet(VC_FUNCOUTINDEX)->iterator();
50 while(it->hasNext()) {
51 if (it->next()==val) {
61 return generateConstraint(numvars, vars, (uint)index);
64 Constraint * FunctionRecord::getNoValueEncoding() {
65 return new Constraint(AND, numvars, vars);