Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
authorbdemsky <bdemsky@uci.edu>
Thu, 7 Sep 2017 22:02:14 +0000 (15:02 -0700)
committerbdemsky <bdemsky@uci.edu>
Thu, 7 Sep 2017 22:02:14 +0000 (15:02 -0700)
22 files changed:
design/notes.txt
src/ASTAnalyses/Order/orderanalysis.cc [new file with mode: 0644]
src/ASTAnalyses/Order/orderanalysis.h [new file with mode: 0644]
src/ASTAnalyses/Order/orderedge.cc [new file with mode: 0644]
src/ASTAnalyses/Order/orderedge.h [new file with mode: 0644]
src/ASTAnalyses/Order/ordergraph.cc [new file with mode: 0644]
src/ASTAnalyses/Order/ordergraph.h [new file with mode: 0644]
src/ASTAnalyses/Order/ordernode.cc [new file with mode: 0644]
src/ASTAnalyses/Order/ordernode.h [new file with mode: 0644]
src/ASTAnalyses/Polarity/polarityassignment.cc [new file with mode: 0644]
src/ASTAnalyses/Polarity/polarityassignment.h [new file with mode: 0644]
src/ASTAnalyses/orderanalysis.cc [deleted file]
src/ASTAnalyses/orderanalysis.h [deleted file]
src/ASTAnalyses/orderedge.cc [deleted file]
src/ASTAnalyses/orderedge.h [deleted file]
src/ASTAnalyses/ordergraph.cc [deleted file]
src/ASTAnalyses/ordergraph.h [deleted file]
src/ASTAnalyses/ordernode.cc [deleted file]
src/ASTAnalyses/ordernode.h [deleted file]
src/ASTAnalyses/polarityassignment.cc [deleted file]
src/ASTAnalyses/polarityassignment.h [deleted file]
src/Makefile

index 4219c89..f7282be 100644 (file)
@@ -1,6 +1,8 @@
 (1) Elements/BooleanVars should link back to expressions that use them
+--> Done
 
 (2) Need to introduce variables in encoding of functions....
+--> Done
 
 (3) Some cases can do variable elimination of introduced variables...
 
@@ -36,6 +38,8 @@ simply link to it again).  Possibly good to do in TreeConstruction...
 This could be lower priority as it isn't really essential to make
 things work.  Should also probably be switchable on/off...
 
+--> Done
+
 (2) Advanced TreeRewriting --- can rewrite functions/predicates to
 eliminate unused entries or to eliminate effectively identical
 outputs...  e.g., consider a function f() that can output the values
@@ -56,5 +60,35 @@ to turn on/off nearly any optimization we have...
 implement other simplifcation strategies
 
 (6) Convert SATCheck to use Constraint Compiler...not sure about order...
+Started...
 
 (7) Profile system....
