Generating constraints for BooleanOrder

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 0432b4395cd772f9eb7a11abc8dd9ae5379b0f96..9d3772381fc889093cd8fc71ae6c44eee4a9e10e 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -18,6 +18,7 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
        tmp->order=order;
        tmp->first=first;
        tmp->second=second;
+       tmp->var=NULL;
        allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp));
        return & tmp -> base;
 }

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index a59aff182407c55035691970e565117a027ee696..cf807c642a0f7fc210ac4617dcd6c528318b6fb3 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -24,6 +24,7 @@ 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 1e39b38606e7e824edc9dbdcee65164098e620af..cbfeac38d3ab0963b1a427263d93e0fa064cf4b9 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -13,6 +13,14 @@ Order* allocOrder(OrderType type, Set * set){
        return order;
 }
 
+void addOrderConstraint(Order* order, BooleanOrder* constraint){
+       pushVectorBoolean( &order->constraints, (Boolean) constraint);
+}
+
+void setOrderEncodingType(Order* order, OrderEncodingType type){
+       order->order.type = type;
+}
+
 void deleteOrder(Order* order){
        deleteVectorArrayBoolean(& order->constraints);
        deleteOrderEncoding(& order->order);

diff --git a/src/AST/order.h b/src/AST/order.h
index 0229982ff5b362e4effd3021ac955478aebc8d19..935787fa08bbc6ee03c3c28bd40344475c53fc9d 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -5,6 +5,7 @@
 #include "structs.h"
 #include "ops.h"
 #include "orderencoding.h"
+#include "boolean.h"
 
 struct Order {
        OrderType type;
@@ -14,5 +15,7 @@ struct Order {
 };
 
 Order* allocOrder(OrderType type, Set * set);
+void addOrderConstraint(Order* order, BooleanOrder* constraint);
+void setOrderEncodingType(Order* order, OrderEncodingType type);
 void deleteOrder(Order* order);
 #endif

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 325b614c18cf593927f904125c93002010008904..fa385aed0222d64fe9a96460bd6e01bd29b624bc 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -8,6 +8,7 @@
 #include "function.h"
 #include "tableentry.h"
 #include "table.h"
+#include "order.h"
 
 
 SATEncoder * allocSATEncoder() {
@@ -113,8 +114,10 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint)
 }
 
 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
-       //TO IMPLEMENT
-       return NULL;
+       if(constraint->var== NULL){
+               constraint->var = getNewVarSATEncoder(This);
+       }
+       return constraint->var;
 }
 
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
@@ -132,7 +135,6 @@ Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction
                default:
                        ASSERT(0);
        }
-       //FIXME
        return NULL;
 }
 
@@ -144,7 +146,6 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun
                default:
                        ASSERT(0);
        }
-       //FIXME
        return NULL;
 }
 
@@ -157,6 +158,7 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
        ArrayElement* elements= &This->inputs;
        Table* table = ((FunctionTable*) (This->function))->table;
        uint size = getSizeVectorTableEntry(&table->entries);
+       Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
        for(uint i=0; i<size; i++){
                TableEntry* entry = getVectorTableEntry(&table->entries, i);
                uint inputNum =getSizeArrayElement(elements);
@@ -167,8 +169,9 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
                }
                Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
                        getElementValueConstraint((Element*)This, entry->output));
-               pushVectorConstraint( getSATEncoderAllConstraints(encoder), row);
+               constraints[i]=row;
        }
-       //FIXME
-       return NULL;
+       Constraint* result = allocArrayConstraint(OR, size, constraints);
+       pushVectorConstraint( getSATEncoderAllConstraints(encoder), result);
+       return result;
 }
\ No newline at end of file

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 1ea5857176e637142619cb3f1afc55924245e7cc..4f9db3ef92a449a5fdd6c18819ce60d620cc5dee 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -10,6 +10,7 @@
 #include "boolean.h"
 #include "table.h"
 #include "tableentry.h"
+#include "order.h"
 #include <strings.h>
 
 
@@ -36,12 +37,15 @@ void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){
        
        size = getSizeVectorBoolean(csolver->allBooleans);
        for(uint i=0; i<size; i++){
-               Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
-               switch(GETBOOLEANTYPE(predicate)){
+               Boolean* boolean = getVectorBoolean(csolver->allBooleans, i);
+               switch(GETBOOLEANTYPE(boolean)){
                        case PREDICATEOP:
-                               setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)predicate),
+                               setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean),
                                        ENUMERATEIMPLICATIONS);
                                break;
+                       case ORDERCONST:
+                               setOrderEncodingType( ((BooleanOrder*)boolean)->order, PAIRWISE );
+                               break;
                        default:
                                continue;
                }