From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 1 Aug 2009 16:12:17 +0000 (+0000)
Subject: Clear the simplify maps after each transformation of div/mod/rem. This reverts back... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=38918af5077092b25730a5190558441445f0c4ff;p=francis%2Fstp.git

Clear the simplify maps after each transformation of div/mod/rem. This reverts back a change I tentatively made. Not clearing the simplify maps after transforming means they will be in memory during SAT solving. Which is a very bad idea.



git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@99 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/AST/Transform.cpp b/AST/Transform.cpp
index d3b73fd..10a56d0 100644
--- a/AST/Transform.cpp
+++ b/AST/Transform.cpp
@@ -52,7 +52,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 
 		//put everything together, simplify, and return
 		ASTNode n = CreateTerm(ITE, len, cond_dividend, minus_modnode, modnode);
-		return SimplifyTerm(n);
+		return SimplifyTerm_TopLevel(n);
 	}
 
 	// This is the modulus of dividing rounding to -infinity.
@@ -95,7 +95,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 		ASTNode ite2 = CreateTerm(ITE, len, CreateNode(AND, isSNeg, isTPos), branch2, ite3);
 		ASTNode ite1 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTPos), branch1, ite2);
 
-		return SimplifyTerm(ite1);
+		return SimplifyTerm_TopLevel(ite1);
 	}
 	else if (SBVDIV == in.GetKind())
 	{
@@ -131,7 +131,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 		ASTNode minus_divnode3 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), CreateTerm(BVUMINUS, len, divisor));
 		ASTNode n = CreateTerm(ITE, len, cond1, minus_divnode1, CreateTerm(ITE, len, cond2, minus_divnode2, CreateTerm(ITE, len, cond3,
 				minus_divnode3, divnode)));
-		return SimplifyTerm(n);
+		return SimplifyTerm_TopLevel(n);
 	}
 
 	FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in);