From 6e30239f4df65eb00da5e4e61785ea4453370026 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 11 Apr 2018 12:00:34 -0700 Subject: [PATCH] Adding the python wrapper for the constraint solver --- src/Test/Makefile | 6 ++++-- src/Test/ccsolvertest.c | 2 +- src/Test/pycsolvertest.py | 35 +++++++++++++++++++++++++++++++++++ src/ccsolver.cc | 6 +++--- src/ccsolver.h | 6 +++--- src/pycsolver.py | 23 +++++++++++++++++++++++ 6 files changed, 69 insertions(+), 9 deletions(-) create mode 100644 src/Test/pycsolvertest.py create mode 100644 src/pycsolver.py diff --git a/src/Test/Makefile b/src/Test/Makefile index f7c2929..50399a0 100644 --- a/src/Test/Makefile +++ b/src/Test/Makefile @@ -2,14 +2,14 @@ BASE := .. OBJECTS := $(patsubst %.cc, ../bin/%, $(wildcard *.cc)) COBJECTS := $(patsubst %.c, ../bin/%, $(wildcard *.c)) - +PYOBJECT := $(patsubst %.py, ../bin/%, $(wildcard *.py)) include $(BASE)/common.mk DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS)))) CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend -I$(BASE)/Tuner -all: $(OBJECTS) $(COBJECTS) ../bin/run.sh +all: $(OBJECTS) $(COBJECTS) ../bin/run.sh $(PYOBJECT) -include $(DEPS) @@ -21,6 +21,8 @@ all: $(OBJECTS) $(COBJECTS) ../bin/run.sh ../bin/run.sh: run.sh cp run.sh ../bin/run.sh +../bin/%: %.py + cp $< ../bin/$< clean:: rm -f $(OBJECTS) $(COBJECTS) $(DEPS) ../bin/run.sh diff --git a/src/Test/ccsolvertest.c b/src/Test/ccsolvertest.c index 3bcb3c6..bdb8898 100644 --- a/src/Test/ccsolvertest.c +++ b/src/Test/ccsolvertest.c @@ -4,7 +4,7 @@ #define SATC_EQUALS 0 int main (int num, char** args){ - void* solver = CreateCCSolver(); + void* solver = createCCSolver(); long set1[] = {0, 1, 2}; long set2[] = {3, 1, 7}; void *s1 = createSet(solver,0, set1, 3); diff --git a/src/Test/pycsolvertest.py b/src/Test/pycsolvertest.py new file mode 100644 index 0000000..ca269ed --- /dev/null +++ b/src/Test/pycsolvertest.py @@ -0,0 +1,35 @@ +import pycsolver as ps +from ctypes import * + +SATC_EQUALS = 0 + +def main(): + csolverlb = ps.loadCSolver() + solver = csolverlb.createCCSolver() + s1 = [0, 1, 2] + set1 = (c_long * len(s1))(*s1) + s2 = [3, 1, 7] + set2 = (c_long*len(s2))(*s2) + s1 = csolverlb.createSet(solver,c_uint(0), set1, c_uint(3)) + s2 = csolverlb.createSet(solver,0, set2, 3) + e1 = csolverlb.getElementVar(solver,s1) + e2 = csolverlb.getElementVar(solver,s2) + d = [s1, s2] + domain = (c_void_p*len(d))(*d) + equals = csolverlb.createPredicateOperator(solver,c_uint(SATC_EQUALS), domain, c_uint(2)); + inp = [e1, e2]; + inputs = (c_void_p*len(inp))(*inp) + b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2)); + csolverlb.addConstraint(solver,b); + if csolverlb.solve(solver) == 1: + print "e1="+ str(csolverlb.getElementValue(solver, e1)) + "\te2=" + str(csolverlb.getElementValue(solver, e2)); + else: + print "UNSAT"; + + csolverlb.deleteCCSolver(solver) + + + +if __name__== "__main__": + main() + diff --git a/src/ccsolver.cc b/src/ccsolver.cc index c58f380..2535c7f 100644 --- a/src/ccsolver.cc +++ b/src/ccsolver.cc @@ -3,14 +3,14 @@ #define CCSOLVER(solver) ((CSolver*)solver) -void* CreateCCSolver(){ +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){ +void *createSet(void* solver,unsigned int type, long *elements, unsigned int num){ return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num); } @@ -54,7 +54,7 @@ void *createFunctionOperator(void* solver,unsigned int op, void *domain, unsigne 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){ +void *createPredicateOperator(void* solver,unsigned int op, void **domain, unsigned int numDomain){ return CCSOLVER(solver)->createPredicateOperator((CompOp) op, (Set **)domain, (uint) numDomain); } diff --git a/src/ccsolver.h b/src/ccsolver.h index c14a3e0..37f1183 100644 --- a/src/ccsolver.h +++ b/src/ccsolver.h @@ -6,9 +6,9 @@ typedef void* CCSolver; #ifdef __cplusplus extern "C" { #endif -void* CreateCCSolver(); +void* createCCSolver(); void deleteCCSolver(void* solver); -void *createSet(void* solver,unsigned int type, void *elements, unsigned int num); +void *createSet(void* solver,unsigned int type, long *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); @@ -19,7 +19,7 @@ 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 *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); diff --git a/src/pycsolver.py b/src/pycsolver.py new file mode 100644 index 0000000..0e7494c --- /dev/null +++ b/src/pycsolver.py @@ -0,0 +1,23 @@ +from ctypes import * + +def loadCSolver(): + csolverlb = cdll.LoadLibrary("lib_cons_comp.so") + csolverlb.createCCSolver.restype = c_void_p + csolverlb.createSet.argtypes = [c_void_p, c_uint, POINTER(c_long), c_uint] + csolverlb.createSet.restype = c_void_p + csolverlb.getElementVar.argtypes = [c_void_p, c_void_p] + csolverlb.getElementVar.restype = c_void_p + csolverlb.createPredicateOperator.argtypes = [c_void_p, c_uint, POINTER(c_void_p), c_uint] + csolverlb.createPredicateOperator.restype = c_void_p + csolverlb.applyPredicate.argtypes = [c_void_p, c_void_p, POINTER(c_void_p), c_uint] + csolverlb.applyPredicate.restype = c_void_p + csolverlb.addConstraint.argtypes = [c_void_p, c_void_p] + csolverlb.addConstraint.restype = None + csolverlb.solve.argtypes = [c_void_p] + csolverlb.solve.restype = c_int + csolverlb.getElementValue.argtypes = [c_void_p, c_void_p] + csolverlb.getElementValue.restype = c_long + csolverlb.deleteCCSolver.argtypes = [c_void_p] + csolverlb.deleteCCSolver.restype = None + return csolverlb + -- 2.34.1