1 package edu.tamu.aser.constraints;
3 import java.util.HashMap;
5 public class SatuneJavaAPI{
7 private static Long order = null;
8 private static Long satune = null;
9 private static SatuneJavaAPI instance = null;
10 public static Long maxRange = 0L;
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
19 public static SatuneJavaAPI getInstance(){
21 instance = new SatuneJavaAPI();
26 public Long lookupBooleanOrder(Long gid1, Long gid2) {
27 return orderConstraint(satune,order, gid1, gid2);
30 public void addConstraint(Long constraint){
31 addConstraint(satune, constraint);
34 public Long LogicalOperationTwo(int op, long arg1, long arg2){
35 return applyLogicalOperationTwo(satune, op, arg1, arg2);
38 public Long getBooleanTrue(){
39 return getBooleanTrue(satune);
43 printConstraints(satune);
46 public void turnoffOptimizations(){
47 turnoffOptimizations(satune);
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);
94 public static void main(String[] args)
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);
102 System.out.println("B1 = " + satuneapi.getBooleanValue(solver, constr));
104 System.out.println("UNSAT");
106 satuneapi.deleteCCSolver(solver);