src/Backend/constraint.h

   1 #ifndef CONSTRAINT_H
   2 #define CONSTRAINT_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 64
  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         long long solveTime;
  67         long long encodeTime;
  68 };
  69
  70 typedef struct CNF CNF;
  71
  72 struct CNFExpr;
  73 typedef struct CNFExpr CNFExpr;
  74
  75 static inline bool getExpanded(Node *n, int isNegated) {
  76         return n->flags.wasExpanded & (1 << isNegated);
  77 }
  78
  79 static inline void setExpanded(Node *n, int isNegated) {
  80         n->flags.wasExpanded |= (1 << isNegated);
  81 }
  82
  83 static inline Edge constraintNegate(Edge e) {
  84         Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
  85         return enew;
  86 }
  87
  88 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
  89         return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~(uintptr_t) NEGATE_EDGE));
  90 }
  91
  92 static inline bool sameSignEdge(Edge e1, Edge e2) {
  93         return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
  94 }
  95
  96 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
  97         return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
  98 }
  99
 100 static inline bool isNegEdge(Edge e) {
 101         return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
 102 }
 103
 104 static inline bool isPosEdge(Edge e) {
 105         return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
 106 }
 107
 108 static inline bool isNodeEdge(Edge e) {
 109         return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
 110 }
 111
 112 static inline bool isNegNodeEdge(Edge e) {
 113         return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
 114 }
 115
 116 static inline Node *getNodePtrFromEdge(Edge e) {
 117         return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
 118 }
 119
 120 static inline NodeType getNodeType(Edge e) {
 121         Node *n = getNodePtrFromEdge(e);
 122         return n->flags.type;
 123 }
 124
 125 static inline bool equalsEdge(Edge e1, Edge e2) {
 126         return e1.node_ptr == e2.node_ptr;
 127 }
 128
 129 static inline bool ltEdge(Edge e1, Edge e2) {
 130         return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
 131 }
 132
 133 static inline uint getNodeSize(Edge e) {
 134         Node *n = getNodePtrFromEdge(e);
 135         return n->numEdges;
 136 }
 137
 138 static inline Edge *getEdgeArray(Edge e) {
 139         Node *n = getNodePtrFromEdge(e);
 140         return n->edges;
 141 }
 142
 143 static inline Edge getNonNeg(Edge e) {
 144         Edge enew = {(Node *)(((uintptr_t)e.node_ptr) & (~((uintptr_t)NEGATE_EDGE)))};
 145         return enew;
 146 }
 147
 148 static inline bool edgeIsConst(Edge e) {
 149         return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 150 }
 151
 152 static inline bool edgeIsNull(Edge e) {
 153         return e.node_ptr == NULL;
 154 }
 155
 156 static inline bool edgeIsVarConst(Edge e) {
 157         return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
 158 }
 159
 160 static inline Edge constraintNegateIf(Edge e, bool negate) {
 161         Edge eret = {(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
 162         return eret;
 163 }
 164
 165 static inline Literal getEdgeVar(Edge e) {
 166         int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
 167         return isNegEdge(e) ? -val : val;
 168 }
 169
 170 static inline bool isProxy(CNFExpr *expr) {
 171         return (bool) (((intptr_t) expr) & 1);
 172 }
 173
 174 static inline Literal getProxy(CNFExpr *expr) {
 175         return (Literal) (((intptr_t) expr) >> 1);
 176 }
 177
 178 CNF *createCNF();
 179 void deleteCNF(CNF *cnf);
 180 void resetCNF(CNF *cnf);
 181
 182 uint hashNode(NodeType type, uint numEdges, Edge *edges);
 183 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashCode);
 184 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
 185 Edge create(CNF *cnf, NodeType type, uint numEdges, Edge *edges);
 186 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
 187 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges);
 188 Edge constraintOR2(CNF *cnf, Edge left, Edge right);
 189 Edge constraintAND2(CNF *cnf, Edge left, Edge right);
 190 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right);
 191 Edge constraintIFF(CNF *cnf, Edge left, Edge right);
 192 static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,right));}
 193 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge);
 194 Edge constraintNewVar(CNF *cnf);
 195 void countPass(CNF *cnf);
 196 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e);
 197 void addConstraintCNF(CNF *cnf, Edge constraint);
 198 int solveCNF(CNF *cnf);
 199 bool getValueCNF(CNF *cnf, Edge var);
 200 void printCNF(Edge e);
 201
 202 void convertPass(CNF *cnf, bool backtrackLit);
 203 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
 204 void constrainCNF(CNF *cnf, Literal l, CNFExpr *exp);
 205 void produceCNF(CNF *cnf, Edge e);
 206 CNFExpr *produceConjunction(CNF *cnf, Edge e);
 207 CNFExpr *produceDisjunction(CNF *cnf, Edge e);
 208 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate);
 209 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign);
 210 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge);
 211 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg);
 212 void outputCNF(CNF *cnf, CNFExpr *expr);
 213
 214 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 215 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 216 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 217 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 218 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 219
 220 extern Edge E_True;
 221 extern Edge E_False;
 222 extern Edge E_BOGUS;
 223 extern Edge E_NULL;
 224 #endif