OrderType type;
Set *set;
OrderGraph *graph;
+ OrderEncoding encoding;
Order *clone(CSolver *solver, CloneMap *map);
void serialize(Serializer *serializer );
void print();
- Vector<BooleanOrder *> 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<BooleanOrder *> constraints;
+public:
+ Vector<BooleanOrder *> *getConstraints() {return &constraints;}
+ uint getNumUsed() {return constraints.getSize();}
+ SetIterator64Int *getUsedIterator() {return useditems.iterator();}
+
};
#endif
OrderGraph *buildOrderGraph(Order *order) {
ASSERT(order->graph == NULL);
OrderGraph *orderGraph = new OrderGraph(order);
- uint constrSize = order->constraints.getSize();
+ Vector<BooleanOrder *> *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;
}
OrderGraph *buildMustOrderGraph(Order *order) {
ASSERT(order->graph == NULL);
OrderGraph *orderGraph = new OrderGraph(order);
- uint constrSize = order->constraints.getSize();
+ Vector<BooleanOrder *> *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;
}
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<BooleanOrder *> *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);
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);
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);
}
}
+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));
+ }
+ }
+ }
+}