renaming

diff --git a/src/AST/function.cc b/src/AST/function.cc
index 1d910e48e9ea0d7d2185357de7633d6384c97fc3..6715e79e06e0115dc91449c02c768f4a7028472d 100644 (file)
--- 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) {
 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;
                return values[0] + values[1];
                break;

-       case SUB:
+       case SATC_SUB:

                return values[0] - values[1];
                break;
        default:
                return values[0] - values[1];
                break;
        default:

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 1f9c19761ba86539f847c48cc7d25fe813c4f0b5..882e793d46dec90a3dcb2c294718bae869adabef 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -1,32 +1,32 @@
 #ifndef OPS_H
 #define OPS_H
 #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;
 
 typedef enum LogicOp LogicOp;
 

-enum ArithOp {ADD, SUB};
+enum ArithOp {SATC_ADD, SATC_SUB};

 typedef enum ArithOp ArithOp;
 
 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;
 
 typedef enum CompOp CompOp;
 

-enum OrderType {PARTIAL, TOTAL};
+enum OrderType {SATC_PARTIAL, SATC_TOTAL};

 typedef enum OrderType OrderType;
 
 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
 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
  */
  *  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;
 
 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};
 typedef enum UndefinedBehavior UndefinedBehavior;
 
 enum FunctionType {TABLEFUNC, OPERATORFUNC};

diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index 99cd311757051f10da2a8dccb0a4b6062fda65f3..d359811663dedab5d83ecb35c7fb84db889548d7 100644 (file)
--- 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) {
 
 bool PredicateOperator::evalPredicateOperator(uint64_t *inputs) {
        switch (op) {

-       case EQUALS:
+       case SATC_EQUALS:

                return inputs[0] == inputs[1];
                return inputs[0] == inputs[1];

-       case LT:
+       case SATC_LT:

                return inputs[0] < inputs[1];
                return inputs[0] < inputs[1];

-       case GT:
+       case SATC_GT:

                return inputs[0] > inputs[1];
                return inputs[0] > inputs[1];

-       case LTE:
+       case SATC_LTE:

                return inputs[0] <= inputs[1];
                return inputs[0] <= inputs[1];

-       case GTE:
+       case SATC_GTE:

                return inputs[0] >= inputs[1];
        }
        ASSERT(0);
                return inputs[0] >= inputs[1];
        }
        ASSERT(0);

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index f32fc91b0e945d74ea94f4e8df5e250ce94e17fe..bfc321cf7b76f62e7fc159e6a39045c1edad3398 100644 (file)
--- 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) {
                Boolean *parent = bexpr->parents.get(i);
                BooleanLogic *logicop = (BooleanLogic *) parent;
                switch (logicop->op) {

-               case L_AND:
+               case SATC_AND:

                        handleANDTrue(logicop, bexpr);
                        break;
                        handleANDTrue(logicop, bexpr);
                        break;

-               case L_OR:
+               case SATC_OR:

                        replaceBooleanWithTrue(parent);
                        break;
                        replaceBooleanWithTrue(parent);
                        break;

-               case L_NOT:
+               case SATC_NOT:

                        replaceBooleanWithFalse(parent);
                        break;
                        replaceBooleanWithFalse(parent);
                        break;

-               case L_XOR:
+               case SATC_XOR:

                        handleXORTrue(logicop, bexpr);
                        break;
                        handleXORTrue(logicop, bexpr);
                        break;

-               case L_IMPLIES:
+               case SATC_IMPLIES:

                        handleIMPLIESTrue(logicop, bexpr);
                        break;
                }
                        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);
        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) {
 }
 
 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);
        } 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) {
                Boolean *parent = bexpr->parents.get(i);
                BooleanLogic *logicop = (BooleanLogic *) parent;
                switch (logicop->op) {

-               case L_AND:
+               case SATC_AND:

                        replaceBooleanWithFalse(parent);
                        break;
                        replaceBooleanWithFalse(parent);
                        break;

-               case L_OR:
+               case SATC_OR:

                        handleORFalse(logicop, bexpr);
                        break;
                        handleORFalse(logicop, bexpr);
                        break;

-               case L_NOT:
+               case SATC_NOT:

                        replaceBooleanWithTrue(parent);
                        break;
                        replaceBooleanWithTrue(parent);
                        break;

-               case L_XOR:
+               case SATC_XOR:

                        handleXORFalse(logicop, bexpr);
                        break;
                        handleXORFalse(logicop, bexpr);
                        break;

-               case L_IMPLIES:
+               case SATC_IMPLIES:

                        handleIMPLIESFalse(logicop, bexpr);
                        break;
                }
                        handleIMPLIESFalse(logicop, bexpr);
                        break;
                }

diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
index 9942b740fec5ee4841fd351de943231aa94f1528..9f53d1134fb3a42256f7aed05017edda007a539a 100644 (file)
--- 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: {
                        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;
                        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: {
                        break;
        }
        case BV_MUSTBEFALSE: {

-               if (order->type == TOTAL) {
+               if (order->type == SATC_TOTAL) {

                        OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
                        _2to1->mustPos = true;
                        _2to1->polPos = true;
                        OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
                        _2to1->mustPos = true;
                        _2to1->polPos = true;

diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h
index 36bb3dfcc339f898a9c4bad0074fc52e7374a492..550bf1ed3719e0bda852928b1e9fc255843d054b 100644 (file)
--- a/src/ASTAnalyses/ordernode.h
+++ b/src/ASTAnalyses/ordernode.h
@@ -14,7 +14,7 @@
 #include "structs.h"
 #include "orderedge.h"
 
 #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 {
 typedef enum NodeStatus NodeStatus;
 
 class OrderNode {

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index ea60ca873741f79b8e2f9a8b849909e719747e2f..f0dac379af4dbb999370f5a35dd0099970393956 100644 (file)
--- 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) {
 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);
                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;
        }
                }
                break;
        }

-       case L_NOT: {
+       case SATC_NOT: {

                Boolean *tmp = This->inputs.get(0);
                updatePolarity(tmp, negatePolarity(parentpolarity));
                break;
        }
                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;
        }
                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);
                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) {
 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++) {
                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;
        }
                }
                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++) {
                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;
        }
                }
                return;
        }

-       case L_NOT:
+       case SATC_NOT:

                updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
                return;
                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();
                //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;
                        updateMustValue(This->inputs.get(1), parentbv);
                }
                return;

-       case L_XOR:
+       case SATC_XOR:

                return;
        default:
                ASSERT(0);
                return;
        default:
                ASSERT(0);

diff --git a/src/ASTTransform/analyzer.cc b/src/ASTTransform/analyzer.cc
index cfc01a840d2224c6977b6b09d917d2f32bb51478..05329a545e10538473620f1cfbbd03dffa285106 100644 (file)
--- a/src/ASTTransform/analyzer.cc
+++ b/src/ASTTransform/analyzer.cc
@@ -28,7 +28,7 @@ void orderAnalysis(CSolver *This) {
                }
 
                OrderGraph *graph = buildOrderGraph(order);
                }
 
                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
                        //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 (mustReachLocal) {
                        //This pair of analysis is also optional

-                       if (order->type == PARTIAL) {
+                       if (order->type == SATC_PARTIAL) {

                                localMustAnalysisPartial(This, graph);
                        } else {
                                localMustAnalysisTotal(This, graph);
                                localMustAnalysisPartial(This, graph);
                        } else {
                                localMustAnalysisTotal(This, graph);

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 598928d7be922455e3ca0f6833dd2add23fac9c2..d458b2f07811e293f6ce65ea6b1fc4515dad60ad 100644 (file)
--- 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);
                                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);
                        }
                                        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);
                        }
                                ((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);
                        }
                                ((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);
                                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) {
        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);
                }
        }
                        model_print("i=%u\t", i);
                }
        }

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 2d405e0fe82712f527d05252829793aff4a0c7b8..7d7ea92896110f8f796e1870cc0b8174e0035958 100644 (file)
--- 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);
 
 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};
        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);
        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 dd536e02e5989b7903eb872908194c1ec4f352f4..b9a991698f48509db855e20bbda4631bc2af913c 100644 (file)
