Adding ASTTransform ...
authorHamed <hamed.gorjiara@gmail.com>
Fri, 25 Aug 2017 04:28:59 +0000 (21:28 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Fri, 25 Aug 2017 04:28:59 +0000 (21:28 -0700)
16 files changed:
src/AST/order.cc
src/AST/order.h
src/ASTAnalyses/orderencoder.cc
src/ASTAnalyses/ordergraph.cc
src/ASTTransform/asttransform.cc [new file with mode: 0644]
src/ASTTransform/asttransform.h [new file with mode: 0644]
src/ASTTransform/integerencoding.cc [new file with mode: 0644]
src/ASTTransform/integerencoding.h [new file with mode: 0644]
src/ASTTransform/orderdecompose.cc [new file with mode: 0644]
src/ASTTransform/orderdecompose.h [new file with mode: 0644]
src/Backend/satencoder.cc
src/Backend/satorderencoder.cc
src/Backend/satorderencoder.h
src/Collections/hashset.h
src/Tuner/tunable.h
src/csolver.cc

index 5e16938..e597e72 100644 (file)
@@ -10,7 +10,9 @@ Order::Order(OrderType _type, Set *_set) :
        orderPairTable(NULL),
        elementTable(NULL),
        graph(NULL),
-       order(this) {
+       order(this)
+{
+       auxSet = new Set(_type,(uint64_t) 1,(uint64_t) _set->getSize());
 }
 
 void Order::initializeOrderHashTable() {
index 1645786..acd6426 100644 (file)
@@ -14,6 +14,7 @@ class Order {
        ~Order();
        OrderType type;
        Set *set;
+       Set* auxSet;
        HashTableOrderPair *orderPairTable;
        HashSetOrderElement* elementTable;
        OrderGraph *graph;
index 35ea575..06668fd 100644 (file)
@@ -369,85 +369,23 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
        delete iterator;
 }
 
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
-       Vector<Order *> ordervec;
-       Vector<Order *> partialcandidatevec;
-       uint size = order->constraints.getSize();
-       for (uint i = 0; i < size; i++) {
-               BooleanOrder *orderconstraint = order->constraints.get(i);
-               OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
-               OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
-               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
-               if (from->sccNum != to->sccNum) {
-                       OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
-                       if (edge->polPos) {
-                               replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
-                       } else if (edge->polNeg) {
-                               replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
-                       } else {
-                               //This case should only be possible if constraint isn't in AST
-                               ASSERT(0);
-                       }
-               } else {
-                       //Build new order and change constraint's order
-                       Order *neworder = NULL;
-                       if (ordervec.getSize() > from->sccNum)
-                               neworder = ordervec.get(from->sccNum);
-                       if (neworder == NULL) {
-                               MutableSet *set = new MutableSet(order->set->type);
-                               neworder = new Order(order->type, set);
-                               This->allOrders.push(neworder);
-                               ordervec.setExpand(from->sccNum, neworder);
-                               if (order->type == PARTIAL)
-                                       partialcandidatevec.setExpand(from->sccNum, neworder);
-                               else
-                                       partialcandidatevec.setExpand(from->sccNum, NULL);
-                       }
-                       if (from->status != ADDEDTOSET) {
-                               from->status = ADDEDTOSET;
-                               ((MutableSet *)neworder->set)->addElementMSet(from->id);
-                       }
-                       if (to->status != ADDEDTOSET) {
-                               to->status = ADDEDTOSET;
-                               ((MutableSet *)neworder->set)->addElementMSet(to->id);
-                       }
-                       if (order->type == PARTIAL) {
-                               OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
-                               if (edge->polNeg)
-                                       partialcandidatevec.setExpand(from->sccNum, NULL);
-                       }
-                       orderconstraint->order = neworder;
-                       neworder->addOrderConstraint(orderconstraint);
-               }
-       }
-
-       uint pcvsize=partialcandidatevec.getSize();
-       for(uint i=0;i<pcvsize;i++) {
-               Order * neworder=partialcandidatevec.get(i);
-               if (neworder != NULL){
-                       neworder->type = TOTAL;
-                       model_print("i=%u\t", i);
-               }
-       }
-}
-
 void orderAnalysis(CSolver *This) {
        uint size = This->allOrders.getSize();
        for (uint i = 0; i < size; i++) {
                Order *order = This->allOrders.get(i);
-               bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
-               if (!doDecompose)
-                       continue;
                
-               OrderGraph *graph = buildOrderGraph(order);
-               if (order->type == PARTIAL) {
-                       //Required to do SCC analysis for partial order graphs.  It
-                       //makes sure we don't incorrectly optimize graphs with negative
-                       //polarity edges
-                       completePartialOrderGraph(graph);
-               }
-
-
+               OrderGraph *graph;
+               if(order->graph == NULL){
+                       graph= buildOrderGraph(order);
+                       if (order->type == PARTIAL) {
+                               //Required to do SCC analysis for partial order graphs.  It
+                               //makes sure we don't incorrectly optimize graphs with negative
+                               //polarity edges
+                               completePartialOrderGraph(graph);
+                       }
+               }else
+                       graph = order->graph;
+               
                bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
 
                if (mustReachGlobal)
@@ -469,11 +407,5 @@ void orderAnalysis(CSolver *This) {
                if (mustReachPrune)
                        removeMustBeTrueNodes(This, graph);
                
-               //This is needed for splitorder
-               computeStronglyConnectedComponentGraph(graph);
-               
-               decomposeOrder(This, order, graph);
-               
-               deleteOrderGraph(graph);
        }
 }
index ee970e1..7e26d74 100644 (file)
@@ -10,6 +10,7 @@ OrderGraph *allocOrderGraph(Order *order) {
        This->nodes = new HashSetOrderNode();
        This->edges = new HashSetOrderEdge();
        This->order = order;
+       order->graph = This;
        return This;
 }
 
diff --git a/src/ASTTransform/asttransform.cc b/src/ASTTransform/asttransform.cc
new file mode 100644 (file)
index 0000000..15b351a
--- /dev/null
@@ -0,0 +1,45 @@
+#include "asttransform.h"
+#include "order.h"
+#include "tunable.h"
+#include "csolver.h"
+#include "ordergraph.h"
+#include "orderencoder.h"
+#include "orderdecompose.h"
+#include "integerencoding.h"
+
+void ASTTransform(CSolver *This){
+       uint size = This->allOrders.getSize();
+       for (uint i = 0; i < size; i++) {
+               Order *order = This->allOrders.get(i);
+               bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
+               if (!doDecompose)
+                       continue;
+               
+               OrderGraph *graph;
+               if(order->graph == NULL){
+                       graph= buildOrderGraph(order);
+                       if (order->type == PARTIAL) {
+                               //Required to do SCC analysis for partial order graphs.  It
+                               //makes sure we don't incorrectly optimize graphs with negative
+                               //polarity edges
+                               completePartialOrderGraph(graph);
+                       }
+               }else{
+                       graph = order->graph;
+               }               
+               //This is needed for splitorder
+               computeStronglyConnectedComponentGraph(graph);
+               decomposeOrder(This, order, graph);
+               
+               bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
+               if(!doIntegerEncoding)
+                       continue;
+               uint size = order->constraints.getSize();
+               for(uint i=0; i<size; i++){
+                       orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+               }
+       }
+       
+       
+}
+
diff --git a/src/ASTTransform/asttransform.h b/src/ASTTransform/asttransform.h
new file mode 100644 (file)
index 0000000..f6482ea
--- /dev/null
@@ -0,0 +1,21 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   asttransform.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:48 PM
+ */
+
+#ifndef ASTTRANSFORM_H
+#define ASTTRANSFORM_H
+#include "classlist.h"
+
+void ASTTransform(CSolver *This); 
+
+#endif /* ASTTRANSFORM_H */
+
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
new file mode 100644 (file)
index 0000000..f4b17b4
--- /dev/null
@@ -0,0 +1,41 @@
+#include "integerencoding.h"
+#include "orderelement.h"
+#include "order.h"
+#include "satencoder.h"
+#include "csolver.h"
+#include "predicate.h"
+#include "element.h"
+
+void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
+       Order* order = boolOrder->order;
+       if (order->elementTable == NULL) {
+               order->initializeOrderElementsHashTable();
+       }
+       //getting two elements and using LT predicate ...
+       Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
+       Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
+       Set * sarray[]={order->auxSet, order->auxSet};
+       Predicate *predicate =new PredicateOperator(LT, sarray, 2);
+       Element * parray[]={elem1, elem2};
+       BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
+       {//Adding new elements and boolean/predicate to solver regarding memory management
+               This->solver->allBooleans.push(boolean);
+               This->solver->allPredicates.push(predicate);
+               This->solver->allElements.push(elem1);
+               This->solver->allElements.push(elem2);
+               This->solver->constraints.add(boolean);
+       }
+}
+
+
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
+       HashSetOrderElement* eset = order->elementTable;
+       OrderElement oelement ={item, NULL};
+       if( !eset->contains(&oelement)){
+               Element* elem = new ElementSet(order->auxSet);
+               eset->add(allocOrderElement(item, elem));
+               return elem;
+       } else
+               return eset->get(&oelement)->elem;
+}
+
diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
new file mode 100644 (file)
index 0000000..9b5a808
--- /dev/null
@@ -0,0 +1,24 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   integerencoding.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:31 PM
+ */
+
+#ifndef INTEGERENCODING_H
+#define INTEGERENCODING_H
+#include "classlist.h"
+#include "structs.h"
+
+Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
+void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
+
+
+#endif /* INTEGERENCODING_H */
+
diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
new file mode 100644 (file)
index 0000000..8ad5f49
--- /dev/null
@@ -0,0 +1,74 @@
+#include "orderdecompose.h"
+#include "common.h"
+#include "order.h"
+#include "boolean.h"
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "rewriter.h"
+#include "orderedge.h"
+#include "mutableset.h"
+#include "ops.h"
+#include "csolver.h"
+
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
+       Vector<Order *> ordervec;
+       Vector<Order *> partialcandidatevec;
+       uint size = order->constraints.getSize();
+       for (uint i = 0; i < size; i++) {
+               BooleanOrder *orderconstraint = order->constraints.get(i);
+               OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
+               OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
+               if (from->sccNum != to->sccNum) {
+                       OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
+                       if (edge->polPos) {
+                               replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
+                       } else if (edge->polNeg) {
+                               replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
+                       } else {
+                               //This case should only be possible if constraint isn't in AST
+                               ASSERT(0);
+                       }
+               } else {
+                       //Build new order and change constraint's order
+                       Order *neworder = NULL;
+                       if (ordervec.getSize() > from->sccNum)
+                               neworder = ordervec.get(from->sccNum);
+                       if (neworder == NULL) {
+                               MutableSet *set = new MutableSet(order->set->type);
+                               neworder = new Order(order->type, set);
+                               This->allOrders.push(neworder);
+                               ordervec.setExpand(from->sccNum, neworder);
+                               if (order->type == PARTIAL)
+                                       partialcandidatevec.setExpand(from->sccNum, neworder);
+                               else
+                                       partialcandidatevec.setExpand(from->sccNum, NULL);
+                       }
+                       if (from->status != ADDEDTOSET) {
+                               from->status = ADDEDTOSET;
+                               ((MutableSet *)neworder->set)->addElementMSet(from->id);
+                       }
+                       if (to->status != ADDEDTOSET) {
+                               to->status = ADDEDTOSET;
+                               ((MutableSet *)neworder->set)->addElementMSet(to->id);
+                       }
+                       if (order->type == PARTIAL) {
+                               OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+                               if (edge->polNeg)
+                                       partialcandidatevec.setExpand(from->sccNum, NULL);
+                       }
+                       orderconstraint->order = neworder;
+                       neworder->addOrderConstraint(orderconstraint);
+               }
+       }
+
+       uint pcvsize=partialcandidatevec.getSize();
+       for(uint i=0;i<pcvsize;i++) {
+               Order * neworder=partialcandidatevec.get(i);
+               if (neworder != NULL){
+                       neworder->type = TOTAL;
+                       model_print("i=%u\t", i);
+               }
+       }
+}
+
diff --git a/src/ASTTransform/orderdecompose.h b/src/ASTTransform/orderdecompose.h
new file mode 100644 (file)
index 0000000..c91f8ff
--- /dev/null
@@ -0,0 +1,22 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   orderdecompose.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:33 PM
+ */
+
+#ifndef ORDERDECOMPOSE_H
+#define ORDERDECOMPOSE_H
+#include "classlist.h"
+#include "structs.h"
+
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
+
+#endif /* ORDERDECOMPOSE_H */
+
index 4b3189f..cd1cb17 100644 (file)
@@ -35,7 +35,8 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
                model_print("Encoding All ...\n\n");
                Edge c = encodeConstraintSATEncoder(This, constraint);
                model_print("Returned Constraint in EncodingAll:\n");
