Fixing the constraint. Adding predicateTable

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 9d3772381fc889093cd8fc71ae6c44eee4a9e10e..bc23b057faffdb4bde94fd007339190f6b3a3a82 100644 (file)
--- 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 cf807c642a0f7fc210ac4617dcd6c528318b6fb3..a59aff182407c55035691970e565117a027ee696 100644 (file)
--- 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 08508b9e7be6287de8b71c21b87ed8fa9c960628..19b1c6e57d41529b1e7e60fd28c9bfd291ca2b38 100644 (file)
--- 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 935787fa08bbc6ee03c3c28bd40344475c53fc9d..933d831a3a53114cc8b3072e05cd9232055d179b 100644 (file)
--- 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 79e81df66443e8a0e8d68ed311da81979272b783..97bbd1818b5f57027ed7eab07c61f0fb46d19c9d 100644 (file)
--- 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 ee432cb70a6a09b8f1767e20ee14c9788c8f23ed..13e5295bc69c2a10e0e90d8d5ab94ed45cb45de9 100644 (file)
--- 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 28dd6af00f65cbd200b61e2fa6530a29eb6bf39a..9fd551985ebbaf39848d73218e3160425a2396e8 100644 (file)
--- 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; i<size; i++){
+                       ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
+                       BooleanOrder* tmp = (BooleanPredicate*)getVectorBoolean(orderConstrs, i);
+                       BooleanOrder* newBool;
+                       Constraint* first, second;
+                       if(tmp->second==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 2a3901db9bceee5f0364c89cc7fa683abb48b4e7..32fb6fae70343d1db989c1a9efcb9a9dd8ac1e06 100644 (file)
--- 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 f7768303a356e299ae3d08ee3d84b4b10c23e8ec..48886ac0fabe2ee1c451abdc5262b9fd32066f3b 100644 (file)
--- 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 243ea4d94ce5bd5404b657c59158a4a73dd99127..1ae5f8ca9eabdfe0f56f7b844bc5bb4208bdd841 100644 (file)
--- 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 7ffd1eca4ab7e7b59282826ad4293caf271b0135..60240990e484371648b6e1b613d5cc8054284aca 100644 (file)
--- 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;
 }