edits
authorbdemsky <bdemsky@uci.edu>
Fri, 25 Aug 2017 02:11:49 +0000 (19:11 -0700)
committerbdemsky <bdemsky@uci.edu>
Fri, 25 Aug 2017 02:11:49 +0000 (19:11 -0700)
src/Test/Makefile
src/Test/buildconstraintstest.cc
src/Test/elemequalunsattest.cc
src/Test/funcencodingtest.cc
src/Test/ordertest.cc
src/classlist.h
src/csolver.cc
src/csolver.h

index 2c24d58..0f1bc39 100644 (file)
@@ -13,7 +13,7 @@ all: $(OBJECTS) ../bin/run.sh
 -include $(DEPS)
 
 ../bin/%: %.cc
-       $(CC) -MMD -MF $(@D)/.$(@F).d -o ../bin/$@ $< $(CPPFLAGS) -L$(BASE)/bin/ -l_cons_comp
+       $(CXX) -MMD -MF $(@D)/.$(@F).d -o ../bin/$@ $< $(CPPFLAGS) -L$(BASE)/bin/ -l_cons_comp
 
 ../bin/run.sh: run.sh
        cp run.sh ../bin/run.sh
index 71dbafd..af28c49 100644 (file)
  * Result: UNSAT!
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {0, 1, 2};
        uint64_t setbigarray[] = {0, 1, 2, 3, 4};
 
-       Set *s = createSet(solver, 0, set1, 3);
-       Set *setbig = createSet(solver, 0, setbigarray, 5);
-       Element *e1 = getElementVar(solver, s);
-       Element *e2 = getElementVar(solver, s);
+       Set *s = solver->createSet(0, set1, 3);
+       Set *setbig = solver->createSet(0, setbigarray, 5);
+       Element *e1 = solver->getElementVar(s);
+       Element *e2 = solver->getElementVar(s);
        Set *domain[] = {s, s};
-       Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};
-       Boolean *b = applyPredicate(solver, equals, inputs, 2);
-       addConstraint(solver, b);
+       Boolean *b = solver->applyPredicate(equals, inputs, 2);
+       solver->addConstraint(b);
 
        uint64_t set2[] = {2, 3};
-       Set *rangef1 = createSet(solver, 1, set2, 2);
-       Function *f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE);
+       Set *rangef1 = solver->createSet(1, set2, 2);
+       Function *f1 = solver->createFunctionOperator(ADD, domain, 2, setbig, IGNORE);
 
-       Table *table = createTable(solver, domain, 2, s);
+       Table *table = solver->createTable(domain, 2, s);
        uint64_t row1[] = {0, 1};
        uint64_t row2[] = {1, 1};
        uint64_t row3[] = {2, 1};
        uint64_t row4[] = {2, 2};
-       addTableEntry(solver, table, row1, 2, 0);
-       addTableEntry(solver, table, row2, 2, 0);
-       addTableEntry(solver, table, row3, 2, 2);
-       addTableEntry(solver, table, row4, 2, 2);
-       Function *f2 = completeTable(solver, table, IGNOREBEHAVIOR);    //its range would be as same as s
-       Boolean *overflow = getBooleanVar(solver, 2);
-       Element *e3 = applyFunction(solver, f1, inputs, 2, overflow);
-       Element *e4 = applyFunction(solver, f2, inputs, 2, overflow);
+       solver->addTableEntry(table, row1, 2, 0);
+       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
+       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 = createPredicateOperator(solver, EQUALS, domain2, 2);
+       Predicate *equal2 = solver->createPredicateOperator(EQUALS, domain2, 2);
        Element *inputs2 [] = {e4, e3};
-       Boolean *pred = applyPredicate(solver, equal2, inputs2, 2);
-       addConstraint(solver, pred);
+       Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
+solver->       addConstraint(pred);
 
-       if (startEncoding(solver) == 1)
-               printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+       if (solver->startEncoding() == 1)
+               printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }
index 5cbdd04..c470485 100644 (file)
@@ -7,22 +7,22 @@
  * Result: UNSAT
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {0, 1, 2};
        uint64_t set2[] = {3, 4};
