src/Backend/nodeedge.h

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