X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fconstraint.h;h=8d2666ca2e17464c8023fccbc3a5ac5c6e594228;hb=e1360c75a71486a0de8c1b30a2a8cd2877902416;hp=772f6c8dafe88bdd312c845d32e676baa1a24278;hpb=510efd1d0ee344fb5bbf4fe8ac94940d7a806402;p=satune.git

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 772f6c8..8d2666c 100644
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -30,57 +30,36 @@ enum NodeType {
 
 typedef enum NodeType NodeType;
 
-struct NodeFlags {
-	NodeType type : 2;
-	int varForced : 1;
-	int wasExpanded : 2;
-	int cnfVisitedDown : 2;
-	int cnfVisitedUp : 2;
-};
-
-typedef struct NodeFlags NodeFlags;
-
 struct Node {
-	NodeFlags flags;
 	uint numEdges;
-	uint hashCode;
-	uint intAnnot[2];
-	void *ptrAnnot[2];
+	uint numVars;
+	union {
+		NodeType type;
+		uint capacity;
+	};
 	Edge edges[];
 };
 
-#define DEFAULT_CNF_ARRAY_SIZE 256
-#define LOAD_FACTOR 0.25
+typedef struct Node Node;
+
+#define DEFAULT_CNF_ARRAY_SIZE 2048
 
 struct CNF {
 	uint varcount;
-	uint capacity;
-	uint size;
-	uint mask;
-	uint maxsize;
-	bool enableMatching;
-	Node **node_array;
+	uint clausecount;
+	uint asize;
 	IncrementalSolver *solver;
-	VectorEdge constraints;
-	VectorEdge args;
+	int *array;
+	long long solveTime;
+	long long encodeTime;
+	bool unsat;
 };
 
 typedef struct CNF CNF;
 
-struct CNFExpr;
-typedef struct CNFExpr CNFExpr;
-
-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;
+	Edge eneg = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
+	return eneg;
 }
 
 static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
@@ -111,13 +90,17 @@ static inline bool isNegNodeEdge(Edge e) {
 	return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
 }
 
+static inline bool isPosNodeEdge(Edge e) {
+	return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == 0;
+}
+
 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;
+	return n->type;
 }
 
 static inline bool equalsEdge(Edge e1, Edge e2) {
@@ -165,21 +148,14 @@ static inline Literal getEdgeVar(Edge e) {
 	return isNegEdge(e) ? -val : val;
 }
 
-static inline bool isProxy(CNFExpr *expr) {
-	return (bool) (((intptr_t) expr) & 1);
-}
-
-static inline Literal getProxy(CNFExpr *expr) {
-	return (Literal) (((intptr_t) expr) >> 1);
-}
-
 CNF *createCNF();
 void deleteCNF(CNF *cnf);
+void resetCNF(CNF *cnf);
 
 uint hashNode(NodeType type, uint numEdges, Edge *edges);
-Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashCode);
+Node *allocNode(NodeType type, uint numEdges, Edge *edges);
 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges);
-Edge create(CNF *cnf, NodeType type, uint numEdges, Edge *edges);
+Edge createNode(NodeType type, uint numEdges, Edge *edges);
 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges);
 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges);
 Edge constraintOR2(CNF *cnf, Edge left, Edge right);
@@ -195,23 +171,22 @@ void addConstraintCNF(CNF *cnf, Edge constraint);
 int solveCNF(CNF *cnf);
 bool getValueCNF(CNF *cnf, Edge var);
 void printCNF(Edge e);
-
-void convertPass(CNF *cnf, bool backtrackLit);
-void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
-void constrainCNF(CNF *cnf, Literal l, CNFExpr *exp);
-void produceCNF(CNF *cnf, Edge e);
-CNFExpr *produceConjunction(CNF *cnf, Edge e);
-CNFExpr *produceDisjunction(CNF *cnf, Edge e);
-bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate);
-void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign);
-CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge);
-Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg);
-void outputCNF(CNF *cnf, CNFExpr *expr);
-
+Node *allocBaseNode(NodeType type, uint numEdges);
+Node *allocResizeNode(uint capacity);
+Edge cloneEdge(Edge e);
+void addEdgeToResizeNode(Node **node, Edge e);
+void mergeFreeNodeToResizeNode(Node **node, Node *innode);
+void mergeNodeToResizeNode(Node **node, Node *innode);
+void freeEdgeRec(Edge e);
+void outputCNF(CNF *cnf, Edge cnfform);
+void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
+void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
+void addClause(CNF *cnf, uint numliterals, int *literals);
 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
+Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
 
 extern Edge E_True;
 extern Edge E_False;