-       Set *s1 = createSet(solver, 0, set1, 3);
-       Set *s2 = createSet(solver, 0, set2, 2);
-       Element *e1 = getElementVar(solver, s1);
-       Element *e2 = getElementVar(solver, s2);
+       Set *s1 = solver->createSet(0, set1, 3);
+       Set *s2 = solver->createSet(0, set2, 2);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
        Set *domain[] = {s1, s2};
-       Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2);
+       Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};
-       Boolean *b = applyPredicate(solver, equals, inputs, 2);
-       addConstraint(solver, b);
+       Boolean *b = solver->applyPredicate(equals, inputs, 2);
+       solver->addConstraint(b);
 
-       if (startEncoding(solver) == 1)
-               printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+       if (solver->startEncoding() == 1)
+               printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }
index 24b652f..c9094cf 100644 (file)
  * Result: e1=6, e2=4, e7=2
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {6};
        uint64_t set2[] = {4, 2};
        uint64_t set3[] = {3, 1};
        uint64_t set4[] = {2, 3, 1};
        uint64_t set5[] = {2, 1, 0};
-       Set *s1 = createSet(solver, 0, set1, 1);
-       Set *s2 = createSet(solver, 0, set2, 2);
-       Set *s3 = createSet(solver, 0, set3, 2);
-       Set *s4 = createSet(solver, 0, set4, 3);
-       Set *s5 = createSet(solver, 0, set5, 3);
-       Element *e1 = getElementVar(solver, s1);
-       Element *e2 = getElementVar(solver, s2);
-       Element *e7 = getElementVar(solver, s5);
-       Boolean *overflow = getBooleanVar(solver, 2);
+       Set *s1 = solver->createSet(0, set1, 1);
+       Set *s2 = solver->createSet(0, set2, 2);
+       Set *s3 = solver->createSet(0, set3, 2);
+       Set *s4 = solver->createSet(0, set4, 3);
+       Set *s5 = solver->createSet(0, set5, 3);
+       Element *e1 = solver->getElementVar(s1);
+       Element *e2 = solver->getElementVar(s2);
+       Element *e7 = solver->getElementVar(s5);
+       Boolean *overflow = solver->getBooleanVar(2);
        Set *d1[] = {s1, s2};
        //change the overflow flag
-       Function *f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE);
+       Function *f1 = solver->createFunctionOperator(SUB, d1, 2, s2, IGNORE);
        Element *in1[] = {e1, e2};
-       Element *e3 = applyFunction(solver, f1, in1, 2, overflow);
-       Table *t1 = createTable(solver, d1, 2, s3);
+       Element *e3 = solver->applyFunction(f1, in1, 2, overflow);
+       Table *t1 = solver->createTable(d1, 2, s3);
        uint64_t row1[] = {6, 2};
        uint64_t row2[] = {6, 4};
-       addTableEntry(solver, t1, row1, 2, 3);
-       addTableEntry(solver, t1, row2, 2, 1);
-       Function *f2 = completeTable(solver, t1, IGNOREBEHAVIOR);
-       Element *e4 = applyFunction(solver, f2, in1, 2, overflow);
+       solver->addTableEntry(t1, row1, 2, 3);
+       solver->addTableEntry(t1, row2, 2, 1);
+       Function *f2 = solver->completeTable(t1, IGNOREBEHAVIOR);
+       Element *e4 = solver->applyFunction(f2, in1, 2, overflow);
 
        Set *d2[] = {s1};
        Element *in2[] = {e1};
-       Table *t2 = createTable(solver, d2, 1, s1);
+       Table *t2 = solver->createTable(d2, 1, s1);
        uint64_t row3[] = {6};
-       addTableEntry(solver, t2, row3, 1, 6);
-       Function *f3 = completeTable(solver, t2, IGNOREBEHAVIOR);
-       Element *e5 = applyFunction(solver, f3, in2, 1, overflow);
+       solver->addTableEntry(t2, row3, 1, 6);
+       Function *f3 = solver->completeTable(t2, IGNOREBEHAVIOR);
+       Element *e5 = solver->applyFunction(f3, in2, 1, overflow);
 
        Set *d3[] = {s2, s3, s1};
        Element *in3[] = {e3, e4, e5};
