--- /dev/null
+package satune;
+
+import java.util.HashMap;
+import java.util.List;
+
+public class SatuneJavaAPI{
+ static {
+ System.loadLibrary("_cons_comp"); // loads lib_cons_comp.so
+ }
+ private Long satune = null;
+ private Long equalPredicate;
+
+ public SatuneJavaAPI(){
+ satune = createCCSolver();
+ equalPredicate = createPredicateOperator(satune, CompOp.SATC_EQUALS.getValue());
+ }
+
+ public long blockingPreviousResultConstraint(List<Long> elements){
+ long constraints [] = new long[elements.size()];
+ for(int i=0; i< elements.size(); i++){
+ long value = getElementValue(elements.get(i));
+ long constr = applyPredicate(CompOp.SATC_EQUALS, elements.get(i), (int)value);
+ constraints[i] = applyLogicalOperationOne(satune, LogicOp.SATC_NOT.getValue(), constr);
+ }
+ return applyLogicalOperation(LogicOp.SATC_OR.getValue(), constraints);
+ }
+
+ public Long createElement(List<Integer> domain){
+ return createElement(domain, false);
+ }
+
+ public Long createElement(List<Integer> domain, boolean freeze){
+
+ long domainArray [] = new long [domain.size()];
+ for ( int i = 0; i< domain.size(); i++){
+ domainArray[i] = domain.get(i);
+ }
+ long set = createSet(satune, 1, domainArray);
+ long el = getElementVar(satune,set);
+ if(freeze){
+ freezeElement(el);
+ }
+ return el;
+ }
+
+ public Long applyPredicate(CompOp op, Long element, int value){
+ Long predicate = getPredicate(op);
+ long inputs [] = {element, getElementConst(satune, 1, (long)value)};
+ return applyPredicate(satune, predicate, inputs);
+ }
+
+ public Long applyExactlyOneConstraint(long array[]){
+ return applyExactlyOneConstraint(satune, array);
+ }
+
+ public void addConstraint(Long constraint){
+ addConstraint(satune, constraint);
+ }
+
+ public Long applyLogicalOperation(int op, long array[]){
+ return applyLogicalOperation(satune, op, array);
+ }
+
+ public Long applyLogicalOperation(int op, long arg1, long arg2){
+ return applyLogicalOperationTwo(satune, op, arg1, arg2);
+ }
+
+ public void atLeastOneValue(long element){
+ mustHaveValue(satune, element);
+ }
+
+ public Long getBooleanTrue(){
+ return getBooleanTrue(satune);
+ }
+
+ public void print(){
+ printConstraints(satune);
+ }
+
+ public void turnOffOptimizations(){
+ turnoffOptimizations(satune);
+ }
+
+ public int solve(){
+ return solve(satune);
+ }
+
+ public int solveIncremental(){
+ return solveIncremental(satune);
+ }
+
+ public void serialize(){
+ serialize(satune);
+ }
+
+ public void resetSolver(){
+ resetCCSolver(satune);
+ }
+
+ public void deleteSolver(){
+ deleteCCSolver(satune);
+ satune = null;
+ }
+
+ public void printConstraint(long constraint){
+ printConstraint(satune, constraint);
+ }
+
+ public long getElementValue(long element){
+ return getElementValue(satune, element);
+ }
+
+ public void freezeElement(long element){
+ freezeElement(satune, element);
+ }
+
+ protected Long getPredicate(CompOp op){
+ switch(op){
+ case SATC_EQUALS: return equalPredicate;
+ default:
+ assert false;
+ }
+ return null;
+ }
+
+ private native long createCCSolver();
+ private native void deleteCCSolver(long solver);
+ private native void resetCCSolver(long solver);
+ private native long createSet(long solver, int type, long [] elements);
+ private native long createRangeSet(long solver,int type, long lowrange, long highrange);
+ private native long createRangeVar(long solver,int type, long lowrange, long highrange);
+ private native long createMutableSet(long solver, int type);
+ private native void addItem(long solver,long set, long element);
+ private native void finalizeMutableSet(long solver,long set);
+ private native long getElementVar(long solver,long set);
+ private native long getElementConst(long solver, int type, long value);
+ private native long getElementRange (long solver,long element);
+ private native long getBooleanVar(long solver, int type);
+ private native long getBooleanTrue(long solver);
+ private native long getBooleanFalse(long solver);
+ private native long createFunctionOperator(long solver, int op, long range, int overflowbehavior);
+ private native long createPredicateOperator(long solver, int op);
+ private native long createPredicateTable(long solver,long table, int behavior);
+ private native long createTable(long solver, long range);
+ private native long createTableForPredicate(long solver);
+ private native void addTableEntry(long solver,long table, long inputs, int inputSize, long result);
+ private native long completeTable(long solver,long table, int behavior);
+ private native long applyFunction(long solver,long function, long array, int numArrays, long overflowstatus);
+ private native long applyPredicateTable(long solver,long predicate, long inputs[], long undefinedStatus);
+ private native long applyPredicate(long solver,long predicate, long inputs []);
+ private native long applyLogicalOperation(long solver, int op, long array[]);
+ private native long applyExactlyOneConstraint(long solver, long array[]);
+ private native long applyLogicalOperationTwo(long solver, int op, long arg1, long arg2);
+ private native long applyLogicalOperationOne(long solver, int op, long arg);
+ private native void addConstraint(long solver,long constraint);
+ private native void printConstraint(long solver,long constraint);
+ private native long createOrder(long solver, int type, long set);
+ private native long orderConstraint(long solver,long order, long first, long second);
+ private native int solve(long solver);
+ private native int solveIncremental(long solver);
+ private native long getElementValue(long solver,long element);
+ private native void freezeElement(long solver,long element);
+ private native int getBooleanValue(long solver,long bool);
+ private native int getOrderConstraintValue(long solver,long order, long first, long second);
+ private native void printConstraints(long solver);
+ private native void turnoffOptimizations(long solver);
+ private native void serialize(long solver);
+ private native void mustHaveValue(long solver, long element);
+ private native void setInterpreter(long solver, int type);
+ private native long clone(long solver);
+
+// public static void main(String[] args)
+// {
+// SatuneJavaAPI satuneapi = new SatuneJavaAPI();
+// long solver = satuneapi.createCCSolver();
+// long constr = satuneapi.getBooleanVar(solver, 1);
+// satuneapi.addConstraint(solver, constr);
+// int value = satuneapi.solve(solver);
+// if (value == 1) {
+// System.out.println("B1 = " + satuneapi.getBooleanValue(solver, constr));
+// } else {
+// System.out.println("UNSAT");
+// }
+// satuneapi.deleteCCSolver(solver);
+// }
+}
+
+
projects / Benchmarks_CSolver.git / blobdiff