-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
* 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;
}
* 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;
}
* 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;
}
* 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;
}
#define true 1
#define false 0
-struct CSolver;
-typedef struct CSolver CSolver;
+class CSolver;
struct SATEncoder;
typedef struct SATEncoder SATEncoder;
#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++) {
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);
}
#include "ops.h"
#include "structs.h"
-struct CSolver {
+class CSolver {
+ public:
+ CSolver();
+ ~CSolver();
+
SATEncoder *satEncoder;
bool unsat;
Tuner *tuner;
/** 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
projects / satune.git / commitdiff