-       Table *t3 = createTable(solver, d3, 3, s4);
+       Table *t3 = solver->createTable(d3, 3, s4);
        uint64_t row4[] = {4, 3, 6};
        uint64_t row5[] = {2, 1, 6};
        uint64_t row6[] = {2, 3, 6};
        uint64_t row7[] = {4, 1, 6};
-       addTableEntry(solver, t3, row4, 3, 3);
-       addTableEntry(solver, t3, row5, 3, 1);
-       addTableEntry(solver, t3, row6, 3, 2);
-       addTableEntry(solver, t3, row7, 3, 1);
-       Function *f4 = completeTable(solver, t3, IGNOREBEHAVIOR);
-       Element *e6 = applyFunction(solver, f4, in3, 3, overflow);
+       solver->addTableEntry(t3, row4, 3, 3);
+       solver->addTableEntry(t3, row5, 3, 1);
+       solver->addTableEntry(t3, row6, 3, 2);
+       solver->addTableEntry(t3, row7, 3, 1);
+       Function *f4 = solver->completeTable(t3, IGNOREBEHAVIOR);
+       Element *e6 = solver->applyFunction(f4, in3, 3, overflow);
 
        Set *deq[] = {s5,s4};
-       Predicate *gt = createPredicateOperator(solver, GT, deq, 2);
+       Predicate *gt = solver->createPredicateOperator(GT, deq, 2);
        Element *inputs2 [] = {e7, e6};
-       Boolean *pred = applyPredicate(solver, gt, inputs2, 2);
-       addConstraint(solver, pred);
+       Boolean *pred = solver->applyPredicate(gt, inputs2, 2);
+       solver->addConstraint(pred);
 
-       if (startEncoding(solver) == 1)
+       if (solver->startEncoding() == 1)
                printf("e1=%llu e2=%llu e7=%llu\n",
-                                        getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));
+                                        solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e7));
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }
index eef8c36..e2d974b 100644 (file)
@@ -7,17 +7,17 @@
  * Result: O(5,1)=0 O(1,4)=0 O(5,4)=0 O(1,5)=1 O(1111,5)=2
  */
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {5, 1, 4};
-       Set *s = createSet(solver, 0, set1, 3);
-       Order *order = createOrder(solver, TOTAL, s);
-       Boolean *b1 =  orderConstraint(solver, order, 5, 1);
-       Boolean *b2 =  orderConstraint(solver, order, 1, 4);
-       addConstraint(solver, b1);
-       addConstraint(solver, b2);
-       if (startEncoding(solver) == 1)
+       Set *s = solver->createSet(0, set1, 3);
+       Order *order = solver->createOrder(TOTAL, s);
+       Boolean *b1 =  solver->orderConstraint(order, 5, 1);
+       Boolean *b2 =  solver->orderConstraint(order, 1, 4);
+       solver->addConstraint(b1);
+       solver->addConstraint(b2);
+       if (solver->startEncoding() == 1)
                printf("SAT\n");
        else
                printf("UNSAT\n");
-       deleteSolver(solver);
+       delete solver;
 }
index 5d748a6..cd0cc82 100644 (file)
@@ -16,8 +16,7 @@
 #define true 1
 #define false 0
 
-struct CSolver;
-typedef struct CSolver CSolver;
+class CSolver;
 struct SATEncoder;
 typedef struct SATEncoder SATEncoder;
 
index 918d484..b6adc3f 100644 (file)
 #include "orderencoder.h"
 #include "polarityassignment.h"
 
