More name changes
authorbdemsky <bdemsky@uci.edu>
Wed, 30 Aug 2017 22:00:17 +0000 (15:00 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 30 Aug 2017 22:00:17 +0000 (15:00 -0700)
src/AST/astnode.h
src/AST/boolean.h
src/AST/function.h
src/AST/ops.h
src/AST/predicate.h
src/Backend/satfuncopencoder.cc
src/Backend/satfunctableencoder.cc
src/Test/tablefuncencodetest.cc
src/Test/tablepredicencodetest.cc
src/csolver.cc

index 749bf8e..0fc94a0 100644 (file)
@@ -2,6 +2,7 @@
 #define ASTNODE_H
 #include "classlist.h"
 #include "ops.h"
+#include "astops.h"
 
 class ASTNode {
 public:
index 894e6cb..f66cee4 100644 (file)
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "mymemory.h"
 #include "ops.h"
+#include "astops.h"
 #include "structs.h"
 #include "astnode.h"
 #include "functionencoding.h"
index 1ade136..6d0e1d0 100644 (file)
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "mymemory.h"
 #include "ops.h"
+#include "astops.h"
 #include "structs.h"
 
 class Function {
index 882e793..8ad60c7 100644 (file)
@@ -16,32 +16,17 @@ enum HappenedBefore {SATC_FIRST, SATC_SECOND, SATC_UNORDERED};
 typedef enum HappenedBefore HappenedBefore;
 
 /**
- *    FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
- *  OVERFLOWSETSFLAG -- sets the flag if the operation overflows
- *  FLAGIFFOVERFLOW -- flag is set iff the operation overflows
+ *    SATC_FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
+ *  SATC_OVERFLOWSETSFLAG -- sets the flag if the operation overflows
+ *  SATC_FLAGIFFOVERFLOW -- flag is set iff the operation overflows
  *  SATC_IGNORE -- doesn't constrain output if the result cannot be represented
  *  SATC_WRAPAROUND -- wraps around like stand integer arithmetic
- *  NOOVERFLOW -- client has ensured that overflow is impossible
+ *  SATC_NOOVERFLOW -- client has ensured that overflow is impossible
  */
-enum OverFlowBehavior {SATC_IGNORE, SATC_WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW};
+enum OverFlowBehavior {SATC_IGNORE, SATC_WRAPAROUND, SATC_FLAGFORCESOVERFLOW, SATC_OVERFLOWSETSFLAG, SATC_FLAGIFFOVERFLOW, SATC_NOOVERFLOW};
 typedef enum OverFlowBehavior OverFlowBehavior;
 
-enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, FLAGFORCEUNDEFINED, UNDEFINEDSETSFLAG, FLAGIFFUNDEFINED};
+enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, SATC_FLAGFORCEUNDEFINED, SATC_UNDEFINEDSETSFLAG, SATC_FLAGIFFUNDEFINED};
 typedef enum UndefinedBehavior UndefinedBehavior;
 
-enum FunctionType {TABLEFUNC, OPERATORFUNC};
-typedef enum FunctionType FunctionType;
-
-enum PredicateType {TABLEPRED, OPERATORPRED};
-typedef enum PredicateType PredicateType;
-
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
-typedef enum ASTNodeType ASTNodeType;
-
-enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
-typedef enum Polarity Polarity;
-
-enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3};
-typedef enum BooleanValue BooleanValue;
-
 #endif
index dc5128b..8d37051 100644 (file)
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "mymemory.h"
 #include "ops.h"
+#include "astops.h"
 #include "structs.h"
 #include "common.h"
 
index 39a50db..41b687e 100644 (file)
@@ -117,7 +117,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
                bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result);
                bool needClause = isInRange;
-               if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
+               if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
                        needClause = true;
                }
 
