decideEdges();
}
+
+void EncodingGraph::validate() {
+ SetIteratorBooleanEdge *it = solver->getConstraints();
+ while (it->hasNext()) {
+ BooleanEdge be = it->next();
+ if (be->type == PREDICATEOP) {
+ BooleanPredicate *b = (BooleanPredicate *)be.getBoolean();
+ if (b->predicate->type == OPERATORPRED) {
+ PredicateOperator *predicate = (PredicateOperator *) b->predicate;
+ if (predicate->getOp() == SATC_EQUALS) {
+ ASSERT(b->inputs.getSize() == 2);
+ Element *e1 = b->inputs.get(0);
+ Element *e2 = b->inputs.get(1);
+ if (e1->type == ELEMCONST || e1->type == ELEMCONST)
+ continue;
+ ElementEncoding *enc1 = e1->getElementEncoding();
+ ElementEncoding *enc2 = e2->getElementEncoding();
+ ASSERT(enc1->getElementEncodingType() != ELEM_UNASSIGNED);
+ ASSERT(enc2->getElementEncodingType() != ELEM_UNASSIGNED);
+ if (enc1->getElementEncodingType() == enc2->getElementEncodingType() && enc1->getElementEncodingType() == BINARYINDEX && b->getFunctionEncoding()->type == CIRCUIT) {
+ for (uint i = 0; i < enc1->encArraySize; i++) {
+ if (enc1->isinUseElement(i)) {
+ uint64_t val1 = enc1->encodingArray[i];
+ if (enc2->isinUseElement(i)) {
+ ASSERT(val1 == enc2->encodingArray[i]);
+ } else {
+ for (uint j = 0; j < enc2->encArraySize; j++) {
+ if (enc2->isinUseElement(j)) {
+ ASSERT(val1 != enc2->encodingArray[j]);
+ }
+ }
+ }
+ }
+ }
+ }
+ //Now make sure that all the elements in the set are appeared in the encoding array!
+ for (uint k = 0; k < b->inputs.getSize(); k++) {
+ Element *e = b->inputs.get(k);
+ ElementEncoding *enc = e->getElementEncoding();
+ Set *s = e->getRange();
+ for (uint i = 0; i < s->getSize(); i++) {
+ uint64_t value = s->getElement(i);
+ bool exist = false;
+ for (uint j = 0; j < enc->encArraySize; j++) {
+ if (enc->isinUseElement(j) && enc->encodingArray[j] == value) {
+ exist = true;
+ break;
+ }
+ }
+ ASSERT(exist);
+ }
+ }
+ }
+ }
+ }
+ }
+ delete it;
+}
+
+
void EncodingGraph::encode() {
+ if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+ return;
+ buildGraph();
SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
+ model_print("#SubGraph = %u\n", subgraphs.getSize());
while (itesg->hasNext()) {
EncodingSubGraph *sg = itesg->next();
sg->encode();
uint64_t value = s->getElement(i);
uint encodingIndex = subgraph->getEncoding(n, value);
encoding->setInUseElement(encodingIndex);
+ ASSERT(encoding->isinUseElement(encodingIndex));
encoding->encodingArray[encodingIndex] = value;
}
}
if (left == NULL || right == NULL)
return;
EncodingEdge *edge = getEdge(left, right, NULL);
- if (edge != NULL && edge->getEncoding() == EDGE_MATCH) {
- fenc->setFunctionEncodingType(CIRCUIT);
+ if (edge != NULL) {
+ EncodingSubGraph *leftGraph = graphMap.get(left);
+ if (leftGraph != NULL && leftGraph == graphMap.get(right)) {
+ fenc->setFunctionEncodingType(CIRCUIT);
+ }
}
}
}
first = tmp;
}
if (graph1 != NULL && graph2 != NULL) {
+ if (graph1 == graph2)
+ return;
+
SetIteratorEncodingNode *nodeit = graph2->nodeIterator();
while (nodeit->hasNext()) {
EncodingNode *node = nodeit->next();
}
uint convertSize(uint cost) {
- cost = 1.2 * cost;// fudge factor
+ cost = FUDGEFACTOR * cost;// fudge factor
return NEXTPOW2(cost);
}
EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
}
- uint leftSize = 0, rightSize = 0, newSize = 0;
- uint64_t totalCost = 0;
+ uint leftSize = 0, rightSize = 0, newSize = 0, max = 0;
+ bool merge = false;
if (leftGraph == NULL && rightGraph == NULL) {
leftSize = convertSize(left->getSize());
rightSize = convertSize(right->getSize());
newSize = convertSize(left->s->getUnionSize(right->s));
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
- totalCost = (newSize - leftSize) * left->elements.getSize() +
- (newSize - rightSize) * right->elements.getSize();
} else if (leftGraph != NULL && rightGraph == NULL) {
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(right->getSize());
newSize = convertSize(leftGraph->estimateNewSize(right));
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
- totalCost = (newSize - leftSize) * leftGraph->numElements +
- (newSize - rightSize) * right->elements.getSize();
+ max = rightSize > leftSize ? rightSize : leftSize;
+// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
+ merge = left->measureSimilarity(right) > 1.5 || max == newSize;
} else {
//Neither are null
-
- //Are we already merged?
- if (leftGraph == rightGraph)
- continue;
-
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(rightGraph->encodingSize);
newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
+// model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
newSize = (leftSize > newSize) ? leftSize : newSize;
newSize = (rightSize > newSize) ? rightSize : newSize;
- totalCost = (newSize - leftSize) * leftGraph->numElements +
- (newSize - rightSize) * rightGraph->numElements;
+ max = rightSize > leftSize ? rightSize : leftSize;
+// model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
+ merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
}
- double conversionfactor = 0.5;
- if ((totalCost * conversionfactor) < eeValue) {
+ if (merge) {
//add the edge
mergeNodes(left, right);
}
return s->getSize();
}
+uint64_t EncodingNode::getIndex(uint index) {
+ return s->getElement(index);
+}
+
VarType EncodingNode::getType() const {
return s->getType();
}
-static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+bool EncodingNode::itemExists(uint64_t item) {
+ for (uint i = 0; i < s->getSize(); i++) {
+ if (item == s->getElement(i))
+ return true;
+ }
+ return false;
+}
+
+double EncodingNode::measureSimilarity(EncodingNode *node) {
+ uint common = 0;
+ for (uint i = 0; i < s->getSize(); i++) {
+ uint64_t item = s->getElement(i);
+ if (node->itemExists(item)) {
+ common++;
+ }
+ }
+// model_print("common=%u\tsize1=%u\tsize2=%u\tsim1=%f\tsim2=%f\n", common, s->getSize(), node->getSize(), 1.0*common/s->getSize(), 1.0*common/node->getSize());
+ return common * 1.0 / s->getSize() + common * 1.0 / node->getSize();
+}
EncodingNode *EncodingGraph::createNode(Element *e) {
if (e->type == ELEMCONST)
projects / satune.git / blobdiff