more code

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index deb63d34efa3ecea67500797e3f5dce1d475e0cf..c64c0ad2c186a3ca75dffe7c1913f5d03d5d9b79 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -2,6 +2,8 @@
 #include <string.h>
 #include <stdlib.h>
 
+VectorImpl(Edge, Edge, 16)
+
 CNF * createCNF() {
        CNF * cnf=ourmalloc(sizeof(CNF));
        cnf->varcount=1;
@@ -10,7 +12,8 @@ CNF * createCNF() {
        cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
        cnf->size=0;
        cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
-       return cnf;
+       allocInlineDefVectorEdge(& cnf->constraints);
+ return cnf;
 }
 
 void deleteCNF(CNF * cnf) {
@@ -19,6 +22,7 @@ void deleteCNF(CNF * cnf) {
                if (n!=NULL)
                        ourfree(n);
        }
+       deleteVectorArrayEdge(& cnf->constraints);
        ourfree(cnf->node_array);
        ourfree(cnf);
 }
@@ -49,9 +53,12 @@ void resizeCNF(CNF *cnf, uint newCapacity) {
 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
        Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
        memcpy(n->edges, edges, sizeof(Edge)*numEdges);
-       n->numEdges=numEdges;
        n->flags.type=type;
+       n->flags.wasExpanded=0;
+       n->numEdges=numEdges;
        n->hashCode=hashcode;
+       n->intAnnot[0]=0;n->intAnnot[1]=0;
+       n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
        return n;
 }
 
@@ -249,8 +256,57 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
        return result;
 }
 
+void addConstraint(CNF *cnf, Edge constraint) {
+       pushVectorEdge(&cnf->constraints, constraint);
+}
+
 Edge constraintNewVar(CNF *cnf) {
        uint varnum=cnf->varcount++;
        Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
        return e;
 }
+
+void countPass(CNF *cnf) {
+       uint numConstraints=getSizeVectorEdge(&cnf->constraints);
+       VectorEdge *ve=allocDefVectorEdge();
+       for(uint i=0; i<numConstraints;i++) {
+               countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
+       }
+       deleteVectorEdge(ve);
+}
+
+void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
+       //Skip constants and variables...
+       if (edgeIsVarConst(e))
+               return;
+
+       clearVectorEdge(stack);pushVectorEdge(stack, e);
+
+       while(getSizeVectorEdge(stack) != 0) {
+               Edge e=lastVectorEdge(stack); popVectorEdge(stack);
+               bool polarity=isNegEdge(e);
+               Node *n=getNodePtrFromEdge(e);
+               if (getExpanded(n,  polarity)) {
+                       if (n->flags.type == NodeType_IFF ||
+                                       n->flags.type == NodeType_ITE) {
+                               Edge pExp={n->ptrAnnot[polarity]};
+                               getNodePtrFromEdge(pExp)->intAnnot[0]++;
+                       } else {
+                               n->intAnnot[polarity]++;
+                       }
+               } else {
+                       setExpanded(n, polarity); n->intAnnot[polarity]=1;
+                       
+                       if (n->flags.type == NodeType_ITE||
+                                       n->flags.type == NodeType_IFF) {
+                               n->intAnnot[polarity]=0;
+                               Edge tst=n->edges[0];
+                               Edge thenedge=n->edges[1];
+                               Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
+                               
+                       }
+               }
+               
+       }
+       
+}

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index a83983d44857178d4236b80fb6abae6f209776c6..4a40e03185e1530a7da52ed5a4262a1fc87d88b8 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -1,6 +1,7 @@
 #ifndef NODEEDGE_H
 #define NODEEDGE_H
 #include "classlist.h"
+#include "vector.h"
 
 #define NEGATE_EDGE 1
 #define EDGE_IS_VAR_CONSTANT 2
@@ -17,6 +18,8 @@ struct Edge {
        Node * node_ptr;
 };
 
+VectorDef(Edge, Edge)
+
 enum NodeType {
        NodeType_AND,
        NodeType_ITE,
@@ -27,6 +30,7 @@ typedef enum NodeType NodeType;
 
 struct NodeFlags {
        NodeType type:2;
+       int wasExpanded:2;
 };
 
 typedef struct NodeFlags NodeFlags;
@@ -35,6 +39,8 @@ struct Node {
        NodeFlags flags;
        uint numEdges;
        uint hashCode;
+       uint intAnnot[2];
+       void * ptrAnnot[2];
        Edge edges[];
 };
 
@@ -49,10 +55,19 @@ struct CNF {
        uint mask;
        uint maxsize;
        Node ** node_array;
+       VectorEdge constraints;
 };
 
 typedef struct CNF CNF;
 
+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;
@@ -118,6 +133,10 @@ 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;
+}
+
 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 +149,9 @@ 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);
+
 
 Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
 Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 86db3ed684870419f3f11fed102056a8c1256d5b..0d57a8a5137b07dbd66697a1ad4773cb5755c826 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -10,20 +10,17 @@ ArrayDef(Element, Element *);
 ArrayDef(Boolean, Boolean *);
 ArrayDef(Set, Set *);
 
-
-VectorDef(Table, Table *, 4);
-VectorDef(Set, Set *, 4);
-VectorDef(Boolean, Boolean *, 4);
-VectorDef(Constraint, Constraint *, 4);
-VectorDef(Function, Function *, 4);
-VectorDef(Predicate, Predicate *, 4);
-VectorDef(Element, Element *, 4);
-VectorDef(Order, Order *, 4);
-VectorDef(TableEntry, TableEntry *, 4);
-VectorDef(ASTNode, ASTNode *, 4);
-VectorDef(Int, uint64_t, 4);
-
-
+VectorDef(Table, Table *);
+VectorDef(Set, Set *);
+VectorDef(Boolean, Boolean *);
+VectorDef(Constraint, Constraint *);
+VectorDef(Function, Function *);
+VectorDef(Predicate, Predicate *);
+VectorDef(Element, Element *);
+VectorDef(Order, Order *);
+VectorDef(TableEntry, TableEntry *);
+VectorDef(ASTNode, ASTNode *);
+VectorDef(Int, uint64_t);
 
 HashTableDef(Void, void *, void *);
 HashTableDef(BoolConst, BooleanOrder *, Constraint *);

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 76da3873dcc633ca553926c9b1bd36725e88f238..00696f1a4f0ef900bb3e627b4f476767be74b60f 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -2,7 +2,7 @@
 #define VECTOR_H
 #include <string.h>
 
-#define VectorDef(name, type, defcap)                                   \
+#define VectorDef(name, type)                                                                                                                                                                          \
        struct Vector ## name {                                               \
                uint size;                                                          \
                uint capacity;                                                      \
@@ -13,7 +13,9 @@
        Vector ## name * allocDefVector ## name();                            \
        Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
        void pushVector ## name(Vector ## name *vector, type item);           \
-       type getVector ## name(Vector ## name *vector, uint index);           \
+       type lastVector ## name(Vector ## name *vector);                                                                                        \
+       void popVector ## name(Vector ## name *vector);                                                                                         \
+       type getVector ## name(Vector ## name *vector, uint index);                                             \
        void setVector ## name(Vector ## name *vector, uint index, type item); \
        uint getSizeVector ## name(Vector ## name *vector);                   \
        void deleteVector ## name(Vector ## name *vector);                    \
@@ -41,7 +43,13 @@
                memcpy(tmp->array, array, capacity * sizeof(type));                                                                     \
                return tmp;                                                         \
        }                                                                     \
-       void pushVector ## name(Vector ## name *vector, type item) {          \
+       void popVector ## name(Vector ## name *vector) {                                                                                        \
+               vector->size--;                                                                                                                                                                                                                 \
+       }                                                                                                                                                                                                                                                                                       \
+       type lastVector ## name(Vector ## name *vector) {                                                                                       \
+               return vector->array[vector->size];                                                                                                                                     \
+       }                                                                                                                                                                                                                                                                                       \
+       void pushVector ## name(Vector ## name *vector, type item) {                                    \
                if (vector->size >= vector->capacity) {                             \
                        uint newcap=vector->capacity * 2;                                 \
                        vector->array=(type *)ourrealloc(vector->array, newcap);          \