Add support for some other operators

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 1f94cb1a037c86cddb33d903a5d422efaf5b26fa..dc0c80a5d6debdce01298d1326530ada2aca6c3e 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -6,7 +6,7 @@ typedef enum LogicOp LogicOp;
 enum ArithOp {ADD, SUB};
 typedef enum ArithOp ArithOp;
 
-enum CompOp {EQUALS};
+enum CompOp {EQUALS, LT, GT, LTE, GTE};
 typedef enum CompOp CompOp;
 
 enum OrderType {PARTIAL, TOTAL};

diff --git a/src/AST/predicate.c b/src/AST/predicate.c
index 19e159760ddc897931494f1782826c64319489c3..8f7b5ee97130eed6ca32b080967d8447968f9593 100644 (file)
--- a/src/AST/predicate.c
+++ b/src/AST/predicate.c
@@ -18,29 +18,6 @@ Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){
        return &This->base;
 }
 
-// BRIAN: REVISIT
-void getEqualitySetIntersection(PredicateOperator* This, uint* size, uint64_t* result){
-       ASSERT( This->op == EQUALS);
-       //make sure equality has 2 operands
-       ASSERT(getSizeArraySet( &This->domains) == 2);
-       *size=0;
-       VectorInt* mems1 = getArraySet(&This->domains, 0)->members; 
-       uint size1 = getSizeVectorInt(mems1);
-       VectorInt* mems2 = getArraySet(&This->domains, 1)->members;
-       uint size2 = getSizeVectorInt(mems2);
-       //FIXME:This isn't efficient, if we a hashset datastructure for Set, we
-       // can reduce it to O(n), but for now .... HG
-       for(uint i=0; i<size1; i++){
-               uint64_t tmp= getVectorInt(mems1, i);
-               for(uint j=0; j<size2; j++){
-                       if(tmp == getVectorInt(mems2, j)){
-                               result[(*size)++]=tmp;
-                               break;
-                       }
-               }
-       }
-}
-
 void deletePredicate(Predicate* This){
        switch(GETPREDICATETYPE(This)) {
        case OPERATORPRED: {
@@ -56,3 +33,19 @@ void deletePredicate(Predicate* This){
        ourfree(This);
 }
 
+bool evalPredicateOperator(PredicateOperator * This, uint64_t * inputs) {
+       switch(This->op) {
+       case EQUALS:
+               return inputs[0]==inputs[1];
+       case LT:
+               return inputs[0]<inputs[1];
+       case GT:
+               return inputs[0]>inputs[1];
+       case LTE:
+               return inputs[0]<=inputs[1];
+       case GTE:
+               return inputs[0]>=inputs[1];
+       }
+       ASSERT(0);
+       return false;
+}

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 6aaacce08de5c292ac5c363dd91b46ec40fa57e3..105e91bd315be90f56bf366ac8042b493377ffea 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -25,7 +25,6 @@ struct PredicateTable {
 
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain);
 Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior);
-// size and result will be modified by this function!
-void getEqualitySetIntersection(PredicateOperator* This, uint* size, uint64_t* result);
+bool evalPredicateOperator(PredicateOperator * This, uint64_t * inputs);
 void deletePredicate(Predicate* This);
 #endif

diff --git a/src/AST/set.c b/src/AST/set.c
index 05aaf910e3cca2343b66895689da59db1432138c..2569ed28b6c140e9868f4df5f2e7087370f2c72b 100644 (file)
--- a/src/AST/set.c
+++ b/src/AST/set.c
@@ -24,7 +24,7 @@ Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) {
 bool existsInSet(Set* This, uint64_t element){
        if(This->isRange){
                return element >= This->low && element <= This->high;
-       }else {
+       } else {
                uint size = getSizeVectorInt(This->members);
                for(uint i=0; i< size; i++){
                        if(element == getVectorInt(This->members, i))
@@ -34,9 +34,16 @@ bool existsInSet(Set* This, uint64_t element){
        }
 }
 
+uint64_t getSetElement(Set * This, uint index) {
+       if (This->isRange)
+               return This->low+index;
+       else
+               return getVectorInt(This->members, index);
+}
+
 uint getSetSize(Set* This){
        if(This->isRange){
-               return This->high- This->low+1;
+               return This->high - This->low+1;
        }else{
                return getSizeVectorInt(This->members);
        }

diff --git a/src/AST/set.h b/src/AST/set.h
index 5139927e690e759592ab18ab5d326f090e0fffca..1555ae9650dc1169795fbd61174c5635461851d3 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -24,6 +24,7 @@ Set * allocSet(VarType t, uint64_t * elements, uint num);
 Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange);
 bool existsInSet(Set * This, uint64_t element);
 uint getSetSize(Set * This);
+uint64_t getSetElement(Set * This, uint index);
 void deleteSet(Set * This);
 #endif/* SET_H */
 

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index d51e2519934f847901c9f41e75c1094d587fa577..cfeb82ae4166069c97ece3989a76d7625da496aa 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -317,7 +317,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
        return generateNegation ? result: constraintNegate(result);
 }
 
-Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
        switch(constraint->encoding.type){
                case ENUMERATEIMPLICATIONS:
                        return encodeEnumOperatorPredicateSATEncoder(This, constraint);
@@ -331,26 +331,60 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 }
 
 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-       ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
        PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
-       ASSERT(predicate->op == EQUALS); //For now, we just only support equals
-       //getting maximum size of in common elements between two sets!
-       uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
-       uint64_t commonElements [size];
-       getEqualitySetIntersection(predicate, &size, commonElements);
-       Edge  carray[size];
-       Element* elem1 = getArrayElement( &constraint->inputs, 0);
-       Element* elem2 = getArrayElement( &constraint->inputs, 1);
-       encodeElementSATEncoder(This,elem1);
-       encodeElementSATEncoder(This, elem2);
+       uint numDomains=getSizeArraySet(&predicate->domains);
+
+       FunctionEncodingType encType = constraint->encoding.type;
+       bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+
+       /* Call base encoders for children */
+       for(uint i=0;i<numDomains;i++) {
+               Element *elem = getArrayElement( &constraint->inputs, i);
+               encodeElementSATEncoder(This, elem);
+       }
+       VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
        
-       for(uint i=0; i<size; i++){
-               Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
-               Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
-               carray[i] =  constraintAND2(This->cnf, arg1, arg2);
+       uint indices[numDomains]; //setup indices
+       bzero(indices, sizeof(uint)*numDomains);
+       
+       uint64_t vals[numDomains]; //setup value array
+       for(uint i=0;i<numDomains; i++) {
+               Set * set=getArraySet(&predicate->domains, i);
+               vals[i]=getSetElement(set, indices[i]);
+       }
+       
+       bool notfinished=true;
+       while(notfinished) {
+               Edge carray[numDomains];
+
+               if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
+                       //Include this in the set of terms
+                       for(uint i=0;i<numDomains;i++) {
+                               Element * elem = getArrayElement(&constraint->inputs, i);
+                               carray[i] = getElementValueConstraint(This, elem, vals[i]);
+                       }
+                       pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray));
+               }
+               
+               notfinished=false;
+               for(uint i=0;i<numDomains; i++) {
+                       uint index=++indices[i];
+                       Set * set=getArraySet(&predicate->domains, i);
+
+                       if (index < getSetSize(set)) {
+                               vals[i]=getSetElement(set, index);
+                               notfinished=true;
+                               break;
+                       } else {
+                               indices[i]=0;
+                               vals[i]=getSetElement(set, 0);
+                       }
+               }
        }
-       //FIXME: the case when there is no intersection ....
-       return constraintOR(This->cnf, size, carray);
+
+       Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+       deleteVectorEdge(clauses);
+       return generateNegation ? cor : constraintNegate(cor);
 }
 
 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){