New approach for Total Order

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index bc23b057faffdb4bde94fd007339190f6b3a3a82..3166c5da6d65cb51a0ccdfa39e69f3bafb76a085 100644 (file)
--- 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 (file)
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 (file)
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 c874c81c6fbcc6bf96d1948173bed6e85390e18c..88868544ca2e01a19e020fca231492692a1aea8d 100644 (file)
--- 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; i<size; i++){
+               uint64_t valueI = getVectorInt(mems, i);
+               for(uint j=i+1; j<size;j++){
+                       uint64_t valueJ = getVectorInt(mems, j);
+                       OrderPair* pairIJ = allocOrderPair(valueI, valueJ);
+                       ASSERT(!containsBoolConst(table, pairIJ));
+                       Constraint* constIJ = getNewVarSATEncoder(This);
+                       putBoolConst(table, pairIJ, constIJ);
+                       for(uint k=j+1; k<size; k++){
+                               uint64_t valueK = getVectorInt(mems, k);
+                               OrderPair* pairJK = allocOrderPair(valueJ, valueK);
+                               OrderPair* pairIK = allocOrderPair(valueI, valueK);
+                               Constraint* constJK, *constIK;
+                               if(!containsBoolConst(table, pairJK)){
+                                       constJK = getNewVarSATEncoder(This);
+                                       putBoolConst(table, pairJK, constJK);
+                               }
+                               if(!containsBoolConst(table, pairIK)){
+                                       constIK = getNewVarSATEncoder(This);
+                                       putBoolConst(table, pairIK, constIK);
+                               }
+                               generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK); 
+                       }
+               }
+       }
+}
+
+Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+       ASSERT(pair->first!= 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 fc79a050ea4e5d561fc2098eaaa64820c0ac6391..46419a407e5b71a3c24c0c1f648084887c541cf2 100644 (file)
--- 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 6fd7ceaa804e63c973074be135d796c36a75b184..58d37286193327f51491701a0f1a7bb2c15bdcdc 100644 (file)
--- 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 86db3ed684870419f3f11fed102056a8c1256d5b..a45eb132cf1eb2c53ae99dd4e5bd259b69ac59cd 100644 (file)
--- 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 3c7d071a66221d25dffd679d5465284efe7cc769..c02268df29bebbe49d56cfca2fb272b297bc7321 100644 (file)
--- 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;