--- 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
 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
        printCNF(constraint);
        model_print("\n******************************\n");
 #endif

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 175cfc9d48c50e681f6f5e93a8e5c0a2128a9e13..dcd70bcc1a37b6c47741efb3eb6f154fc1a0f001 100644 (file)
--- 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) {
                array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
 
        switch (constraint->op) {

-       case L_AND:
+       case SATC_AND:

                return constraintAND(cnf, constraint->inputs.getSize(), array);
                return constraintAND(cnf, constraint->inputs.getSize(), array);

-       case L_OR:
+       case SATC_OR:

                return constraintOR(cnf, constraint->inputs.getSize(), array);
                return constraintOR(cnf, constraint->inputs.getSize(), array);

-       case L_NOT:
+       case SATC_NOT:

                return constraintNegate(array[0]);
                return constraintNegate(array[0]);

-       case L_XOR:
+       case SATC_XOR:

                return constraintXOR(cnf, array[0], array[1]);
                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);
                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 d416a15a48113f6c3cc7b5d95ed5ed224b77de01..39a50dba6ba9439384e76765df79f0efa4fcd5b9 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -133,9 +133,9 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 
                        Edge clause;
                        switch (function->overflowbehavior) {
 
                        Edge clause;
                        switch (function->overflowbehavior) {

-                       case IGNORE:
+                       case SATC_IGNORE:

                        case NOOVERFLOW:
                        case NOOVERFLOW:

-                       case WRAPAROUND: {
+                       case SATC_WRAPAROUND: {

                                clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
                                break;
                        }
                                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) {
        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);
                return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);

-       case LT:
+       case SATC_LT:

                return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
                return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);

-       case GT:
+       case SATC_GT:

                return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
        default:
                ASSERT(0);
                return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
        default:
                ASSERT(0);

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 633d7163e7a0f1bb2dcd21b7d4ac37430f8272fb..ed8b6c9dff06e629163179e45e7e19e2dfa04451 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;
 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<Element *> *inputs = &constraint->inputs;
        Table *table = ((PredicateTable *)constraint->predicate)->table;
        FunctionEncodingType encType = constraint->encoding.type;
        Array<Element *> *inputs = &constraint->inputs;


@@ -28,7 +28,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
        uint i = 0;
        while (iterator->hasNext()) {
                TableEntry *entry = iterator->next();
        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;
                }
                        //Skip the irrelevant entries
                        continue;
                }


