Adding the python wrapper for the constraint solver

diff --git a/src/Test/Makefile b/src/Test/Makefile
index f7c2929e7c4d79d2a5907ad628fdf0f8b5f89909..50399a008cafbaefdd4e26c89c058a3ea586c3d2 100644 (file)
--- 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 3bcb3c6753abe751dbd32d4049f9a08c73585f70..bdb8898f05267e0f1651417c1eb92d970aa72f86 100644 (file)
--- 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 (file)
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 c58f380385001745a69254a764d5cdbaa508c206..2535c7f935b3c4f2c92a8a9c634c597dda278706 100644 (file)
--- 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 c14a3e0cd5ee519ef6b268ddb2cbca6abe650c9f..37f1183755a7ba3ccac22f94ced0f79cd2c3457b 100644 (file)
--- 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 (file)
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
+