From c8954c8746a9bb18f8d346efca56ed7536f94b07 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 9 Jun 2010 03:15:23 +0000 Subject: [PATCH] * In the bvsolver perform cheap tests which maybe short-cut before expensive tests. * Lazily count the number of symbols in the bvsolver. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@820 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/CountOfSymbols.h | 27 +++------- src/simplifier/bvsolver.cpp | 91 +++++++-------------------------- 2 files changed, 27 insertions(+), 91 deletions(-) diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h index 3c10ab0..1fee0f1 100644 --- a/src/simplifier/CountOfSymbols.h +++ b/src/simplifier/CountOfSymbols.h @@ -3,16 +3,14 @@ #include "../AST/AST.h" #include -#include "simplifier.h" + +// Count the number of times each symbol appears in the input term. +// This can be expensive to build for large terms, so it's built lazily. namespace BEEV { class CountOfSymbols { - - //collect all the vars in the lhs and rhs - //Build this only if it's needed. - typedef hash_map ASTNodeToIntMap; @@ -20,20 +18,11 @@ class CountOfSymbols { const ASTNode& top; bool loaded; - ASTNodeSet TermsAlreadySeenMap; - - //collects the vars in the term 'lhs' into the multiset Vars - void VarsInTheTerm_TopLevel(const ASTNode& lhs) { - TermsAlreadySeenMap.clear(); - VarsInTheTerm(lhs); - } + ASTNodeSet visited; - //collects the vars in the term 'lhs' into the multiset Vars void VarsInTheTerm(const ASTNode& term) { - ASTNodeSet::const_iterator it; - bool inserted = (TermsAlreadySeenMap.insert(term).second); - if (!inserted) + if (visited.find(term) != visited.end()) return; switch (term.GetKind()) { @@ -63,8 +52,7 @@ class CountOfSymbols { } } - //ensures that you don't double count. if you have seen the term - //once, then memoize + visited.insert(term); return; } //end of VarsInTheTerm() @@ -78,8 +66,9 @@ public: bool single(const ASTNode &m) { if (!loaded) { - VarsInTheTerm_TopLevel(top); + VarsInTheTerm(top); loaded = true; + visited.clear(); } ASTNodeToIntMap::const_iterator it = Vars.find(m); diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index e1d9edd..bca6fdd 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -11,6 +11,7 @@ #include "../AST/AST.h" #include "../STPManager/STPManager.h" #include "bvsolver.h" +#include "CountOfSymbols.h" //This file contains the implementation of member functions of //bvsolver class, which represents the bitvector arithmetic linear @@ -196,63 +197,6 @@ namespace BEEV return false; } //end of UpdateSolverMap() - //collects the vars in the term 'lhs' into the multiset Vars - void BVSolver::VarsInTheTerm_TopLevel(const ASTNode& lhs, - ASTNodeMultiSet& Vars) - { - TermsAlreadySeenMap.clear(); - VarsInTheTerm(lhs, Vars); - } - - //collects the vars in the term 'lhs' into the multiset Vars - void BVSolver::VarsInTheTerm(const ASTNode& term, ASTNodeMultiSet& Vars) - { - ASTNode a = term; - ASTNodeMap::iterator it; - if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) - { - //if the term has been seen, then simply return - return; - } - - switch (term.GetKind()) - { - case BVCONST: - return; - case SYMBOL: - //cerr << "debugging: symbol added: " << term << endl; - Vars.insert(term); - return; - case READ: - //skip the arrayname, provided the arrayname is a SYMBOL - if (SYMBOL == term[0].GetKind()) - { - VarsInTheTerm(term[1], Vars); - } - else - { - VarsInTheTerm(term[0], Vars); - VarsInTheTerm(term[1], Vars); - } - break; - default: - { - ASTVec c = term.GetChildren(); - for (ASTVec::iterator - it = c.begin(), itend = c.end(); it != itend; it++) - { - VarsInTheTerm(*it, Vars); - } - break; - } - } - - //ensures that you don't double count. if you have seen the term - //once, then memoize - TermsAlreadySeenMap[term] = ASTTrue; - return; - } //end of VarsInTheTerm() - bool BVSolver::DoNotSolveThis(const ASTNode& var) { if (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end()) @@ -275,8 +219,7 @@ namespace BEEV ASTNode zero = _bm->CreateZeroConst(32); //collect all the vars in the lhs and rhs - ASTNodeMultiSet Vars; - VarsInTheTerm_TopLevel(lhs, Vars); + CountOfSymbols count(lhs); //handle BVPLUS case ASTVec c = lhs.GetChildren(); @@ -290,19 +233,22 @@ namespace BEEV { ASTNode monom = *it; if (SYMBOL == monom.GetKind() - && Vars.count(monom) == 1 - && !VarSeenInTerm(monom, rhs) - && !DoNotSolveThis(monom) && !chosen_symbol) + && !chosen_symbol + && !DoNotSolveThis(monom) + && count.single(monom) + && !VarSeenInTerm(monom, rhs) + ) { outmonom = monom; chosen_symbol = true; } else if (BVUMINUS == monom.GetKind() - && SYMBOL == monom[0].GetKind() - && Vars.count(monom[0]) == 1 - && !DoNotSolveThis(monom[0]) - && !VarSeenInTerm(monom[0], rhs) - && !chosen_symbol) + && SYMBOL == monom[0].GetKind() + && !chosen_symbol + && !DoNotSolveThis(monom[0]) + && count.single(monom[0]) + && !VarSeenInTerm(monom[0], rhs) + ) { //cerr << "Chosen Monom: " << monom << endl; outmonom = monom; @@ -330,17 +276,18 @@ namespace BEEV if (BVMULT == monom.GetKind() && BVCONST == monom[0].GetKind() && _simp->BVConstIsOdd(monom[0]) + && !chosen_odd + && !DoNotSolveThis(var) && ((SYMBOL == var.GetKind() - && Vars.count(var) == 1) + && count.single(var)) || (BVEXTRACT == var.GetKind() && SYMBOL == var[0].GetKind() && BVCONST == var[1].GetKind() && zero == var[2] - && !VarSeenInTerm(var[0], rhs) - && !DoNotSolveThis(var[0]))) - && !DoNotSolveThis(var) + && !DoNotSolveThis(var[0]) + && !VarSeenInTerm(var[0], rhs))) && !VarSeenInTerm(var, rhs) - && !chosen_odd) + ) { //monom[0] is odd. outmonom = monom; -- 2.47.3