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