+
+---------------------------------------------------------------------
+
+To do:
+
+(0) Support for saving/loading problem instances...
+
+(1) Complete satcheck support
+
+(2) Advance tree rewriting...  Variable value elimination...
+
+(3) Think about undefined semantics...
+
+(4) Smart encoding...
+    Variable Graphs....
+
+    Split graph into connected components
+
+Encoding ideas:
+*    Monotonic increasing index
+*    Matched index (equality)
+*    Bit exposes
+*    Single var
+*    Support arithmetic
+*    Sparse encoding
+
+--------------------------------------------------------------------
+
+
diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc
new file mode 100644 (file)
index 0000000..a77a1a8
--- /dev/null
@@ -0,0 +1,382 @@
+#include "orderanalysis.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "ordergraph.h"
+#include "order.h"
+#include "ordernode.h"
+#include "rewriter.h"
+#include "mutableset.h"
+#include "tunable.h"
+
+void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
+       SetIteratorOrderNode *iterator = graph->getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (node->status == NOTVISITED) {
+                       node->status = VISITED;
+                       DFSNodeVisit(node, finishNodes, false, false, 0);
+                       node->status = FINISHED;
+                       finishNodes->push(node);
+               }
+       }
+       delete iterator;
+}
+
+void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
+       uint size = finishNodes->getSize();
+       uint sccNum = 1;
+       for (int i = size - 1; i >= 0; i--) {
+               OrderNode *node = finishNodes->get(i);
+               if (node->status == NOTVISITED) {
+                       node->status = VISITED;
+                       DFSNodeVisit(node, NULL, true, false, sccNum);
+                       node->sccNum = sccNum;
+                       node->status = FINISHED;
+                       sccNum++;
+               }
+       }
+}
+
+void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
+       SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (mustvisit) {
+                       if (!edge->mustPos)
+                               continue;
+               } else
+               if (!edge->polPos && !edge->pseudoPos)  //Ignore edges that do not have positive polarity
+                       continue;
+
+               OrderNode *child = isReverse ? edge->source : edge->sink;
+
+               if (child->status == NOTVISITED) {
+                       child->status = VISITED;
+                       DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
+                       child->status = FINISHED;
+                       if (finishNodes != NULL)
+                               finishNodes->push(child);
+                       if (isReverse)
+                               child->sccNum = sccNum;
+               }
+       }
+       delete iterator;
+}
+
+void resetNodeInfoStatusSCC(OrderGraph *graph) {
+       SetIteratorOrderNode *iterator = graph->getNodes();
+       while (iterator->hasNext()) {
+               iterator->next()->status = NOTVISITED;
+       }
+       delete iterator;
+}
+
+void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
+       Vector<OrderNode *> finishNodes;
+       DFS(graph, &finishNodes);
+       resetNodeInfoStatusSCC(graph);
+       DFSReverse(graph, &finishNodes);
+       resetNodeInfoStatusSCC(graph);
+}
+
+bool isMustBeTrueNode(OrderNode *node) {
+       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (!edge->mustPos) {
+                       delete iterator;
+                       return false;
+               }
+       }
+       delete iterator;
+       iterator = node->outEdges.iterator();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (!edge->mustPos) {
+                       delete iterator;
+                       return false;
+               }
+       }
+       delete iterator;
+       return true;
+}
+
+void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
+       SetIteratorOrderEdge *iterin = node->inEdges.iterator();
+       while (iterin->hasNext()) {
+               OrderEdge *inEdge = iterin->next();
+               OrderNode *srcNode = inEdge->source;
+               srcNode->outEdges.remove(inEdge);
+               SetIteratorOrderEdge *iterout = node->outEdges.iterator();
+               while (iterout->hasNext()) {
+                       OrderEdge *outEdge = iterout->next();
+                       OrderNode *sinkNode = outEdge->sink;
+                       sinkNode->inEdges.remove(outEdge);
+                       //Adding new edge to new sink and src nodes ...
+                       if(srcNode == sinkNode){
+                               This->setUnSAT();
+                               delete iterout;
+                               delete iterin;
+                               return;
+                       }
+                       OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
+                       newEdge->mustPos = true;
+                       newEdge->polPos = true;
+                       if (newEdge->mustNeg){
+                               This->setUnSAT();
+                       }
+                       srcNode->outEdges.add(newEdge);
+                       sinkNode->inEdges.add(newEdge);
+               }
+               delete iterout;
+       }
+       delete iterin;
+}
+
+void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
+       SetIteratorOrderNode *iterator = graph->getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (isMustBeTrueNode(node)) {
+                       bypassMustBeTrueNode(This, graph, node);
+               }
+       }
+       delete iterator;
+}
+
+/** This function computes a source set for every nodes, the set of
+    nodes that can reach that node via pospolarity edges.  It then
+    looks for negative polarity edges from nodes in the the source set
+    to determine whether we need to generate pseudoPos edges. */
+
+void completePartialOrderGraph(OrderGraph *graph) {
+       Vector<OrderNode *> finishNodes;
+       DFS(graph, &finishNodes);
+       resetNodeInfoStatusSCC(graph);
+       HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
+
+       Vector<OrderNode *> sccNodes;
+
+       uint size = finishNodes.getSize();
+       uint sccNum = 1;
+       for (int i = size - 1; i >= 0; i--) {
+               OrderNode *node = finishNodes.get(i);
+               HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
+               table->put(node, sources);
+
+               if (node->status == NOTVISITED) {
+                       //Need to do reverse traversal here...
+                       node->status = VISITED;
+                       DFSNodeVisit(node, &sccNodes, true, false, sccNum);
+                       node->status = FINISHED;
+                       node->sccNum = sccNum;
+                       sccNum++;
+                       sccNodes.push(node);
+
+                       //Compute in set for entire SCC
+                       uint rSize = sccNodes.getSize();
+                       for (uint j = 0; j < rSize; j++) {
+                               OrderNode *rnode = sccNodes.get(j);
+                               //Compute source sets
+                               SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
+                               while (iterator->hasNext()) {
+                                       OrderEdge *edge = iterator->next();
+                                       OrderNode *parent = edge->source;
+                                       if (edge->polPos) {
+                                               sources->add(parent);
+                                               HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
+                                               sources->addAll(parent_srcs);
+                                       }
+                               }
+                               delete iterator;
+                       }
+                       for (uint j = 0; j < rSize; j++) {
+                               //Copy in set of entire SCC
+                               OrderNode *rnode = sccNodes.get(j);
+                               HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
+                               table->put(rnode, set);
+
+                               //Use source sets to compute pseudoPos edges
+                               SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+                               while (iterator->hasNext()) {
+                                       OrderEdge *edge = iterator->next();
+                                       OrderNode *parent = edge->source;
+                                       ASSERT(parent != rnode);
+                                       if (edge->polNeg && parent->sccNum != rnode->sccNum &&
+                                                       sources->contains(parent)) {
+                                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
+                                               newedge->pseudoPos = true;
+                                       }
+                               }
+                               delete iterator;
+                       }
+
+                       sccNodes.clear();
+               }
+       }
+
+       table->resetanddelete();
+       delete table;
+       resetNodeInfoStatusSCC(graph);
+}
+
+void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
+       SetIteratorOrderNode *iterator = graph->getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (node->status == NOTVISITED) {
+                       node->status = VISITED;
+                       DFSNodeVisit(node, finishNodes, false, true, 0);
+                       node->status = FINISHED;
+                       finishNodes->push(node);
+               }
+       }
+       delete iterator;
+}
+
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
+       uint size = finishNodes->getSize();
+       HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
+
+       for (int i = size - 1; i >= 0; i--) {
+               OrderNode *node = finishNodes->get(i);
+               HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
+               table->put(node, sources);
+
+               {
+                       //Compute source sets
+                       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+                       while (iterator->hasNext()) {
+                               OrderEdge *edge = iterator->next();
+                               OrderNode *parent = edge->source;
+                               if (edge->mustPos) {
+                                       sources->add(parent);
+                                       HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
+                                       sources->addAll(parent_srcs);
+                               }
+                       }
+                       delete iterator;
+               }
+               if (computeTransitiveClosure) {
+                       //Compute full transitive closure for nodes
+                       SetIteratorOrderNode *srciterator = sources->iterator();
+                       while (srciterator->hasNext()) {
+                               OrderNode *srcnode = srciterator->next();
+                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
+                               newedge->mustPos = true;
+                               newedge->polPos = true;
+                               if (newedge->mustNeg)
+                                       solver->setUnSAT();
+                               srcnode->outEdges.add(newedge);
+                               node->inEdges.add(newedge);
+                       }
+                       delete srciterator;
+               }
+               {
+                       //Use source sets to compute mustPos edges
+                       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+                       while (iterator->hasNext()) {
+                               OrderEdge *edge = iterator->next();
+                               OrderNode *parent = edge->source;
+                               if (!edge->mustPos && sources->contains(parent)) {
+                                       edge->mustPos = true;
+                                       edge->polPos = true;
+                                       if (edge->mustNeg)
+                                               solver->setUnSAT();
+                               }
+                       }
+                       delete iterator;
+               }
+               {
+                       //Use source sets to compute mustNeg for edges that would introduce cycle if true
+                       SetIteratorOrderEdge *iterator = node->outEdges.iterator();
+                       while (iterator->hasNext()) {
+                               OrderEdge *edge = iterator->next();
+                               OrderNode *child = edge->sink;
+                               if (!edge->mustNeg && sources->contains(child)) {
+                                       edge->mustNeg = true;
+                                       edge->polNeg = true;
+                                       if (edge->mustPos)
+                                               solver->setUnSAT();
+                               }
+                       }
+                       delete iterator;
+               }
+       }
+
+       table->resetanddelete();
+       delete table;
+}
+
+/* This function finds edges that would form a cycle with must edges
+   and forces them to be mustNeg.  It also decides whether an edge
+   must be true because of transitivity from other must be true
+   edges. */
+
+void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
+       Vector<OrderNode *> finishNodes;
+       //Topologically sort the mustPos edge graph
+       DFSMust(graph, &finishNodes);
+       resetNodeInfoStatusSCC(graph);
+
+       //Find any backwards edges that complete cycles and force them to be mustNeg
+       DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
+}
+
+/* This function finds edges that must be positive and forces the
+   inverse edge to be negative (and clears its positive polarity if it
+   had one). */
+
+void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
+       SetIteratorOrderEdge *iterator = graph->getEdges();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (edge->mustPos) {
+                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
+                       if (invEdge != NULL) {
+                               if (!invEdge->mustPos) {
+                                       invEdge->polPos = false;
+                               } else {
+                                       solver->setUnSAT();
+                               }
+                               invEdge->mustNeg = true;
+                               invEdge->polNeg = true;
+                       }
+               }
+       }
+       delete iterator;
+}
+
+/** This finds edges that must be positive and forces the inverse edge
+    to be negative.  It also clears the negative flag of this edge.
+    It also finds edges that must be negative and clears the positive
+    polarity. */
+
+void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
+       SetIteratorOrderEdge *iterator = graph->getEdges();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (edge->mustPos) {
+                       if (!edge->mustNeg) {
+                               edge->polNeg = false;
+                       } else
+                               solver->setUnSAT();
+
+                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
+                       if (invEdge != NULL) {
+                               if (!invEdge->mustPos)
+                                       invEdge->polPos = false;
+                               else
+                                       solver->setUnSAT();
+
+                               invEdge->mustNeg = true;
+                               invEdge->polNeg = true;
+                       }
+               }
+               if (edge->mustNeg && !edge->mustPos) {
+                       edge->polPos = false;
+               }
+       }
+       delete iterator;
+}
diff --git a/src/ASTAnalyses/Order/orderanalysis.h b/src/ASTAnalyses/Order/orderanalysis.h
new file mode 100644 (file)
index 0000000..b04ccfd
--- /dev/null
@@ -0,0 +1,24 @@
+#ifndef ORDERANALYSIS_H
+#define ORDERANALYSIS_H
+#include "classlist.h"
+#include "structs.h"
+#include "mymemory.h"
+
+void computeStronglyConnectedComponentGraph(OrderGraph *graph);
+void initializeNodeInfoSCC(OrderGraph *graph);
+void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
+void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void completePartialOrderGraph(OrderGraph *graph);
+void resetNodeInfoStatusSCC(OrderGraph *graph);
+bool isMustBeTrueNode(OrderNode *node);
+void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node);
+void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
+void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
+void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
+void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
+void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
+
+#endif
+
diff --git a/src/ASTAnalyses/Order/orderedge.cc b/src/ASTAnalyses/Order/orderedge.cc
new file mode 100644 (file)
index 0000000..c0cd678
--- /dev/null
@@ -0,0 +1,12 @@
+#include "orderedge.h"
+#include "ordergraph.h"
+
+OrderEdge::OrderEdge(OrderNode *_source, OrderNode *_sink) {
+       source = _source;
+       sink = _sink;
+       polPos = false;
+       polNeg = false;
+       mustPos = false;
+       mustNeg = false;
+       pseudoPos = false;
+}
diff --git a/src/ASTAnalyses/Order/orderedge.h b/src/ASTAnalyses/Order/orderedge.h
new file mode 100644 (file)
index 0000000..b10b781
--- /dev/null
@@ -0,0 +1,28 @@
+/*
+ * File:   orderedge.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:44 PM
+ */
+
+#ifndef ORDEREDGE_H
+#define ORDEREDGE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+class OrderEdge {
+public:
+       OrderEdge(OrderNode *begin, OrderNode *end);
+
+       OrderNode *source;
+       OrderNode *sink;
+       unsigned int polPos : 1;
+       unsigned int polNeg : 1;
+       unsigned int mustPos : 1;
+       unsigned int mustNeg : 1;
+       unsigned int pseudoPos : 1;
+       CMEMALLOC;
+};
+
+#endif/* ORDEREDGE_H */
+
diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
new file mode 100644 (file)
index 0000000..ce9a071
--- /dev/null
@@ -0,0 +1,227 @@
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "boolean.h"
+#include "orderedge.h"
+#include "ordergraph.h"
+#include "order.h"
+
+OrderGraph::OrderGraph(Order *_order) :
+       nodes(new HashsetOrderNode()),
+       edges(new HashsetOrderEdge()),
+       order(_order) {
+}
+
+OrderGraph *buildOrderGraph(Order *order) {
+       OrderGraph *orderGraph = new OrderGraph(order);
+       order->graph = orderGraph;
+       uint constrSize = order->constraints.getSize();
+       for (uint j = 0; j < constrSize; j++) {
+               orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
+       }
+       return orderGraph;
+}
+
+//Builds only the subgraph for the must order graph.
+OrderGraph *buildMustOrderGraph(Order *order) {
+       OrderGraph *orderGraph = new OrderGraph(order);
+       uint constrSize = order->constraints.getSize();
+       for (uint j = 0; j < constrSize; j++) {
+               orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
+       }
+       return orderGraph;
+}
+
+void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+       Polarity polarity = constr->polarity;
+       BooleanValue mustval = constr->boolVal;
+       switch (polarity) {
+       case P_BOTHTRUEFALSE:
+       case P_TRUE: {
+               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
+               if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
+                       _1to2->mustPos = true;
+               _1to2->polPos = true;
+               node1->addNewOutgoingEdge(_1to2);
+               node2->addNewIncomingEdge(_1to2);
+               if (constr->polarity == P_TRUE)
+                       break;
+       }
+       case P_FALSE: {
+               if (order->type == SATC_TOTAL) {
+                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
+                       if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
+                               _2to1->mustPos = true;
+                       _2to1->polPos = true;
+                       node2->addNewOutgoingEdge(_2to1);
+                       node1->addNewIncomingEdge(_2to1);
+               } else {
+                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
+                       if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
+                               _1to2->mustNeg = true;
+                       _1to2->polNeg = true;
+                       node1->addNewOutgoingEdge(_1to2);
+                       node2->addNewIncomingEdge(_1to2);
+               }
+               break;
+       }
+       case P_UNDEFINED:
+               //There is an unreachable order constraint if this assert fires
+               //Clients can easily do this, so don't do anything.
+               ;
+       }
+}
+
+void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+       BooleanValue mustval = constr->boolVal;
+       switch (mustval) {
+       case BV_UNSAT:
+       case BV_MUSTBETRUE: {
+               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
+               _1to2->mustPos = true;
+               _1to2->polPos = true;
+               node1->addNewOutgoingEdge(_1to2);
+               node2->addNewIncomingEdge(_1to2);
+               if (constr->boolVal == BV_MUSTBETRUE)
+                       break;
+       }
+       case BV_MUSTBEFALSE: {
+               if (order->type == SATC_TOTAL) {
+                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
+                       _2to1->mustPos = true;
+                       _2to1->polPos = true;
+                       node2->addNewOutgoingEdge(_2to1);
+                       node1->addNewIncomingEdge(_2to1);
+               } else {
+                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
+                       _1to2->mustNeg = true;
+                       _1to2->polNeg = true;
+                       node1->addNewOutgoingEdge(_1to2);
+                       node2->addNewIncomingEdge(_1to2);
+               }
+               break;
+       }
+       case BV_UNDEFINED:
+               //Do Nothing
+               break;
+       }
+}
+
+OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
+       OrderNode *node = new OrderNode(id);
+       OrderNode *tmp = nodes->get(node);
+       if ( tmp != NULL) {
+               delete node;
+               node = tmp;
+       } else {
+               nodes->add(node);
+       }
+       return node;
+}
+
+OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
+       OrderNode node(id);
+       OrderNode *tmp = nodes->get(&node);
+       return tmp;
+}
+
+OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
+       OrderEdge *edge = new OrderEdge(begin, end);
+       OrderEdge *tmp = edges->get(edge);
+       if ( tmp != NULL ) {
+               delete edge;
+               edge = tmp;
+       } else {
+               edges->add(edge);
+       }
+       return edge;
+}
+
+OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
+       OrderEdge edge(begin, end);
+       OrderEdge *tmp = edges->get(&edge);
+       return tmp;
+}
+
+OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
+       OrderEdge inverseedge(edge->sink, edge->source);
+       OrderEdge *tmp = edges->get(&inverseedge);
+       return tmp;
+}
+
+void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+       OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+       OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+       addOrderEdge(from, to, bOrder);
+}
+
+void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+       OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+       OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+       addMustOrderEdge(from, to, bOrder);
+}
+
+OrderGraph::~OrderGraph() {
+       SetIteratorOrderNode *iterator = nodes->iterator();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               delete node;
+       }
+       delete iterator;
+
+       SetIteratorOrderEdge *eiterator = edges->iterator();
+       while (eiterator->hasNext()) {
+               OrderEdge *edge = eiterator->next();
+               delete edge;
+       }
+       delete eiterator;
+       delete nodes;
+       delete edges;
+}
+
+bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
+       HashsetOrderNode visited;
+       visited.add(source);
+       SetIteratorOrderEdge *iterator = source->outEdges.iterator();
+       bool found = false;
+       while(iterator->hasNext()){
+               OrderEdge* edge = iterator->next();
+               if(edge->polPos){
+                       OrderNode* node = edge->sink;
+                       if(!visited.contains(node)){
+                               if( node == destination ){
+                                       found = true;
+                                       break;
+                               }
+                               visited.add(node);
+                               found =isTherePathVisit(visited, node, destination);
+                               if(found){
+                                       break;
+                               }
+                       }
+               }
+       }
+       delete iterator;
+       return found;
+}
+
+bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
+       SetIteratorOrderEdge *iterator = current->outEdges.iterator();
+       bool found = false;
+       while(iterator->hasNext()){
+               OrderEdge* edge = iterator->next();
+               if(edge->polPos){
+                       OrderNode* node = edge->sink;
+                       if(node == destination){
+                               found = true;
+                               break;
+                       }
+                       visited.add(node);
+                       if(isTherePathVisit(visited, node, destination)){
+                               found = true;
+                               break;
+                       }
+               }
+       }
+       delete iterator;
+       return found;
+}
diff --git a/src/ASTAnalyses/Order/ordergraph.h b/src/ASTAnalyses/Order/ordergraph.h
new file mode 100644 (file)
index 0000000..a155c7f
--- /dev/null
@@ -0,0 +1,43 @@
+/*
+ * File:   ordergraph.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:42 PM
+ */
+
+#ifndef ORDERGRAPH_H
+#define ORDERGRAPH_H
+#include "classlist.h"
+#include "structs.h"
+#include "mymemory.h"
+
+class OrderGraph {
+public:
+       OrderGraph(Order *order);
+       ~OrderGraph();
+       void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+       void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+       OrderNode *getOrderNodeFromOrderGraph(uint64_t id);
+       OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+       OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id);
+       OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+       void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+       void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+       OrderEdge *getInverseOrderEdge(OrderEdge *edge);
+       Order *getOrder() {return order;} 
+       bool isTherePath(OrderNode* source, OrderNode* destination);
+       bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
+       SetIteratorOrderNode *getNodes() {return nodes->iterator();}
+       SetIteratorOrderEdge *getEdges() {return edges->iterator();}
+
+       CMEMALLOC;
+private:
+       HashsetOrderNode *nodes;
+       HashsetOrderEdge *edges;
+       Order *order;
+};
+
+OrderGraph *buildOrderGraph(Order *order);
+OrderGraph *buildMustOrderGraph(Order *order);
+#endif/* ORDERGRAPH_H */
+
diff --git a/src/ASTAnalyses/Order/ordernode.cc b/src/ASTAnalyses/Order/ordernode.cc
new file mode 100644 (file)
index 0000000..02f3146
--- /dev/null
@@ -0,0 +1,18 @@
+#include "ordernode.h"
+#include "orderedge.h"
+
+OrderNode::OrderNode(uint64_t _id) :
+       id(_id),
+       status(NOTVISITED),
+       sccNum(0),
+       inEdges(),
+       outEdges() {
+}
+
+void OrderNode::addNewIncomingEdge(OrderEdge *edge) {
+       inEdges.add(edge);
+}
+
+void OrderNode::addNewOutgoingEdge(OrderEdge *edge) {
+       outEdges.add(edge);
+}
diff --git a/src/ASTAnalyses/Order/ordernode.h b/src/ASTAnalyses/Order/ordernode.h
new file mode 100644 (file)
index 0000000..50543ac
--- /dev/null
@@ -0,0 +1,34 @@
+
+/*
+ * File:   ordernode.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:43 PM
+ */
+
+#ifndef ORDERNODE_H
+#define ORDERNODE_H
+
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "orderedge.h"
+
+enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
+typedef enum NodeStatus NodeStatus;
+
+class OrderNode {
+public:
+       OrderNode(uint64_t id);
+       void addNewIncomingEdge(OrderEdge *edge);
+       void addNewOutgoingEdge(OrderEdge *edge);
+
+       uint64_t id;
+       NodeStatus status;
+       uint sccNum;
+       HashsetOrderEdge inEdges;
+       HashsetOrderEdge outEdges;
+       CMEMALLOC;
+};
+#endif/* ORDERNODE_H */
+
diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
new file mode 100644 (file)
index 0000000..0be8066
--- /dev/null
@@ -0,0 +1,96 @@
+#include "polarityassignment.h"
+#include "csolver.h"
+
+void computePolarities(CSolver *This) {
+       SetIteratorBooleanEdge *iterator = This->getConstraints();
+       while (iterator->hasNext()) {
+               BooleanEdge boolean = iterator->next();
+               Boolean *b = boolean.getBoolean();
+               bool isNegated = boolean.isNegated();
+               computePolarity(b, isNegated ? P_FALSE : P_TRUE);
+       }
+       delete iterator;
+}
+
+bool updatePolarity(Boolean *This, Polarity polarity) {
+       Polarity oldpolarity = This->polarity;
+       Polarity newpolarity = (Polarity) (This->polarity | polarity);
+       This->polarity = newpolarity;
+       return newpolarity != oldpolarity;
+}
+
+void updateMustValue(Boolean *This, BooleanValue value) {
+       This->boolVal = (BooleanValue) (This->boolVal | value);
+}
+
+void computePolarity(Boolean *This, Polarity polarity) {
+       if (updatePolarity(This, polarity)) {
+               switch (This->type) {
+               case BOOLEANVAR:
+               case ORDERCONST:
+                       return;
+               case PREDICATEOP:
+                       return computePredicatePolarity((BooleanPredicate *)This);
+               case LOGICOP:
+                       return computeLogicOpPolarity((BooleanLogic *)This);
+               default:
+                       ASSERT(0);
+               }
+       }
+}
+
+void computePredicatePolarity(BooleanPredicate *This) {
+       if (This->undefStatus) {
+               computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
+       }
+}
+
+void computeLogicOpPolarity(BooleanLogic *This) {
+       Polarity child=computeLogicOpPolarityChildren(This);
+       uint size = This->inputs.getSize();
+       for (uint i = 0; i < size; i++) {
+               BooleanEdge b=This->inputs.get(i);
+               computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
+       }
+}
+
+Polarity negatePolarity(Polarity This) {
+       switch (This) {
+       case P_UNDEFINED:
+       case P_BOTHTRUEFALSE:
+               return This;
+       case P_TRUE:
+               return P_FALSE;
+       case P_FALSE:
+               return P_TRUE;
+       default:
+               ASSERT(0);
+       }
+}
+
+BooleanValue negateBooleanValue(BooleanValue This) {
+       switch (This) {
+       case BV_UNDEFINED:
+       case BV_UNSAT:
+               return This;
+       case BV_MUSTBETRUE:
+               return BV_MUSTBEFALSE;
+       case BV_MUSTBEFALSE:
+               return BV_MUSTBETRUE;
+       default:
+               ASSERT(0);
+       }
+}
+
+Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
+       switch (This->op) {
+       case SATC_AND: {
+               return This->polarity;
+       }
+       case SATC_IFF: {
+               return P_BOTHTRUEFALSE;
+       }
+       default:
+               ASSERT(0);
+       }
+}
diff --git a/src/ASTAnalyses/Polarity/polarityassignment.h b/src/ASTAnalyses/Polarity/polarityassignment.h
new file mode 100644 (file)
index 0000000..8873ef2
--- /dev/null
@@ -0,0 +1,26 @@
+/*
+ * File:   polarityassignment.h
+ * Author: hamed
+ *
+ * Created on August 6, 2017, 12:18 PM
+ */
+
+#ifndef POLARITYASSIGNMENT_H
+#define POLARITYASSIGNMENT_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "common.h"
+#include "ops.h"
+#include "boolean.h"
+
+void computePolarities(CSolver *This);
+bool updatePolarity(Boolean *This, Polarity polarity);
+void updateMustValue(Boolean *This, BooleanValue value);
+void computePolarity(Boolean *boolean, Polarity polarity);
+void computePredicatePolarity(BooleanPredicate *This);
+void computeLogicOpPolarity(BooleanLogic *boolean);
+Polarity negatePolarity(Polarity This);
+BooleanValue negateBooleanValue(BooleanValue This);
+Polarity computeLogicOpPolarityChildren(BooleanLogic *boolean);
+
+#endif/* POLARITYASSIGNMENT_H */
diff --git a/src/ASTAnalyses/orderanalysis.cc b/src/ASTAnalyses/orderanalysis.cc
deleted file mode 100644 (file)
index a77a1a8..0000000
+++ /dev/null
@@ -1,382 +0,0 @@
-#include "orderanalysis.h"
-#include "structs.h"
-#include "csolver.h"
-#include "boolean.h"
-#include "ordergraph.h"
-#include "order.h"
-#include "ordernode.h"
-#include "rewriter.h"
-#include "mutableset.h"
-#include "tunable.h"
-
-void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSNodeVisit(node, finishNodes, false, false, 0);
-                       node->status = FINISHED;
-                       finishNodes->push(node);
-               }
-       }
-       delete iterator;
-}
-
-void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       uint size = finishNodes->getSize();
-       uint sccNum = 1;
-       for (int i = size - 1; i >= 0; i--) {
-               OrderNode *node = finishNodes->get(i);
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSNodeVisit(node, NULL, true, false, sccNum);
-                       node->sccNum = sccNum;
-                       node->status = FINISHED;
-                       sccNum++;
-               }
-       }
-}
-
-void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
-       SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (mustvisit) {
-                       if (!edge->mustPos)
-                               continue;
-               } else
-               if (!edge->polPos && !edge->pseudoPos)  //Ignore edges that do not have positive polarity
-                       continue;
-
-               OrderNode *child = isReverse ? edge->source : edge->sink;
-
-               if (child->status == NOTVISITED) {
-                       child->status = VISITED;
-                       DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
-                       child->status = FINISHED;
-                       if (finishNodes != NULL)
-                               finishNodes->push(child);
-                       if (isReverse)
-                               child->sccNum = sccNum;
-               }
-       }
-       delete iterator;
-}
-
-void resetNodeInfoStatusSCC(OrderGraph *graph) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               iterator->next()->status = NOTVISITED;
-       }
-       delete iterator;
-}
-
-void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
-       Vector<OrderNode *> finishNodes;
-       DFS(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-       DFSReverse(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-}
-
-bool isMustBeTrueNode(OrderNode *node) {
-       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (!edge->mustPos) {
-                       delete iterator;
-                       return false;
-               }
-       }
-       delete iterator;
-       iterator = node->outEdges.iterator();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (!edge->mustPos) {
-                       delete iterator;
-                       return false;
-               }
-       }
-       delete iterator;
-       return true;
-}
-
-void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
-       SetIteratorOrderEdge *iterin = node->inEdges.iterator();
-       while (iterin->hasNext()) {
-               OrderEdge *inEdge = iterin->next();
-               OrderNode *srcNode = inEdge->source;
-               srcNode->outEdges.remove(inEdge);
-               SetIteratorOrderEdge *iterout = node->outEdges.iterator();
-               while (iterout->hasNext()) {
-                       OrderEdge *outEdge = iterout->next();
-                       OrderNode *sinkNode = outEdge->sink;
-                       sinkNode->inEdges.remove(outEdge);
-                       //Adding new edge to new sink and src nodes ...
-                       if(srcNode == sinkNode){
-                               This->setUnSAT();
-                               delete iterout;
-                               delete iterin;
-                               return;
-                       }
-                       OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
-                       newEdge->mustPos = true;
-                       newEdge->polPos = true;
-                       if (newEdge->mustNeg){
-                               This->setUnSAT();
-                       }
-                       srcNode->outEdges.add(newEdge);
-                       sinkNode->inEdges.add(newEdge);
-               }
-               delete iterout;
-       }
-       delete iterin;
-}
-
-void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               if (isMustBeTrueNode(node)) {
-                       bypassMustBeTrueNode(This, graph, node);
-               }
-       }
-       delete iterator;
-}
-
-/** This function computes a source set for every nodes, the set of
-    nodes that can reach that node via pospolarity edges.  It then
-    looks for negative polarity edges from nodes in the the source set
-    to determine whether we need to generate pseudoPos edges. */
-
-void completePartialOrderGraph(OrderGraph *graph) {
-       Vector<OrderNode *> finishNodes;
-       DFS(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-       HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-
-       Vector<OrderNode *> sccNodes;
-
-       uint size = finishNodes.getSize();
-       uint sccNum = 1;
-       for (int i = size - 1; i >= 0; i--) {
-               OrderNode *node = finishNodes.get(i);
-               HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
-               table->put(node, sources);
-
-               if (node->status == NOTVISITED) {
-                       //Need to do reverse traversal here...
-                       node->status = VISITED;
-                       DFSNodeVisit(node, &sccNodes, true, false, sccNum);
-                       node->status = FINISHED;
-                       node->sccNum = sccNum;
-                       sccNum++;
-                       sccNodes.push(node);
-
-                       //Compute in set for entire SCC
-                       uint rSize = sccNodes.getSize();
-                       for (uint j = 0; j < rSize; j++) {
-                               OrderNode *rnode = sccNodes.get(j);
-                               //Compute source sets
-                               SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
-                               while (iterator->hasNext()) {
-                                       OrderEdge *edge = iterator->next();
-                                       OrderNode *parent = edge->source;
-                                       if (edge->polPos) {
-                                               sources->add(parent);
-                                               HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
-                                               sources->addAll(parent_srcs);
-                                       }
-                               }
-                               delete iterator;
-                       }
-                       for (uint j = 0; j < rSize; j++) {
-                               //Copy in set of entire SCC
-                               OrderNode *rnode = sccNodes.get(j);
-                               HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
-                               table->put(rnode, set);
-
-                               //Use source sets to compute pseudoPos edges
-                               SetIteratorOrderEdge *iterator = node->inEdges.iterator();
-                               while (iterator->hasNext()) {
-                                       OrderEdge *edge = iterator->next();
-                                       OrderNode *parent = edge->source;
-                                       ASSERT(parent != rnode);
-                                       if (edge->polNeg && parent->sccNum != rnode->sccNum &&
-                                                       sources->contains(parent)) {
-                                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
-                                               newedge->pseudoPos = true;
-                                       }
-                               }
-                               delete iterator;
-                       }
-
-                       sccNodes.clear();
-               }
-       }
-
-       table->resetanddelete();
-       delete table;
-       resetNodeInfoStatusSCC(graph);
-}
-
-void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSNodeVisit(node, finishNodes, false, true, 0);
-                       node->status = FINISHED;
-                       finishNodes->push(node);
-               }
-       }
-       delete iterator;
-}
-
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
-       uint size = finishNodes->getSize();
-       HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-
-       for (int i = size - 1; i >= 0; i--) {
-               OrderNode *node = finishNodes->get(i);
-               HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
-               table->put(node, sources);
-
-               {
-                       //Compute source sets
-                       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
-                       while (iterator->hasNext()) {
-                               OrderEdge *edge = iterator->next();
-                               OrderNode *parent = edge->source;
-                               if (edge->mustPos) {
-                                       sources->add(parent);
-                                       HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
-                                       sources->addAll(parent_srcs);
-                               }
-                       }
-                       delete iterator;
-               }
-               if (computeTransitiveClosure) {
-                       //Compute full transitive closure for nodes
-                       SetIteratorOrderNode *srciterator = sources->iterator();
-                       while (srciterator->hasNext()) {
-                               OrderNode *srcnode = srciterator->next();
-                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
-                               newedge->mustPos = true;
-                               newedge->polPos = true;
-                               if (newedge->mustNeg)
-                                       solver->setUnSAT();
-                               srcnode->outEdges.add(newedge);
-                               node->inEdges.add(newedge);
-                       }
-                       delete srciterator;
-               }
-               {
-                       //Use source sets to compute mustPos edges
-                       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
-                       while (iterator->hasNext()) {
-                               OrderEdge *edge = iterator->next();
-                               OrderNode *parent = edge->source;
-                               if (!edge->mustPos && sources->contains(parent)) {
-                                       edge->mustPos = true;
-                                       edge->polPos = true;
-                                       if (edge->mustNeg)
-                                               solver->setUnSAT();
-                               }
-                       }
-                       delete iterator;
-               }
-               {
-                       //Use source sets to compute mustNeg for edges that would introduce cycle if true
-                       SetIteratorOrderEdge *iterator = node->outEdges.iterator();
-                       while (iterator->hasNext()) {
-                               OrderEdge *edge = iterator->next();
-                               OrderNode *child = edge->sink;
-                               if (!edge->mustNeg && sources->contains(child)) {
-                                       edge->mustNeg = true;
-                                       edge->polNeg = true;
-                                       if (edge->mustPos)
-                                               solver->setUnSAT();
-                               }
-                       }
-                       delete iterator;
-               }
-       }
-
-       table->resetanddelete();
-       delete table;
-}
-
-/* This function finds edges that would form a cycle with must edges
-   and forces them to be mustNeg.  It also decides whether an edge
-   must be true because of transitivity from other must be true
-   edges. */
-
-void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
-       Vector<OrderNode *> finishNodes;
-       //Topologically sort the mustPos edge graph
-       DFSMust(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-
-       //Find any backwards edges that complete cycles and force them to be mustNeg
-       DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
-}
-
-/* This function finds edges that must be positive and forces the
-   inverse edge to be negative (and clears its positive polarity if it
-   had one). */
-
-void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
-       SetIteratorOrderEdge *iterator = graph->getEdges();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (edge->mustPos) {
-                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
-                       if (invEdge != NULL) {
-                               if (!invEdge->mustPos) {
-                                       invEdge->polPos = false;
-                               } else {
-                                       solver->setUnSAT();
-                               }
-                               invEdge->mustNeg = true;
-                               invEdge->polNeg = true;
-                       }
-               }
-       }
-       delete iterator;
-}
-
-/** This finds edges that must be positive and forces the inverse edge
-    to be negative.  It also clears the negative flag of this edge.
-    It also finds edges that must be negative and clears the positive
-    polarity. */
-
-void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
-       SetIteratorOrderEdge *iterator = graph->getEdges();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (edge->mustPos) {
-                       if (!edge->mustNeg) {
-                               edge->polNeg = false;
-                       } else
-                               solver->setUnSAT();
-
-                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
-                       if (invEdge != NULL) {
-                               if (!invEdge->mustPos)
-                                       invEdge->polPos = false;
-                               else
-                                       solver->setUnSAT();
-
-                               invEdge->mustNeg = true;
-                               invEdge->polNeg = true;
-                       }
-               }
-               if (edge->mustNeg && !edge->mustPos) {
-                       edge->polPos = false;
-               }
-       }
-       delete iterator;
-}
diff --git a/src/ASTAnalyses/orderanalysis.h b/src/ASTAnalyses/orderanalysis.h
deleted file mode 100644 (file)
index b04ccfd..0000000
+++ /dev/null
@@ -1,24 +0,0 @@
-#ifndef ORDERANALYSIS_H
-#define ORDERANALYSIS_H
-#include "classlist.h"
-#include "structs.h"
-#include "mymemory.h"
-
-void computeStronglyConnectedComponentGraph(OrderGraph *graph);
-void initializeNodeInfoSCC(OrderGraph *graph);
-void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
-void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void completePartialOrderGraph(OrderGraph *graph);
-void resetNodeInfoStatusSCC(OrderGraph *graph);
-bool isMustBeTrueNode(OrderNode *node);
-void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node);
-void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
-void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
-void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
-void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
-void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
-
-#endif
-
diff --git a/src/ASTAnalyses/orderedge.cc b/src/ASTAnalyses/orderedge.cc
deleted file mode 100644 (file)
index c0cd678..0000000
+++ /dev/null
@@ -1,12 +0,0 @@
-#include "orderedge.h"
-#include "ordergraph.h"
-
-OrderEdge::OrderEdge(OrderNode *_source, OrderNode *_sink) {
-       source = _source;
-       sink = _sink;
-       polPos = false;
-       polNeg = false;
-       mustPos = false;
-       mustNeg = false;
-       pseudoPos = false;
-}
diff --git a/src/ASTAnalyses/orderedge.h b/src/ASTAnalyses/orderedge.h
deleted file mode 100644 (file)
index b10b781..0000000
+++ /dev/null
@@ -1,28 +0,0 @@
-/*
- * File:   orderedge.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:44 PM
- */
-
-#ifndef ORDEREDGE_H
-#define ORDEREDGE_H
-#include "classlist.h"
-#include "mymemory.h"
-
-class OrderEdge {
-public:
-       OrderEdge(OrderNode *begin, OrderNode *end);
-
-       OrderNode *source;
-       OrderNode *sink;
-       unsigned int polPos : 1;
-       unsigned int polNeg : 1;
-       unsigned int mustPos : 1;
-       unsigned int mustNeg : 1;
-       unsigned int pseudoPos : 1;
-       CMEMALLOC;
-};
-
-#endif/* ORDEREDGE_H */
-
diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
deleted file mode 100644 (file)
index ce9a071..0000000
+++ /dev/null
@@ -1,227 +0,0 @@
-#include "ordergraph.h"
-#include "ordernode.h"
-#include "boolean.h"
-#include "orderedge.h"
-#include "ordergraph.h"
-#include "order.h"
-
-OrderGraph::OrderGraph(Order *_order) :
-       nodes(new HashsetOrderNode()),
-       edges(new HashsetOrderEdge()),
-       order(_order) {
-}
-
-OrderGraph *buildOrderGraph(Order *order) {
-       OrderGraph *orderGraph = new OrderGraph(order);
-       order->graph = orderGraph;
-       uint constrSize = order->constraints.getSize();
-       for (uint j = 0; j < constrSize; j++) {
-               orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
-       }
-       return orderGraph;
-}
-
-//Builds only the subgraph for the must order graph.
-OrderGraph *buildMustOrderGraph(Order *order) {
-       OrderGraph *orderGraph = new OrderGraph(order);
-       uint constrSize = order->constraints.getSize();
-       for (uint j = 0; j < constrSize; j++) {
-               orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
-       }
-       return orderGraph;
-}
-
-void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
-       Polarity polarity = constr->polarity;
-       BooleanValue mustval = constr->boolVal;
-       switch (polarity) {
-       case P_BOTHTRUEFALSE:
-       case P_TRUE: {
-               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
-               if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
-                       _1to2->mustPos = true;
-               _1to2->polPos = true;
-               node1->addNewOutgoingEdge(_1to2);
-               node2->addNewIncomingEdge(_1to2);
-               if (constr->polarity == P_TRUE)
-                       break;
-       }
-       case P_FALSE: {
-               if (order->type == SATC_TOTAL) {
-                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
-                       if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
-                               _2to1->mustPos = true;
-                       _2to1->polPos = true;
-                       node2->addNewOutgoingEdge(_2to1);
-                       node1->addNewIncomingEdge(_2to1);
-               } else {
-                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
-                       if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
-                               _1to2->mustNeg = true;
-                       _1to2->polNeg = true;
-                       node1->addNewOutgoingEdge(_1to2);
-                       node2->addNewIncomingEdge(_1to2);
-               }
-               break;
-       }
-       case P_UNDEFINED:
-               //There is an unreachable order constraint if this assert fires
-               //Clients can easily do this, so don't do anything.
-               ;
-       }
-}
-
-void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
-       BooleanValue mustval = constr->boolVal;
-       switch (mustval) {
-       case BV_UNSAT:
-       case BV_MUSTBETRUE: {
-               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
-               _1to2->mustPos = true;
-               _1to2->polPos = true;
-               node1->addNewOutgoingEdge(_1to2);
-               node2->addNewIncomingEdge(_1to2);
-               if (constr->boolVal == BV_MUSTBETRUE)
-                       break;
-       }
-       case BV_MUSTBEFALSE: {
-               if (order->type == SATC_TOTAL) {
-                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
-                       _2to1->mustPos = true;
-                       _2to1->polPos = true;
-                       node2->addNewOutgoingEdge(_2to1);
-                       node1->addNewIncomingEdge(_2to1);
-               } else {
-                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
-                       _1to2->mustNeg = true;
-                       _1to2->polNeg = true;
-                       node1->addNewOutgoingEdge(_1to2);
-                       node2->addNewIncomingEdge(_1to2);
-               }
-               break;
-       }
-       case BV_UNDEFINED:
-               //Do Nothing
-               break;
-       }
-}
-
-OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
-       OrderNode *node = new OrderNode(id);
-       OrderNode *tmp = nodes->get(node);
-       if ( tmp != NULL) {
-               delete node;
-               node = tmp;
-       } else {
-               nodes->add(node);
-       }
-       return node;
-}
-
-OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
-       OrderNode node(id);
-       OrderNode *tmp = nodes->get(&node);
-       return tmp;
-}
-
-OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
-       OrderEdge *edge = new OrderEdge(begin, end);
-       OrderEdge *tmp = edges->get(edge);
-       if ( tmp != NULL ) {
-               delete edge;
-               edge = tmp;
-       } else {
-               edges->add(edge);
-       }
-       return edge;
-}
-
-OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
-       OrderEdge edge(begin, end);
-       OrderEdge *tmp = edges->get(&edge);
-       return tmp;
-}
-
-OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
-       OrderEdge inverseedge(edge->sink, edge->source);
-       OrderEdge *tmp = edges->get(&inverseedge);
-       return tmp;
-}
-
-void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
-       OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
-       OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
-       addOrderEdge(from, to, bOrder);
-}
-
-void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
-       OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
-       OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
-       addMustOrderEdge(from, to, bOrder);
-}
-
-OrderGraph::~OrderGraph() {
-       SetIteratorOrderNode *iterator = nodes->iterator();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               delete node;
-       }
-       delete iterator;
-
-       SetIteratorOrderEdge *eiterator = edges->iterator();
-       while (eiterator->hasNext()) {
-               OrderEdge *edge = eiterator->next();
-               delete edge;
-       }
-       delete eiterator;
-       delete nodes;
-       delete edges;
-}
-
-bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
-       HashsetOrderNode visited;
-       visited.add(source);
-       SetIteratorOrderEdge *iterator = source->outEdges.iterator();
-       bool found = false;
-       while(iterator->hasNext()){
-               OrderEdge* edge = iterator->next();
-               if(edge->polPos){
-                       OrderNode* node = edge->sink;
-                       if(!visited.contains(node)){
-                               if( node == destination ){
-                                       found = true;
-                                       break;
-                               }
-                               visited.add(node);
-                               found =isTherePathVisit(visited, node, destination);
-                               if(found){
-                                       break;
-                               }
-                       }
-               }
-       }
-       delete iterator;
-       return found;
-}
-
-bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
-       SetIteratorOrderEdge *iterator = current->outEdges.iterator();
-       bool found = false;
-       while(iterator->hasNext()){
-               OrderEdge* edge = iterator->next();
-               if(edge->polPos){
-                       OrderNode* node = edge->sink;
-                       if(node == destination){
-                               found = true;
-                               break;
-                       }
-                       visited.add(node);
-                       if(isTherePathVisit(visited, node, destination)){
-                               found = true;
-                               break;
-                       }
-               }
-       }
-       delete iterator;
-       return found;
-}
diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h
deleted file mode 100644 (file)
index a155c7f..0000000
+++ /dev/null
@@ -1,43 +0,0 @@
-/*
- * File:   ordergraph.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:42 PM
- */
-
-#ifndef ORDERGRAPH_H
-#define ORDERGRAPH_H
-#include "classlist.h"
-#include "structs.h"
-#include "mymemory.h"
-
-class OrderGraph {
-public:
-       OrderGraph(Order *order);
-       ~OrderGraph();
-       void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
-       void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder);
-       OrderNode *getOrderNodeFromOrderGraph(uint64_t id);
-       OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
-       OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id);
-       OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
-       void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-       void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-       OrderEdge *getInverseOrderEdge(OrderEdge *edge);
-       Order *getOrder() {return order;} 
-       bool isTherePath(OrderNode* source, OrderNode* destination);
-       bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
-       SetIteratorOrderNode *getNodes() {return nodes->iterator();}
-       SetIteratorOrderEdge *getEdges() {return edges->iterator();}
-
-       CMEMALLOC;
-private:
-       HashsetOrderNode *nodes;
-       HashsetOrderEdge *edges;
-       Order *order;
-};
-
-OrderGraph *buildOrderGraph(Order *order);
-OrderGraph *buildMustOrderGraph(Order *order);
-#endif/* ORDERGRAPH_H */
-
diff --git a/src/ASTAnalyses/ordernode.cc b/src/ASTAnalyses/ordernode.cc
deleted file mode 100644 (file)
index 02f3146..0000000
+++ /dev/null
@@ -1,18 +0,0 @@
-#include "ordernode.h"
-#include "orderedge.h"
-
-OrderNode::OrderNode(uint64_t _id) :
-       id(_id),
-       status(NOTVISITED),
-       sccNum(0),
-       inEdges(),
-       outEdges() {
-}
-
-void OrderNode::addNewIncomingEdge(OrderEdge *edge) {
-       inEdges.add(edge);
-}
-
-void OrderNode::addNewOutgoingEdge(OrderEdge *edge) {
-       outEdges.add(edge);
-}
diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h
deleted file mode 100644 (file)
index 50543ac..0000000
+++ /dev/null
@@ -1,34 +0,0 @@
-
-/*
- * File:   ordernode.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:43 PM
- */
-
-#ifndef ORDERNODE_H
-#define ORDERNODE_H
-
-#include "classlist.h"
-#include "mymemory.h"
-#include "structs.h"
-#include "orderedge.h"
-
-enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
-typedef enum NodeStatus NodeStatus;
-
-class OrderNode {
-public:
-       OrderNode(uint64_t id);
-       void addNewIncomingEdge(OrderEdge *edge);
-       void addNewOutgoingEdge(OrderEdge *edge);
-
-       uint64_t id;
-       NodeStatus status;
-       uint sccNum;
-       HashsetOrderEdge inEdges;
-       HashsetOrderEdge outEdges;
-       CMEMALLOC;
-};
-#endif/* ORDERNODE_H */
-
diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
deleted file mode 100644 (file)
index 0be8066..0000000
+++ /dev/null
@@ -1,96 +0,0 @@
-#include "polarityassignment.h"
-#include "csolver.h"
-
-void computePolarities(CSolver *This) {
-       SetIteratorBooleanEdge *iterator = This->getConstraints();
-       while (iterator->hasNext()) {
-               BooleanEdge boolean = iterator->next();
-               Boolean *b = boolean.getBoolean();
-               bool isNegated = boolean.isNegated();
-               computePolarity(b, isNegated ? P_FALSE : P_TRUE);
-       }
-       delete iterator;
-}
-
-bool updatePolarity(Boolean *This, Polarity polarity) {
-       Polarity oldpolarity = This->polarity;
-       Polarity newpolarity = (Polarity) (This->polarity | polarity);
-       This->polarity = newpolarity;
-       return newpolarity != oldpolarity;
-}
-
-void updateMustValue(Boolean *This, BooleanValue value) {
-       This->boolVal = (BooleanValue) (This->boolVal | value);
-}
-
-void computePolarity(Boolean *This, Polarity polarity) {
-       if (updatePolarity(This, polarity)) {
-               switch (This->type) {
-               case BOOLEANVAR:
-               case ORDERCONST:
-                       return;
-               case PREDICATEOP:
-                       return computePredicatePolarity((BooleanPredicate *)This);
-               case LOGICOP:
-                       return computeLogicOpPolarity((BooleanLogic *)This);
-               default:
-                       ASSERT(0);
-               }
-       }
-}
-
-void computePredicatePolarity(BooleanPredicate *This) {
-       if (This->undefStatus) {
-               computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
-       }
-}
-
-void computeLogicOpPolarity(BooleanLogic *This) {
-       Polarity child=computeLogicOpPolarityChildren(This);
-       uint size = This->inputs.getSize();
-       for (uint i = 0; i < size; i++) {
-               BooleanEdge b=This->inputs.get(i);
-               computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
-       }
-}
-
-Polarity negatePolarity(Polarity This) {
-       switch (This) {
-       case P_UNDEFINED:
-       case P_BOTHTRUEFALSE:
-               return This;
-       case P_TRUE:
-               return P_FALSE;
-       case P_FALSE:
-               return P_TRUE;
-       default:
-               ASSERT(0);
-       }
-}
-
-BooleanValue negateBooleanValue(BooleanValue This) {
-       switch (This) {
-       case BV_UNDEFINED:
-       case BV_UNSAT:
-               return This;
-       case BV_MUSTBETRUE:
-               return BV_MUSTBEFALSE;
-       case BV_MUSTBEFALSE:
-               return BV_MUSTBETRUE;
-       default:
-               ASSERT(0);
-       }
-}
-
-Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
-       switch (This->op) {
-       case SATC_AND: {
-               return This->polarity;
-       }
-       case SATC_IFF: {
-               return P_BOTHTRUEFALSE;
-       }
-       default:
-               ASSERT(0);
-       }
-}
diff --git a/src/ASTAnalyses/polarityassignment.h b/src/ASTAnalyses/polarityassignment.h
deleted file mode 100644 (file)
index 8873ef2..0000000
+++ /dev/null
@@ -1,26 +0,0 @@
-/*
- * File:   polarityassignment.h
- * Author: hamed
- *
- * Created on August 6, 2017, 12:18 PM
- */
-
-#ifndef POLARITYASSIGNMENT_H
-#define POLARITYASSIGNMENT_H
-#include "classlist.h"
-#include "mymemory.h"
-#include "common.h"
-#include "ops.h"
-#include "boolean.h"
-
-void computePolarities(CSolver *This);
-bool updatePolarity(Boolean *This, Polarity polarity);
-void updateMustValue(Boolean *This, BooleanValue value);
-void computePolarity(Boolean *boolean, Polarity polarity);
-void computePredicatePolarity(BooleanPredicate *This);
-void computeLogicOpPolarity(BooleanLogic *boolean);
-Polarity negatePolarity(Polarity This);
-BooleanValue negateBooleanValue(BooleanValue This);
-Polarity computeLogicOpPolarityChildren(BooleanLogic *boolean);
-
-#endif/* POLARITYASSIGNMENT_H */
index e6699e6..442a1c6 100644 (file)
@@ -4,16 +4,16 @@ PHONY += directories
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
 
-C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c)
+C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c)
 
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
 
 CFLAGS := -Wall -g -O0
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner
 LDFLAGS := -ldl -lrt -rdynamic
 SHARED := -shared
 
@@ -33,6 +33,8 @@ ${OBJ_DIR}:
        ${MKDIR_P} ${OBJ_DIR}
        ${MKDIR_P} ${OBJ_DIR}/AST
        ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses
+       ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses/Order
+       ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses/Polarity
        ${MKDIR_P} ${OBJ_DIR}/ASTTransform
        ${MKDIR_P} ${OBJ_DIR}/Translator
        ${MKDIR_P} ${OBJ_DIR}/Tuner
@@ -75,10 +77,10 @@ tags:
        ctags -R
 
 tabbing:
-       uncrustify -c C.cfg --no-backup *.cc */*.cc
-       uncrustify -c C.cfg --no-backup *.h */*.h
+       uncrustify -c C.cfg --no-backup *.cc */*.cc */*/*.cc
+       uncrustify -c C.cfg --no-backup *.h */*.h */*/*.h
 
 wc:
-       wc */*.cc */*.h *.cc *.h
+       wc */*.cc */*.h *.cc *.h */*/*.cc */*/*.h
 
 .PHONY: $(PHONY)