From 4c23ace7b399ab58a9030b157573e0850cf133d3 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 16 Aug 2017 18:11:10 -0700 Subject: [PATCH] Add rewriting support --- src/AST/rewriter.c | 149 ++++++++++++++++++++++++++++++++++++ src/AST/rewriter.h | 15 ++++ src/Collections/array.h | 8 +- src/Encoders/orderencoder.c | 16 +++- 4 files changed, 186 insertions(+), 2 deletions(-) create mode 100644 src/AST/rewriter.c create mode 100644 src/AST/rewriter.h diff --git a/src/AST/rewriter.c b/src/AST/rewriter.c new file mode 100644 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;iparents, 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;iparents, i); + BooleanLogic * logicop=(BooleanLogic*) parent; + + uint parentsize=getSizeArrayBoolean(&logicop->inputs); + + for(uint j=0;jinputs, 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;iinputs, 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;iinputs, 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;iparents, 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 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 19a22b3..f823d8c 100644 --- 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(;indexsize;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 8f83906..ee3480d 100644 --- 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;iconstraints, 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 + + } } } -- 2.34.1