Adding predicateOperator (equality operation ...)

diff --git a/src/AST/predicate.c b/src/AST/predicate.c
index ebb3c14f1c8650f411c259e2699ad11ce1f2fc09..116f152673cd3a2d23239a09d46c497b512a9c91 100644 (file)
--- a/src/AST/predicate.c
+++ b/src/AST/predicate.c
@@ -1,4 +1,6 @@
 #include "predicate.h"
+#include "boolean.h"
+#include "set.h"
 
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){
        PredicateOperator* predicate = ourmalloc(sizeof(PredicateOperator));
@@ -16,6 +18,29 @@ Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){
        return &predicate->base;
 }
 
+void getEqualitySetIntersection(PredicateOperator* predicate, uint* size, uint64_t* result){
+       ASSERT( predicate->op == EQUALS);
+       //make sure equality has 2 operands
+       ASSERT(getSizeArraySet( &predicate->domains) == 2);
+       *size=0;
+       VectorInt* mems1 = getArraySet(&predicate->domains, 0)->members; 
+       uint size1 = getSizeVectorInt(mems1);
+       VectorInt* mems2 = getArraySet(&predicate->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* predicate){
        switch(GETPREDICATETYPE(predicate)) {
        case OPERATORPRED: {

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 13e5295bc69c2a10e0e90d8d5ab94ed45cb45de9..22f33d0e2e4bacaac23a6f22ac608e475d36c72c 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -26,5 +26,7 @@ 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* predicate, uint* size, uint64_t* result);
 void deletePredicate(Predicate* predicate);
 #endif

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index fa124a68f741e7044cd10c2b3cbe0ec0bdbdc494..dc557b5ee40b7147744e22cc84dc54cebb10c144 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -282,7 +282,7 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const
 }
 
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
-       switch(GETPREDICATETYPE(constraint) ){
+       switch(GETPREDICATETYPE(constraint->predicate) ){
                case TABLEPRED:
                        return encodeTablePredicateSATEncoder(This, constraint);
                case OPERATORPRED:
@@ -311,7 +311,7 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
        VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
        FunctionEncodingType encType = constraint->encoding.type;
        uint size = getSizeVectorTableEntry(entries);
-       Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
+       Constraint* constraints[size];
        for(uint i=0; i<size; i++){
                TableEntry* entry = getVectorTableEntry(entries, i);
                if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
@@ -323,19 +323,21 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
                Constraint* carray[inputNum];
                Element* el = getArrayElement(inputs, i);
                for(uint j=0; j<inputNum; j++){
-                       carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+                       carray[j] = getElementValueConstraint(el, entry->inputs[j]);
                }
                constraints[i]=allocArrayConstraint(AND, inputNum, carray);
        }
        Constraint* result= allocArrayConstraint(OR, size, constraints);
+       //FIXME: if it didn't match with any entry
        return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
 }
 
 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        switch(constraint->encoding.type){
                case ENUMERATEIMPLICATIONS:
-                       break;
+                       return encodeEnumOperatorPredicateSATEncoder(This, constraint);
                case CIRCUIT:
+                       ASSERT(0);
                        break;
                default:
                        ASSERT(0);
@@ -343,6 +345,26 @@ Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredica
        return NULL;
 }
 
+Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+       ASSERT(GETPREDICATETYPE(constraint)==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);
+       Constraint*  carray[size];
+       Element* elem1 = getArrayElement( &constraint->inputs, 0);
+       Element* elem2 = getArrayElement( &constraint->inputs, 1);
+       for(uint i=0; i<size; i++){
+               
+               carray[i] =  allocConstraint(AND, getElementValueConstraint(elem1, commonElements[i]),
+                       getElementValueConstraint(elem2, commonElements[i]) );
+       }
+       //FIXME: the case when there is no intersection ....
+       return allocArrayConstraint(OR, size, carray);
+}
+
 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
        switch(GETFUNCTIONTYPE(This->function)){
                case TABLEFUNC:

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 46419a407e5b71a3c24c0c1f648084887c541cf2..6963feefcfe83da08bd6e75c08e475887d3c15bd 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -27,6 +27,7 @@ Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 
 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 Constraint * getElementValueConstraint(Element* This, uint64_t value);