src/SatuneJavaAPI.java

   1
   2 public class SatuneJavaAPI{
   3         static {
   4                 System.loadLibrary("_cons_comp");    // loads lib_cons_comp.so
   5         }
   6         public native long createCCSolver();
   7         public native void deleteCCSolver(long solver);
   8         public native long createSet(long solver, int type, long elements, int num);
   9         public native long createRangeSet(long solver,int type, long lowrange, long highrange);
  10         public native long createRangeVar(long solver,int type, long lowrange, long highrange);
  11         public native long createMutableSet(long solver, int type);
  12         public native void addItem(long solver,long set, long element);
  13         public native void finalizeMutableSet(long solver,long set);
  14         public native long getElementVar(long solver,long set);
  15         public native long getElementConst(long solver, int type, long value);
  16         public native long getElementRange (long solver,long element);
  17         public native long getBooleanVar(long solver, int type);
  18         public native long createFunctionOperator(long solver, int op, long range, int overflowbehavior);
  19         public native long createPredicateOperator(long solver, int op);
  20         public native long createPredicateTable(long solver,long table, int behavior);
  21         public native long createTable(long solver, long range);
  22         public native long createTableForPredicate(long solver);
  23         public native void addTableEntry(long solver,long table, long inputs, int inputSize, long result);
  24         public native long completeTable(long solver,long table, int behavior);
  25         public native long applyFunction(long solver,long function, long array, int numArrays, long overflowstatus);
  26         public native long applyPredicateTable(long solver,long predicate, long inputs, int numInputs, long undefinedStatus);
  27         public native long applyPredicate(long solver,long predicate, long inputs, int numInputs);
  28         public native long applyLogicalOperation(long solver, int op, long array, int asize);
  29         public native long applyLogicalOperationTwo(long solver, int op, long arg1, long arg2);
  30         public native long applyLogicalOperationOne(long solver, int op, long arg);
  31         public native void addConstraint(long solver,long constraint);
  32         public native long createOrder(long solver, int type, long set);
  33         public native long orderConstraint(long solver,long order, long first, long second);
  34         public native int solve(long solver);
  35         public native long getElementValue(long solver,long element);
  36         public native int getBooleanValue(long solver,long bool);
  37         public native int getOrderConstraintValue(long solver,long order, long first, long second);
  38         public native void printConstraints(long solver);
  39         public native void serialize(long solver);
  40         public native void mustHaveValue(long solver, long element);
  41         public native void setInterpreter(long solver, int type);
  42         public native long clone(long solver);
  43
  44         public static void main(String[] args)
  45         {
  46                 SatuneJavaAPI satuneapi = new SatuneJavaAPI();
  47                 long solver = satuneapi.createCCSolver();
  48                 long constr = satuneapi.getBooleanVar(solver, 1);
  49                 satuneapi.addConstraint(solver, constr);
  50                 int value = satuneapi.solve(solver);
  51                 if (value == 1) {
  52                         System.out.println("B1 = " + satuneapi.getBooleanValue(solver, constr));
  53                 } else {
  54                         System.out.println("UNSAT");
  55                 }
  56                 satuneapi.deleteCCSolver(solver);
  57         }
  58 }
  59
  60