From d98defe8f9c222258e0286adf9d2f627f7d197ed Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 24 Aug 2017 19:11:49 -0700 Subject: [PATCH] edits --- src/Test/Makefile | 2 +- src/Test/buildconstraintstest.cc | 50 ++++----- src/Test/elemequalunsattest.cc | 22 ++-- src/Test/funcencodingtest.cc | 68 ++++++------ src/Test/ordertest.cc | 18 +-- src/classlist.h | 3 +- src/csolver.cc | 184 +++++++++++++++---------------- src/csolver.h | 126 +++++++++++---------- 8 files changed, 233 insertions(+), 240 deletions(-) diff --git a/src/Test/Makefile b/src/Test/Makefile index 2c24d58..0f1bc39 100644 --- a/src/Test/Makefile +++ b/src/Test/Makefile @@ -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 diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc index 71dbafd..af28c49 100644 --- a/src/Test/buildconstraintstest.cc +++ b/src/Test/buildconstraintstest.cc @@ -14,46 +14,46 @@ * 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; } diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc index 5cbdd04..c470485 100644 --- a/src/Test/elemequalunsattest.cc +++ b/src/Test/elemequalunsattest.cc @@ -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; } diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc index 24b652f..c9094cf 100644 --- a/src/Test/funcencodingtest.cc +++ b/src/Test/funcencodingtest.cc @@ -17,66 +17,66 @@ * 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; } diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc index eef8c36..e2d974b 100644 --- a/src/Test/ordertest.cc +++ b/src/Test/ordertest.cc @@ -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; } diff --git a/src/classlist.h b/src/classlist.h index 5d748a6..cd0cc82 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -16,8 +16,7 @@ #define true 1 #define false 0 -struct CSolver; -typedef struct CSolver CSolver; +class CSolver; struct SATEncoder; typedef struct SATEncoder SATEncoder; diff --git a/src/csolver.cc b/src/csolver.cc index 918d484..b6adc3f 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -13,198 +13,194 @@ #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); } diff --git a/src/csolver.h b/src/csolver.h index fbf22da..e8527f0 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -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 -- 2.34.1