From 506f2ba3d156b222c7344920f21d09381da8ebb0 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 4 Jul 2017 19:28:05 -0700
Subject: [PATCH] more edits
---
src/Backend/nodeedge.c | 39 ++++++++++++++++++++++++++++++++++-----
src/Backend/nodeedge.h | 8 +++++++-
2 files changed, 41 insertions(+), 6 deletions(-)
diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index c64c0ad..c244754 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -12,6 +12,7 @@ CNF * createCNF() {
cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
cnf->size=0;
cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
+ cnf->enableMatching=true;
allocInlineDefVectorEdge(& cnf->constraints);
return cnf;
}
@@ -161,7 +162,7 @@ Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
if (lowindex==1)
return edges[0];
- if (enableMatching && lowindex==2 &&
+ if (cnf->enableMatching && lowindex==2 &&
isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
getNodeType(edges[0]) == NodeType_AND &&
getNodeType(edges[1]) == NodeType_AND &&
@@ -282,6 +283,8 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
clearVectorEdge(stack);pushVectorEdge(stack, e);
+ bool isMatching=cnf->enableMatching;
+
while(getSizeVectorEdge(stack) != 0) {
Edge e=lastVectorEdge(stack); popVectorEdge(stack);
bool polarity=isNegEdge(e);
@@ -300,13 +303,39 @@ void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
if (n->flags.type == NodeType_ITE||
n->flags.type == NodeType_IFF) {
n->intAnnot[polarity]=0;
- Edge tst=n->edges[0];
+ Edge cond=n->edges[0];
Edge thenedge=n->edges[1];
Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
-
+ thenedge=constraintNegateIf(thenedge, !polarity);
+ elseedge=constraintNegateIf(elseedge, !polarity);
+ thenedge=constraintAND2(cnf, cond, thenedge);
+ cond=constraintNegate(cond);
+ elseedge=constraintAND2(cnf, cond, elseedge);
+ thenedge=constraintNegate(thenedge);
+ elseedge=constraintNegate(elseedge);
+ cnf->enableMatching=false;
+ Edge succ1=constraintAND2(cnf, thenedge, elseedge);
+ n->ptrAnnot[polarity]=succ1.node_ptr;
+ cnf->enableMatching=isMatching;
+ pushVectorEdge(stack, succ1);
+ if (getExpanded(n, !polarity)) {
+ Edge succ2={(Node *)n->ptrAnnot[!polarity]};
+ Node *n1=getNodePtrFromEdge(succ1);
+ Node *n2=getNodePtrFromEdge(succ2);
+ n1->ptrAnnot[0]=succ2.node_ptr;
+ n2->ptrAnnot[0]=succ1.node_ptr;
+ n1->ptrAnnot[1]=succ2.node_ptr;
+ n2->ptrAnnot[1]=succ1.node_ptr;
+ }
+ } else {
+ for (uint i=0;i<n->numEdges;i++) {
+ Edge succ=n->edges[i];
+ succ=constraintNegateIf(succ, polarity);
+ if(!edgeIsVarConst(succ)) {
+ pushVectorEdge(stack, succ);
+ }
+ }
}
}
-
}
-
}
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index 4a40e03..e17bba6 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -46,7 +46,6 @@ struct Node {
#define DEFAULT_CNF_ARRAY_SIZE 256
#define LOAD_FACTOR 0.25
-#define enableMatching 1
struct CNF {
uint varcount;
@@ -54,6 +53,7 @@ struct CNF {
uint size;
uint mask;
uint maxsize;
+ bool enableMatching;
Node ** node_array;
VectorEdge constraints;
};
@@ -137,6 +137,12 @@ 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;
+}
+
+
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);
--
2.34.1