src/SatuneJavaAPI.java

   1 package edu.tamu.aser.constraints;
   2
   3 import java.util.HashMap;
   4
   5 public class SatuneJavaAPI{
   6
   7         private static Long order = null;
   8         private static Long satune = null;
   9         private static SatuneJavaAPI instance = null;
  10         public static Long maxRange = 0L;
  11
  12         private SatuneJavaAPI(){
  13             System.loadLibrary("_cons_comp");    // loads lib_cons_comp.so
  14             satune = createCCSolver();
  15             Long set = createRangeSet(satune, 1, 0, maxRange);
  16             order = createOrder(satune, 1, set); // 0= Partial Order, 1 = total order
  17         }
  18
  19         public static SatuneJavaAPI getInstance(){
  20             if(instance == null){
  21                 instance = new SatuneJavaAPI();
  22             }
  23             return instance;
  24         }
  25
  26         public Long lookupBooleanOrder(Long gid1, Long gid2) {
  27             return orderConstraint(satune,order, gid1, gid2);
  28         }
  29
  30         public void addConstraint(Long constraint){
  31             addConstraint(satune, constraint);
  32         }
  33
  34         public Long LogicalOperationTwo(int op, long arg1, long arg2){
  35             return applyLogicalOperationTwo(satune, op, arg1, arg2);
  36         }
  37
  38         public Long getBooleanTrue(){
  39             return getBooleanTrue(satune);
  40         }
  41
  42         public void print(){
  43             printConstraints(satune);
  44         }
  45
  46         public void turnoffOptimizations(){
  47             turnoffOptimizations(satune);
  48         }
  49
  50         public int solve(){
  51             return solve(satune);
  52         }
  53         private native long createCCSolver();
  54         private native void deleteCCSolver(long solver);
  55         private native long createSet(long solver, int type, long elements, int num);
  56         private native long createRangeSet(long solver,int type, long lowrange, long highrange);
  57         private native long createRangeVar(long solver,int type, long lowrange, long highrange);
  58         private native long createMutableSet(long solver, int type);
  59         private native void addItem(long solver,long set, long element);
  60         private native void finalizeMutableSet(long solver,long set);
  61         private native long getElementVar(long solver,long set);
  62         private native long getElementConst(long solver, int type, long value);
  63         private native long getElementRange (long solver,long element);
  64         private native long getBooleanVar(long solver, int type);
  65         private native long getBooleanTrue(long solver);
  66         private native long getBooleanFalse(long solver);
  67         private native long createFunctionOperator(long solver, int op, long range, int overflowbehavior);
  68         private native long createPredicateOperator(long solver, int op);
  69         private native long createPredicateTable(long solver,long table, int behavior);
  70         private native long createTable(long solver, long range);
  71         private native long createTableForPredicate(long solver);
  72         private native void addTableEntry(long solver,long table, long inputs, int inputSize, long result);
  73         private native long completeTable(long solver,long table, int behavior);
  74         private native long applyFunction(long solver,long function, long array, int numArrays, long overflowstatus);
  75         private native long applyPredicateTable(long solver,long predicate, long inputs, int numInputs, long undefinedStatus);
  76         private native long applyPredicate(long solver,long predicate, long inputs, int numInputs);
  77         private native long applyLogicalOperation(long solver, int op, long array, int asize);
  78         private native long applyLogicalOperationTwo(long solver, int op, long arg1, long arg2);
  79         private native long applyLogicalOperationOne(long solver, int op, long arg);
  80         private native void addConstraint(long solver,long constraint);
  81         private native long createOrder(long solver, int type, long set);
  82         private native long orderConstraint(long solver,long order, long first, long second);
  83         private native int solve(long solver);
  84         private native long getElementValue(long solver,long element);
  85         private native int getBooleanValue(long solver,long bool);
  86         private native int getOrderConstraintValue(long solver,long order, long first, long second);
  87         private native void printConstraints(long solver);
  88         private native void turnoffOptimizations(long solver);
  89         private native void serialize(long solver);
  90         private native void mustHaveValue(long solver, long element);
  91         private native void setInterpreter(long solver, int type);
  92         private native long clone(long solver);
  93
  94         public static void main(String[] args)
  95         {
  96                 SatuneJavaAPI satuneapi = SatuneJavaAPI.getInstance();
  97                 long solver = SatuneJavaAPI.getInstance().createCCSolver();
  98                 long constr = satuneapi.getBooleanVar(solver, 1);
  99                 satuneapi.addConstraint(solver, constr);
 100                 int value = satuneapi.solve(solver);
 101                 if (value == 1) {
 102                         System.out.println("B1 = " + satuneapi.getBooleanValue(solver, constr));
 103                 } else {
 104                         System.out.println("UNSAT");
 105                 }
 106                 satuneapi.deleteCCSolver(solver);
 107         }
 108 }
 109
 110