@@ -134,16 +134,16 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                        Edge clause;
                        switch (function->overflowbehavior) {
                        case SATC_IGNORE:
-                       case NOOVERFLOW:
+                       case SATC_NOOVERFLOW:
                        case SATC_WRAPAROUND: {
                                clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                break;
                        }
-                       case FLAGFORCESOVERFLOW: {
+                       case SATC_FLAGFORCESOVERFLOW: {
                                clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                break;
                        }
-                       case OVERFLOWSETSFLAG: {
+                       case SATC_OVERFLOWSETSFLAG: {
                                if (isInRange) {
                                        clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                } else {
@@ -151,7 +151,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                                }
                                break;
                        }
-                       case FLAGIFFOVERFLOW: {
+                       case SATC_FLAGIFFOVERFLOW: {
                                if (isInRange) {
                                        clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
                                } else {
index ed8b6c9..15094ee 100644 (file)
@@ -13,7 +13,7 @@
 Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
        ASSERT(constraint->predicate->type == TABLEPRED);
        UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
-       ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+       ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
        Table *table = ((PredicateTable *)constraint->predicate)->table;
        FunctionEncodingType encType = constraint->encoding.type;
        Array<Element *> *inputs = &constraint->inputs;
@@ -44,7 +44,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
                case SATC_IGNOREBEHAVIOR:
                        row = constraintAND(cnf, inputNum, carray);
                        break;
-               case FLAGFORCEUNDEFINED: {
+               case SATC_FLAGFORCEUNDEFINED: {
                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray),  constraintNegate(undefConst)));
                        if (generateNegation == (entry->output != 0)) {
                                continue;
@@ -82,7 +82,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
        PredicateTable *predicate = (PredicateTable *)constraint->predicate;
        switch (predicate->undefinedbehavior) {
        case SATC_IGNOREBEHAVIOR:
-       case FLAGFORCEUNDEFINED:
+       case SATC_FLAGFORCEUNDEFINED:
                return encodeEnumEntriesTablePredicateSATEncoder(constraint);
        default:
                break;
@@ -118,14 +118,14 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                }
 
                switch (predicate->undefinedbehavior) {
-               case UNDEFINEDSETSFLAG:
+               case SATC_UNDEFINEDSETSFLAG:
                        if (isInRange) {
                                clause = constraintAND(cnf, numDomains, carray);
                        } else {
                                addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
                        }
                        break;
-               case FLAGIFFUNDEFINED:
+               case SATC_FLAGIFFUNDEFINED:
                        if (isInRange) {
                                clause = constraintAND(cnf, numDomains, carray);
                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
@@ -178,7 +178,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 
 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
        UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
-       ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+       ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
        Array<Element *> *elements = &func->inputs;
        Table *table = ((FunctionTable *) (func->function))->table;
        uint size = table->entries->getSize();
@@ -201,7 +201,7 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func)
                        row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
                        break;
                }
-               case FLAGFORCEUNDEFINED: {
+               case SATC_FLAGFORCEUNDEFINED: {
                        Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
                        row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)));
                        break;
@@ -231,7 +231,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
        FunctionTable *function = (FunctionTable *)elemFunc->function;
        switch (function->undefBehavior) {
        case SATC_IGNOREBEHAVIOR:
-       case FLAGFORCEUNDEFINED:
+       case SATC_FLAGFORCEUNDEFINED:
                return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
        default:
                break;
@@ -256,7 +256,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                Edge carray[numDomains + 1];
                TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
                bool isInRange = tableEntry != NULL;
-               ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
+               ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED);
                for (uint i = 0; i < numDomains; i++) {
                        Element *elem = elemFunc->inputs.get(i);
                        carray[i] = getElementValueConstraint(elem, vals[i]);
@@ -267,7 +267,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 
                Edge clause;
                switch (function->undefBehavior) {
-               case UNDEFINEDSETSFLAG: {
+               case SATC_UNDEFINEDSETSFLAG: {
                        if (isInRange) {
                                //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
                                clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
@@ -276,7 +276,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                        }
                        break;
                }
-               case FLAGIFFUNDEFINED: {
+               case SATC_FLAGIFFUNDEFINED: {
                        if (isInRange) {
                                clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) ));
index a7367c9..e998f3b 100644 (file)
@@ -40,7 +40,7 @@ int main(int numargs, char **argv) {
        solver->addTableEntry(t1, row4, 2, 5);
        solver->addTableEntry(t1, row5, 2, 3);
        solver->addTableEntry(t1, row6, 2, 5);
-       Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED);
+       Function *f1 = solver->completeTable(t1, SATC_FLAGIFFUNDEFINED);
        Element *tmparray[] = {e1, e2};
        Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow);
 
index ee60877..e0575e7 100644 (file)
@@ -40,7 +40,7 @@ int main(int numargs, char **argv) {
        solver->addTableEntry(t1, row4, 3, false);
        solver->addTableEntry(t1, row5, 3, false);
        solver->addTableEntry(t1, row6, 3, true);
-       Predicate *p1 = solver->createPredicateTable(t1, FLAGIFFUNDEFINED);
+       Predicate *p1 = solver->createPredicateTable(t1, SATC_FLAGIFFUNDEFINED);
        Boolean *undef = solver->getBooleanVar(2);
        Element *tmparray[] = {e1, e2, e3};
        Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
index 8631518..9092af9 100644 (file)
@@ -13,6 +13,7 @@
 #include "polarityassignment.h"
 #include "analyzer.h"
 #include "autotuner.h"
+#include "astops.h"
 
 CSolver::CSolver() :
        boolTrue(new BooleanConst(true)),