From 32896683de91abd3b9950400dff6034582484603 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 1 Jan 2011 04:15:27 +0000 Subject: [PATCH] Speedup. The old Flatten was too slow. On an instance of binary AND nodes 2 million deep it took longer than 1 hour to flatten. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1044 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ASTmisc.cpp | 18 +++--- src/simplifier/simplifier.cpp | 110 +++++++++------------------------- src/simplifier/simplifier.h | 5 -- 3 files changed, 36 insertions(+), 97 deletions(-) diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp index 9520cfd..1507909 100644 --- a/src/AST/ASTmisc.cpp +++ b/src/AST/ASTmisc.cpp @@ -161,30 +161,28 @@ bool containsArrayOps(const ASTNode&n) } } - - // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...) - ASTVec FlattenKind(Kind k, const ASTVec &children) + void FlattenKind(const Kind k, const ASTVec &children, ASTVec & flat_children) { - ASTVec flat_children; - ASTVec::const_iterator ch_end = children.end(); for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++) { Kind ck = it->GetKind(); if (k == ck) { - const ASTVec gchildren = FlattenKind(k,it->GetChildren()); - //const ASTVec gchildren = it->GetChildren(); - // append grandchildren to children - flat_children.insert(flat_children.end(), - gchildren.begin(), gchildren.end()); + FlattenKind(k,it->GetChildren(), flat_children); } else { flat_children.push_back(*it); } } + } + // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...) + ASTVec FlattenKind(Kind k, const ASTVec &children) + { + ASTVec flat_children; + FlattenKind(k,children,flat_children); return flat_children; } diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 67fe0a3..64e829f 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -27,20 +27,6 @@ namespace BEEV // so that's disabled. const bool simplify_upfront = true; - ASTNode Simplifier::Flatten(const ASTNode& a) - { - ASTNode n = a; - while (true) - { - ASTNode nold = n; - n = FlattenOneLevel(n); - if ((n == nold)) - break; - } - - return n; - } - // is it ITE(p,bv0[1], bv1[1]) OR ITE(p,bv0[0], bv1[0]) bool isPropositionToTerm(const ASTNode& n) { @@ -1071,16 +1057,9 @@ namespace BEEV if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) return output; - ASTNode flat = Flatten(a); - ASTVec c, outvec; - c = flat.GetChildren(); + ASTVec c = FlattenKind(a.GetKind(),a.GetChildren()); SortByArith(c); - Kind k = flat.GetKind(); - - // If the simplifying node factory is enabled, a - // constant may be returned by Flatten. - if (AND !=k && OR !=k) - return SimplifyFormula(flat,pushNeg, VarConstMap); + Kind k = a.GetKind(); bool isAnd = (k == AND) ? true : false; @@ -1094,6 +1073,8 @@ namespace BEEV (pushNeg ? ASTFalse : ASTTrue) : (pushNeg ? ASTTrue : ASTFalse); + ASTVec outvec; + //do the work ASTVec::const_iterator next_it; for (ASTVec::const_iterator i = c.begin(), iend = c.end(); i != iend; i++) @@ -1168,7 +1149,6 @@ namespace BEEV (pushNeg ? nf->CreateNode(AND, outvec) : nf->CreateNode(OR,outvec)); - //output = FlattenOneLevel(output); break; } } @@ -1565,47 +1545,6 @@ namespace BEEV return output; } - //one level deep flattening - ASTNode Simplifier::FlattenOneLevel(const ASTNode& a) - { - const Kind k = a.GetKind(); - if (!(BVPLUS == k || AND == k || OR == k - //|| BVAND == k - //|| BVOR == k - )) - { - return a; - } - - ASTNode output; - // if(CheckSimplifyMap(a,output,false)) { - // //check memo table - // //cerr << "output of SimplifyTerm Cache: " << output << endl; - // return output; - // } - - const ASTVec& c = a.GetChildren(); - ASTVec o; - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) - { - const ASTNode& aaa = *it; - if (k == aaa.GetKind()) - { - const ASTVec& ac = aaa.GetChildren(); - o.insert(o.end(), ac.begin(), ac.end()); - } - else - o.push_back(aaa); - } - - if (is_Form_kind(k)) - output = nf->CreateNode(k, o); - else - output = nf->CreateTerm(k, a.GetValueWidth(), o); - - return output; - } //end of flattenonelevel() - ASTNode Simplifier::makeTower(const Kind k, const BEEV::ASTVec &children) @@ -2465,10 +2404,10 @@ namespace BEEV ASTNode identity = (BVAND == k) ? max : zero; ASTNode annihilator = (BVAND == k) ? zero : max; - ASTVec c = Flatten(inputterm).GetChildren(); + ASTVec c = FlattenKind(inputterm.GetKind(), inputterm.GetChildren()); SortByArith(c); + ASTVec constants; ASTVec o; - bool constant = true; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { @@ -2477,12 +2416,6 @@ namespace BEEV aaa = SimplifyTerm(aaa); assert(hasBeenSimplified(aaa)); - - if (BVCONST != aaa.GetKind()) - { - constant = false; - } - if (aaa == annihilator) { output = annihilator; @@ -2508,14 +2441,31 @@ namespace BEEV return output; } - - if (aaa != identity) + if (BVCONST == aaa.GetKind()) + { + constants.push_back(aaa); + } + else { o.push_back(aaa); } - } + while(constants.size() >=2) + { + ASTNode a = constants.back(); + constants.pop_back(); + ASTNode b = constants.back(); + constants.pop_back(); + + ASTNode c = BVConstEvaluator(nf->CreateTerm(inputterm.GetKind(),inputterm.GetValueWidth(), a,b)); + + constants.push_back(c); + + } + if (constants.size() != 0 && constants.back() != identity) + o.push_back(constants.back()); + switch (o.size()) { case 0: @@ -2526,11 +2476,7 @@ namespace BEEV break; default: SortByArith(o); - output = nf->CreateTerm(k, inputValueWidth, o); - if (constant) - { - output = BVConstEvaluator(output); - } + output = makeTower(inputterm.GetKind(),o ); break; } @@ -2597,7 +2543,7 @@ namespace BEEV assert(BVTypeCheck(output)); } } - break; + break; } case BVCONCAT: { diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 8a57d28..0798e2b 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -203,11 +203,6 @@ namespace BEEV ASTNode SimplifyForFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL); - ASTNode Flatten(const ASTNode& a); - - ASTNode FlattenOneLevel(const ASTNode& a); - - ASTNode FlattenAndOr(const ASTNode& a); ASTNode CombineLikeTerms(const ASTNode& a); ASTNode CombineLikeTerms(const ASTVec& a); -- 2.47.3