Improvement. Use the simplifying node factory in transformer.

This is a hopefully correct implementation of r1260.

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 668614a8923676e0cfa584680c0e98ce37425fad..391bc7367ea45fe61363d9aa94bee6b93643c7e3 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -654,7 +654,9 @@ namespace BEEV
                                        nf->CreateTerm(READ, width, arrName[0], readIndex);
                                  assert(BVTypeCheck(readTerm));
 
-                                 ASTNode readPushedIn = TransformArrayRead(readTerm);
+                                 // The simplifying node factory may have produced
+                                 // something that's not a READ.
+                                 ASTNode readPushedIn = TransformTerm(readTerm);
                                  assert(BVTypeCheck(readPushedIn));
 
                                  result =

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);