From: Hamed Gorjiara Date: Thu, 21 Mar 2019 23:01:31 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=b0e243e3701d8b5bdad82b60138fa3b54466c705;hp=e5c1ee81132998d6a80d83e95f1faf2ca06ac7fb Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into sparseOrderOpt --- diff --git a/src/AST/order.cc b/src/AST/order.cc index 315b112..82e4c53 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -16,6 +16,8 @@ Order::Order(OrderType _type, Set *_set) : void Order::addOrderConstraint(BooleanOrder *constraint) { constraints.push(constraint); + useditems.add(constraint->first); + useditems.add(constraint->second); } void Order::setOrderEncodingType(OrderEncodingType type) { diff --git a/src/AST/order.h b/src/AST/order.h index cbbe846..4badbdc 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -15,18 +15,24 @@ public: OrderType type; Set *set; OrderGraph *graph; + OrderEncoding encoding; Order *clone(CSolver *solver, CloneMap *map); void serialize(Serializer *serializer ); void print(); - Vector constraints; - OrderEncoding encoding; - - void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;}; + void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;} void initializeOrderElementsHashtable(); void addOrderConstraint(BooleanOrder *constraint); void setOrderEncodingType(OrderEncodingType type); HashtableOrderPair *getOrderPairTable(); CMEMALLOC; +private: + Hashset64Int useditems; + Vector constraints; +public: + Vector *getConstraints() {return &constraints;} + uint getNumUsed() {return constraints.getSize();} + SetIterator64Int *getUsedIterator() {return useditems.iterator();} + }; #endif diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc index cbc2e25..57d0db8 100644 --- a/src/ASTAnalyses/Order/ordergraph.cc +++ b/src/ASTAnalyses/Order/ordergraph.cc @@ -12,9 +12,10 @@ OrderGraph::OrderGraph(Order *_order) : OrderGraph *buildOrderGraph(Order *order) { ASSERT(order->graph == NULL); OrderGraph *orderGraph = new OrderGraph(order); - uint constrSize = order->constraints.getSize(); + Vector *constraints = order->getConstraints(); + uint constrSize = constraints->getSize(); for (uint j = 0; j < constrSize; j++) { - orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j)); + orderGraph->addOrderConstraintToOrderGraph(constraints->get(j)); } return orderGraph; } @@ -23,9 +24,10 @@ OrderGraph *buildOrderGraph(Order *order) { OrderGraph *buildMustOrderGraph(Order *order) { ASSERT(order->graph == NULL); OrderGraph *orderGraph = new OrderGraph(order); - uint constrSize = order->constraints.getSize(); + Vector *constraints = order->getConstraints(); + uint constrSize = constraints->getSize(); for (uint j = 0; j < constrSize; j++) { - orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j)); + orderGraph->addMustOrderConstraintToOrderGraph(constraints->get(j)); } return orderGraph; } diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index e63cb74..2a4f4af 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -88,9 +88,10 @@ void DecomposeOrderTransform::doTransform() { void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) { Vector partialcandidatevec; - uint size = currOrder->constraints.getSize(); + Vector *constraints = currOrder->getConstraints(); + uint size = constraints->getSize(); for (uint i = 0; i < size; i++) { - BooleanOrder *orderconstraint = currOrder->constraints.get(i); + BooleanOrder *orderconstraint = constraints->get(i); OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first); OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second); OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to); diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index d5d769d..34bcd74 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -33,11 +33,13 @@ void IntegerEncodingTransform::doTransform() { void IntegerEncodingTransform::integerEncode(Order *currOrder) { IntegerEncodingRecord *encodingRecord = new IntegerEncodingRecord( - solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1)); + solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->getNumUsed() - 1)); currOrder->setOrderEncodingType( INTEGERENCODING ); - uint size = currOrder->constraints.getSize(); + + Vector *constraints = currOrder->getConstraints(); + uint size = constraints->getSize(); for (uint i = 0; i < size; i++) { - orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord); + orderIntegerEncodingSATEncoder(constraints->get(i), encodingRecord); } currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord)); solver->getActiveOrders()->remove(currOrder); diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 63b5a61..84329ef 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -55,6 +55,8 @@ private: Edge encodePartialOrderSATEncoder(BooleanOrder *constraint); void createAllTotalOrderConstraintsSATEncoder(Order *order); void createAllPartialOrderConstraintsSATEncoder(Order *order); + void createAllTotalOrderConstraintsSATEncoderSparse(Order *order); + void createAllPartialOrderConstraintsSATEncoderSparse(Order *order); Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair); Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK); Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki); diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 9982039..e3d2f33 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -108,7 +108,10 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) { boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); reachMustAnalysis(solver, boolOrder->order->graph, true); } - createAllTotalOrderConstraintsSATEncoder(boolOrder->order); + if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) + createAllTotalOrderConstraintsSATEncoderSparse(boolOrder->order); + else + createAllTotalOrderConstraintsSATEncoder(boolOrder->order); } OrderPair pair(boolOrder->first, boolOrder->second, E_NULL); Edge constraint = getPairConstraint(boolOrder->order, &pair); @@ -214,7 +217,10 @@ Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) { boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); reachMustAnalysis(solver, boolOrder->order->graph, true); } - createAllPartialOrderConstraintsSATEncoder(boolOrder->order); + if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) + createAllPartialOrderConstraintsSATEncoderSparse(boolOrder->order); + else + createAllPartialOrderConstraintsSATEncoder(boolOrder->order); } OrderPair pair(boolOrder->first, boolOrder->second, E_NULL); Edge constraint = getPartialPairConstraint(boolOrder->order, &pair); @@ -254,4 +260,63 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) { } } +void SATEncoder::createAllTotalOrderConstraintsSATEncoderSparse(Order *order) { +#ifdef CONFIG_DEBUG + model_print("in total order ...\n"); +#endif + ASSERT(order->type == SATC_TOTAL); + SetIterator64Int *iti = order->getUsedIterator(); + while (iti->hasNext()) { + uint64_t valueI = iti->next(); + SetIterator64Int *itj = new SetIterator64Int(iti); + while (itj->hasNext()) { + uint64_t valueJ = itj->next(); + OrderPair pairIJ(valueI, valueJ, E_NULL); + Edge constIJ = getPairConstraint(order, &pairIJ); + SetIterator64Int *itk = new SetIterator64Int(itj); + while (itk->hasNext()) { + uint64_t valueK = itk->next(); + OrderPair pairJK(valueJ, valueK, E_NULL); + OrderPair pairIK(valueI, valueK, E_NULL); + Edge constIK = getPairConstraint(order, &pairIK); + Edge constJK = getPairConstraint(order, &pairJK); + addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK)); + } + } + } +} +void SATEncoder::createAllPartialOrderConstraintsSATEncoderSparse(Order *order) { +#ifdef CONFIG_DEBUG + model_print("in partial order ...\n"); +#endif + ASSERT(order->type == SATC_TOTAL); + SetIterator64Int *iti = order->getUsedIterator(); + while (iti->hasNext()) { + uint64_t valueI = iti->next(); + SetIterator64Int *itj = new SetIterator64Int(iti); + while (itj->hasNext()) { + uint64_t valueJ = itj->next(); + OrderPair pairIJ(valueI, valueJ, E_NULL); + OrderPair pairJI(valueJ, valueI, E_NULL); + Edge constIJ = getPartialPairConstraint(order, &pairIJ); + Edge constJI = getPartialPairConstraint(order, &pairJI); + SetIterator64Int *itk = new SetIterator64Int(itj); + while (itk->hasNext()) { + uint64_t valueK = itk->next(); + OrderPair pairJK(valueJ, valueK, E_NULL); + OrderPair pairIK(valueI, valueK, E_NULL); + Edge constIK = getPartialPairConstraint(order, &pairIK); + Edge constJK = getPartialPairConstraint(order, &pairJK); + OrderPair pairKJ(valueK, valueJ, E_NULL); + OrderPair pairKI(valueK, valueI, E_NULL); + Edge constKI = getPartialPairConstraint(order, &pairKI); + Edge constKJ = getPartialPairConstraint(order, &pairKJ); + addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI, + + + constJK, constKJ, constIK, constKI)); + } + } + } +} diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index 86cbce9..05bb7af 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -30,6 +30,11 @@ public: { } + SetIterator(SetIterator *s) : curr(s->curr), + last(s->last), + set(s->set) { + } + /** Override: new operator */ void *operator new(size_t size) { return ourmalloc(size);