-               addConstraintCNF(This->cnf, c);
+               if( equalsEdge(c, E_BOGUS) )
+                       addConstraintCNF(This->cnf, c);
        }
        delete iterator;
 }
index e9c4824..2e24629 100644 (file)
 #include "orderelement.h"
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
-       if(constraint->order->order.type == INTEGERENCODING){
-               return orderIntegerEncodingSATEncoder(This, constraint);
-       }
-       switch ( constraint->order->type) {
-       case PARTIAL:
-               return encodePartialOrderSATEncoder(This, constraint);
-       case TOTAL:
-               return encodeTotalOrderSATEncoder(This, constraint);
-       default:
-               ASSERT(0);
-       }
-       return E_BOGUS;
-}
-
-Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
-       if(boolOrder->order->graph == NULL){
-               bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type,
-                       OPTIMIZEORDERSTRUCTURE, &onoff);
-               if (doOptOrderStructure ) {
-                       boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
-                       reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+       switch (constraint->order->order.type){
+               case PAIRWISE:
+                       switch ( constraint->order->type) {
+                               case PARTIAL:
+                                       return encodePartialOrderSATEncoder(This, constraint);
+                               case TOTAL:
+                                       return encodeTotalOrderSATEncoder(This, constraint);
+                               default:
+                                       ASSERT(0);
+                       }
+               case INTEGERENCODING:{
+                       //Infer the value from graph ...
+                       Order* order = constraint->order;
+                       Edge gvalue = inferOrderConstraintFromGraph(order, constraint->first, constraint->second);
+                       if(!edgeIsNull(gvalue))
+                               return gvalue;
+                       //If we couldn't infer the value from graph, we have already generated a predicate for that ...
+                       // So, we should do nothing
+                       return E_BOGUS;
                }
+               default:
+                       ASSERT(0);
        }
-       Order* order = boolOrder->order;
-       Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
-       if(!edgeIsNull(gvalue))
-               return gvalue;
-       
-       if (boolOrder->order->elementTable == NULL) {
-               boolOrder->order->initializeOrderElementsHashTable();
-       }
-       //getting two elements and using LT predicate ...
-       Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
-       ElementEncoding *encoding = getElementEncoding(elem1);
-       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
-               encoding->setElementEncodingType(BINARYINDEX);
-               encoding->encodingArrayInitialization();
-       }
-       Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
-       encoding = getElementEncoding(elem2);
-       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
-               encoding->setElementEncodingType(BINARYINDEX);
-               encoding->encodingArrayInitialization();
-       }
-       Set * sarray[]={order->set, order->set};
-       Predicate *predicate =new PredicateOperator(LT, sarray, 2);
-       Element * parray[]={elem1, elem2};
-       BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
-       boolean->getFunctionEncoding()->setFunctionEncodingType(CIRCUIT);
-       {//Adding new elements and boolean/predicate to solver regarding memory management
-               This->solver->allBooleans.push(boolean);
-               This->solver->allPredicates.push(predicate);
-               This->solver->allElements.push(elem1);
-               This->solver->allElements.push(elem2);
-       }
-       return encodeConstraintSATEncoder(This, boolean);
+       return E_BOGUS;
 }
 
 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
