X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fnodeedge.h;h=7933bf8b57b70704764c0c953c594e4eaef36ed0;hb=14fbe267209e1321043476b9cc4d9302e2603a42;hp=bc0eb5cec3fe55530147a09e55f064dd7be03373;hpb=8f3dd7736e18334b23238dcc8c819e6c7154c3f8;p=satune.git

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index bc0eb5c..7933bf8 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -147,6 +147,10 @@ static inline bool edgeIsConst(Edge e) {
 	return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 }
 
+static inline bool edgeIsNull(Edge e) {
+	return e.node_ptr == NULL;
+}
+
 static inline bool edgeIsVarConst(Edge e) {
 	return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
 }
@@ -192,6 +196,8 @@ CNFExpr* produceDisjunction(CNF *cnf, Edge e);
 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
 CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
+Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);
+void outputCNF(CNF *cnf, CNFExpr *expr);
 
 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};