Merge branch 'sparseOrderOpt' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler...

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
old mode 100644 (file)
new mode 100755 (executable)
index 45f2c5f..d69e194
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -192,13 +192,24 @@ Edge createNode(NodeType type, uint numEdges, Edge *edges) {
 }
 
 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
-       Edge edgearray[numEdges];
+       if (numEdges < 200000) {
+               Edge edgearray[numEdges];
 
-       for (uint i = 0; i < numEdges; i++) {
-               edgearray[i] = constraintNegate(edges[i]);
+               for (uint i = 0; i < numEdges; i++) {
+                       edgearray[i] = constraintNegate(edges[i]);
+               }
+               Edge eand = constraintAND(cnf, numEdges, edgearray);
+               return constraintNegate(eand);
+       } else {
+               Edge * edgearray=(Edge *)ourmalloc(numEdges*sizeof(Edge));
+               
+               for (uint i = 0; i < numEdges; i++) {
+                       edgearray[i] = constraintNegate(edges[i]);
+               }
+               Edge eand = constraintAND(cnf, numEdges, edgearray);
+               ourfree(edgearray);
+               return constraintNegate(eand);
        }
-       Edge eand = constraintAND(cnf, numEdges, edgearray);
-       return constraintNegate(eand);
 }
 
 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
old mode 100644 (file)
new mode 100755 (executable)