@@ -41,7 +41,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
                }
                Edge row;
                switch (undefStatus) {
                }
                Edge row;
                switch (undefStatus) {

-               case IGNOREBEHAVIOR:
+               case SATC_IGNOREBEHAVIOR:

                        row = constraintAND(cnf, inputNum, carray);
                        break;
                case FLAGFORCEUNDEFINED: {
                        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) {
        }
        PredicateTable *predicate = (PredicateTable *)constraint->predicate;
        switch (predicate->undefinedbehavior) {

-       case IGNOREBEHAVIOR:
+       case SATC_IGNOREBEHAVIOR:

        case FLAGFORCEUNDEFINED:
                return encodeEnumEntriesTablePredicateSATEncoder(constraint);
        default:
        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;
 
 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
        UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;

-       ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+       ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);

        Array<Element *> *elements = &func->inputs;
        Table *table = ((FunctionTable *) (func->function))->table;
        uint size = table->entries->getSize();
        Array<Element *> *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 ) {
                Edge output = getElementValueConstraint(func, entry->output);
                Edge row;
                switch (undefStatus ) {

-               case IGNOREBEHAVIOR: {
+               case SATC_IGNOREBEHAVIOR: {

                        row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
                        break;
                }
                        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) {
 
        FunctionTable *function = (FunctionTable *)elemFunc->function;
        switch (function->undefBehavior) {

-       case IGNOREBEHAVIOR:
+       case SATC_IGNOREBEHAVIOR:

        case FLAGFORCEUNDEFINED:
                return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
        default:
        case FLAGFORCEUNDEFINED:
                return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
        default:

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index f48b72dbd7ee4dead8e55780ae36c47b3af93b94..10a87dd8c8a6e705d725b9b3677f5ab3c0040191 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -15,9 +15,9 @@
 
 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
        switch ( constraint->order->type) {
 
 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
        switch ( constraint->order->type) {

-       case PARTIAL:
+       case SATC_PARTIAL:

                return encodePartialOrderSATEncoder(constraint);
                return encodePartialOrderSATEncoder(constraint);

-       case TOTAL:
+       case SATC_TOTAL:

                return encodeTotalOrderSATEncoder(constraint);
        default:
                ASSERT(0);
                return encodeTotalOrderSATEncoder(constraint);
        default:
                ASSERT(0);


@@ -76,7 +76,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 }
 
 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
 }
 
 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);
        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
 #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++) {
        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) {
 }
 
 Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {

-       ASSERT(constraint->order->type == PARTIAL);
+       ASSERT(constraint->order->type == SATC_PARTIAL);

        return E_BOGUS;
 }
        return E_BOGUS;
 }

diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc
index 1cd08156282b9263c03b2a39dc1ebc861e94d9fb..766c5c7cf6928f78e481a49d27d98ce85c09a06b 100644 (file)
--- 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))
        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 07295844d4c51b33825577b90881612ea3cc2863..bbb2485bc3245fa82b55826a69e37de1736e5f35 100644 (file)
--- 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};
        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);
        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};
 
        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);
        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};
        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);
        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 87355b11df7fa4c18ea5f6e854cba56f88ca3f99..53f82127939f5316072b4c01916d501e3403a322 100644 (file)
--- 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};
        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);
        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 5b78583806ca291a2f7596ecee0f13a9fc0a4268..5ec2bcafcd9002234d83fba9f867edcb90efa386 100644 (file)
--- 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};
        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);
        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 b842ff02117e8f3c496a92bb88a43a2fa6645404..d6a796200d7dc30fee4e8eeafa4d231ac902a3a1 100644 (file)
--- 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
        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);
        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);
        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};
        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);
        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};
        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);
        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};
        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);
        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 7e1104dd8fe24870fd39ac8c0889d0e1f4ea6d0c..ece659e4699aafa14fc8861ac2d31a871677d118 100644 (file)
--- 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);
        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 *barray1[] = {b1,b2};

-       Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2);
+       Boolean *andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);

        Boolean *barray2[] = {andb1b2, b3};
        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};
        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};
        Boolean *barray4[] = {notb3, b4};

-       solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));

        Boolean *barray5[] = {b1, b4};
        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),
        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 4828882e67a39002ad8ed16908d7e8e0f31fb37b..b110f29b8698b06d0e6cd19de9abc863afc7d484 100644 (file)
--- 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};
        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);
        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 c6f59186ca2013559a1c113aa083f8545484644a..ccf1933a5e9110dbc99bc81e97410ac602f6a57b 100644 (file)
--- 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);
        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);
        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};
        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 * array2[]={o41, o57};
        

-       Boolean *b1 = solver->applyLogicalOperation(L_XOR, array2, 2);
+       Boolean *b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);

        Boolean * array3[]={o34};
        Boolean * array3[]={o34};

-       Boolean *o34n = solver->applyLogicalOperation(L_NOT, array3, 1);
+       Boolean *o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);

        Boolean * array4[]={o24};
        Boolean * array4[]={o24};

-       Boolean *o24n = solver->applyLogicalOperation(L_NOT, array4, 1);
+       Boolean *o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);

        Boolean * array5[]={o34n, o24n};
        Boolean * array5[]={o34n, o24n};

