From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 13 Jul 2017 23:44:48 +0000 (-0700)
Subject: resolving conflict ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=43cc444d4eb88a1508dce97e4001e648e12c28fd;p=satune.git

resolving conflict ...
---

43cc444d4eb88a1508dce97e4001e648e12c28fd
diff --cc src/Backend/constraint.c
index b1ec593,4859a93..72c74c7
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@@ -712,20 -711,34 +712,34 @@@ void printCNF(Edge e) 
  		return;
  	}
  	Node *n=getNodePtrFromEdge(e);
- 	if (isNeg)
+ 	if (isNeg) {
+ 		//Pretty print things that are equivalent to OR's
+ 		if (getNodeType(e)==NodeType_AND) {
 -			printf("or(");
++			model_print("or(");
+ 			for(uint i=0;i<n->numEdges;i++) {
+ 				Edge e=n->edges[i];
+ 				if (i!=0)
 -					printf(" ");
++					model_print(" ");
+ 				printCNF(constraintNegate(e));
+ 			}
 -			printf(")");
++			model_print(")");
+ 			return;
+ 		}
+ 
 -		printf("!");
 +		model_print("!");
+ 	}
  	switch(getNodeType(e)) {
  	case NodeType_AND:
 -		printf("and");
 +		model_print("and");
  		break;
  	case NodeType_ITE:
 -		printf("ite");
 +		model_print("ite");
  		break;
  	case NodeType_IFF:
 -		printf("iff");
 +		model_print("iff");
  		break;
  	}
 -	printf("(");
 +	model_print("(");
  	for(uint i=0;i<n->numEdges;i++) {
  		Edge e=n->edges[i];
  		if (i!=0)