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 Node {
  34         uint numEdges;
  35         uint numVars;
  36         union {
  37                 NodeType type;
  38                 uint capacity;
  39         };
  40         Edge edges[];
  41 };
  42
  43 typedef struct Node Node;
  44
  45 #define DEFAULT_CNF_ARRAY_SIZE 2048
  46
  47 struct CNF {
  48         uint varcount;
  49         uint clausecount;
  50         uint asize;
  51         IncrementalSolver *solver;
  52         int *array;
  53         long long solveTime;
  54         long long encodeTime;
  55         bool unsat;
  56 };
  57
  58 typedef struct CNF CNF;
  59
  60 static inline Edge constraintNegate(Edge e) {
  61         Edge eneg = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
  62         return eneg;
  63 }
  64
  65 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
  66         return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~(uintptr_t) NEGATE_EDGE));
  67 }
  68
  69 static inline bool sameSignEdge(Edge e1, Edge e2) {
  70         return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
  71 }
  72
  73 static inline bool sameNodeOppSign(Edge e1, Edge e2) {
  74         return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
  75 }
  76
  77 static inline bool isNegEdge(Edge e) {
  78         return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
  79 }
  80
  81 static inline bool isPosEdge(Edge e) {
  82         return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
  83 }
  84
  85 static inline bool isNodeEdge(Edge e) {
  86         return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
  87 }
  88
  89 static inline bool isNegNodeEdge(Edge e) {
  90         return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
  91 }
  92
  93 static inline bool isPosNodeEdge(Edge e) {
  94         return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == 0;
  95 }
  96
  97 static inline Node *getNodePtrFromEdge(Edge e) {
  98         return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
  99 }
 100
 101 static inline NodeType getNodeType(Edge e) {
 102         Node *n = getNodePtrFromEdge(e);
 103         return n->type;
 104 }
 105
 106 static inline bool equalsEdge(Edge e1, Edge e2) {
 107         return e1.node_ptr == e2.node_ptr;
 108 }
 109
 110 static inline bool ltEdge(Edge e1, Edge e2) {
 111         return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
 112 }
 113
 114 static inline uint getNodeSize(Edge e) {
 115         Node *n = getNodePtrFromEdge(e);
 116         return n->numEdges;
 117 }
 118
 119 static inline Edge *getEdgeArray(Edge e) {
 120         Node *n = getNodePtrFromEdge(e);
 121         return n->edges;
 122 }
 123
 124 static inline Edge getNonNeg(Edge e) {
 125         Edge enew = {(Node *)(((uintptr_t)e.node_ptr) & (~((uintptr_t)NEGATE_EDGE)))};
 126         return enew;
 127 }
 128
 129 static inline bool edgeIsConst(Edge e) {
 130         return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 131 }
 132
 133 static inline bool edgeIsNull(Edge e) {
 134         return e.node_ptr == NULL;
 135 }
 136
 137 static inline bool edgeIsVarConst(Edge e) {
 138         return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
 139 }
 140
 141 static inline Edge constraintNegateIf(Edge e, bool negate) {
 142         Edge eret = {(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
 143         return eret;
 144 }
 145
 146 static inline Literal getEdgeVar(Edge e) {
 147         int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
 148         return isNegEdge(e) ? -val : val;
 149 }
 150
 151 CNF *createCNF();
 152 void deleteCNF(CNF *cnf);
 153 void resetCNF(CNF *cnf);
 154
 155 uint hashNode(NodeType type, uint numEdges, Edge *edges);
 156 Node *allocNode(NodeType type, uint numEdges, Edge *edges);
 157 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
 158 Edge createNode(NodeType type, uint numEdges, Edge *edges);
 159 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
 160 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges);
 161 Edge constraintOR2(CNF *cnf, Edge left, Edge right);
 162 Edge constraintAND2(CNF *cnf, Edge left, Edge right);
 163 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right);
 164 Edge constraintIFF(CNF *cnf, Edge left, Edge right);
 165 static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,right));}
 166 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge);
 167 Edge constraintNewVar(CNF *cnf);
 168 void countPass(CNF *cnf);
 169 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e);
 170 void addConstraintCNF(CNF *cnf, Edge constraint);
 171 int solveCNF(CNF *cnf);
 172 bool getValueCNF(CNF *cnf, Edge var);
 173 void printCNF(Edge e);
 174 Node *allocBaseNode(NodeType type, uint numEdges);
 175 Node *allocResizeNode(uint capacity);
 176 Edge cloneEdge(Edge e);
 177 void addEdgeToResizeNode(Node **node, Edge e);
 178 void mergeFreeNodeToResizeNode(Node **node, Node *innode);
 179 void mergeNodeToResizeNode(Node **node, Node *innode);
 180 void freeEdgeRec(Edge e);
 181 void outputCNF(CNF *cnf, Edge cnfform);
 182 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
 183 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
 184 void addClause(CNF *cnf, uint numliterals, int *literals);
 185 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 186 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 187 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 188 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 189 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 190
 191 extern Edge E_True;
 192 extern Edge E_False;
 193 extern Edge E_BOGUS;
 194 extern Edge E_NULL;
 195 #endif