From: bdemsky Date: Wed, 30 Aug 2017 22:00:17 +0000 (-0700) Subject: More name changes X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=bb49b371775e60638e71a99febce2bc4a21e075e;p=satune.git More name changes --- diff --git a/src/AST/astnode.h b/src/AST/astnode.h index 749bf8e..0fc94a0 100644 --- 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 894e6cb..f66cee4 100644 --- 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 1ade136..6d0e1d0 100644 --- 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 882e793..8ad60c7 100644 --- 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 dc5128b..8d37051 100644 --- 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 39a50db..41b687e 100644 --- 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 ed8b6c9..15094ee 100644 --- 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 *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 *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 a7367c9..e998f3b 100644 --- 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 ee60877..e0575e7 100644 --- 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 8631518..9092af9 100644 --- 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)),