diff --git a/src/SatuneJavaAPI.java b/src/SatuneJavaAPI.java
index a2c35f3b51b9526eb7ddc6361eda177b90bcf760..2b6baeaf6a05840123a9761e9ca69211ee74ca70 100644 (file)
--- a/src/SatuneJavaAPI.java
+++ b/src/SatuneJavaAPI.java
@@ -1,50 +1,95 @@
+package edu.tamu.aser.constraints;
+
+import java.util.HashMap;
 
 public class SatuneJavaAPI{
-       static {
-               System.loadLibrary("_cons_comp");    // loads lib_cons_comp.so
-       }
-       public native long createCCSolver();
-       public native void deleteCCSolver(long solver);
-       public native long createSet(long solver, int type, long elements, int num);
-       public native long createRangeSet(long solver,int type, long lowrange, long highrange);
-       public native long createRangeVar(long solver,int type, long lowrange, long highrange);
-       public native long createMutableSet(long solver, int type);
-       public native void addItem(long solver,long set, long element);
-       public native void finalizeMutableSet(long solver,long set);
-       public native long getElementVar(long solver,long set);
-       public native long getElementConst(long solver, int type, long value);
-       public native long getElementRange (long solver,long element);
-       public native long getBooleanVar(long solver, int type);
-       public native long createFunctionOperator(long solver, int op, long range, int overflowbehavior);
-       public native long createPredicateOperator(long solver, int op);
-       public native long createPredicateTable(long solver,long table, int behavior);
-       public native long createTable(long solver, long range);
-       public native long createTableForPredicate(long solver);
-       public native void addTableEntry(long solver,long table, long inputs, int inputSize, long result);
-       public native long completeTable(long solver,long table, int behavior);
-       public native long applyFunction(long solver,long function, long array, int numArrays, long overflowstatus);
-       public native long applyPredicateTable(long solver,long predicate, long inputs, int numInputs, long undefinedStatus);
-       public native long applyPredicate(long solver,long predicate, long inputs, int numInputs);
-       public native long applyLogicalOperation(long solver, int op, long array, int asize);
-       public native long applyLogicalOperationTwo(long solver, int op, long arg1, long arg2);
-       public native long applyLogicalOperationOne(long solver, int op, long arg);
-       public native void addConstraint(long solver,long constraint);
-       public native long createOrder(long solver, int type, long set);
-       public native long orderConstraint(long solver,long order, long first, long second);
-       public native int solve(long solver);
-       public native long getElementValue(long solver,long element);
-       public native int getBooleanValue(long solver,long bool);
-       public native int getOrderConstraintValue(long solver,long order, long first, long second);
-       public native void printConstraints(long solver);
-       public native void serialize(long solver);
-       public native void mustHaveValue(long solver, long element);
-       public native void setInterpreter(long solver, int type);
-       public native long clone(long solver);
+        
+        private static Long order = null;
+        private static Long satune = null;
+        private static SatuneJavaAPI instance = null;
+        public static Long maxRange = 0L;
+
+        private SatuneJavaAPI(){
+            System.loadLibrary("_cons_comp");    // loads lib_cons_comp.so
+            satune = createCCSolver();
+            Long set = createRangeSet(satune, 1, 0, maxRange);
+            order = createOrder(satune, 1, set); // 0= Partial Order, 1 = total order
+        }
+        
+        public static SatuneJavaAPI getInstance(){
+            if(instance == null){
+                instance = new SatuneJavaAPI();
+            }
+            return instance;
+        }
+        
+        public Long lookupBooleanOrder(Long gid1, Long gid2) {
+            return orderConstraint(satune,order, gid1, gid2);
+        }
+        
+        public void addConstraint(Long constraint){
+            addConstraint(satune, constraint);
+        }
+        
+        public Long LogicalOperationTwo(int op, long arg1, long arg2){
+            return applyLogicalOperationTwo(satune, op, arg1, arg2);
+        }
+        
+        public Long getBooleanTrue(){
+            return getBooleanTrue(satune);
+        }
+        
+        public void print(){
+            printConstraints(satune);
+        }
+       
+        public int solve(){
+            return solve(satune);
+        }
+        private native long createCCSolver();
+       private native void deleteCCSolver(long solver);
+       private native long createSet(long solver, int type, long elements, int num);
+       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, int numInputs, long undefinedStatus);
+       private native long applyPredicate(long solver,long predicate, long inputs, int numInputs);
+       private native long applyLogicalOperation(long solver, int op, long array, int asize);
+       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 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 long getElementValue(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 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();
+               SatuneJavaAPI satuneapi = SatuneJavaAPI.getInstance();
+               long solver = SatuneJavaAPI.getInstance().createCCSolver();
                long constr = satuneapi.getBooleanVar(solver, 1);
                satuneapi.addConstraint(solver, constr);
                int value = satuneapi.solve(solver);

diff --git a/src/Tuner/basictuner.cc b/src/Tuner/basictuner.cc
index 31b43750482fcc1cd82f255ed3a42c8008fda03b..122f4d332c1915163997c1e8b45378e3dd91cbc5 100644 (file)
--- a/src/Tuner/basictuner.cc
+++ b/src/Tuner/basictuner.cc
@@ -157,9 +157,10 @@ long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
        uint timeinsecs = problem->getBestTime() / NANOSEC;
        uint adaptive = (timeinsecs > 30) ? timeinsecs * 5 : 150;
        uint maxtime = (adaptive < timeout) ? adaptive : timeout;
-
+       uint satuneTimeout = 2*maxtime;
        //Do run
-       snprintf(buffer, sizeof(buffer), "./run.sh deserializerun %s %u tuner%u result%u > log%u", problem->getProblem(), maxtime, execnum, execnum, execnum);
+       snprintf(buffer, sizeof(buffer), "timeout %u ./run.sh deserializerun %s %u tuner%u result%u > log%u", satuneTimeout, problem->getProblem(), maxtime, execnum, execnum, execnum);
+       model_print("Running: %s\n", buffer);
        int status = system(buffer);
 
        long long metric = -1;

diff --git a/src/Tuner/satuner.cc b/src/Tuner/satuner.cc
index 4844ce37a2f8f5796188225e7272f10c94bbcfa3..277508160b323a0b5d84d78da941d5c226d480a6 100644 (file)
--- a/src/Tuner/satuner.cc
+++ b/src/Tuner/satuner.cc
@@ -153,11 +153,20 @@ void SATuner::tune() {
                        TunerRecord *tuner2 = tunerV->get(tunerNumber + i);
                        ASSERT( tunerNumber + i < tunerV->getSize());
                        model_print("Tuner1 = %d \tTuner2 = %d\n", tuner1->getTunerNumber(), tuner2->getTunerNumber());
-                       ASSERT(scores.contains(tuner1));
-                       ASSERT(scores.contains(tuner2));
-                       int score1 = scores.get(tuner1);
-                       int score2 = scores.get(tuner2);
-                       if ( score2 > score1 ) {
+                       
+                       int score1, score2;
+                       if(!scores.contains(tuner1)){
+                               score1 = 0;
+                       }else {
+                               score1 = scores.get(tuner1);
+                       }
+                       if(!scores.contains(tuner2)){
+                               score2=0;
+                       }else {
+                               score2= scores.get(tuner2);
+                       }
+                       
+                       if( score2 > score1 ){
                                removeTunerIndex(tunerV, i, allplaces);
                        } else if ( score2 < score1) {
                                model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1 - score2) * 1.0 / t));