Add rewriting support

diff --git a/src/AST/rewriter.c b/src/AST/rewriter.c
new file mode 100644 (file)
index 0000000..1ff40a3
--- /dev/null
+++ b/src/AST/rewriter.c
@@ -0,0 +1,149 @@
+#include "rewriter.h"
+#include "boolean.h"
+
+void replaceBooleanWithTrue(Boolean * This) {
+       uint size=getSizeVectorBoolean(&This->parents);
+       for(uint i=0;i<size;i++) {
+               Boolean * parent=getVectorBoolean(&This->parents, i);
+               BooleanLogic * logicop=(BooleanLogic*) parent;
+               switch(logicop->op) {
+               case L_AND:
+                       handleANDTrue(logicop, This);
+                       break;
+               case L_OR:
+                       replaceBooleanWithTrue(parent);
+                       break;
+               case L_NOT:
+                       replaceBooleanWithFalse(parent);
+                       break;
+               case L_XOR:
+                       handleXORTrue(logicop, This);
+                       break;
+               case L_IMPLIES:
+                       handleIMPLIESTrue(logicop, This);
+                       break;
+               }
+       }
+}
+
+void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
+       uint size=getSizeVectorBoolean(&oldb->parents);
+       for(uint i=0;i<size;i++) {
+               Boolean * parent=getVectorBoolean(&oldb->parents, i);
+               BooleanLogic * logicop=(BooleanLogic*) parent;
+
+               uint parentsize=getSizeArrayBoolean(&logicop->inputs);
+               
+               for(uint j=0;j<parentsize;j++) {
+                       Boolean *b=getArrayBoolean(&logicop->inputs, i);
+                       if (b==oldb) {
+                               setArrayBoolean(&logicop->inputs, i, newb);
+                               pushVectorBoolean(&newb->parents, parent);
+                       }
+               }
+       }
+}
+
+void handleXORTrue(BooleanLogic *This, Boolean *child) {
+       uint size=getSizeArrayBoolean(&This->inputs);
+       Boolean *b=getArrayBoolean(&This->inputs, 0);
+       uint otherindex=(b==child)?1:0;
+       removeElementArrayBoolean(&This->inputs, otherindex);
+       This->op=L_NOT;
+}
+
+void handleXORFalse(BooleanLogic *This, Boolean *child) {
+       uint size=getSizeArrayBoolean(&This->inputs);
+       Boolean *b=getArrayBoolean(&This->inputs, 0);
+       uint otherindex=(b==child)?1:0;
+       replaceBooleanWithBoolean((Boolean *)This, getArrayBoolean(&This->inputs, otherindex));
+}
+
+void handleIMPLIESTrue(BooleanLogic *This, Boolean *child) {
+       uint size=getSizeArrayBoolean(&This->inputs);
+       Boolean *b=getArrayBoolean(&This->inputs, 0);
+       if (b==child) {
+               //Replace with other term
+               replaceBooleanWithBoolean((Boolean *)This, getArrayBoolean(&This->inputs, 1));
+       } else {
+               //Statement is true...
+               replaceBooleanWithTrue((Boolean *)This);
+       }
+}
+
+void handleIMPLIESFalse(BooleanLogic *This, Boolean *child) {
+       uint size=getSizeArrayBoolean(&This->inputs);
+       Boolean *b=getArrayBoolean(&This->inputs, 0);
+       if (b==child) {
+               //Statement is true...
+               replaceBooleanWithTrue((Boolean *)This);
+       } else {
+               //Make into negation of first term
+               removeElementArrayBoolean(&This->inputs, 1);
+               This->op=L_NOT;
+       }
+}
+
+void handleANDTrue(BooleanLogic *This, Boolean *child) {
+       uint size=getSizeArrayBoolean(&This->inputs);
+
+       if (size==1) {
+               replaceBooleanWithTrue((Boolean *)This);
+               return;
+       }
+       
+       for(uint i=0;i<size;i++) {
+               Boolean *b=getArrayBoolean(&This->inputs, i);
+               if (b==child) {
+                       removeElementArrayBoolean(&This->inputs, i);
+               }
+       }
+       
+       if (size==2) {
+               replaceBooleanWithBoolean((Boolean *)This, getArrayBoolean(&This->inputs, 0));
+       }
+}
+
+void handleORFalse(BooleanLogic *This, Boolean *child) {
+       uint size=getSizeArrayBoolean(&This->inputs);
+
+       if (size==1) {
+               replaceBooleanWithFalse((Boolean*) This);
+       }
+               
+       for(uint i=0;i<size;i++) {
+               Boolean *b=getArrayBoolean(&This->inputs, i);
+               if (b==child) {
+                       removeElementArrayBoolean(&This->inputs, i);
+               }
+       }
+
+       if (size==2) {
+               replaceBooleanWithBoolean((Boolean *)This, getArrayBoolean(&This->inputs, 0));
+       }
+}
+
+void replaceBooleanWithFalse(Boolean * This) {
+       uint size=getSizeVectorBoolean(&This->parents);
+       for(uint i=0;i<size;i++) {
+               Boolean * parent=getVectorBoolean(&This->parents, i);
+               BooleanLogic * logicop=(BooleanLogic*) parent;
+               switch(logicop->op) {
+               case L_AND:
+                       replaceBooleanWithFalse(parent);
+                       break;
+               case L_OR:
+                       handleORFalse(logicop, This);
+                       break;
+               case L_NOT:
+                       replaceBooleanWithTrue(parent);
+                       break;
+               case L_XOR:
+                       handleXORFalse(logicop, This);
+                       break;
+               case L_IMPLIES:
+                       handleIMPLIESFalse(logicop, This);
+                       break;
+               }
+       }       
+}