-CSolver *allocCSolver() {
-       CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
-       This->unsat = false;
-       This->constraints = allocDefHashSetBoolean();
-       This->allBooleans = allocDefVectorBoolean();
-       This->allSets = allocDefVectorSet();
-       This->allElements = allocDefVectorElement();
-       This->allPredicates = allocDefVectorPredicate();
-       This->allTables = allocDefVectorTable();
-       This->allOrders = allocDefVectorOrder();
-       This->allFunctions = allocDefVectorFunction();
-       This->tuner = allocTuner();
-       This->satEncoder = allocSATEncoder(This);
-       return This;
+CSolver::CSolver() : unsat(false) {
+       constraints = allocDefHashSetBoolean();
+       allBooleans = allocDefVectorBoolean();
+       allSets = allocDefVectorSet();
+       allElements = allocDefVectorElement();
+       allPredicates = allocDefVectorPredicate();
+       allTables = allocDefVectorTable();
+       allOrders = allocDefVectorOrder();
+       allFunctions = allocDefVectorFunction();
+       tuner = allocTuner();
+       satEncoder = allocSATEncoder(this);
 }
 
 /** This function tears down the solver and the entire AST */
 
-void deleteSolver(CSolver *This) {
-       deleteHashSetBoolean(This->constraints);
+CSolver::~CSolver() {
+       deleteHashSetBoolean(constraints);
 
-       uint size = getSizeVectorBoolean(This->allBooleans);
+       uint size = getSizeVectorBoolean(allBooleans);
        for (uint i = 0; i < size; i++) {
-               delete getVectorBoolean(This->allBooleans, i);
+               delete getVectorBoolean(allBooleans, i);
        }
-       deleteVectorBoolean(This->allBooleans);
+       deleteVectorBoolean(allBooleans);
 
-       size = getSizeVectorSet(This->allSets);
+       size = getSizeVectorSet(allSets);
        for (uint i = 0; i < size; i++) {
-               delete getVectorSet(This->allSets, i);
+               delete getVectorSet(allSets, i);
        }
-       deleteVectorSet(This->allSets);
+       deleteVectorSet(allSets);
 
-       size = getSizeVectorElement(This->allElements);
+       size = getSizeVectorElement(allElements);
        for (uint i = 0; i < size; i++) {
-               delete getVectorElement(This->allElements, i);
+               delete getVectorElement(allElements, i);
        }
-       deleteVectorElement(This->allElements);
+       deleteVectorElement(allElements);
 
-       size = getSizeVectorTable(This->allTables);
+       size = getSizeVectorTable(allTables);
        for (uint i = 0; i < size; i++) {
-               delete getVectorTable(This->allTables, i);
+               delete getVectorTable(allTables, i);
        }
-       deleteVectorTable(This->allTables);
+       deleteVectorTable(allTables);
 
-       size = getSizeVectorPredicate(This->allPredicates);
+       size = getSizeVectorPredicate(allPredicates);
        for (uint i = 0; i < size; i++) {
-               delete getVectorPredicate(This->allPredicates, i);
+               delete getVectorPredicate(allPredicates, i);
        }
-       deleteVectorPredicate(This->allPredicates);
+       deleteVectorPredicate(allPredicates);
 
-       size = getSizeVectorOrder(This->allOrders);
+       size = getSizeVectorOrder(allOrders);
        for (uint i = 0; i < size; i++) {
-               delete getVectorOrder(This->allOrders, i);
+               delete getVectorOrder(allOrders, i);
        }
-       deleteVectorOrder(This->allOrders);
+       deleteVectorOrder(allOrders);
 
-       size = getSizeVectorFunction(This->allFunctions);
+       size = getSizeVectorFunction(allFunctions);
        for (uint i = 0; i < size; i++) {
-               delete getVectorFunction(This->allFunctions, i);
+               delete getVectorFunction(allFunctions, i);
        }
-       deleteVectorFunction(This->allFunctions);
-       deleteSATEncoder(This->satEncoder);
-       deleteTuner(This->tuner);
-       ourfree(This);
+       deleteVectorFunction(allFunctions);
+       deleteSATEncoder(satEncoder);
+       deleteTuner(tuner);
 }
 
-Set *createSet(CSolver *This, VarType type, uint64_t *elements, uint numelements) {
+Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
        Set *set = new Set(type, elements, numelements);
-       pushVectorSet(This->allSets, set);
+       pushVectorSet(allSets, set);
        return set;
 }
 
-Set *createRangeSet(CSolver *This, VarType type, uint64_t lowrange, uint64_t highrange) {
+Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
        Set *set = new Set(type, lowrange, highrange);
-       pushVectorSet(This->allSets, set);
+       pushVectorSet(allSets, set);
        return set;
 }
 
-MutableSet *createMutableSet(CSolver *This, VarType type) {
+MutableSet *CSolver::createMutableSet(VarType type) {
        MutableSet *set = allocMutableSet(type);
-       pushVectorSet(This->allSets, set);
+       pushVectorSet(allSets, set);
        return set;
 }
 
-void addItem(CSolver *This, MutableSet *set, uint64_t element) {
+void CSolver::addItem(MutableSet *set, uint64_t element) {
        addElementMSet(set, element);
 }
 
-uint64_t createUniqueItem(CSolver *This, MutableSet *set) {
+uint64_t CSolver::createUniqueItem(MutableSet *set) {
        uint64_t element = set->low++;
        addElementMSet(set, element);
        return element;
 }
 
-Element *getElementVar(CSolver *This, Set *set) {
+Element *CSolver::getElementVar(Set *set) {
        Element *element = new ElementSet(set);
-       pushVectorElement(This->allElements, element);
+       pushVectorElement(allElements, element);
        return element;
 }
 
-Element *getElementConst(CSolver *This, VarType type, uint64_t value) {
+Element *CSolver::getElementConst(VarType type, uint64_t value) {
        Element *element = new ElementConst(value, type);
-       pushVectorElement(This->allElements, element);
+       pushVectorElement(allElements, element);
        return element;
 }
 
-Boolean *getBooleanVar(CSolver *This, VarType type) {
+Boolean *CSolver::getBooleanVar(VarType type) {
        Boolean *boolean = new BooleanVar(type);
-       pushVectorBoolean(This->allBooleans, boolean);
+       pushVectorBoolean(allBooleans, boolean);
        return boolean;
 }
 
-Function *createFunctionOperator(CSolver *This, ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
+Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
        Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
-       pushVectorFunction(This->allFunctions, function);
+       pushVectorFunction(allFunctions, function);
        return function;
 }
 
-Predicate *createPredicateOperator(CSolver *This, CompOp op, Set **domain, uint numDomain) {
+Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
        Predicate *predicate = new PredicateOperator(op, domain,numDomain);
-       pushVectorPredicate(This->allPredicates, predicate);
+       pushVectorPredicate(allPredicates, predicate);
        return predicate;
 }
 
-Predicate *createPredicateTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
+Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
        Predicate *predicate = new PredicateTable(table, behavior);
-       pushVectorPredicate(This->allPredicates, predicate);
+       pushVectorPredicate(allPredicates, predicate);
        return predicate;
 }
 
-Table *createTable(CSolver *This, Set **domains, uint numDomain, Set *range) {
+Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
        Table *table = new Table(domains,numDomain,range);
-       pushVectorTable(This->allTables, table);
+       pushVectorTable(allTables, table);
        return table;
 }
 
-Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain) {
-       return createTable(solver, domains, numDomain, NULL);
+Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
+       return createTable(domains, numDomain, NULL);
 }
 
-void addTableEntry(CSolver *This, Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
-       table->addNewTableEntry(inputs, inputSize,result);
+void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
+       table->addNewTableEntry(inputs, inputSize, result);
 }
 
-Function *completeTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
+Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
        Function *function = new FunctionTable(table, behavior);
-       pushVectorFunction(This->allFunctions,function);
+       pushVectorFunction(allFunctions,function);
        return function;
 }
 
-Element *applyFunction(CSolver *This, Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
+Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
        Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
-       pushVectorElement(This->allElements, element);
+       pushVectorElement(allElements, element);
        return element;
 }
 
-Boolean *applyPredicate(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs) {
-       return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
+Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
+       return applyPredicateTable(predicate, inputs, numInputs, NULL);
 }
-Boolean *applyPredicateTable(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
+
+Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
        Boolean *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
-       pushVectorBoolean(This->allBooleans, boolean);
+       pushVectorBoolean(allBooleans, boolean);
        return boolean;
 }
 
-Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint asize) {
-       return new BooleanLogic(This, op, array, asize);
+Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
+       return new BooleanLogic(this, op, array, asize);
 }
 
-void addConstraint(CSolver *This, Boolean *constraint) {
-       addHashSetBoolean(This->constraints, constraint);
+void CSolver::addConstraint(Boolean *constraint) {
+       addHashSetBoolean(constraints, constraint);
 }
 
-Order *createOrder(CSolver *This, OrderType type, Set *set) {
+Order *CSolver::createOrder(OrderType type, Set *set) {
        Order *order = new Order(type, set);
-       pushVectorOrder(This->allOrders, order);
+       pushVectorOrder(allOrders, order);
        return order;
 }
 
-Boolean *orderConstraint(CSolver *This, Order *order, uint64_t first, uint64_t second) {
+Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
        Boolean *constraint = new BooleanOrder(order, first, second);
-       pushVectorBoolean(This->allBooleans,constraint);
+       pushVectorBoolean(allBooleans,constraint);
        return constraint;
 }
 
-int startEncoding(CSolver *This) {
-       naiveEncodingDecision(This);
-       SATEncoder *satEncoder = This->satEncoder;
-       computePolarities(This);
-       orderAnalysis(This);
-       encodeAllSATEncoder(This, satEncoder);
+int CSolver::startEncoding() {
+       naiveEncodingDecision(this);
+       computePolarities(this);
+       orderAnalysis(this);
+       encodeAllSATEncoder(this, satEncoder);
        int result = solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
        for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {
@@ -214,29 +210,29 @@ int startEncoding(CSolver *This) {
        return result;
 }
 
-uint64_t getElementValue(CSolver *This, Element *element) {
+uint64_t CSolver::getElementValue(Element *element) {
        switch (GETELEMENTTYPE(element)) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return getElementValueSATTranslator(This, element);
+               return getElementValueSATTranslator(this, element);
        default:
                ASSERT(0);
        }
        exit(-1);
 }
 
-bool getBooleanValue( CSolver *This, Boolean *boolean) {
+bool CSolver::getBooleanValue(Boolean *boolean) {
        switch (GETBOOLEANTYPE(boolean)) {
        case BOOLEANVAR:
-               return getBooleanVariableValueSATTranslator(This, boolean);
+               return getBooleanVariableValueSATTranslator(this, boolean);
        default:
                ASSERT(0);
        }
        exit(-1);
 }
 
-HappenedBefore getOrderConstraintValue(CSolver *This, Order *order, uint64_t first, uint64_t second) {
-       return getOrderConstraintValueSATTranslator(This, order, first, second);
+HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
+       return getOrderConstraintValueSATTranslator(this, order, first, second);
 }
 
index fbf22da..e8527f0 100644 (file)
@@ -4,7 +4,11 @@
 #include "ops.h"
 #include "structs.h"
 
-struct CSolver {
+class CSolver {
+ public:
+       CSolver();
+       ~CSolver();
+       
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;
@@ -32,107 +36,101 @@ struct CSolver {
 
        /** This is a vector of all function structs that we have allocated. */
        VectorFunction *allFunctions;
-};
-
-/** Create a new solver instance. */
-
-CSolver *allocCSolver();
-
-/** Delete solver instance. */
-
-void deleteSolver(CSolver *This);
 
-/** This function creates a set containing the elements passed in the array. */
+       /** This function creates a set containing the elements passed in the array. */
 
-Set *createSet(CSolver *, VarType type, uint64_t *elements, uint num);
+       Set *createSet(VarType type, uint64_t *elements, uint num);
 
-/** This function creates a set from lowrange to highrange (inclusive). */
+       /** This function creates a set from lowrange to highrange (inclusive). */
 
-Set *createRangeSet(CSolver *, VarType type, uint64_t lowrange, uint64_t highrange);
-
-/** This function creates a mutable set. */
-
-MutableSet *createMutableSet(CSolver *, VarType type);
+       Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
+       
+       /** This function creates a mutable set. */
+       
+       MutableSet *createMutableSet(VarType type);
 
-/** This function adds a new item to a set. */
+       /** This function adds a new item to a set. */
 
-void addItem(CSolver *, MutableSet *set, uint64_t element);
+       void addItem(MutableSet *set, uint64_t element);
 
-/** This function adds a new unique item to the set and returns it.
-    This function cannot be used in conjunction with manually adding
-    items to the set. */
+       /** This function adds a new unique item to the set and returns it.
+                       This function cannot be used in conjunction with manually adding
+                       items to the set. */
+       
+       uint64_t createUniqueItem(MutableSet *set);
 
-uint64_t createUniqueItem(CSolver *, MutableSet *set);
+       /** This function creates an element variable over a set. */
 
-/** This function creates an element variable over a set. */
+       Element *getElementVar(Set *set);
 
-Element *getElementVar(CSolver *, Set *set);
+       /** This function creates an element constrant. */
+       Element *getElementConst(VarType type, uint64_t value);
 
-/** This function creates an element constrant. */
-Element *getElementConst(CSolver *, VarType type, uint64_t value);
+       /** This function creates a boolean variable. */
 
-/** This function creates a boolean variable. */
+       Boolean *getBooleanVar(VarType type);
 
-Boolean *getBooleanVar(CSolver *, VarType type);
+       /** This function creates a function operator. */
 
-/** This function creates a function operator. */
+       Function *createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,
+                                                                                                                                        OverFlowBehavior overflowbehavior);
 
-Function *createFunctionOperator(CSolver *solver, ArithOp op, Set **domain, uint numDomain, Set *range,
-                                                                                                                                OverFlowBehavior overflowbehavior);
+       /** This function creates a predicate operator. */
 
-/** This function creates a predicate operator. */
+       Predicate *createPredicateOperator(CompOp op, Set **domain, uint numDomain);
 
-Predicate *createPredicateOperator(CSolver *solver, CompOp op, Set **domain, uint numDomain);
+       Predicate *createPredicateTable(Table *table, UndefinedBehavior behavior);
 
-Predicate *createPredicateTable(CSolver *solver, Table *table, UndefinedBehavior behavior);
+       /** This function creates an empty instance table.*/
 
-/** This function creates an empty instance table.*/
+       Table *createTable(Set **domains, uint numDomain, Set *range);
 
-Table *createTable(CSolver *solver, Set **domains, uint numDomain, Set *range);
+       Table *createTableForPredicate(Set **domains, uint numDomain);
+       /** This function adds an input output relation to a table. */
 
-Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain);
-/** This function adds an input output relation to a table. */
+       void addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result);
 
-void addTableEntry(CSolver *solver, Table *table, uint64_t *inputs, uint inputSize, uint64_t result);
+       /** This function converts a completed table into a function. */
 
-/** This function converts a completed table into a function. */
+       Function *completeTable(Table *, UndefinedBehavior behavior);
 
-Function *completeTable(CSolver *, Table *, UndefinedBehavior behavior);
+       /** This function applies a function to the Elements in its input. */
 
-/** This function applies a function to the Elements in its input. */
+       Element *applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
 
-Element *applyFunction(CSolver *, Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
+       /** This function applies a predicate to the Elements in its input. */
 
-/** This function applies a predicate to the Elements in its input. */
+       Boolean *applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus);
 
-Boolean *applyPredicateTable(CSolver *, Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus);
+       Boolean *applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
 
-Boolean *applyPredicate(CSolver *, Predicate *predicate, Element **inputs, uint numInputs);
+       /** This function applies a logical operation to the Booleans in its input. */
 
-/** This function applies a logical operation to the Booleans in its input. */
+       Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
 
-Boolean *applyLogicalOperation(CSolver *, LogicOp op, Boolean **array, uint asize);
+       /** This function adds a boolean constraint to the set of constraints
+                       to be satisfied */
 
-/** This function adds a boolean constraint to the set of constraints
-    to be satisfied */
+       void addConstraint(Boolean *constraint);
 
-void addConstraint(CSolver *, Boolean *constraint);
+       /** This function instantiates an order of type type over the set set. */
+       Order *createOrder(OrderType type, Set *set);
 
-/** This function instantiates an order of type type over the set set. */
-Order *createOrder(CSolver *, OrderType type, Set *set);
+       /** This function instantiates a boolean on two items in an order. */
+       Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
 
-/** This function instantiates a boolean on two items in an order. */
-Boolean *orderConstraint(CSolver *, Order *order, uint64_t first, uint64_t second);
+       /** When everything is done, the client calls this function and then csolver starts to encode*/
+       int startEncoding();
 
-/** When everything is done, the client calls this function and then csolver starts to encode*/
-int startEncoding(CSolver *);
+       /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
+       uint64_t getElementValue(Element *element);
 
-/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
-uint64_t getElementValue(CSolver *, Element *element);
+       /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
+       bool getBooleanValue(Boolean *boolean);
 
-/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
-bool getBooleanValue( CSolver *, Boolean *boolean);
+       HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
-HappenedBefore getOrderConstraintValue(CSolver *, Order *order, uint64_t first, uint64_t second);
+       MEMALLOC;
+};
 
 #endif