From 8642947cea83f16f02d0ff371cec5bb1a0163ed4 Mon Sep 17 00:00:00 2001 From: Hamed Date: Sat, 1 Jul 2017 17:44:36 -0700 Subject: [PATCH] New approach for Total Order --- src/AST/boolean.c | 3 ++ src/Backend/orderpair.c | 12 ++++++ src/Backend/orderpair.h | 23 +++++++++++ src/Backend/satencoder.c | 83 +++++++++++++++++++++++++++++++++------ src/Backend/satencoder.h | 4 +- src/Collections/structs.c | 12 +++--- src/Collections/structs.h | 2 +- src/classlist.h | 3 ++ 8 files changed, 124 insertions(+), 18 deletions(-) create mode 100644 src/Backend/orderpair.c create mode 100644 src/Backend/orderpair.h diff --git a/src/AST/boolean.c b/src/AST/boolean.c index bc23b05..3166c5d 100644 --- a/src/AST/boolean.c +++ b/src/AST/boolean.c @@ -19,6 +19,9 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) { tmp->order=order; tmp->first=first; tmp->second=second; + //FIXME: what if client calls this function with the same arguments? + //Instead of vector we should keep a hashtable from PAIR->BOOLEANOrder with + //asymmetric hash function. pushVectorBoolean(&order->constraints, &tmp->base); allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp)); return & tmp -> base; diff --git a/src/Backend/orderpair.c b/src/Backend/orderpair.c new file mode 100644 index 0000000..2290b36 --- /dev/null +++ b/src/Backend/orderpair.c @@ -0,0 +1,12 @@ +#include "orderpair.h" + + +OrderPair* allocOrderPair(uint64_t first, uint64_t second){ + OrderPair* pair = (OrderPair*) ourmalloc(sizeof(OrderPair)); + pair->first = first; + pair->second = second; + return pair; +} +void deleteOrderPair(OrderPair* pair){ + ourfree(pair); +} \ No newline at end of file diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h new file mode 100644 index 0000000..21bddd7 --- /dev/null +++ b/src/Backend/orderpair.h @@ -0,0 +1,23 @@ +/* + * File: orderpair.h + * Author: hamed + * + * Created on July 1, 2017, 4:22 PM + */ + +#ifndef ORDERPAIR_H +#define ORDERPAIR_H + +#include "classlist.h" +#include "mymemory.h" + +struct OrderPair{ + uint64_t first; + uint64_t second; +}; + +OrderPair* allocOrderPair(uint64_t first, uint64_t second); +void deleteOrderPair(OrderPair* pair); + +#endif /* ORDERPAIR_H */ + diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index c874c81..8886854 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -10,7 +10,8 @@ #include "table.h" #include "order.h" #include "predicate.h" - +#include "orderpair.h" +#include "set.h" SATEncoder * allocSATEncoder() { SATEncoder *This=ourmalloc(sizeof (SATEncoder)); @@ -165,6 +166,7 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) } } + Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) { switch( constraint->order->type){ case PARTIAL: @@ -177,8 +179,76 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) return NULL; } + Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){ ASSERT(boolOrder->order->type == TOTAL); + HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints; + OrderPair* pair = allocOrderPair(boolOrder->first, boolOrder->second); + if( !containsBoolConst(boolToConsts, pair) ){ + createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); + } + Constraint* constraint = getOrderConstraint(boolToConsts, pair); + deleteOrderPair(pair); + return constraint; +} + +void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){ + ASSERT(order->type == TOTAL); + VectorInt* mems = order->set->members; + HashTableBoolConst* table = order->boolsToConstraints; + uint size = getSizeVectorInt(mems); + for(uint i=0; ifirst!= pair->second); + Constraint* constraint= getBoolConst(table, pair); + ASSERT(constraint!= NULL); + if(pair->first > pair->second) + return constraint; + else + return negateConstraint(constraint); +} + +Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){ + //FIXME: first we should add the the constraint to the satsolver! + Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)}; + Constraint * loop1= allocArrayConstraint(OR, 3, carray); + Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK}; + Constraint * loop2= allocArrayConstraint(OR, 3,carray2 ); + return allocConstraint(AND, loop1, loop2); +} + +Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){ + // FIXME: we can have this implementation for partial order. Basically, + // we compute the transitivity between two order constraints specified by the client! (also can be used + // when client specify sparse constraints for the total order!) + ASSERT(boolOrder->order->type == PARTIAL); +/* HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints; if( containsBoolConst(boolToConsts, boolOrder) ){ return getBoolConst(boolToConsts, boolOrder); @@ -208,16 +278,7 @@ Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrd } 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; } diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index fc79a05..46419a4 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -16,7 +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); +void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order); +Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair); +Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK); Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint); Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint); diff --git a/src/Collections/structs.c b/src/Collections/structs.c index 6fd7cea..58d3728 100644 --- a/src/Collections/structs.c +++ b/src/Collections/structs.c @@ -1,6 +1,6 @@ #include "structs.h" #include "mymemory.h" -#include "order.h" +#include "orderpair.h" VectorImpl(Table, Table *, 4); VectorImpl(Set, Set *, 4); @@ -22,12 +22,14 @@ inline bool Ptr_equals(void * key1, void * key2) { return key1 == key2; } -inline unsigned int BooleanOrder_hash_Function(BooleanOrder* This){ - return This->first ^ This->second; +inline unsigned int order_pair_hash_Function(OrderPair* This){ + uint64_t x=This->first^This->second; + uint64_t a=This->first&This->second; + return (uint)((x<<4)^(a)); } -inline unsigned int BooleanOrder_equals(BooleanOrder* key1, BooleanOrder* key2){ +inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){ return key1->first== key2->first && key1->second == key2->second; } -HashTableImpl(BoolConst, BooleanOrder *, Constraint *, BooleanOrder_hash_Function, BooleanOrder_equals); +HashTableImpl(BoolConst, OrderPair *, Constraint *, order_pair_hash_Function, order_pair_equals); diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 86db3ed..a45eb13 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -26,7 +26,7 @@ VectorDef(Int, uint64_t, 4); HashTableDef(Void, void *, void *); -HashTableDef(BoolConst, BooleanOrder *, Constraint *); +HashTableDef(BoolConst, OrderPair *, Constraint *); HashSetDef(Void, void *); diff --git a/src/classlist.h b/src/classlist.h index 3c7d071..c02268d 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -70,6 +70,9 @@ typedef struct Table Table; struct Order; typedef struct Order Order; +struct OrderPair; +typedef struct OrderPair OrderPair; + struct ElementEncoding; typedef struct ElementEncoding ElementEncoding; -- 2.34.1