src/Test/pycsolvertest.py

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