diff --git a/src/AST/rewriter.h b/src/AST/rewriter.h
new file mode 100644 (file)
index 0000000..9050b73
--- /dev/null
+++ b/src/AST/rewriter.h
@@ -0,0 +1,15 @@
+#ifndef REWRITER_H
+#define REWRITER_H
+#include "classlist.h"
+
+void replaceBooleanWithTrue(Boolean * This);
+void replaceBooleanWithFalse(Boolean * This);
+void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+void handleXORTrue(BooleanLogic *This, Boolean *child);
+void handleXORFalse(BooleanLogic *This, Boolean *child);
+void handleIMPLIESTrue(BooleanLogic *This, Boolean *child);
+void handleIMPLIESFalse(BooleanLogic *This, Boolean *child);
+void handleANDTrue(BooleanLogic *This, Boolean *child);
+void handleORFalse(BooleanLogic *This, Boolean *child);
+
+#endif

diff --git a/src/Collections/array.h b/src/Collections/array.h
index 19a22b3cdb7c947a70204f05623dfd53aa9a8212..f823d8c43119014f513e23a03b94acf9ba5a0377 100644 (file)
--- a/src/Collections/array.h
+++ b/src/Collections/array.h
@@ -18,7 +18,13 @@
                memcpy(tmp->array, array, size * sizeof(type));                                                                                 \
                return tmp;                                                         \
        }                                                                     \
-       static inline type getArray ## name(Array ## name * This, uint index) {                 \
+       static inline void removeElementArray ## name(Array ## name * This, uint index) { \
+               This->size--;                                                                                                                                                                                                                           \
+               for(;index<This->size;index++) {                                                                                                                                                \
+                       This->array[index]=This->array[index+1];                                                                                                        \
+               }                                                                                                                                                                                                                                                                               \
+       }                                                                                                                                                                                                                                                                                       \
+       static inline type getArray ## name(Array ## name * This, uint index) { \
                return This->array[index];                                                                                                                                                                      \
        }                                                                     \
        static inline void setArray ## name(Array ## name * This, uint index, type item) {      \

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 8f83906d1d9b70e5701346e52789bb22e1f3e2e8..ee3480d9c2c4159769217dde510a9f686d0201d3 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -5,7 +5,7 @@
 #include "ordergraph.h"
 #include "order.h"
 #include "ordernode.h"
-
+#include "rewriter.h"
 
 OrderGraph* buildOrderGraph(Order *order) {
        OrderGraph* orderGraph = allocOrderGraph(order);
@@ -267,6 +267,20 @@ void localMustAnalysisPartial(OrderGraph *graph) {
 void decomposeOrder(Order *order, OrderGraph *graph) {
        uint size=getSizeVectorBooleanOrder(&order->constraints);
        for(uint i=0;i<size;i++) {
+               BooleanOrder *orderconstraint=getVectorBooleanOrder(&order->constraints, i);
+               OrderNode *from=getOrderNodeFromOrderGraph(graph, orderconstraint->first);
+               OrderNode *to=getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+               OrderEdge* edge=getOrderEdgeFromOrderGraph(graph, from, to);
+               if (from->sccNum < to->sccNum) {
+                       //replace with true
+                       replaceBooleanWithTrue((Boolean *)orderconstraint);
+               } else if (to->sccNum < from->sccNum) {
+                       //replace with false
+                       replaceBooleanWithFalse((Boolean *)orderconstraint);
+               } else {
+                       //Build new order and change constraint's order
+
+               }
        }
 }