turning of the optimizations when using alloy ...
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 7 Feb 2019 00:23:13 +0000 (16:23 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 7 Feb 2019 00:23:13 +0000 (16:23 -0800)
src/csolver.cc

index 5b0d073..3c8fffa 100644 (file)
@@ -390,80 +390,88 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-       BooleanEdge newarray[asize];
-       switch (op) {
-       case SATC_NOT: {
-               return array[0].negate();
-       }
-       case SATC_IFF: {
-               for (uint i = 0; i < 2; i++) {
-                       if (isTrue(array[i])) { // It can be undefined
-                               return array[1 - i];
-                       } else if (isFalse(array[i])) {
-                               newarray[0] = array[1 - i];
-                               return applyLogicalOperation(SATC_NOT, newarray, 1);
-                       } else if (array[i]->type == LOGICOP) {
-                               BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
-                               if (b->replaced) {
-                                       return rewriteLogicalOperation(op, array, asize);
+       if(!useAlloyCompiler()){
+               BooleanEdge newarray[asize];
+               switch (op) {
+               case SATC_NOT: {
+                       return array[0].negate();
+               }
+               case SATC_IFF: {
+                       for (uint i = 0; i < 2; i++) {
+                               if (isTrue(array[i])) { // It can be undefined
+                                       return array[1 - i];
+                               } else if (isFalse(array[i])) {
+                                       newarray[0] = array[1 - i];
+                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
+                               } else if (array[i]->type == LOGICOP) {
+                                       BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
+                                       if (b->replaced) {
+                                               return rewriteLogicalOperation(op, array, asize);
+                                       }
                                }
                        }
+                       break;
                }
-               break;
-       }
-       case SATC_OR: {
-               for (uint i = 0; i < asize; i++) {
-                       newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
+               case SATC_OR: {
+                       for (uint i = 0; i < asize; i++) {
+                               newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
+                       }
+                       return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
                }
-               return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
-       }
-       case SATC_AND: {
-               uint newindex = 0;
-               for (uint i = 0; i < asize; i++) {
-                       BooleanEdge b = array[i];
-                       if (b->type == LOGICOP) {
-                               if (((BooleanLogic *)b.getBoolean())->replaced)
-                                       return rewriteLogicalOperation(op, array, asize);
+               case SATC_AND: {
+                       uint newindex = 0;
+                       for (uint i = 0; i < asize; i++) {
+                               BooleanEdge b = array[i];
+                               if (b->type == LOGICOP) {
+                                       if (((BooleanLogic *)b.getBoolean())->replaced)
+                                               return rewriteLogicalOperation(op, array, asize);
+                               }
+                               if (isTrue(b))
+                                       continue;
+                               else if (isFalse(b)) {
+                                       return boolFalse;
+                               } else
+                                       newarray[newindex++] = b;
                        }
-                       if (isTrue(b))
-                               continue;
-                       else if (isFalse(b)) {
-                               return boolFalse;
-                       } else
-                               newarray[newindex++] = b;
+                       if (newindex == 0) {
+                               return boolTrue;
+                       } else if (newindex == 1) {
+                               return newarray[0];
+                       } else {
+                               bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
+                               array = newarray;
+                               asize = newindex;
+                       }
+                       break;
+               }
+               case SATC_XOR: {
+                       //handle by translation
+                       return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
+               }
+               case SATC_IMPLIES: {
+                       //handle by translation
+                       return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
                }
-               if (newindex == 0) {
-                       return boolTrue;
-               } else if (newindex == 1) {
-                       return newarray[0];
+               }
+       
+               ASSERT(asize != 0);
+               Boolean *boolean = new BooleanLogic(this, op, array, asize);
+               Boolean *b = boolMap.get(boolean);
+               if (b == NULL) {
+                       boolean->updateParents();
+                       boolMap.put(boolean, boolean);
+                       allBooleans.push(boolean);
+                       return BooleanEdge(boolean);
                } else {
-                       bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
-                       array = newarray;
-                       asize = newindex;
+                       delete boolean;
+                       return BooleanEdge(b);
                }
-               break;
-       }
-       case SATC_XOR: {
-               //handle by translation
-               return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
-       }
-       case SATC_IMPLIES: {
-               //handle by translation
-               return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
-       }
-       }
-
-       ASSERT(asize != 0);
-       Boolean *boolean = new BooleanLogic(this, op, array, asize);
-       Boolean *b = boolMap.get(boolean);
-       if (b == NULL) {
-               boolean->updateParents();
-               boolMap.put(boolean, boolean);
+       } else {
+               ASSERT(asize != 0);
+               Boolean *boolean = new BooleanLogic(this, op, array, asize);
                allBooleans.push(boolean);
                return BooleanEdge(boolean);
-       } else {
-               delete boolean;
-               return BooleanEdge(b);
+       
        }
 }
 
@@ -482,77 +490,83 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                }
        }
        Boolean *constraint = new BooleanOrder(order, first, second);
-       Boolean *b = boolMap.get(constraint);
-
-       if (b == NULL) {
-               allBooleans.push(constraint);
-               boolMap.put(constraint, constraint);
-               constraint->updateParents();
-               if (order->graph != NULL) {
-                       OrderGraph *graph = order->graph;
-                       OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
-                       if (from != NULL) {
-                               OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
-                               if (to != NULL) {
-                                       OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-                                       OrderEdge *invedge;
-
-                                       if (edge != NULL && edge->mustPos) {
-                                               replaceBooleanWithTrueNoRemove(constraint);
-                                       } else if (edge != NULL && edge->mustNeg) {
-                                               replaceBooleanWithFalseNoRemove(constraint);
-                                       } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
-                                                                                && invedge->mustPos) {
-                                               replaceBooleanWithFalseNoRemove(constraint);
+       if (!useAlloyCompiler() ){ 
+               Boolean *b = boolMap.get(constraint);
+
+               if (b == NULL) {
+                       allBooleans.push(constraint);
+                       boolMap.put(constraint, constraint);
+                       constraint->updateParents();
+                       if ( order->graph != NULL) {
+                               OrderGraph *graph = order->graph;
+                               OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
+                               if (from != NULL) {
+                                       OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
+                                       if (to != NULL) {
+                                               OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
+                                               OrderEdge *invedge;
+
+                                               if (edge != NULL && edge->mustPos) {
+                                                       replaceBooleanWithTrueNoRemove(constraint);
+                                               } else if (edge != NULL && edge->mustNeg) {
+                                                       replaceBooleanWithFalseNoRemove(constraint);
+                                               } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+                                                                                        && invedge->mustPos) {
+                                                       replaceBooleanWithFalseNoRemove(constraint);
+                                               }
                                        }
                                }
                        }
+               } else {
+                       delete constraint;
+                       constraint = b;
                }
-       } else {
-               delete constraint;
-               constraint = b;
        }
-
        BooleanEdge be = BooleanEdge(constraint);
        return negate ? be.negate() : be;
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if (isTrue(constraint))
-               return;
-       else if (isFalse(constraint)) {
-               setUnSAT();
-       }
-       else {
-               if (constraint->type == LOGICOP) {
-                       BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
-                       if (!constraint.isNegated()) {
-                               if (b->op == SATC_AND) {
-                                       uint size = b->inputs.getSize();
-                                       //Handle potential concurrent modification
-                                       BooleanEdge array[size];
-                                       for (uint i = 0; i < size; i++) {
-                                               array[i] = b->inputs.get(i);
-                                       }
-                                       for (uint i = 0; i < size; i++) {
-                                               addConstraint(array[i]);
+       if(!useAlloyCompiler()){
+               if (isTrue(constraint))
+                       return;
+               else if (isFalse(constraint)) {
+                       setUnSAT();
+               }
+               else {
+                       if (constraint->type == LOGICOP) {
+                               BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
+                               if (!constraint.isNegated()) {
+                                       if (b->op == SATC_AND) {
+                                               uint size = b->inputs.getSize();
+                                               //Handle potential concurrent modification
+                                               BooleanEdge array[size];
+                                               for (uint i = 0; i < size; i++) {
+                                                       array[i] = b->inputs.get(i);
+                                               }
+                                               for (uint i = 0; i < size; i++) {
+                                                       addConstraint(array[i]);
+                                               }
+                                               return;
                                        }
+                               }
+                               if (b->replaced) {
+                                       addConstraint(doRewrite(constraint));
                                        return;
                                }
                        }
-                       if (b->replaced) {
-                               addConstraint(doRewrite(constraint));
-                               return;
+                       constraints.add(constraint);
+                       Boolean *ptr = constraint.getBoolean();
+
+                       if (ptr->boolVal == BV_UNSAT) {
+                               setUnSAT();
                        }
-               }
-               constraints.add(constraint);
-               Boolean *ptr = constraint.getBoolean();
 
-               if (ptr->boolVal == BV_UNSAT) {
-                       setUnSAT();
+                       replaceBooleanWithTrueNoRemove(constraint);
+                       constraint->parents.clear();
                }
-
-               replaceBooleanWithTrueNoRemove(constraint);
+       } else{
+               constraints.add(constraint);
                constraint->parents.clear();
        }
 }
@@ -590,61 +604,64 @@ int CSolver::solve() {
                tuner = new DefaultTuner();
                deleteTuner = true;
        }
-
-
-       {
-               SetIteratorOrder *orderit = activeOrders.iterator();
-               while (orderit->hasNext()) {
-                       Order *order = orderit->next();
-                       if (order->graph != NULL) {
-                               delete order->graph;
-                               order->graph = NULL;
+       int result = IS_INDETER;
+       if(useAlloyCompiler()){
+               alloyEncoder->encode();
+               model_print("Problem encoded in Alloy\n");
+               result = alloyEncoder->solve();
+               model_print("Problem solved by Alloy\n");
+       } else{
+
+               {
+                       SetIteratorOrder *orderit = activeOrders.iterator();
+                       while (orderit->hasNext()) {
+                               Order *order = orderit->next();
+                               if (order->graph != NULL) {
+                                       delete order->graph;
+                                       order->graph = NULL;
+                               }
                        }
+                       delete orderit;
                }
-               delete orderit;
-       }
-       computePolarities(this);
-       long long time1 = getTimeNano();
-       model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
-       Preprocess pp(this);
-       pp.doTransform();
-       long long time2 = getTimeNano();
-       model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
+               computePolarities(this);
+               long long time1 = getTimeNano();
+               model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+               Preprocess pp(this);
+               pp.doTransform();
+               long long time2 = getTimeNano();
+               model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 
-       DecomposeOrderTransform dot(this);
-       dot.doTransform();
-       time1 = getTimeNano();
-       model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+               DecomposeOrderTransform dot(this);
+               dot.doTransform();
+               time1 = getTimeNano();
+               model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 
-       IntegerEncodingTransform iet(this);
-       iet.doTransform();
+               IntegerEncodingTransform iet(this);
+               iet.doTransform();
 
-       ElementOpt eop(this);
-       eop.doTransform();
+               ElementOpt eop(this);
+               eop.doTransform();
 
-       EncodingGraph eg(this);
-       eg.encode();
+               EncodingGraph eg(this);
+               eg.encode();
 
-       naiveEncodingDecision(this);
-//     eg.validate();
+               naiveEncodingDecision(this);
+       //      eg.validate();
 
-       VarOrderingOpt bor(this, satEncoder);
-       bor.doTransform();
+               VarOrderingOpt bor(this, satEncoder);
+               bor.doTransform();
 
-       time2 = getTimeNano();
-       model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               time2 = getTimeNano();
+               model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 
-       satEncoder->encodeAllSATEncoder(this);
-       time1 = getTimeNano();
+               satEncoder->encodeAllSATEncoder(this);
+               time1 = getTimeNano();
 
-       model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+               model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
+               model_print("Is problem UNSAT after encoding: %d\n", unsat);
+               
 
-       model_print("Is problem UNSAT after encoding: %d\n", unsat);
-       int result = IS_INDETER;
-       if(alloyEncoder != NULL){
-               alloyEncoder->encode();
-               result = alloyEncoder->solve();
-       }else{
                result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
                model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
                time2 = getTimeNano();