-       Boolean *b2 = solver->applyLogicalOperation(L_OR, array5, 2);
+       Boolean *b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);

        Boolean * array6[] = {b1, b2};
        Boolean * array6[] = {b1, b2};

-       solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, array6, 2) );
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );

 
        Boolean * array7[] = {o12, o13};
 
        Boolean * array7[] = {o12, o13};

-       solver->addConstraint(solver->applyLogicalOperation(L_AND, array7, 2) );
+       solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );

 
        Boolean * array8[] = {o76, o65};
 
        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 * array9[] = {o76, o65};

-       Boolean* b3= solver->applyLogicalOperation(L_AND, array9, 2) ;
+       Boolean* b3= solver->applyLogicalOperation(SATC_AND, array9, 2) ;

        Boolean * array10[] = {o57};
        Boolean * array10[] = {o57};

-       Boolean* o57n= solver->applyLogicalOperation(L_NOT, array10, 1);
+       Boolean* o57n= solver->applyLogicalOperation(SATC_NOT, array10, 1);

        Boolean * array11[] = {b3, o57n};
        Boolean * array11[] = {b3, o57n};

-       solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, array11, 2));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));

 
        Boolean * array12[] = {o58, o81};
 
        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");
        
        /*      if (solver->startEncoding() == 1)
                printf("SAT\n");

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index e2d974bed1d3893d256d491bcc9fd284a7f9e508..893338dd5419da5e9e0617ec1e079019054f9792 100644 (file)
--- 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);
        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);
        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 f0610e4bb28f3d10d8a48509299497f16fb6a12d..a7367c993233422f09b94a09d4f7e1f453ad0939 100644 (file)
--- 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};
        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);
        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 d1e45dedb707670447b05ac0d0dcde1c7c6a32f2..ee608779d6b20c036b952ca75b85994440188ac8 100644 (file)
--- 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};
        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};
        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);
        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 660472f3aded9552611aca28fbe2771812ab845d..f54756b523ea07abca8f8c1256b3492965cad416 100644 (file)
--- 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__);
 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 9102add0d16d83043e588274fcc80c445f8e3d7a..86315183a179da649ff08a179ec1fc8a8c4284d3 100644 (file)
--- 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) {
 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;
                        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;
        }
                }
                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];
                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;
        }
                                } else
                                        return array[1-i];
                        }
                }
                break;
        }

-       case L_OR: {
+       case SATC_OR: {

                uint newindex=0;
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                uint newindex=0;
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];


@@ -253,8 +253,8 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                if (newindex==1)
                        return newarray[0];
                else if (newindex == 2) {
                if (newindex==1)
                        return newarray[0];
                else if (newindex == 2) {

-                       bool isNot0 = (newarray[0]->type==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) {
 
                        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;
                                }
                                        array[1] = array[0];
                                        array[0] = tmp;
                                }

-                               return applyLogicalOperation(L_IMPLIES, newarray, 2);
+                               return applyLogicalOperation(SATC_IMPLIES, newarray, 2);

                        }
                } else {
                        array = newarray;
                        }
                } else {
                        array = newarray;


@@ -272,7 +272,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                }
                break;
        }
                }
                break;
        }

-       case L_AND: {
+       case SATC_AND: {

                uint newindex=0;
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                uint newindex=0;
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];


@@ -293,7 +293,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                }
                break;
        }
                }
                break;
        }

-       case L_IMPLIES: {
+       case SATC_IMPLIES: {

                if (array[0]->type == BOOLCONST) {
                        BooleanConst *b=(BooleanConst *) array[0];
                        if (b->isTrue) {
                if (array[0]->type == 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 {
                        if (b->isTrue) {
                                return b;
                        } else {

-                               return applyLogicalOperation(L_NOT, array, 1);
+                               return applyLogicalOperation(SATC_NOT, array, 1);

                        }
                }
                break;
                        }
                }
                break;