+
+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;
+}
+
+