Improvement. Use the simplifying node factory in transformer.

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

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index eb03e544b7c17811510d1706cee5a76d74959ae0..660ebd9a8e379204264ec8ead9f2070518ca9971 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -12,7 +12,7 @@
 
 #include "AST.h"
 #include "../STPManager/STPManager.h"
-
+#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 
 namespace BEEV
 {
@@ -111,7 +111,7 @@ namespace BEEV
       debug_transform(0),
       TransformMap(NULL)
     {
-      nf = bm->defaultNodeFactory;
+      nf = new SimplifyingNodeFactory(*(bm->hashingNodeFactory), *bm);
 
       runTimes = bm->GetRunTimes();
       ASTTrue  = bm->CreateNode(TRUE);
@@ -119,6 +119,11 @@ namespace BEEV
       ASTUndefined = bm->CreateNode(UNDEFINED);
     }
 
+    ~ArrayTransformer()
+    {
+      delete nf;
+    }
+
     // Takes a formula, transforms it by replacing array reads with
     // variables, and returns the transformed formula
     ASTNode TransformFormula_TopLevel(const ASTNode& form);