From: Hamed Date: Fri, 25 Aug 2017 04:28:59 +0000 (-0700) Subject: Adding ASTTransform ... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=40bb2cf09b939039af96b9d1ee9196a51046b535 Adding ASTTransform ... --- diff --git a/src/AST/order.cc b/src/AST/order.cc index 5e16938..e597e72 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -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() { diff --git a/src/AST/order.h b/src/AST/order.h index 1645786..acd6426 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -14,6 +14,7 @@ class Order { ~Order(); OrderType type; Set *set; + Set* auxSet; HashTableOrderPair *orderPairTable; HashSetOrderElement* elementTable; OrderGraph *graph; diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc index 35ea575..06668fd 100644 --- a/src/ASTAnalyses/orderencoder.cc +++ b/src/ASTAnalyses/orderencoder.cc @@ -369,85 +369,23 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { delete iterator; } -void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { - Vector ordervec; - Vector 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;itype = 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); } } diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index ee970e1..7e26d74 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -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 index 0000000..15b351a --- /dev/null +++ b/src/ASTTransform/asttransform.cc @@ -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; isatEncoder, order->constraints.get(i)); + } + } + + +} + diff --git a/src/ASTTransform/asttransform.h b/src/ASTTransform/asttransform.h new file mode 100644 index 0000000..f6482ea --- /dev/null +++ b/src/ASTTransform/asttransform.h @@ -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 index 0000000..f4b17b4 --- /dev/null +++ b/src/ASTTransform/integerencoding.cc @@ -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 index 0000000..9b5a808 --- /dev/null +++ b/src/ASTTransform/integerencoding.h @@ -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 index 0000000..8ad5f49 --- /dev/null +++ b/src/ASTTransform/orderdecompose.cc @@ -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 ordervec; + Vector 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;itype = TOTAL; + model_print("i=%u\t", i); + } + } +} + diff --git a/src/ASTTransform/orderdecompose.h b/src/ASTTransform/orderdecompose.h new file mode 100644 index 0000000..c91f8ff --- /dev/null +++ b/src/ASTTransform/orderdecompose.h @@ -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 */ + diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 4b3189f..cd1cb17 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -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; } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index e9c4824..2e24629 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -14,62 +14,30 @@ #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)) diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h index 8faa73d..9b143d9 100644 --- a/src/Backend/satorderencoder.h +++ b/src/Backend/satorderencoder.h @@ -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); diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index cc9a1df..b0b987a 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -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. */ diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h index cbd9f29..24390ca 100644 --- a/src/Tuner/tunable.h +++ b/src/Tuner/tunable.h @@ -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 diff --git a/src/csolver.cc b/src/csolver.cc index e2bb4bc..43c780b 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -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);