From 53c7024baac3d67a18e987a0c313891b26da2f79 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 4 Jul 2017 19:03:43 -0700
Subject: [PATCH] more code

---
 src/Backend/nodeedge.c    | 60 +++++++++++++++++++++++++++++++++++++--
 src/Backend/nodeedge.h    | 22 ++++++++++++++
 src/Collections/structs.h | 25 +++++++---------
 src/Collections/vector.h  | 14 +++++++--
 4 files changed, 102 insertions(+), 19 deletions(-)

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index deb63d3..c64c0ad 100644
--- 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 a83983d..4a40e03 100644
--- 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 86db3ed..0d57a8a 100644
--- 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 76da387..00696f1 100644
--- 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);          \
-- 
2.34.1