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