Completing the python wrapper + editing the c APIs
[satune.git] / src / Test / pycsolvertest.py
1 import pycsolver as ps
2 from ctypes import *
3
4 SATC_EQUALS = 0
5
6 def main():
7         csolverlb = ps.loadCSolver()
8         solver = csolverlb.createCCSolver()
9         s1 = [0, 1, 2]
10         set1 = (c_long * len(s1))(*s1)
11         s2 = [3, 1, 7]
12         set2 = (c_long*len(s2))(*s2)
13         s1 = csolverlb.createSet(solver,c_uint(0), set1, c_uint(3))
14         s2 = csolverlb.createSet(solver,0, set2, 3)
15         e1 = csolverlb.getElementVar(solver,s1)
16         e2 = csolverlb.getElementVar(solver,s2)
17         d = [s1, s2]
18         domain = (c_void_p*len(d))(*d)
19         equals = csolverlb.createPredicateOperator(solver,c_uint(SATC_EQUALS), domain, c_uint(2));
20         inp = [e1, e2];
21         inputs = (c_void_p*len(inp))(*inp)
22         b = csolverlb.applyPredicate(solver,equals, inputs, c_uint(2));
23         csolverlb.addConstraint(solver,b);
24         if csolverlb.solve(solver) == 1:
25                 print "e1="+ str(csolverlb.getElementValue(solver, e1)) + "\te2=" + str(csolverlb.getElementValue(solver, e2));
26         else:
27                 print "UNSAT";
28
29         csolverlb.deleteCCSolver(solver)
30
31
32   
33 if __name__== "__main__":
34         main()
35