From 32f0e484ad03e167ba45ddeeb78f1093a013e675 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 14:32:45 -0700 Subject: [PATCH] Add support for some other operators --- src/AST/ops.h | 2 +- src/AST/predicate.c | 39 +++++++++------------- src/AST/predicate.h | 3 +- src/AST/set.c | 11 +++++-- src/AST/set.h | 1 + src/Backend/satencoder.c | 70 +++++++++++++++++++++++++++++----------- 6 files changed, 80 insertions(+), 46 deletions(-) diff --git a/src/AST/ops.h b/src/AST/ops.h index 1f94cb1..dc0c80a 100644 --- 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 19e1597..8f7b5ee 100644 --- 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; iop) { + case EQUALS: + return inputs[0]==inputs[1]; + case LT: + 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 6aaacce..105e91b 100644 --- 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 05aaf91..2569ed2 100644 --- 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 5139927..1555ae9 100644 --- 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 d51e251..cfeb82a 100644 --- 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;iinputs, i); + encodeElementSATEncoder(This, elem); + } + VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses - for(uint i=0; icnf, arg1, arg2); + uint indices[numDomains]; //setup indices + bzero(indices, sizeof(uint)*numDomains); + + uint64_t vals[numDomains]; //setup value array + for(uint i=0;idomains, 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;iinputs, i); + carray[i] = getElementValueConstraint(This, elem, vals[i]); + } + pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray)); + } + + notfinished=false; + for(uint i=0;idomains, 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){ -- 2.34.1