From faac5894230d569848367149a130486b965eb329 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 30 Aug 2017 14:46:10 -0700 Subject: [PATCH] renaming --- src/AST/function.cc | 4 ++-- src/AST/ops.h | 18 +++++++------- src/AST/predicate.cc | 10 ++++---- src/AST/rewriter.cc | 24 +++++++++---------- src/ASTAnalyses/ordergraph.cc | 4 ++-- src/ASTAnalyses/ordernode.h | 2 +- src/ASTAnalyses/polarityassignment.cc | 20 ++++++++-------- src/ASTTransform/analyzer.cc | 4 ++-- src/ASTTransform/decomposeordertransform.cc | 14 +++++------ src/ASTTransform/integerencoding.cc | 4 ++-- src/Backend/constraint.cc | 2 +- src/Backend/satencoder.cc | 10 ++++---- src/Backend/satfuncopencoder.cc | 10 ++++---- src/Backend/satfunctableencoder.cc | 14 +++++------ src/Backend/satorderencoder.cc | 10 ++++---- src/Backend/sattranslator.cc | 4 ++-- src/Test/buildconstraintstest.cc | 8 +++---- src/Test/elemequalsattest.cc | 2 +- src/Test/elemequalunsattest.cc | 2 +- src/Test/funcencodingtest.cc | 10 ++++---- src/Test/logicopstest.cc | 12 +++++----- src/Test/ltelemconsttest.cc | 2 +- src/Test/ordergraphtest.cc | 26 ++++++++++----------- src/Test/ordertest.cc | 2 +- src/Test/tablefuncencodetest.cc | 2 +- src/Test/tablepredicencodetest.cc | 4 ++-- src/common.cc | 2 +- src/csolver.cc | 22 ++++++++--------- 28 files changed, 124 insertions(+), 124 deletions(-) diff --git a/src/AST/function.cc b/src/AST/function.cc index 1d910e4..6715e79 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -12,10 +12,10 @@ FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) : uint64_t FunctionOperator::applyFunctionOperator(uint numVals, uint64_t *values) { ASSERT(numVals == 2); switch (op) { - case ADD: + case SATC_ADD: return values[0] + values[1]; break; - case SUB: + case SATC_SUB: return values[0] - values[1]; break; default: diff --git a/src/AST/ops.h b/src/AST/ops.h index 1f9c197..882e793 100644 --- a/src/AST/ops.h +++ b/src/AST/ops.h @@ -1,32 +1,32 @@ #ifndef OPS_H #define OPS_H -enum LogicOp {L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES}; +enum LogicOp {SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES}; typedef enum LogicOp LogicOp; -enum ArithOp {ADD, SUB}; +enum ArithOp {SATC_ADD, SATC_SUB}; typedef enum ArithOp ArithOp; -enum CompOp {EQUALS, LT, GT, LTE, GTE}; +enum CompOp {SATC_EQUALS, SATC_LT, SATC_GT, SATC_LTE, SATC_GTE}; typedef enum CompOp CompOp; -enum OrderType {PARTIAL, TOTAL}; +enum OrderType {SATC_PARTIAL, SATC_TOTAL}; typedef enum OrderType OrderType; -enum HappenedBefore {FIRST, SECOND, UNORDERED}; +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 - * IGNORE -- doesn't constrain output if the result cannot be represented - * WRAPAROUND -- wraps around like stand integer arithmetic + * 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 */ -enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW}; +enum OverFlowBehavior {SATC_IGNORE, SATC_WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW}; typedef enum OverFlowBehavior OverFlowBehavior; -enum UndefinedBehavior {IGNOREBEHAVIOR, FLAGFORCEUNDEFINED, UNDEFINEDSETSFLAG, FLAGIFFUNDEFINED}; +enum UndefinedBehavior {SATC_IGNOREBEHAVIOR, FLAGFORCEUNDEFINED, UNDEFINEDSETSFLAG, FLAGIFFUNDEFINED}; typedef enum UndefinedBehavior UndefinedBehavior; enum FunctionType {TABLEFUNC, OPERATORFUNC}; diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index 99cd311..d359811 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -12,15 +12,15 @@ PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) bool PredicateOperator::evalPredicateOperator(uint64_t *inputs) { switch (op) { - case EQUALS: + case SATC_EQUALS: return inputs[0] == inputs[1]; - case LT: + case SATC_LT: return inputs[0] < inputs[1]; - case GT: + case SATC_GT: return inputs[0] > inputs[1]; - case LTE: + case SATC_LTE: return inputs[0] <= inputs[1]; - case GTE: + case SATC_GTE: return inputs[0] >= inputs[1]; } ASSERT(0); diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index f32fc91..bfc321c 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -12,19 +12,19 @@ void CSolver::replaceBooleanWithTrue(Boolean *bexpr) { Boolean *parent = bexpr->parents.get(i); BooleanLogic *logicop = (BooleanLogic *) parent; switch (logicop->op) { - case L_AND: + case SATC_AND: handleANDTrue(logicop, bexpr); break; - case L_OR: + case SATC_OR: replaceBooleanWithTrue(parent); break; - case L_NOT: + case SATC_NOT: replaceBooleanWithFalse(parent); break; - case L_XOR: + case SATC_XOR: handleXORTrue(logicop, bexpr); break; - case L_IMPLIES: + case SATC_IMPLIES: handleIMPLIESTrue(logicop, bexpr); break; } @@ -59,7 +59,7 @@ void handleXORTrue(BooleanLogic *bexpr, Boolean *child) { Boolean *b = bexpr->inputs.get(0); uint childindex = (b == child) ? 0 : 1; bexpr->inputs.remove(childindex); - bexpr->op = L_NOT; + bexpr->op = SATC_NOT; } void CSolver::handleXORFalse(BooleanLogic *bexpr, Boolean *child) { @@ -90,7 +90,7 @@ void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) { } else { //Make into negation of first term bexpr->inputs.get(1); - bexpr->op = L_NOT; + bexpr->op = SATC_NOT; } } @@ -144,19 +144,19 @@ void CSolver::replaceBooleanWithFalse(Boolean *bexpr) { Boolean *parent = bexpr->parents.get(i); BooleanLogic *logicop = (BooleanLogic *) parent; switch (logicop->op) { - case L_AND: + case SATC_AND: replaceBooleanWithFalse(parent); break; - case L_OR: + case SATC_OR: handleORFalse(logicop, bexpr); break; - case L_NOT: + case SATC_NOT: replaceBooleanWithTrue(parent); break; - case L_XOR: + case SATC_XOR: handleXORFalse(logicop, bexpr); break; - case L_IMPLIES: + case SATC_IMPLIES: handleIMPLIESFalse(logicop, bexpr); break; } diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index 9942b74..9f53d11 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -46,7 +46,7 @@ void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder * break; } case P_FALSE: { - if (order->type == TOTAL) { + if (order->type == SATC_TOTAL) { OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1); if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT) _2to1->mustPos = true; @@ -83,7 +83,7 @@ void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrd break; } case BV_MUSTBEFALSE: { - if (order->type == TOTAL) { + if (order->type == SATC_TOTAL) { OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1); _2to1->mustPos = true; _2to1->polPos = true; diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h index 36bb3df..550bf1e 100644 --- a/src/ASTAnalyses/ordernode.h +++ b/src/ASTAnalyses/ordernode.h @@ -14,7 +14,7 @@ #include "structs.h" #include "orderedge.h" -enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET}; +enum NodeStatus {NOTVISITED, VISITED, FINISHED, SATC_ADDEDTOSET}; typedef enum NodeStatus NodeStatus; class OrderNode { diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc index ea60ca8..f0dac37 100644 --- a/src/ASTAnalyses/polarityassignment.cc +++ b/src/ASTAnalyses/polarityassignment.cc @@ -81,8 +81,8 @@ BooleanValue negateBooleanValue(BooleanValue This) { void computeLogicOpPolarity(BooleanLogic *This) { Polarity parentpolarity = This->polarity; switch (This->op) { - case L_AND: - case L_OR: { + case SATC_AND: + case SATC_OR: { uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { Boolean *tmp = This->inputs.get(i); @@ -90,17 +90,17 @@ void computeLogicOpPolarity(BooleanLogic *This) { } break; } - case L_NOT: { + case SATC_NOT: { Boolean *tmp = This->inputs.get(0); updatePolarity(tmp, negatePolarity(parentpolarity)); break; } - case L_XOR: { + case SATC_XOR: { updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE); updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE); break; } - case L_IMPLIES: { + case SATC_IMPLIES: { Boolean *left = This->inputs.get(0); updatePolarity(left, negatePolarity( parentpolarity)); Boolean *right = This->inputs.get(1); @@ -115,7 +115,7 @@ void computeLogicOpPolarity(BooleanLogic *This) { void computeLogicOpBooleanValue(BooleanLogic *This) { BooleanValue parentbv = This->boolVal; switch (This->op) { - case L_AND: { + case SATC_AND: { if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) { uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { @@ -124,7 +124,7 @@ void computeLogicOpBooleanValue(BooleanLogic *This) { } return; } - case L_OR: { + case SATC_OR: { if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) { uint size = This->inputs.getSize(); for (uint i = 0; i < size; i++) { @@ -133,10 +133,10 @@ void computeLogicOpBooleanValue(BooleanLogic *This) { } return; } - case L_NOT: + case SATC_NOT: updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv)); return; - case L_IMPLIES: + case SATC_IMPLIES: //implies is really an or with the first term negated if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) { uint size = This->inputs.getSize(); @@ -144,7 +144,7 @@ void computeLogicOpBooleanValue(BooleanLogic *This) { updateMustValue(This->inputs.get(1), parentbv); } return; - case L_XOR: + case SATC_XOR: return; default: ASSERT(0); diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc index cfc01a8..05329a5 100644 --- a/src/ASTTransform/analyzer.cc +++ b/src/ASTTransform/analyzer.cc @@ -28,7 +28,7 @@ void orderAnalysis(CSolver *This) { } OrderGraph *graph = buildOrderGraph(order); - if (order->type == PARTIAL) { + if (order->type == SATC_PARTIAL) { //Required to do SCC analysis for partial order graphs. It //makes sure we don't incorrectly optimize graphs with negative //polarity edges @@ -45,7 +45,7 @@ void orderAnalysis(CSolver *This) { if (mustReachLocal) { //This pair of analysis is also optional - if (order->type == PARTIAL) { + if (order->type == SATC_PARTIAL) { localMustAnalysisPartial(This, graph); } else { localMustAnalysisTotal(This, graph); diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 598928d..d458b2f 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -56,20 +56,20 @@ void DecomposeOrderTransform::doTransform(){ MutableSet *set = solver->createMutableSet(order->set->getType()); neworder = solver->createOrder(order->type, set); ordervec.setExpand(from->sccNum, neworder); - if (order->type == PARTIAL) + if (order->type == SATC_PARTIAL) partialcandidatevec.setExpand(from->sccNum, neworder); else partialcandidatevec.setExpand(from->sccNum, NULL); } - if (from->status != ADDEDTOSET) { - from->status = ADDEDTOSET; + if (from->status != SATC_ADDEDTOSET) { + from->status = SATC_ADDEDTOSET; ((MutableSet *)neworder->set)->addElementMSet(from->id); } - if (to->status != ADDEDTOSET) { - to->status = ADDEDTOSET; + if (to->status != SATC_ADDEDTOSET) { + to->status = SATC_ADDEDTOSET; ((MutableSet *)neworder->set)->addElementMSet(to->id); } - if (order->type == PARTIAL) { + if (order->type == SATC_PARTIAL) { OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to); if (edge->polNeg) partialcandidatevec.setExpand(from->sccNum, NULL); @@ -83,7 +83,7 @@ void DecomposeOrderTransform::doTransform(){ for (uint i = 0; i < pcvsize; i++) { Order *neworder = partialcandidatevec.get(i); if (neworder != NULL) { - neworder->type = TOTAL; + neworder->type = SATC_TOTAL; model_print("i=%u\t", i); } } diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index 2d405e0..7d7ea92 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -36,11 +36,11 @@ void IntegerEncodingTransform::doTransform(){ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) { IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order); - //getting two elements and using LT predicate ... + //getting two elements and using SATC_LT predicate ... Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first); Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second); Set *sarray[] = {ierec->set, ierec->set}; - Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2); + Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2); Element *parray[] = {elem1, elem2}; Boolean *boolean = solver->applyPredicate(predicate, parray, 2); solver->addConstraint(boolean); diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index dd536e0..b9a9916 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -317,7 +317,7 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) { void addConstraintCNF(CNF *cnf, Edge constraint) { pushVectorEdge(&cnf->constraints, constraint); #ifdef CONFIG_DEBUG - model_print("****ADDING NEW Constraint*****\n"); + model_print("****SATC_ADDING NEW Constraint*****\n"); printCNF(constraint); model_print("\n******************************\n"); #endif diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 175cfc9..dcd70bc 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -85,15 +85,15 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) { array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i)); switch (constraint->op) { - case L_AND: + case SATC_AND: return constraintAND(cnf, constraint->inputs.getSize(), array); - case L_OR: + case SATC_OR: return constraintOR(cnf, constraint->inputs.getSize(), array); - case L_NOT: + case SATC_NOT: return constraintNegate(array[0]); - case L_XOR: + case SATC_XOR: return constraintXOR(cnf, array[0], array[1]); - case L_IMPLIES: + case SATC_IMPLIES: return constraintIMPLIES(cnf, array[0], array[1]); default: model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op); diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index d416a15..39a50db 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -133,9 +133,9 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) Edge clause; switch (function->overflowbehavior) { - case IGNORE: + case SATC_IGNORE: case NOOVERFLOW: - case WRAPAROUND: { + case SATC_WRAPAROUND: { clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]); break; } @@ -205,11 +205,11 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra ASSERT(ee0->numVars == ee1->numVars); uint numVars = ee0->numVars; switch (predicate->op) { - case EQUALS: + case SATC_EQUALS: return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables); - case LT: + case SATC_LT: return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables); - case GT: + case SATC_GT: return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables); default: ASSERT(0); diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 633d716..ed8b6c9 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 == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); + ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); Table *table = ((PredicateTable *)constraint->predicate)->table; FunctionEncodingType encType = constraint->encoding.type; Array *inputs = &constraint->inputs; @@ -28,7 +28,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con uint i = 0; while (iterator->hasNext()) { TableEntry *entry = iterator->next(); - if (generateNegation == (entry->output != 0) && undefStatus == IGNOREBEHAVIOR) { + if (generateNegation == (entry->output != 0) && undefStatus == SATC_IGNOREBEHAVIOR) { //Skip the irrelevant entries continue; } @@ -41,7 +41,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con } Edge row; switch (undefStatus) { - case IGNOREBEHAVIOR: + case SATC_IGNOREBEHAVIOR: row = constraintAND(cnf, inputNum, carray); break; case FLAGFORCEUNDEFINED: { @@ -81,7 +81,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint } PredicateTable *predicate = (PredicateTable *)constraint->predicate; switch (predicate->undefinedbehavior) { - case IGNOREBEHAVIOR: + case SATC_IGNOREBEHAVIOR: case FLAGFORCEUNDEFINED: return encodeEnumEntriesTablePredicateSATEncoder(constraint); default: @@ -178,7 +178,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) { UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior; - ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); + ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); Array *elements = &func->inputs; Table *table = ((FunctionTable *) (func->function))->table; uint size = table->entries->getSize(); @@ -197,7 +197,7 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) Edge output = getElementValueConstraint(func, entry->output); Edge row; switch (undefStatus ) { - case IGNOREBEHAVIOR: { + case SATC_IGNOREBEHAVIOR: { row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output); break; } @@ -230,7 +230,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc FunctionTable *function = (FunctionTable *)elemFunc->function; switch (function->undefBehavior) { - case IGNOREBEHAVIOR: + case SATC_IGNOREBEHAVIOR: case FLAGFORCEUNDEFINED: return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc); default: diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index f48b72d..10a87dd 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -15,9 +15,9 @@ Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) { switch ( constraint->order->type) { - case PARTIAL: + case SATC_PARTIAL: return encodePartialOrderSATEncoder(constraint); - case TOTAL: + case SATC_TOTAL: return encodeTotalOrderSATEncoder(constraint); default: ASSERT(0); @@ -76,7 +76,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) { } Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) { - ASSERT(boolOrder->order->type == TOTAL); + ASSERT(boolOrder->order->type == SATC_TOTAL); if (boolOrder->order->orderPairTable == NULL) { boolOrder->order->initializeOrderHashTable(); bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); @@ -96,7 +96,7 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) { #ifdef CONFIG_DEBUG model_print("in total order ...\n"); #endif - ASSERT(order->type == TOTAL); + ASSERT(order->type == SATC_TOTAL); Set *set = order->set; uint size = order->set->getSize(); for (uint i = 0; i < size; i++) { @@ -144,6 +144,6 @@ Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJ } Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) { - ASSERT(constraint->order->type == PARTIAL); + ASSERT(constraint->order->type == SATC_PARTIAL); return E_BOGUS; } diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc index 1cd0815..766c5c7 100644 --- a/src/Backend/sattranslator.cc +++ b/src/Backend/sattranslator.cc @@ -90,7 +90,7 @@ HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, OrderPair pair(first, second, E_NULL); Edge var = getOrderConstraint(order->orderPairTable, &pair); if (edgeIsNull(var)) - return UNORDERED; - return getValueCNF(This->getSATEncoder()->getCNF(), var) ? FIRST : SECOND; + return SATC_UNORDERED; + return getValueCNF(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND; } diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc index 0729584..bbb2485 100644 --- a/src/Test/buildconstraintstest.cc +++ b/src/Test/buildconstraintstest.cc @@ -23,14 +23,14 @@ int main(int numargs, char **argv) { Element *e1 = solver->getElementVar(s); Element *e2 = solver->getElementVar(s); Set *domain[] = {s, s}; - Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2); + Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2); Element *inputs[] = {e1, e2}; Boolean *b = solver->applyPredicate(equals, inputs, 2); solver->addConstraint(b); uint64_t set2[] = {2, 3}; Set *rangef1 = solver->createSet(1, set2, 2); - Function *f1 = solver->createFunctionOperator(ADD, domain, 2, setbig, IGNORE); + Function *f1 = solver->createFunctionOperator(SATC_ADD, domain, 2, setbig, SATC_IGNORE); Table *table = solver->createTable(domain, 2, s); uint64_t row1[] = {0, 1}; @@ -41,12 +41,12 @@ int main(int numargs, char **argv) { solver->addTableEntry(table, row2, 2, 0); solver->addTableEntry(table, row3, 2, 2); solver->addTableEntry(table, row4, 2, 2); - Function *f2 = solver->completeTable(table, IGNOREBEHAVIOR); //its range would be as same as s + Function *f2 = solver->completeTable(table, SATC_IGNOREBEHAVIOR); //its range would be as same as s Boolean *overflow = solver->getBooleanVar(2); Element *e3 = solver->applyFunction(f1, inputs, 2, overflow); Element *e4 = solver->applyFunction(f2, inputs, 2, overflow); Set *domain2[] = {s,rangef1}; - Predicate *equal2 = solver->createPredicateOperator(EQUALS, domain2, 2); + Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2); Element *inputs2 [] = {e4, e3}; Boolean *pred = solver->applyPredicate(equal2, inputs2, 2); solver->addConstraint(pred); diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc index 87355b1..53f8212 100644 --- a/src/Test/elemequalsattest.cc +++ b/src/Test/elemequalsattest.cc @@ -20,7 +20,7 @@ int main(int numargs, char **argv) { Element *e1 = solver->getElementVar(s1); Element *e2 = solver->getElementVar(s2); Set *domain[] = {s1, s2}; - Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2); + Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2); Element *inputs[] = {e1, e2}; Boolean *b = solver->applyPredicate(equals, inputs, 2); solver->addConstraint(b); diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc index 5b78583..5ec2bca 100644 --- a/src/Test/elemequalunsattest.cc +++ b/src/Test/elemequalunsattest.cc @@ -15,7 +15,7 @@ int main(int numargs, char **argv) { Element *e1 = solver->getElementVar(s1); Element *e2 = solver->getElementVar(s2); Set *domain[] = {s1, s2}; - Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2); + Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2); Element *inputs[] = {e1, e2}; Boolean *b = solver->applyPredicate(equals, inputs, 2); solver->addConstraint(b); diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc index b842ff0..d6a7962 100644 --- a/src/Test/funcencodingtest.cc +++ b/src/Test/funcencodingtest.cc @@ -34,7 +34,7 @@ int main(int numargs, char **argv) { Boolean *overflow = solver->getBooleanVar(2); Set *d1[] = {s1, s2}; //change the overflow flag - Function *f1 = solver->createFunctionOperator(SUB, d1, 2, s2, IGNORE); + Function *f1 = solver->createFunctionOperator(SATC_SUB, d1, 2, s2, SATC_IGNORE); Element *in1[] = {e1, e2}; Element *e3 = solver->applyFunction(f1, in1, 2, overflow); Table *t1 = solver->createTable(d1, 2, s3); @@ -42,7 +42,7 @@ int main(int numargs, char **argv) { uint64_t row2[] = {6, 4}; solver->addTableEntry(t1, row1, 2, 3); solver->addTableEntry(t1, row2, 2, 1); - Function *f2 = solver->completeTable(t1, IGNOREBEHAVIOR); + Function *f2 = solver->completeTable(t1, SATC_IGNOREBEHAVIOR); Element *e4 = solver->applyFunction(f2, in1, 2, overflow); Set *d2[] = {s1}; @@ -50,7 +50,7 @@ int main(int numargs, char **argv) { Table *t2 = solver->createTable(d2, 1, s1); uint64_t row3[] = {6}; solver->addTableEntry(t2, row3, 1, 6); - Function *f3 = solver->completeTable(t2, IGNOREBEHAVIOR); + Function *f3 = solver->completeTable(t2, SATC_IGNOREBEHAVIOR); Element *e5 = solver->applyFunction(f3, in2, 1, overflow); Set *d3[] = {s2, s3, s1}; @@ -64,11 +64,11 @@ int main(int numargs, char **argv) { solver->addTableEntry(t3, row5, 3, 1); solver->addTableEntry(t3, row6, 3, 2); solver->addTableEntry(t3, row7, 3, 1); - Function *f4 = solver->completeTable(t3, IGNOREBEHAVIOR); + Function *f4 = solver->completeTable(t3, SATC_IGNOREBEHAVIOR); Element *e6 = solver->applyFunction(f4, in3, 3, overflow); Set *deq[] = {s5,s4}; - Predicate *gt = solver->createPredicateOperator(GT, deq, 2); + Predicate *gt = solver->createPredicateOperator(SATC_GT, deq, 2); Element *inputs2 [] = {e7, e6}; Boolean *pred = solver->applyPredicate(gt, inputs2, 2); solver->addConstraint(pred); diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc index 7e1104d..ece659e 100644 --- a/src/Test/logicopstest.cc +++ b/src/Test/logicopstest.cc @@ -12,18 +12,18 @@ int main(int numargs, char **argv) { Boolean *b2 = solver->getBooleanVar(0); Boolean *b3 = solver->getBooleanVar(0); Boolean *b4 = solver->getBooleanVar(0); - //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES + //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES Boolean *barray1[] = {b1,b2}; - Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2); + Boolean *andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2); Boolean *barray2[] = {andb1b2, b3}; - Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2); + Boolean *imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2); solver->addConstraint(imply); Boolean *barray3[] = {b3}; - Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1); + Boolean *notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1); Boolean *barray4[] = {notb3, b4}; - solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2)); + solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2)); Boolean *barray5[] = {b1, b4}; - solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2)); + solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2)); if (solver->startEncoding() == 1) printf("b1=%d b2=%d b3=%d b4=%d\n", solver->getBooleanValue(b1), solver->getBooleanValue(b2), diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc index 4828882..b110f29 100644 --- a/src/Test/ltelemconsttest.cc +++ b/src/Test/ltelemconsttest.cc @@ -14,7 +14,7 @@ int main(int numargs, char **argv) { Element *e1 = solver->getElementConst(4, 5); Element *e2 = solver->getElementVar(s3); Set *domain2[] = {s1, s3}; - Predicate *lt = solver->createPredicateOperator(LT, domain2, 2); + Predicate *lt = solver->createPredicateOperator(SATC_LT, domain2, 2); Element *inputs2[] = {e1, e2}; Boolean *b = solver->applyPredicate(lt, inputs2, 2); solver->addConstraint(b); diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index c6f5918..ccf1933 100644 --- a/src/Test/ordergraphtest.cc +++ b/src/Test/ordergraphtest.cc @@ -4,7 +4,7 @@ int main(int numargs, char **argv) { CSolver *solver = new CSolver(); uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8}; Set *s = solver->createSet(0, set1, 8); - Order *order = solver->createOrder(TOTAL, s); + Order *order = solver->createOrder(SATC_TOTAL, s); Boolean *o12 = solver->orderConstraint(order, 1, 2); Boolean *o13 = solver->orderConstraint(order, 1, 3); Boolean *o24 = solver->orderConstraint(order, 2, 4); @@ -17,34 +17,34 @@ int main(int numargs, char **argv) { Boolean *o81 = solver->orderConstraint(order, 8, 1); Boolean * array1[]={o12, o13, o24, o34}; - solver->addConstraint(solver->applyLogicalOperation(L_OR, array1, 4) ); + solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) ); Boolean * array2[]={o41, o57}; - Boolean *b1 = solver->applyLogicalOperation(L_XOR, array2, 2); + Boolean *b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2); Boolean * array3[]={o34}; - Boolean *o34n = solver->applyLogicalOperation(L_NOT, array3, 1); + Boolean *o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1); Boolean * array4[]={o24}; - Boolean *o24n = solver->applyLogicalOperation(L_NOT, array4, 1); + Boolean *o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1); Boolean * array5[]={o34n, o24n}; - Boolean *b2 = solver->applyLogicalOperation(L_OR, array5, 2); + Boolean *b2 = solver->applyLogicalOperation(SATC_OR, array5, 2); Boolean * array6[] = {b1, b2}; - solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, array6, 2) ); + solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) ); Boolean * array7[] = {o12, o13}; - solver->addConstraint(solver->applyLogicalOperation(L_AND, array7, 2) ); + solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) ); Boolean * array8[] = {o76, o65}; - solver->addConstraint(solver->applyLogicalOperation(L_OR, array8, 2) ); + solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) ); Boolean * array9[] = {o76, o65}; - Boolean* b3= solver->applyLogicalOperation(L_AND, array9, 2) ; + Boolean* b3= solver->applyLogicalOperation(SATC_AND, array9, 2) ; Boolean * array10[] = {o57}; - Boolean* o57n= solver->applyLogicalOperation(L_NOT, array10, 1); + Boolean* o57n= solver->applyLogicalOperation(SATC_NOT, array10, 1); Boolean * array11[] = {b3, o57n}; - solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, array11, 2)); + solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2)); Boolean * array12[] = {o58, o81}; - solver->addConstraint(solver->applyLogicalOperation(L_AND, array12, 2) ); + solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) ); /* if (solver->startEncoding() == 1) printf("SAT\n"); diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc index e2d974b..893338d 100644 --- a/src/Test/ordertest.cc +++ b/src/Test/ordertest.cc @@ -10,7 +10,7 @@ int main(int numargs, char **argv) { CSolver *solver = new CSolver(); uint64_t set1[] = {5, 1, 4}; Set *s = solver->createSet(0, set1, 3); - Order *order = solver->createOrder(TOTAL, s); + Order *order = solver->createOrder(SATC_TOTAL, s); Boolean *b1 = solver->orderConstraint(order, 5, 1); Boolean *b2 = solver->orderConstraint(order, 1, 4); solver->addConstraint(b1); diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc index f0610e4..a7367c9 100644 --- a/src/Test/tablefuncencodetest.cc +++ b/src/Test/tablefuncencodetest.cc @@ -45,7 +45,7 @@ int main(int numargs, char **argv) { Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow); Set *deq[] = {s3,s2}; - Predicate *lte = solver->createPredicateOperator(LTE, deq, 2); + Predicate *lte = solver->createPredicateOperator(SATC_LTE, deq, 2); Element *inputs2 [] = {e4, e3}; Boolean *pred = solver->applyPredicate(lte, inputs2, 2); solver->addConstraint(pred); diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc index d1e45de..ee60877 100644 --- a/src/Test/tablepredicencodetest.cc +++ b/src/Test/tablepredicencodetest.cc @@ -47,13 +47,13 @@ int main(int numargs, char **argv) { solver->addConstraint(b1); Set *deq[] = {s3,s2}; - Predicate *gte = solver->createPredicateOperator(GTE, deq, 2); + Predicate *gte = solver->createPredicateOperator(SATC_GTE, deq, 2); Element *inputs2 [] = {e3, e2}; Boolean *pred = solver->applyPredicate(gte, inputs2, 2); solver->addConstraint(pred); Set *d1[] = {s1, s2}; - Predicate *eq = solver->createPredicateOperator(EQUALS, d1, 2); + Predicate *eq = solver->createPredicateOperator(SATC_EQUALS, d1, 2); Element *tmparray2[] = {e1, e2}; Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2); solver->addConstraint(pred2); diff --git a/src/common.cc b/src/common.cc index 660472f..f54756b 100644 --- a/src/common.cc +++ b/src/common.cc @@ -3,4 +3,4 @@ void assert_hook(void) { model_print("Add breakpoint to line %u in file %s.\n", __LINE__, __FILE__); -} \ No newline at end of file +} diff --git a/src/csolver.cc b/src/csolver.cc index 9102add..8631518 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -215,8 +215,8 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { Boolean * newarray[asize]; switch(op) { - case L_NOT: { - if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==L_NOT) { + case SATC_NOT: { + if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) { return ((BooleanLogic *) array[0])->inputs.get(0); } else if (array[0]->type == BOOLCONST) { bool isTrue = ((BooleanConst *) array[0])->isTrue; @@ -224,20 +224,20 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) } break; } - case L_XOR: { + case SATC_XOR: { for(uint i=0;i<2;i++) { if (array[i]->type == BOOLCONST) { bool isTrue = ((BooleanConst *) array[i])->isTrue; if (isTrue) { newarray[0]=array[1-i]; - return applyLogicalOperation(L_NOT, newarray, 1); + return applyLogicalOperation(SATC_NOT, newarray, 1); } else return array[1-i]; } } break; } - case L_OR: { + case SATC_OR: { uint newindex=0; for(uint i=0;itype==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == L_NOT; - bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == L_NOT; + bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT; + bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT; if (isNot0 != isNot1) { if (isNot0) { @@ -264,7 +264,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) array[1] = array[0]; array[0] = tmp; } - return applyLogicalOperation(L_IMPLIES, newarray, 2); + return applyLogicalOperation(SATC_IMPLIES, newarray, 2); } } else { array = newarray; @@ -272,7 +272,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) } break; } - case L_AND: { + case SATC_AND: { uint newindex=0; for(uint i=0;itype == BOOLCONST) { BooleanConst *b=(BooleanConst *) array[0]; if (b->isTrue) { @@ -306,7 +306,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) if (b->isTrue) { return b; } else { - return applyLogicalOperation(L_NOT, array, 1); + return applyLogicalOperation(SATC_NOT, array, 1); } } break; -- 2.34.1