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 typedef int Literal;
  12
  13 struct Edge;
  14 typedef struct Edge Edge;
  15
  16 struct Node;
  17 typedef struct Node Node;
  18
  19 struct Edge {
  20         Node * node_ptr;
  21 };
  22
  23 VectorDef(Edge, Edge)
  24
  25 enum NodeType {
  26         NodeType_AND,
  27         NodeType_ITE,
  28         NodeType_IFF
  29 };
  30
  31 typedef enum NodeType NodeType;
  32
  33 struct NodeFlags {
  34         NodeType type:2;
  35         int varForced:1;
  36         int wasExpanded:2;
  37         int cnfVisitedDown:2;
  38         int cnfVisitedUp:2;
  39 };
  40
  41 typedef struct NodeFlags NodeFlags;
  42
  43 struct Node {
  44         NodeFlags flags;
  45         uint numEdges;
  46         uint hashCode;
  47         uint intAnnot[2];
  48         void * ptrAnnot[2];
  49         Edge edges[];
  50 };
  51
  52 #define DEFAULT_CNF_ARRAY_SIZE 256
  53 #define LOAD_FACTOR 0.25
  54
  55 struct CNF {
  56         uint varcount;
  57         uint capacity;
  58         uint size;
  59         uint mask;
  60         uint maxsize;
  61         bool enableMatching;
  62         Node ** node_array;
  63         IncrementalSolver * solver;
  64         VectorEdge constraints;
  65         VectorEdge args;
  66 };
  67
  68 typedef struct CNF CNF;
  69
  70 struct CNFExpr;
  71 typedef struct CNFExpr CNFExpr;
  72
  73 static inline bool getExpanded(Node *n, int isNegated) {
  74         return n->flags.wasExpanded & (1<<isNegated);
  75 }
  76
  77 static inline void setExpanded(Node *n, int isNegated) {
  78         n->flags.wasExpanded |= (1<<isNegated);
  79 }
  80
  81 static inline Edge constraintNegate(Edge e) {
  82         Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
  83         return enew;
  84 }
  85
  86 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
  87         return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
  88 }
  89
  90 static inline bool sameSignEdge(Edge e1, Edge e2) {
  91         return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
  92 }
  93
  94 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
  95         return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
  96 }
  97
  98 static inline bool isNegEdge(Edge e) {
  99         return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
 100 }
 101
 102 static inline bool isPosEdge(Edge e) {
 103         return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
 104 }
 105
 106 static inline bool isNodeEdge(Edge e) {
 107         return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
 108 }
 109
 110 static inline bool isNegNodeEdge(Edge e) {
 111         return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
 112 }
 113
 114 static inline Node * getNodePtrFromEdge(Edge e) {
 115         return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
 116 }
 117
 118 static inline NodeType getNodeType(Edge e) {
 119         Node * n=getNodePtrFromEdge(e);
 120         return n->flags.type;
 121 }
 122
 123 static inline bool equalsEdge(Edge e1, Edge e2) {
 124         return e1.node_ptr == e2.node_ptr;
 125 }
 126
 127 static inline bool ltEdge(Edge e1, Edge e2) {
 128         return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
 129 }
 130
 131 static inline uint getNodeSize(Edge e) {
 132         Node * n=getNodePtrFromEdge(e);
 133         return n->numEdges;
 134 }
 135
 136 static inline Edge * getEdgeArray(Edge e) {
 137         Node * n=getNodePtrFromEdge(e);
 138         return n->edges;
 139 }
 140
 141 static inline Edge getNonNeg(Edge e) {
 142         Edge enew={(Node *)(((uintptr_t)e.node_ptr)&(~((uintptr_t)NEGATE_EDGE)))};
 143         return enew;
 144 }
 145
 146 static inline bool edgeIsConst(Edge e) {
 147         return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 148 }
 149
 150 static inline bool edgeIsNull(Edge e) {
 151         return e.node_ptr == NULL;
 152 }
 153
 154 static inline bool edgeIsVarConst(Edge e) {
 155         return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
 156 }
 157
 158 static inline Edge constraintNegateIf(Edge e, bool negate) {
 159         Edge eret={(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
 160         return eret;
 161 }
 162
 163 static inline Literal getEdgeVar(Edge e) {
 164         int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
 165         return isNegEdge(e) ? -val : val;
 166 }
 167
 168 static inline bool isProxy(CNFExpr *expr) {
 169         return (bool) (((intptr_t) expr) & 1);
 170 }
 171
 172 static inline Literal getProxy(CNFExpr *expr) {
 173         return (Literal) (((intptr_t) expr) >> 1);
 174 }
 175
 176 uint hashNode(NodeType type, uint numEdges, Edge * edges);
 177 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
 178 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
 179 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges);
 180 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges);
 181 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges);
 182 Edge constraintOR2(CNF * cnf, Edge left, Edge right);
 183 Edge constraintAND2(CNF * cnf, Edge left, Edge right);
 184 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
 185 Edge constraintIFF(CNF * cnf, Edge left, Edge right);
 186 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
 187 Edge constraintNewVar(CNF *cnf);
 188 void countPass(CNF *cnf);
 189 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
 190 void convertPass(CNF *cnf, bool backtrackLit);
 191 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
 192 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
 193 void produceCNF(CNF * cnf, Edge e);
 194 CNFExpr * produceConjunction(CNF * cnf, Edge e);
 195 CNFExpr* produceDisjunction(CNF *cnf, Edge e);
 196 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
 197 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
 198 CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
 199 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);
 200 void outputCNF(CNF *cnf, CNFExpr *expr);
 201
 202 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 203 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
 204 #endif