More name changes

diff --git a/src/AST/astnode.h b/src/AST/astnode.h
index 749bf8e7ed596c1abcd2434a4bbf753f464025c2..0fc94a03285168e6be07a147cd4f2062d904055d 100644 (file)
--- a/src/AST/astnode.h
+++ b/src/AST/astnode.h
@@ -2,6 +2,7 @@
 #define ASTNODE_H
 #include "classlist.h"
 #include "ops.h"
+#include "astops.h"
 
 class ASTNode {
 public:

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 894e6cb071eee91e50ea839b98655b3641713a20..f66cee42adbed31269f1a2ad57c8b9e80e83ad76 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -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"

diff --git a/src/AST/function.h b/src/AST/function.h
index 1ade1368c924aab0fe22a69835bf0e71858e1cdc..6d0e1d05ff79e863081875be19710079908a75ed 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "mymemory.h"
 #include "ops.h"
+#include "astops.h"
 #include "structs.h"
 
 class Function {

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 882e793d46dec90a3dcb2c294718bae869adabef..8ad60c7545ad1884d7c18247473025749540a2aa 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -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

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index dc5128b2ca48a45eb9ccda66566ec50724db4bd5..8d370512723b322e3bb4bc749168a7fdeea01dc4 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -3,6 +3,7 @@
 #include "classlist.h"
 #include "mymemory.h"
 #include "ops.h"
+#include "astops.h"
 #include "structs.h"
 #include "common.h"
 

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 39a50dba6ba9439384e76765df79f0efa4fcd5b9..41b687ec17aa2d6cac9d10511c91ea33c9af52c9 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -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 {

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index ed8b6c9dff06e629163179e45e7e19e2dfa04451..15094ee31ea0dd07e4b68dcc5d30be8a78e25a30 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -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) ));

diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc
index a7367c993233422f09b94a09d4f7e1f453ad0939..e998f3bb6dbf42588c1b1f61ed948e6351c967d2 100644 (file)
--- a/src/Test/tablefuncencodetest.cc
+++ b/src/Test/tablefuncencodetest.cc
@@ -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);
 

diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc
index ee608779d6b20c036b952ca75b85994440188ac8..e0575e77450f42051020ed085142a05b9a7b406d 100644 (file)
--- a/src/Test/tablepredicencodetest.cc
+++ b/src/Test/tablepredicencodetest.cc
@@ -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);

diff --git a/src/csolver.cc b/src/csolver.cc
index 86315183a179da649ff08a179ec1fc8a8c4284d3..9092af9e91fe37db62d931ded3c7c2ae6a1979ac 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -13,6 +13,7 @@
 #include "polarityassignment.h"
 #include "analyzer.h"
 #include "autotuner.h"
+#include "astops.h"
 
 CSolver::CSolver() :
        boolTrue(new BooleanConst(true)),