void EncodingGraph::validate() {
- SetIteratorBooleanEdge* it= solver->getConstraints();
- while(it->hasNext()){
+ SetIteratorBooleanEdge *it = solver->getConstraints();
+ while (it->hasNext()) {
BooleanEdge be = it->next();
- if(be->type == PREDICATEOP){
+ if (be->type == PREDICATEOP) {
BooleanPredicate *b = (BooleanPredicate *)be.getBoolean();
- if(b->predicate->type == OPERATORPRED){
- PredicateOperator* predicate = (PredicateOperator*) b->predicate;
- if(predicate->getOp() == SATC_EQUALS){
+ 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)
+ 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)){
+ 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)){
+ if (enc2->isinUseElement(i)) {
ASSERT(val1 == enc2->encodingArray[i]);
- }else{
- for(uint j=0; j< enc2->encArraySize; j++){
- if(enc2->isinUseElement(j)){
+ } 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++){
+ 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){
+ bool exist = false;
+ for (uint j = 0; j < enc->encArraySize; j++) {
+ if (enc->isinUseElement(j) && enc->encodingArray[j] == value) {
exist = true;
break;
}
void EncodingGraph::encode() {
+ if (solver->isUnSAT() || 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();
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->setEncoding(BINARYINDEX);
if (graph2 == NULL)
second->setEncoding(BINARYINDEX);
-
+
if (graph1 == NULL && graph2 == NULL) {
graph1 = new EncodingSubGraph();
subgraphs.add(graph1);
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 = 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, min = 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();
+ min = rightSize > leftSize ? leftSize : rightSize;
+ merge = left->measureSimilarity(right) > 1.5 || min == newSize;
} else if (leftGraph != NULL && rightGraph == NULL) {
- leftSize = convertSize(leftGraph->encodingSize);
+ leftSize = convertSize(leftGraph->numValues());
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();
+ min = rightSize > leftSize ? leftSize : rightSize;
+ merge = leftGraph->measureSimilarity(right) > 1.5 || min == newSize;
+// model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
} else {
//Neither are null
-
- //Are we already merged?
- if (leftGraph == rightGraph)
- continue;
-
- leftSize = convertSize(leftGraph->encodingSize);
- rightSize = convertSize(rightGraph->encodingSize);
+ leftSize = convertSize(leftGraph->numValues());
+ rightSize = convertSize(rightGraph->numValues());
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;
+ min = rightSize > leftSize ? leftSize : rightSize;
+ merge = leftGraph->measureSimilarity(rightGraph) > 1.5 || min == newSize;
+// model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
}
-
- 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);
+double EncodingNode::measureSimilarity(EncodingNode *node) {
+ uint common = 0;
+ for (uint i = 0, j = 0; i < s->getSize() && j < node->s->getSize(); ) {
+ uint64_t item = s->getElement(i);
+ uint64_t item2 = node->s->getElement(j);
+ if (item < item2)
+ i++;
+ else if (item2 > item)
+ j++;
+ else {
+ i++;
+ j++;
+ common++;
+ }
+ }
+
+ return common * 1.0 / s->getSize() + common * 1.0 / node->getSize();
+}
EncodingNode *EncodingGraph::createNode(Element *e) {
if (e->type == ELEMCONST)
projects / satune.git / blobdiff