(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...
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
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
+
+--------------------------------------------------------------------
+
+
--- /dev/null
+#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;
+}
--- /dev/null
+#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
+
--- /dev/null
+#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;
+}
--- /dev/null
+/*
+ * 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 */
+
--- /dev/null
+#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()){
+ OrderNode* node = iterator->next()->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()){
+ OrderNode* node = iterator->next()->sink;
+ if(node == destination){
+ found = true;
+ break;
+ }
+ visited.add(node);
+ if(isTherePathVisit(visited, node, destination)){
+ found = true;
+ break;
+ }
+ }
+ delete iterator;
+ return found;
+}
--- /dev/null
+/*
+ * 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 */
+
--- /dev/null
+#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);
+}
--- /dev/null
+
+/*
+ * 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 */
+
--- /dev/null
+#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);
+ }
+}
--- /dev/null
+/*
+ * 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 */
+++ /dev/null
-#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;
-}
+++ /dev/null
-#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
-
+++ /dev/null
-#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;
-}
+++ /dev/null
-/*
- * 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 */
-
+++ /dev/null
-#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()){
- OrderNode* node = iterator->next()->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()){
- OrderNode* node = iterator->next()->sink;
- if(node == destination){
- found = true;
- break;
- }
- visited.add(node);
- if(isTherePathVisit(visited, node, destination)){
- found = true;
- break;
- }
- }
- delete iterator;
- return found;
-}
+++ /dev/null
-/*
- * 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 */
-
+++ /dev/null
-#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);
-}
+++ /dev/null
-
-/*
- * 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 */
-
+++ /dev/null
-#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);
- }
-}
+++ /dev/null
-/*
- * 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 */
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
${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
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)
void * ourrealloc(void *ptr, size_t size);
*/
-#if 1
+#if 0
void * model_malloc(size_t size);
void model_free(void *ptr);
void * model_calloc(size_t count, size_t size);