@@ -97,21 +65,6 @@ Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _seco
        return E_NULL;
 }
 
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
-       HashSetOrderElement* eset = order->elementTable;
-       OrderElement oelement ={item, NULL};
-       if( !eset->contains(&oelement)){
-               Element* elem = new ElementSet(order->set);
-               ElementEncoding* encoding = getElementEncoding(elem);
-               encoding->setElementEncodingType(BINARYINDEX);
-               encoding->encodingArrayInitialization();
-               encodeElementSATEncoder(This, elem);
-               eset->add(allocOrderElement(item, elem));
-               return elem;
-       } else
-               return eset->get(&oelement)->elem;
-}
-
 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
        Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
        if(!edgeIsNull(gvalue))
index 8faa73d..9b143d9 100644 (file)
@@ -2,9 +2,7 @@
 #define SATORDERENCODER_H
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder);
 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second);
-Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item);
 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
index cc9a1df..b0b987a 100644 (file)
@@ -120,12 +120,12 @@ public:
        /** @brief Adds a new key to the hashset.  Returns false if the key
         *  is already present. */
 
-  void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) {
+       void addAll(HashSet<_Key, _KeyInt, _Shift, hash_function, equals> * table) {
                HSIterator<_Key, _KeyInt, _Shift, hash_function, equals> * it=iterator();
                while(it->hasNext())
                        add(it->next());
                delete it;
-  }
+       }
 
        /** @brief Adds a new key to the hashset.  Returns false if the key
         *  is already present. */
index cbd9f29..24390ca 100644 (file)
@@ -23,6 +23,6 @@ int getVarTunable(Tuner *This, VarType vartype, TunableParam param, TunableDesc
 
 static TunableDesc onoff={0, 1, 1};
 static TunableDesc offon={0, 1, 0};
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING};
 typedef enum Tunables Tunables;
 #endif
index e2bb4bc..43c780b 100644 (file)
@@ -12,6 +12,7 @@
 #include "tunable.h"
 #include "orderencoder.h"
 #include "polarityassignment.h"
+#include "asttransform.h"
 
 CSolver::CSolver() : unsat(false) {
        tuner = allocTuner();
@@ -181,8 +182,9 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second)
 }
 
 int CSolver::startEncoding() {
-       naiveEncodingDecision(this);
        computePolarities(this);
+       ASTTransform(this);
+       naiveEncodingDecision(this);
        orderAnalysis(this);
        encodeAllSATEncoder(this, satEncoder);
        int result = solveCNF(satEncoder->cnf);