From 2f37735947671909a3f788f083bf91d547b9f283 Mon Sep 17 00:00:00 2001 From: Hamed Date: Thu, 29 Jun 2017 20:20:54 -0700 Subject: [PATCH] Fixing the constraint. Adding predicateTable --- src/AST/boolean.c | 3 ++- src/AST/boolean.h | 1 - src/AST/order.c | 2 ++ src/AST/order.h | 1 + src/AST/predicate.c | 10 ++++++- src/AST/predicate.h | 3 ++- src/Backend/satencoder.c | 55 ++++++++++++++++++++++++++++++++++++--- src/Backend/satencoder.h | 3 +++ src/Collections/structs.c | 2 ++ src/Collections/structs.h | 11 +++++++- src/csolver.c | 2 +- 11 files changed, 84 insertions(+), 9 deletions(-) diff --git a/src/AST/boolean.c b/src/AST/boolean.c index 9d37723..bc23b05 100644 --- a/src/AST/boolean.c +++ b/src/AST/boolean.c @@ -2,6 +2,7 @@ #include "structs.h" #include "csolver.h" #include "element.h" +#include "order.h" Boolean* allocBoolean(VarType t) { BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar)); @@ -18,7 +19,7 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) { tmp->order=order; tmp->first=first; tmp->second=second; - tmp->var=NULL; + pushVectorBoolean(&order->constraints, &tmp->base); allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp)); return & tmp -> base; } diff --git a/src/AST/boolean.h b/src/AST/boolean.h index cf807c6..a59aff1 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -24,7 +24,6 @@ struct BooleanOrder { Order* order; uint64_t first; uint64_t second; - Constraint* var; }; struct BooleanVar { diff --git a/src/AST/order.c b/src/AST/order.c index 08508b9..19b1c6e 100644 --- a/src/AST/order.c +++ b/src/AST/order.c @@ -10,6 +10,7 @@ Order* allocOrder(OrderType type, Set * set){ allocInlineDefVectorBoolean(& order->constraints); order->type=type; allocOrderEncoding(& order->order, order); + order->boolsToConstraints = allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); return order; } @@ -24,5 +25,6 @@ void setOrderEncodingType(Order* order, OrderEncodingType type){ void deleteOrder(Order* order){ deleteVectorArrayBoolean(& order->constraints); deleteOrderEncoding(& order->order); + deleteHashTableBoolConst(order->boolsToConstraints); ourfree(order); } diff --git a/src/AST/order.h b/src/AST/order.h index 935787f..933d831 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -10,6 +10,7 @@ struct Order { OrderType type; Set * set; + HashTableBoolConst* boolsToConstraints; VectorBoolean constraints; OrderEncoding order; }; diff --git a/src/AST/predicate.c b/src/AST/predicate.c index 79e81df..97bbd18 100644 --- a/src/AST/predicate.c +++ b/src/AST/predicate.c @@ -1,6 +1,6 @@ #include "predicate.h" -Predicate* allocPredicate(CompOp op, Set ** domain, uint numDomain){ +Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){ PredicateOperator* predicate = ourmalloc(sizeof(PredicateOperator)); GETPREDICATETYPE(predicate)=OPERATORPRED; allocInlineArrayInitSet(&predicate->domains, domain, numDomain); @@ -8,6 +8,14 @@ Predicate* allocPredicate(CompOp op, Set ** domain, uint numDomain){ return &predicate->base; } +Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){ + PredicateTable* predicate = ourmalloc(sizeof(PredicateTable)); + GETPREDICATETYPE(predicate) = TABLEPRED; + predicate->table=table; + predicate->undefinedbehavior=undefBehavior; + return predicate; +} + void deletePredicate(Predicate* predicate){ switch(GETPREDICATETYPE(predicate)) { case OPERATORPRED: { diff --git a/src/AST/predicate.h b/src/AST/predicate.h index ee432cb..13e5295 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -24,6 +24,7 @@ struct PredicateTable { }; -Predicate* allocPredicate(CompOp op, Set ** domain, uint numDomain); +Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain); +Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior); void deletePredicate(Predicate* predicate); #endif diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index 28dd6af..9fd5519 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -164,10 +164,59 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) } Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { - if(constraint->var== NULL){ - constraint->var = getNewVarSATEncoder(This); + switch( constraint->order->type){ + case PARTIAL: + return encodePartialOrderSATEncoder(This, constraint); + case TOTAL: + return encodeTotalOrderSATEncoder(This, constraint); + default: + ASSERT(0); } - return constraint->var; + return NULL; +} + +Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){ + ASSERT(boolOrder->order->type == TOTAL); + HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints; + if( containsBoolConst(boolToConsts, boolOrder) ){ + return getBoolConst(boolToConsts, boolOrder); + } else { + Constraint* constraint = getNewVarSATEncoder(This); + putBoolConst(boolToConsts,boolOrder, constraint); + VectorBoolean* orderConstrs = &boolOrder->order->constraints; + uint size= getSizeVectorBoolean(orderConstrs); + for(uint i=0; isecond==boolOrder->first){ + newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second); + first = encodeTotalOrderSATEncoder(This, tmp); + second = constraint; + + }else if (boolOrder->second == tmp->first){ + newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second); + first = constraint; + second = encodeTotalOrderSATEncoder(This, tmp); + }else + continue; + Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool); + generateTransOrderConstraintSATEncoder(This, first, second, transConstr ); + } + return constraint; + } + + return NULL; +} + +Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *first,Constraint *second,Constraint *third){ + //FIXME: first we should add the the constraint to the satsolver! + return allocConstraint(IMPLIES, allocConstraint(AND, first, second), third); +} + +Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){ + return NULL; } Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 2a3901d..32fb6fa 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -16,6 +16,9 @@ Constraint * getNewVarSATEncoder(SATEncoder *This); void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray); Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint); Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *first,Constraint *second,Constraint *third); +Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); +Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint); Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); diff --git a/src/Collections/structs.c b/src/Collections/structs.c index f776830..48886ac 100644 --- a/src/Collections/structs.c +++ b/src/Collections/structs.c @@ -12,3 +12,5 @@ VectorImpl(Order, Order *, 4); VectorImpl(TableEntry, TableEntry *, 4); VectorImpl(ASTNode, ASTNode *, 4); VectorImpl(Int, uint64_t, 4); + +HashTableImpl(BoolConst, BooleanOrder *, Constraint *, BooleanOrder_hash_Function, BooleanOrder_equals); diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 243ea4d..1ae5f8c 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -32,8 +32,17 @@ inline bool Ptr_equals(void * key1, void * key2) { return key1 == key2; } +inline unsigned int BooleanOrder_hash_Function(BooleanOrder* This){ + return ((This->first+This->second)(This->first+This->second+1))/2 + This->second; +} + +inline unsigned int BooleanOrder_equals(BooleanOrder* key1, BooleanOrder* key2){ + return key1->first== key2->first && key1->second == key2->second; +} + HashTableDef(Void, void *, void *, Ptr_hash_function, Ptr_equals); -HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals); +HashTableDef(BoolConst, BooleanOrder *, Constraint *, BooleanOrder_hash_Function, BooleanOrder_equals); +HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals); #endif diff --git a/src/csolver.c b/src/csolver.c index 7ffd1ec..6024099 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -118,7 +118,7 @@ Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, ui } Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain) { - Predicate* predicate= allocPredicate(op, domain,numDomain); + Predicate* predicate= allocPredicateOperator(op, domain,numDomain); pushVectorPredicate(solver->allPredicates, predicate); return predicate; } -- 2.34.1