+ bsdqsort(edgeVector.expose(), edgeVector.getSize(), sizeof(EncodingEdge *), sortEncodingEdge);
+ 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();
+ }
+ delete itesg;
+
+ ElementIterator it(solver);
+ while (it.hasNext()) {
+ Element *e = it.next();
+ switch (e->type) {
+ case ELEMSET:
+ case ELEMFUNCRETURN: {
+ ElementEncoding *encoding = e->getElementEncoding();
+ if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+ EncodingNode *n = getNode(e);
+ if (n == NULL)
+ continue;
+ ElementEncodingType encodetype = n->getEncoding();
+ encoding->setElementEncodingType(encodetype);
+ if (encodetype == UNARY || encodetype == ONEHOT) {
+ encoding->encodingArrayInitialization();
+ } else if (encodetype == BINARYINDEX) {
+ EncodingSubGraph *subgraph = graphMap.get(n);
+ DEBUG("graphMap.get(subgraph=%p, n=%p)\n", subgraph, n);
+ if (subgraph == NULL) {
+ encoding->encodingArrayInitialization();
+ continue;
+ }
+ uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
+ uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
+ encoding->allocInUseArrayElement(paddedSize);
+ encoding->allocEncodingArrayElement(paddedSize);
+ Set *s = e->getRange();
+ for (uint i = 0; i < s->getSize(); 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;
+ }
+ default:
+ break;
+ }
+ encodeParent(e);
+ }
+}
+
+void EncodingGraph::encodeParent(Element *e) {
+ uint size = e->parents.getSize();
+ for (uint i = 0; i < size; i++) {
+ ASTNode *n = e->parents.get(i);
+ if (n->type == PREDICATEOP) {
+ BooleanPredicate *b = (BooleanPredicate *)n;
+ FunctionEncoding *fenc = b->getFunctionEncoding();
+ if (fenc->getFunctionEncodingType() != FUNC_UNASSIGNED)
+ continue;
+ 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);
+ if (edge != NULL) {
+ EncodingSubGraph *leftGraph = graphMap.get(left);
+ if (leftGraph != NULL && leftGraph == graphMap.get(right)) {
+ fenc->setFunctionEncodingType(CIRCUIT);
+ }
+ }
+ }
+ }
+ }