From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 28 Jan 2012 04:02:57 +0000 (+0000)
Subject: Improvement. Enable the simplifying node factory by default for the SMT, SMT2 and... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=094db60822f78ce1e1e5fc3c26efb9c4a7eb384e;p=francis%2Fstp.git

Improvement. Enable the simplifying node factory by default for the SMT, SMT2 and CVC3 languages.

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

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 48c7b2f..25de099 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -120,6 +120,10 @@ int main(int argc, char ** argv) {
             Ctr_Example);
   
 
+  auto_ptr<SimplifyingNodeFactory> simplifyingNF( new SimplifyingNodeFactory(*bm->hashingNodeFactory, *bm));
+  bm->defaultNodeFactory = simplifyingNF.get();
+
+
   //populate the help string
   helpstring += 
     "STP version            : " + version + "\n"
@@ -413,8 +417,7 @@ int main(int argc, char ** argv) {
 
   bm->GetRunTimes()->start(RunTimes::Parsing);
 	{
- 	    SimplifyingNodeFactory simpNF(*bm->hashingNodeFactory, *bm);
-		TypeChecker nfTypeCheckSimp(simpNF, *bm);
+                TypeChecker nfTypeCheckSimp(*simplifyingNF.get(), *bm);
 		TypeChecker nfTypeCheckDefault(*bm->defaultNodeFactory, *bm);
 
 		Cpp_interface piTypeCheckSimp(*bm, &nfTypeCheckSimp);