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