From: Hamed Gorjiara Date: Tue, 10 Apr 2018 22:28:03 +0000 (-0700) Subject: Adding the c wrapper for CSolver X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=806a79424211fba5d68b6b802a6ceea2db47196f Adding the c wrapper for CSolver --- diff --git a/src/Test/Makefile b/src/Test/Makefile index 5ec7989..f7c2929 100644 --- a/src/Test/Makefile +++ b/src/Test/Makefile @@ -1,6 +1,7 @@ BASE := .. OBJECTS := $(patsubst %.cc, ../bin/%, $(wildcard *.cc)) +COBJECTS := $(patsubst %.c, ../bin/%, $(wildcard *.c)) include $(BASE)/common.mk @@ -8,15 +9,18 @@ DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJ CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend -I$(BASE)/Tuner -all: $(OBJECTS) ../bin/run.sh +all: $(OBJECTS) $(COBJECTS) ../bin/run.sh -include $(DEPS) ../bin/%: %.cc $(CXX) -MMD -MF $(@D)/.$(@F).d -o ../bin/$@ $< $(CPPFLAGS) -L$(BASE)/bin/ -l_cons_comp +../bin/%: %.c + $(CC) -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 clean:: - rm -f $(OBJECTS) $(DEPS) ../bin/run.sh + rm -f $(OBJECTS) $(COBJECTS) $(DEPS) ../bin/run.sh diff --git a/src/Test/ccsolvertest.c b/src/Test/ccsolvertest.c new file mode 100644 index 0000000..3bcb3c6 --- /dev/null +++ b/src/Test/ccsolvertest.c @@ -0,0 +1,25 @@ +#include "ccsolver.h" +#include + +#define SATC_EQUALS 0 + +int main (int num, char** args){ + void* solver = CreateCCSolver(); + long set1[] = {0, 1, 2}; + long set2[] = {3, 1, 7}; + void *s1 = createSet(solver,0, set1, 3); + void *s2 = createSet(solver,0, set2, 3); + void *e1 = getElementVar(solver,s1); + void *e2 = getElementVar(solver,s2); + void *domain[] = {s1, s2}; + void *equals = createPredicateOperator(solver,SATC_EQUALS, domain, 2); + void *inputs[] = {e1, e2}; + void* b = applyPredicate(solver,equals, inputs, 2); + addConstraint(solver,b); + if (solve(solver) == 1) + printf("e1=%ld \t e2=%ld\n", getElementValue(solver, e1), getElementValue(solver, e2)); + else + printf("UNSAT\n"); + deleteCCSolver(solver); +} + diff --git a/src/ccsolver.cc b/src/ccsolver.cc new file mode 100644 index 0000000..c58f380 --- /dev/null +++ b/src/ccsolver.cc @@ -0,0 +1,139 @@ +#include "csolver.h" +#include "ccsolver.h" + +#define CCSOLVER(solver) ((CSolver*)solver) + +void* CreateCCSolver(){ + return (void*) new CSolver(); +} +void deleteCCSolver(void* solver){ + delete CCSOLVER(solver); +} + +void *createSet(void* solver,unsigned int type, void *elements, unsigned int num){ + return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num); +} + +void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange){ + return CCSOLVER(solver)->createRangeSet((VarType) type, (uint64_t) lowrange, (uint64_t) highrange); +} + +void *createRangeVar(void* solver,unsigned type, long lowrange, long highrange){ + return CCSOLVER(solver)->createRangeVar((VarType) type, (uint64_t) lowrange, (uint64_t) highrange); +} + +void *createMutableSet(void* solver,unsigned type){ + return CCSOLVER(solver)->createMutableSet((VarType) type); +} + +void addItem(void* solver,void *set, long element){ + CCSOLVER(solver)->addItem((MutableSet*) set, (uint64_t) element); +} + +void finalizeMutableSet(void* solver,void *set){ + CCSOLVER(solver)->finalizeMutableSet((MutableSet*) set); +} + +void *getElementVar(void* solver,void *set){ + return CCSOLVER(solver)->getElementVar((Set*) set); +} + +void *getElementConst(void* solver,unsigned type, long value){ + return CCSOLVER(solver)->getElementConst((VarType) type, (uint64_t) value); +} + +void *getElementRange (void* solver,void *element){ + return CCSOLVER(solver)->getElementRange ((Element*) element); +} + +void* getBooleanVar(void* solver,unsigned int type){ + return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw(); +} + +void *createFunctionOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain, void *range,unsigned int overflowbehavior){ + return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set **)domain, (uint) numDomain, (Set *)range, (OverFlowBehavior) overflowbehavior); +} + +void *createPredicateOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain){ + return CCSOLVER(solver)->createPredicateOperator((CompOp) op, (Set **)domain, (uint) numDomain); +} + +void *createPredicateTable(void* solver,void *table, unsigned int behavior){ + return CCSOLVER(solver)->createPredicateTable((Table *)table, (UndefinedBehavior) behavior); +} + +void *createTable(void* solver,void*domains, unsigned int numDomain, void *range){ + return CCSOLVER(solver)->createTable((Set **)domains, (uint) numDomain, (Set *)range); +} + +void *createTableForPredicate(void* solver,void*domains, unsigned int numDomain){ + return CCSOLVER(solver)->createTableForPredicate((Set **)domains, (uint) numDomain); +} + +void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result){ + CCSOLVER(solver)->addTableEntry((Table *)table, (uint64_t *)inputs, (uint) inputSize, (uint64_t) result); +} + +void *completeTable(void* solver,void *table, unsigned int behavior){ + return CCSOLVER(solver)->completeTable((Table *) table, (UndefinedBehavior) behavior); +} + +void *applyFunction(void* solver,void *function, void*array, unsigned int numArrays, void* overflowstatus){ + return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean*)overflowstatus)); +} + +void* applyPredicateTable(void* solver,void *predicate, void *inputs, unsigned int numInputs, void* undefinedStatus){ + return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean*) undefinedStatus)).getRaw(); +} + +void* applyPredicate(void* solver,void *predicate, void *inputs, unsigned int numInputs){ + return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw(); +} + +void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize){ + return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw(); +} + +void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2){ + return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg1), BooleanEdge((Boolean*) arg2)).getRaw(); +} + +void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg){ + return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg)).getRaw(); +} + +void addConstraint(void* solver,void* constraint){ + CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean*) constraint)); +} + +void *createOrder(void* solver,unsigned int type, void *set){ + return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set); +} + +void* orderConstraint(void* solver,void *order, long first, long second){ + return CCSOLVER(solver)->orderConstraint((Order *)order, (uint64_t) first, (uint64_t) second).getRaw(); +} + +int solve(void* solver){ + return CCSOLVER(solver)->solve(); +} + +long getElementValue(void* solver,void *element){ + return (long) CCSOLVER(solver)->getElementValue((Element *)element); +} + +int getBooleanValue(void* solver, void* boolean){ + return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean*) boolean)); +} + +int getOrderConstraintValue(void* solver,void *order, long first, long second){ + return CCSOLVER(solver)->getOrderConstraintValue((Order *)order, (uint64_t) first, (uint64_t) second); +} + +void printConstraints(void* solver){ + CCSOLVER(solver)->printConstraints(); +} + + + + diff --git a/src/ccsolver.h b/src/ccsolver.h new file mode 100644 index 0000000..c14a3e0 --- /dev/null +++ b/src/ccsolver.h @@ -0,0 +1,46 @@ +#ifndef __CCSOLVER_H +#define __CCSOLVER_H + + +typedef void* CCSolver; +#ifdef __cplusplus +extern "C" { +#endif +void* CreateCCSolver(); +void deleteCCSolver(void* solver); +void *createSet(void* solver,unsigned int type, void *elements, unsigned int num); +void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange); +void *createRangeVar(void* solver,unsigned type, long lowrange, long highrange); +void *createMutableSet(void* solver,unsigned type); +void addItem(void* solver,void *set, long element); +void finalizeMutableSet(void* solver,void *set); +void *getElementVar(void* solver,void *set); +void *getElementConst(void* solver,unsigned type, long value); +void *getElementRange (void* solver,void *element); +void* getBooleanVar(void* solver,unsigned int type); +void *createFunctionOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain, void *range,unsigned int overflowbehavior); +void *createPredicateOperator(void* solver,unsigned int op, void *domain, unsigned int numDomain); +void *createPredicateTable(void* solver,void *table, unsigned int behavior); +void *createTable(void* solver,void*domains, unsigned int numDomain, void *range); +void *createTableForPredicate(void* solver,void*domains, unsigned int numDomain); +void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result); +void *completeTable(void* solver,void *table, unsigned int behavior); +void *applyFunction(void* solver,void *function, void*array, unsigned int numArrays, long overflowstatus); +void* applyPredicateTable(void* solver,void *predicate, void *inputs, unsigned int numInputs, long undefinedStatus); +void* applyPredicate(void* solver,void *predicate, void *inputs, unsigned int numInputs); +void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize); +void* applyLogicalOperationTwo(void* solver,unsigned int op, long arg1, long arg2); +void* applyLogicalOperationOne(void* solver,unsigned int op, long arg); +void addConstraint(void* solver,void* constraint); +void *createOrder(void* solver,unsigned int type, void *set); +void* orderConstraint(void* solver,void *order, long first, long second); +int solve(void* solver); +long getElementValue(void* solver,void *element); +int getBooleanValue(void* solver,long boolean); +int getOrderConstraintValue(void* solver,void *order, long first, long second); +void printConstraints(void* solver); +#ifdef __cplusplus +} +#endif + +#endif diff --git a/src/common.h b/src/common.h index 256aaf3..3a0eeaa 100644 --- a/src/common.h +++ b/src/common.h @@ -19,7 +19,7 @@ #include "time.h" -#if 1 +#if 0 extern int model_out; extern int model_err; extern int switch_alloc; diff --git a/src/csolver.cc b/src/csolver.cc index be65781..9007467 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -583,15 +583,13 @@ int CSolver::solve() { } delete orderit; } - model_print("*****************Before any modifications:************\n"); - printConstraints(); computePolarities(this); long long time2 = getTimeNano(); model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC); -// Preprocess pp(this); -// pp.doTransform(); + Preprocess pp(this); + pp.doTransform(); long long time3 = getTimeNano(); -// model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC); + model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC); DecomposeOrderTransform dot(this); dot.doTransform(); @@ -617,8 +615,6 @@ int CSolver::solve() { model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC); model_print("Is problem UNSAT after encoding: %d\n", unsat); - model_print("########## After all modifications: #############\n"); - printConstraints(); int result = unsat ? IS_UNSAT : satEncoder->solve(); model_print("Result Computed in CSolver: %d\n", result); diff --git a/src/mymemory.h b/src/mymemory.h index b87e2c8..b78eb54 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -26,7 +26,7 @@ void * ourrealloc(void *ptr, size_t size); */ -#if 1 +#if 0 void *model_malloc(size_t size); void model_free(void *ptr); void *model_calloc(size_t count, size_t size);