From: bdemsky <bdemsky@uci.edu>
Date: Wed, 5 Jul 2017 02:03:43 +0000 (-0700)
Subject: more code
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=53c7024baac3d67a18e987a0c313891b26da2f79;p=satune.git
more code
---
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); \