Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
[satune.git] / src / Backend / satfuncopencoder.cc
index bfd4ea6b6cb63f0921f7707458d5877aa4ac4afb..3f85fec3700ac5a7e7905f1f627f7f183b320931 100644 (file)
@@ -88,7 +88,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 #ifdef TRACE_DEBUG
        model_print("Operator Function ...\n");
 #endif
-       FunctionOperator *function = (FunctionOperator *) func->function;
+       FunctionOperator *function = (FunctionOperator *) func->getFunction();
        uint numDomains = func->inputs.getSize();
 
        /* Call base encoders for children */
@@ -115,7 +115,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                Edge carray[numDomains + 1];
 
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
-               bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result);
+               bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
                bool needClause = isInRange;
                if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
                        needClause = true;
@@ -200,11 +200,11 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        encodeElementSATEncoder(elem0);
        Element *elem1 = constraint->inputs.get(1);
        encodeElementSATEncoder(elem1);
-       ElementEncoding *ee0 = getElementEncoding(elem0);
-       ElementEncoding *ee1 = getElementEncoding(elem1);
+       ElementEncoding *ee0 = elem0->getElementEncoding();
+       ElementEncoding *ee1 = elem1->getElementEncoding();
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
-       switch (predicate->op) {
+       switch (predicate->getOp()) {
        case SATC_EQUALS:
                return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case SATC_LT: