From: bdemsky <bdemsky@uci.edu>
Date: Sat, 1 Jul 2017 22:23:25 +0000 (-0700)
Subject: more code
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f0dba6a31f70f7249dad6919ef51cd58c992e3e5;p=satune.git

more code
---

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 533a9f1..a1fd4c5 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -1,5 +1,6 @@
 #include "nodeedge.h"
 #include <string.h>
+#include <stdlib.h>
 
 CNF * createCNF() {
 	CNF * cnf=ourmalloc(sizeof(CNF));
@@ -117,20 +118,67 @@ Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
 	return constraintNegate(eand);
 }
 
+int comparefunction(const Edge * e1, const Edge * e2) {
+	return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
+}
+
 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
+	qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
+	int initindex=0;
+	while(initindex<numEdges && edges[initindex].node_ptr == E_True.node_ptr)
+		initindex++;
+
+	uint remainSize=numEdges-initindex;
+
+	if (remainSize == 0)
+		return E_True;
+	else if (remainSize == 1)
+		return edges[initindex];
+	else if (edges[initindex].node_ptr==E_False.node_ptr)
+		return E_False;
+
+	/** De-duplicate array */
+	uint lowindex=0;
+	edges[lowindex++]=edges[initindex++];
+
+	for(;initindex<numEdges;initindex++) {
+		Edge e1=edges[lowindex];
+		Edge e2=edges[initindex];
+		if (sameNodeVarEdge(e1, e2)) {
+			if (!sameSignEdge(e1, e2)) {
+				return E_False;
+			}
+		} else
+			edges[lowindex++]=edges[initindex];
+	}
+	if (lowindex==1)
+		return edges[0];
+
+	if (enableMatching && lowindex==2 &&
+			isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
+			getNodeType(edges[0]) == NodeType_AND &&
+			getNodeType(edges[1]) == NodeType_AND &&
+			getNodeSize(edges[0]) == 2 &&
+			getNodeSize(edges[1]) == 2) {
+		Edge * e0edges=getEdgeArray(edges[0]);
+		Edge * e1edges=getEdgeArray(edges[1]);
+		if (sameNodeOppSign(e0edges[0], e1edges[0])) {
+			return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+		} else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
+			return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+		} else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
+			return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+		} else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
+			return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+		}
+	}
+	
 	return createNode(cnf, NodeType_AND, numEdges, edges);
 }
 
 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
-	Edge edges[2];
-	if ((uintptr_t)left.node_ptr<(uintptr_t)right.node_ptr) {
-		edges[0]=left;
-		edges[1]=right;
-	} else {
-		edges[0]=right;
-		edges[1]=left;
-	}
-	return createNode(cnf, NodeType_AND, 2, edges);
+	Edge edges[2]={left, right};
+	return constraintAND(cnf, 2, edges);
 }
 
 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index 4a4f6d3..e5302a0 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -5,6 +5,7 @@
 #define NEGATE_EDGE 1
 #define EDGE_IS_VAR_CONSTANT 2
 #define VAR_SHIFT 2
+#define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
 
 struct Edge;
 typedef struct Edge Edge;
@@ -39,6 +40,7 @@ struct Node {
 
 #define DEFAULT_CNF_ARRAY_SIZE 256
 #define LOAD_FACTOR 0.25
+#define enableMatching 1
 
 struct CNF {
 	uint varcount;
@@ -56,6 +58,49 @@ static inline Edge constraintNegate(Edge e) {
 	return enew;
 }
 
+static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
+	return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
+}
+
+static inline bool sameSignEdge(Edge e1, Edge e2) {
+	return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool sameNodeOppSign(Edge e1, Edge e2) {
+	return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
+}
+
+static inline bool isNegEdge(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);
+}
+
+static inline bool isNegNodeEdge(Edge e) {
+	return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
+}
+
+static inline Node * getNodePtrFromEdge(Edge e) {
+	return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
+}
+
+static inline NodeType getNodeType(Edge e) {
+	Node * n=getNodePtrFromEdge(e);
+	return n->flags.type;
+}
+
+static inline uint getNodeSize(Edge e) {
+	Node * n=getNodePtrFromEdge(e);
+	return n->numEdges;
+}
+
+static inline Edge * getEdgeArray(Edge e) {
+	Node * n=getNodePtrFromEdge(e);
+	return n->edges;
+}
+
 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);