From 6851b03f695a8aa546a203c2caa099f4feab6a29 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 10 Apr 2011 04:13:22 +0000 Subject: [PATCH] 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 --- src/AST/ArrayTransformer.cpp | 4 +++- src/AST/ArrayTransformer.h | 9 +++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 668614a..391bc73 100644 --- 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 eb03e54..660ebd9 100644 --- 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); -- 2.47.3