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() {
SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
+ model_print("#SubGraph = %u", subgraphs.getSize());
while (itesg->hasNext()) {
EncodingSubGraph *sg = itesg->next();
sg->encode();
encoding->encodingArrayInitialization();
} else if (encodetype == BINARYINDEX) {
EncodingSubGraph *subgraph = graphMap.get(n);
- if (subgraph == NULL)
+ DEBUG("graphMap.get(subgraph=%p, n=%p)\n", subgraph, n);
+ if (subgraph == NULL) {
+ encoding->encodingArrayInitialization();
continue;
- uint encodingSize = subgraph->getEncodingMaxVal(n)+1;
+ }
+ uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
- model_print("encoding size=%u\n", encodingSize);
- model_print("padded=%u\n", paddedSize);
encoding->allocInUseArrayElement(paddedSize);
encoding->allocEncodingArrayElement(paddedSize);
Set *s = e->getRange();
for (uint i = 0; i < s->getSize(); i++) {
- model_print("index=%u\n", i);
uint64_t value = s->getElement(i);
uint encodingIndex = subgraph->getEncoding(n, value);
encoding->setInUseElement(encodingIndex);
+ ASSERT(encoding->isinUseElement(encodingIndex));
encoding->encodingArray[encodingIndex] = value;
}
+ } else{
+ model_print("DAMN in encode()\n");
+ e->print();
}
}
break;
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);
+ }
}
}
}
void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
EncodingSubGraph *graph1 = graphMap.get(first);
+ DEBUG("graphMap.get(first=%p, graph1=%p)\n", first, graph1);
EncodingSubGraph *graph2 = graphMap.get(second);
+ DEBUG("graphMap.get(second=%p, graph2=%p)\n", second, graph2);
if (graph1 == NULL)
first->setEncoding(BINARYINDEX);
if (graph2 == NULL)
second->setEncoding(BINARYINDEX);
-
+
if (graph1 == NULL && graph2 == NULL) {
graph1 = new EncodingSubGraph();
subgraphs.add(graph1);
+ DEBUG("graphMap.put(first=%p, graph1=%p)\n", first, graph1);
graphMap.put(first, graph1);
graph1->addNode(first);
}
first = tmp;
}
if (graph1 != NULL && graph2 != NULL) {
+ if (graph1 == graph2)
+ return;
+
SetIteratorEncodingNode *nodeit = graph2->nodeIterator();
while (nodeit->hasNext()) {
EncodingNode *node = nodeit->next();
graph1->addNode(node);
+ DEBUG("graphMap.put(node=%p, graph1=%p)\n", node, graph1);
graphMap.put(node, graph1);
}
subgraphs.remove(graph2);
delete nodeit;
+ DEBUG("Deleting graph2 =%p \n", graph2);
delete graph2;
} else {
ASSERT(graph1 != NULL && graph2 == NULL);
graph1->addNode(second);
+ DEBUG("graphMap.put(first=%p, graph1=%p)\n", first, graph1);
graphMap.put(second, graph1);
}
}
}
uint convertSize(uint cost) {
- cost = 1.2 * cost;// fudge factor
+ cost = FUDGEFACTOR * cost;// fudge factor
return NEXTPOW2(cost);
}
return;
EncodingSubGraph *leftGraph = graphMap.get(left);
+ DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
EncodingSubGraph *rightGraph = graphMap.get(right);
+ DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
if (leftGraph == NULL && rightGraph != NULL) {
EncodingNode *tmp = left; left = right; right = tmp;
EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
}
-
- uint leftSize = 0, rightSize = 0, newSize = 0;
+ //model_print("Right=%p RGraph=%p\tLeft=%p LGraph=%p\n", right, rightGraph, left, leftGraph);
+ uint leftSize = 0, rightSize = 0, newSize = 0, max=0;
uint64_t totalCost = 0;
+ bool merge = false;
+// model_print("**************decideEdge*************\n");
+// model_print("LeftNode Size = %u\n", left->getSize());
+// model_print("rightNode Size = %u\n", right->getSize());
+// model_print("UnionSize = %u\n", left->s->getUnionSize(right->s));
+
if (leftGraph == NULL && rightGraph == NULL) {
leftSize = convertSize(left->getSize());
rightSize = convertSize(right->getSize());
newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * left->elements.getSize() +
(newSize - rightSize) * right->elements.getSize();
+ //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
+ max = rightSize > leftSize? rightSize : leftSize;
+ if(newSize == max){
+ merge = true;
+ }
} else if (leftGraph != NULL && rightGraph == NULL) {
leftSize = convertSize(leftGraph->encodingSize);
rightSize = convertSize(right->getSize());
newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * leftGraph->numElements +
(newSize - rightSize) * right->elements.getSize();
+ //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
+ max = rightSize > leftSize? rightSize : leftSize;
+ if(newSize == max){
+ merge = true;
+ }
} else {
//Neither are null
leftSize = convertSize(leftGraph->encodingSize);
newSize = (rightSize > newSize) ? rightSize : newSize;
totalCost = (newSize - leftSize) * leftGraph->numElements +
(newSize - rightSize) * rightGraph->numElements;
+// model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
+// model_print("RightGraph size=%u\n", rightGraph->encodingSize);
+// model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
+ if(rightSize < 64 && leftSize < 64){
+ merge = true;
+ }
}
- double conversionfactor = 0.5;
- if ((totalCost * conversionfactor) < eeValue) {
+// model_print("******************************\n");
+ if (merge) {
//add the edge
mergeNodes(left, right);
}
projects / satune.git / blobdiff