From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 5 Mar 2011 11:57:10 +0000 (+0000)
Subject: improvement. Use the simplifying node factory be default in the substitution map.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=51ef8fc1839ed7d771861132e89de33bb4a7dd96;p=francis%2Fstp.git

improvement. Use the simplifying node factory be default in the substitution map.

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index b950bb9..3da7fff 100644
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -191,7 +191,8 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
 {
 	bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions);
 	ASTNodeMap cache;
-	ASTNode result =  replace(n,*SolverMap,cache,bm->defaultNodeFactory, false);
+	SimplifyingNodeFactory nf(*bm->hashingNodeFactory, *bm);
+	ASTNode result =  replace(n,*SolverMap,cache,&nf, false);
 	bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions);
 	return result;
 }
@@ -200,7 +201,8 @@ ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n)
 {
 	bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions);
 	ASTNodeMap cache;
-	ASTNode result = replace(n,*SolverMap,cache,bm->defaultNodeFactory, true);
+	SimplifyingNodeFactory nf(*bm->hashingNodeFactory, *bm);
+	ASTNode result = replace(n,*SolverMap,cache,&nf, true);
 	bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions);
 	return result;
 }