more edits

[satune.git] / src / Backend / nodeedge.h

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index e17bba659666d20b0967fcf80c4d1c84b3cc0f89..e515640354a06353483a85dcc7b147268bd6e9c3 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -31,6 +31,8 @@ typedef enum NodeType NodeType;
 struct NodeFlags {
        NodeType type:2;
        int wasExpanded:2;
+       int cnfVisitedDown:2;
+       int cnfVisitedUp:2;
 };
 
 typedef struct NodeFlags NodeFlags;
@@ -55,11 +57,15 @@ struct CNF {
        uint maxsize;
        bool enableMatching;
        Node ** node_array;
+       IncrementalSolver * solver;
        VectorEdge constraints;
 };
 
 typedef struct CNF CNF;
 
+struct CNFExpr;
+typedef struct CNFExpr CNFExpr;
+
 static inline bool getExpanded(Node *n, int isNegated) {
        return n->flags.wasExpanded & (1<<isNegated);
 }
@@ -89,6 +95,10 @@ static inline bool isNegEdge(Edge e) {
        return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
 }
 
+static inline bool isPosEdge(Edge e) {
+       return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
+}
+
 static inline bool isNodeEdge(Edge e) {
        return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
 }
@@ -142,6 +152,18 @@ static inline Edge constraintNegateIf(Edge e, bool negate) {
        return eret;
 }
 
+static inline Literal getEdgeVar(Edge e) {
+       int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
+       return isNegEdge(e) ? -val : val;
+}
+
+static inline bool isProxy(CNFExpr *expr) {
+       return (bool) (((intptr_t) expr) & 1);
+}
+
+static inline Literal getProxy(CNFExpr *expr) {
+       return (Literal) (((intptr_t) expr) >> 1);
+}
 
 uint hashNode(NodeType type, uint numEdges, Edge * edges);
 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
@@ -157,6 +179,10 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
 Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
+void convertPass(CNF *cnf, bool backtrackLit);
+void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
+void constrain(CNF * cnf, Literal l, CNFExpr *exp);
+void produceCNF(CNF * cnf, Edge e);
 
 
 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};