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