more edits

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

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index a83983d44857178d4236b80fb6abae6f209776c6..559c05822732b6f694ef96ec973f80c1440c259e 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -1,12 +1,15 @@
 #ifndef NODEEDGE_H
 #define NODEEDGE_H
 #include "classlist.h"
+#include "vector.h"
 
 #define NEGATE_EDGE 1
 #define EDGE_IS_VAR_CONSTANT 2
 #define VAR_SHIFT 2
 #define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
 
+typedef int Literal;
+
 struct Edge;
 typedef struct Edge Edge;
 
@@ -17,6 +20,8 @@ struct Edge {
        Node * node_ptr;
 };
 
+VectorDef(Edge, Edge)
+
 enum NodeType {
        NodeType_AND,
        NodeType_ITE,
@@ -27,6 +32,10 @@ typedef enum NodeType NodeType;
 
 struct NodeFlags {
        NodeType type:2;
+       int varForced:1;
+       int wasExpanded:2;
+       int cnfVisitedDown:2;
+       int cnfVisitedUp:2;
 };
 
 typedef struct NodeFlags NodeFlags;
@@ -35,12 +44,13 @@ struct Node {
        NodeFlags flags;
        uint numEdges;
        uint hashCode;
+       uint intAnnot[2];
+       void * ptrAnnot[2];
        Edge edges[];
 };
 
 #define DEFAULT_CNF_ARRAY_SIZE 256
 #define LOAD_FACTOR 0.25
-#define enableMatching 1
 
 struct CNF {
        uint varcount;
@@ -48,11 +58,26 @@ struct CNF {
        uint size;
        uint mask;
        uint maxsize;
+       bool enableMatching;
        Node ** node_array;
+       IncrementalSolver * solver;
+       VectorEdge constraints;
+       VectorEdge args;
 };
 
 typedef struct CNF CNF;
 
+struct CNFExpr;
+typedef struct CNFExpr CNFExpr;
+
+static inline bool getExpanded(Node *n, int isNegated) {
+       return n->flags.wasExpanded & (1<<isNegated);
+}
+
+static inline void setExpanded(Node *n, int isNegated) {
+       n->flags.wasExpanded |= (1<<isNegated);
+}
+
 static inline Edge constraintNegate(Edge e) {
        Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
        return enew;
@@ -74,6 +99,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);
 }
@@ -118,6 +147,28 @@ static inline bool edgeIsConst(Edge e) {
        return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
 }
 
+static inline bool edgeIsVarConst(Edge e) {
+       return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
+}
+
+static inline Edge constraintNegateIf(Edge e, bool negate) {
+       Edge eret={(Node *)(((uintptr_t)e.node_ptr) ^ 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);
 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
@@ -130,6 +181,19 @@ Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
 Edge constraintIFF(CNF * cnf, Edge left, Edge right);
 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 constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
+void produceCNF(CNF * cnf, Edge e);
+CNFExpr * produceConjunction(CNF * cnf, Edge e);
+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);
+
+
 
 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};