struct CNF {
uint varcount;
+ uint clausecount;
uint asize;
IncrementalSolver *solver;
- int * array;
+ int *array;
long long solveTime;
long long encodeTime;
bool unsat;
Node *allocBaseNode(NodeType type, uint numEdges);
Node *allocResizeNode(uint capacity);
Edge cloneEdge(Edge e);
-void addEdgeToResizeNode(Node ** node, Edge e);
-void mergeFreeNodeToResizeNode(Node **node, Node * innode);
-void mergeNodeToResizeNode(Node **node, Node * innode);
+void addEdgeToResizeNode(Node **node, Edge e);
+void mergeFreeNodeToResizeNode(Node **node, Node *innode);
+void mergeNodeToResizeNode(Node **node, Node *innode);
void freeEdgeRec(Edge e);
void outputCNF(CNF *cnf, Edge cnfform);
void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
-
+void addClause(CNF *cnf, uint numliterals, int *literals);
+void freezeVariable(CNF *cnf, Edge e);
Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);