+ Predicate *p=b->getPredicate();
+ if (p->type==OPERATORPRED) {
+ PredicateOperator *po=(PredicateOperator *)p;
+ ASSERT(b->inputs.getSize()==2);
+ EncodingNode *left=createNode(b->inputs.get(0));
+ EncodingNode *right=createNode(b->inputs.get(1));
+ if (left == NULL || right == NULL)
+ return;
+ EncodingEdge *edge=getEdge(left, right, NULL);
+ CompOp op=po->getOp();
+ switch(op) {
+ case SATC_EQUALS:
+ edge->numEquals++;
+ break;
+ case SATC_LT:
+ case SATC_LTE:
+ case SATC_GT:
+ case SATC_GTE:
+ edge->numComparisons++;
+ break;
+ default:
+ ASSERT(0);
+ }
+ }
+}
+
+static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
+
+EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+ EncodingEdge e(left, right, dst);
+ EncodingEdge *result = edgeMap.get(&e);
+ if (result == NULL) {
+ result=new EncodingEdge(left, right, dst);
+ VarType v1=left->getType();
+ VarType v2=right->getType();
+ if (v1 > v2) {
+ VarType tmp=v2;
+ v2=v1;
+ v1=tmp;
+ }
+ result->setEncoding((EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc));
+ edgeMap.put(result, result);
+ }
+ return result;
+}
+
+EncodingNode::EncodingNode(Set *_s) :
+ s(_s),
+ numElements(0) {
+}
+
+uint EncodingNode::getSize() {
+ return s->getSize();
+}