From 37345d3fce06dcfff2ea32110f9bb344c949dbf6 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 14 Mar 2011 03:57:45 +0000
Subject: [PATCH] * The simplifying node factory now removes TRUEs when
 creating ANDS. * The simplifying node factory never creates IFF, just XORS.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1213 e59a4935-1847-0410-ae03-e826735625c1
---
 .../NodeFactory/SimplifyingNodeFactory.cpp    | 55 +++++++++----------
 src/STPManager/STP.cpp                        |  1 +
 2 files changed, 27 insertions(+), 29 deletions(-)

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index c3bf3bd..7c009c9 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -100,6 +100,17 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
 	case BEEV::EQ:
 		result = CreateSimpleEQ(children);
 		break;
+	case BEEV::IFF:
+	{
+		assert(children.size() ==2);
+		ASTVec newCh;
+		newCh.reserve(2);
+		newCh.push_back(CreateSimpleNot(children[0]));
+		newCh.push_back(children[1]);
+	    result = CreateSimpleXor(newCh);
+	    break;
+	}
+
 	default:
 		result = hashing.CreateNode(kind, children);
 	}
@@ -171,17 +182,12 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
 {
 	const Kind k = IsAnd ? BEEV::AND : BEEV::OR;
 
-	if (debug_simplifyingNodeFactory)
-	{
-		cout << "========" << endl << "CreateSimpAndOr " << k << " ";
-		lpvec(children);
-		cout << endl;
-	}
-
 	const ASTNode& annihilator = (IsAnd ? ASTFalse : ASTTrue);
 	const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse);
 
 	ASTNode retval;
+	ASTVec new_children;
+	new_children.reserve(children.size());
 
 	const ASTVec::const_iterator it_end = children.end();
 	for (ASTVec::const_iterator it = children.begin(); it != it_end; it++)
@@ -196,41 +202,32 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
 
 		if (*it == annihilator)
 		{
-			retval = annihilator;
-			if (debug_simplifyingNodeFactory)
-			{
-				cout << "Annihilator" << endl;
-			}
-			return retval;
+			return annihilator;
 		}
 		else if (*it == identity || (nextexists && (*next_it == *it)))
 		{
 			// just drop it
-		}
+		}else
+			new_children.push_back(*it);
 	}
 
 	// If we get here, we saw no annihilators, and children should
 	// be only the non-True nodes.
-	if (children.size() < 2)
+
+
+	if (0 == new_children.size())
 	{
-		if (0 == children.size())
-		{
-			retval = identity;
-		}
-		else
-		{
-			// there is just one child
-			retval = children[0];
-		}
+		retval = identity;
 	}
-	else
+	else if (1==new_children.size())
 	{
-		// 2 or more children.  Create a new node.
-		retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, children);
+		// there is just one child
+		retval = new_children[0];
 	}
-	if (debug_simplifyingNodeFactory)
+	else
 	{
-		cout << "returns " << retval << endl;
+		// 2 or more children.  Create a new node.
+		retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, new_children);
 	}
 	return retval;
 }
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 3f0ecfd..7c4cf1f 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -173,6 +173,7 @@ namespace BEEV {
     BVSolver* bvSolver = new BVSolver(bm,simp);
 
     simplified_solved_InputToSAT = sizeReducing(inputToSAT,bvSolver);
+    //simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT,bvSolver);
 
     initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
     if (bm->UserFlags.stats_flag)
-- 
2.47.3