From 700edd13c184343230dd93fb0f556b86ba5854c0 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 28 Mar 2011 03:49:09 +0000 Subject: [PATCH] Make applySubstitutionMap idempotent (I hope). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1245 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/SubstitutionMap.cpp | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 3da7fff..d77af5e 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -186,17 +186,26 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a, ArrayTransform return output; } //end of CreateSubstitutionMap() - +// idempotent. ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n) { bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); ASTNodeMap cache; SimplifyingNodeFactory nf(*bm->hashingNodeFactory, *bm); ASTNode result = replace(n,*SolverMap,cache,&nf, false); + + // NB. This is an expensive check. Remove it after it's been idempotent + // for a while. + #ifndef NDEBUG + cache.clear(); + assert( result == replace(result,*SolverMap,cache,&nf, false)); + #endif + bm->GetRunTimes()->stop(RunTimes::ApplyingSubstitutions); return result; } +// not always idempotent. ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n) { bm->GetRunTimes()->start(RunTimes::ApplyingSubstitutions); @@ -291,6 +300,14 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, result = nf->CreateArrayTerm(k,indexWidth, valueWidth,new_children); } + // We may have created something that should be mapped. For instance, + // if n is READ(A, x), and the fromTo is: {x==0, READ(A,0) == 1}, then + // by here the result will be READ(A,0). Which needs to be mapped again.. + // I hope that this makes it idempotent. + + if (fromTo.find(result) != fromTo.end()) + result = replace(result, fromTo, cache,nf,stopAtArrays); + assert(result.GetValueWidth() == valueWidth); assert(result.GetIndexWidth() == indexWidth); -- 2.47.3