src/Backend/nodeedge.h

   1 #ifndef NODEEDGE_H
   2 #define NODEEDGE_H
   3 #include "classlist.h"
   4 #include "vector.h"
   5
   6 #define NEGATE_EDGE 1
   7 #define EDGE_IS_VAR_CONSTANT 2
   8 #define VAR_SHIFT 2
   9 #define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
  10
  11 struct Edge;
  12 typedef struct Edge Edge;
  13
  14 struct Node;
  15 typedef struct Node Node;
  16
  17 struct Edge {
  18         Node * node_ptr;
  19 };
  20
  21 VectorDef(Edge, Edge)
  22
  23 enum NodeType {
  24         NodeType_AND,
  25         NodeType_ITE,
  26         NodeType_IFF
  27 };
  28
  29 typedef enum NodeType NodeType;
  30
  31 struct NodeFlags {
  32         NodeType type:2;
  33         int wasExpanded:2;
  34 };
  35
  36 typedef struct NodeFlags NodeFlags;
  37
  38 struct Node {
  39         NodeFlags flags;
  40         uint numEdges;
  41         uint hashCode;
  42         uint intAnnot[2];
  43         void * ptrAnnot[2];
  44         Edge edges[];
  45 };
  46
  47 #define DEFAULT_CNF_ARRAY_SIZE 256
  48 #define LOAD_FACTOR 0.25
  49 #define enableMatching 1
  50
  51 struct CNF {
  52         uint varcount;
  53         uint capacity;
  54         uint size;
  55         uint mask;
  56         uint maxsize;
  57         Node ** node_array;
  58         VectorEdge constraints;
  59 };
  60
  61 typedef struct CNF CNF;
  62
  63 static inline bool getExpanded(Node *n, int isNegated) {
  64         return n->flags.wasExpanded & (1<<isNegated);
  65 }
  66
  67 static inline void setExpanded(Node *n, int isNegated) {
  68         n->flags.wasExpanded |= (1<<isNegated);
  69 }
  70
  71 static inline Edge constraintNegate(Edge e) {
  72         Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
  73         return enew;
  74 }
  75
  76 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
  77         return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
  78 }
  79
  80 static inline bool sameSignEdge(Edge e1, Edge e2) {
  81         return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
  82 }
  83
  84 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
  85         return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
  86 }
  87
  88 static inline bool isNegEdge(Edge e) {
  89         return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
  90 }
  91
  92 static inline bool isNodeEdge(Edge e) {
  93         return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
  94 }
  95
  96 static inline bool isNegNodeEdge(Edge e) {
  97         return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
  98 }
  99
 100 static inline Node * getNodePtrFromEdge(Edge e) {
 101         return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
 102 }
 103
 104 static inline NodeType getNodeType(Edge e) {
 105         Node * n=getNodePtrFromEdge(e);
 106         return n->flags.type;
 107 }
 108
 109 static inline bool equalsEdge(Edge e1, Edge e2) {
 110         return e1.node_ptr == e2.node_ptr;
 111 }
 112
 113 static inline bool ltEdge(Edge e1, Edge e2) {
 114         return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
 115 }
 116
 117 static inline uint getNodeSize(Edge e) {
 118         Node * n=getNodePtrFromEdge(e);
 119         return n->numEdges;
 120 }
 121
 122 static inline Edge * getEdgeArray(Edge e) {
 123         Node * n=getNodePtrFromEdge(e);
 124         return n->edges;
 125 }
 126
 127 static inline Edge getNonNeg(Edge e) {
 128         Edge enew={(Node *)(((uintptr_t)e.node_ptr)&(~((uintptr_t)NEGATE_EDGE)))};
 129         return enew;
 130 }
 131
 132 static inline bool edgeIsConst(Edge e) {
 133         return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 134 }
 135
 136 static inline bool edgeIsVarConst(Edge e) {
 137         return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
 138 }
 139
 140 uint hashNode(NodeType type, uint numEdges, Edge * edges);
 141 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
 142 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
 143 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges);
 144 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges);
 145 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges);
 146 Edge constraintOR2(CNF * cnf, Edge left, Edge right);
 147 Edge constraintAND2(CNF * cnf, Edge left, Edge right);
 148 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
 149 Edge constraintIFF(CNF * cnf, Edge left, Edge right);
 150 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
 151 Edge constraintNewVar(CNF *cnf);
 152 void countPass(CNF *cnf);
 153 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
 154
 155
 156 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 157 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
 158 #endif