From: trevor_hansen Date: Tue, 1 Sep 2009 04:09:37 +0000 (+0000) Subject: * lhsminusrhs(..) does not perform its simplification if it will increase the number... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=85a1cdd4147230c3ce01f7bb4db12c01858b5024;p=francis%2Fstp.git * lhsminusrhs(..) does not perform its simplification if it will increase the number of PLUS nodes (which are expensive). * The Transform functions are now mostly non-member. The cache is created on entry to TopLevel and deleted on exit. * regress_smt only checks the smt-test folder, not its subfolders! These regression tests take under a minute to run. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@165 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/run_smt_tests.pl b/scripts/run_smt_tests.pl index c686c91..69fd71b 100755 --- a/scripts/run_smt_tests.pl +++ b/scripts/run_smt_tests.pl @@ -90,9 +90,9 @@ my %options = (); # The list of testcases to run # my @testcases = "../../stp-tests/smt-test"; -my @testcases1 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2"; -my @testcases2 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2"; -my @testcases3 = "../../stp-tests/smt-test/QF_AUFBV/platania"; +#my @testcases1 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2"; +#my @testcases2 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2"; +#my @testcases3 = "../../stp-tests/smt-test/QF_AUFBV/platania"; # Temporary array for STP options my @stpOptions = (); @@ -250,7 +250,7 @@ my $totalTime = time; my $defaultDir = `pwd`; $defaultDir =~ s/\n//; -foreach my $testcase ((@testcases,@testcases1,@testcases2,@testcases3)) { +foreach my $testcase ((@testcases)) { chdir $defaultDir or die "Cannot chdir to $defaultDir: $?"; my @testcasesTmp = (); if(-f $testcase) { push @testcasesTmp, $testcase; } diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index f67589a..ec02c4f 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -1265,12 +1265,13 @@ void BeevMgr::ClearAllTables(void) AlreadyPrintedSet.clear(); SimplifyMap->clear(); SimplifyNegMap->clear(); + ReferenceCount->clear(); SolverMap.clear(); AlwaysTrueFormMap.clear(); _arrayread_ite.clear(); _arrayread_symbol.clear(); _introduced_symbols.clear(); - TransformMap.clear(); + //TransformMap.clear(); _letid_expr_map->clear(); CounterExampleMap.clear(); ComputeFormulaMap.clear(); @@ -1324,12 +1325,12 @@ void BeevMgr::ClearAllCaches(void) AlreadyPrintedSet.clear(); SimplifyMap->clear(); SimplifyNegMap->clear(); + ReferenceCount->clear(); SolverMap.clear(); AlwaysTrueFormMap.clear(); _arrayread_ite.clear(); _arrayread_symbol.clear(); _introduced_symbols.clear(); - TransformMap.clear(); _letid_expr_map->clear(); CounterExampleMap.clear(); ComputeFormulaMap.clear(); @@ -1421,6 +1422,7 @@ BeevMgr::~BeevMgr() delete SimplifyMap; delete SimplifyNegMap; delete _letid_expr_map; + delete ReferenceCount; } } diff --git a/src/AST/AST.h b/src/AST/AST.h index bdcbdc6..58602ab 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -32,6 +32,7 @@ #include #include "ASTUtil.h" #include "ASTKind.h" +#include #include "../sat/core/Solver.h" //#include "../sat/simp/SimpSolver.h" //#include "../sat/unsound/UnsoundSimpSolver.h" @@ -1027,6 +1028,9 @@ inline unsigned int GetUnsignedConst(const ASTNode n) // Hash table from ASTNodes to ASTNodes typedef hash_map ASTNodeMap; +typedef hash_map ASTNodeCountMap; + + // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); @@ -1532,6 +1536,8 @@ public: ASTNode SimplifyTerm(const ASTNode& a); ASTNode SimplifyTermAux(const ASTNode& a); void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output); + void BuildReferenceCountMap(const ASTNode& b); + private: //memo table for simplifcation ASTNodeMap *SimplifyMap; @@ -1540,6 +1546,15 @@ private: ASTNodeSet AlwaysTrueFormMap; ASTNodeMap MultInverseMap; + + // The number of direct parents of each node. i.e. the number of times the pointer is in "children". + // When we simplify we want to be careful sometimes about using the context of a node. For example, + // given ((x + 23) = 2), the obvious simplification is to join the constants. However, if there are + // lots of references to the plus node. Then each time we simplify, we'll create an additional plus. + // nextpoweroftwo064.smt is the motivating benchmark. The splitting increased the number of pluses + // from 1 to 65. + ASTNodeCountMap *ReferenceCount; + public: ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg); ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2); @@ -1610,6 +1625,8 @@ public: ///print SAT solver statistics void PrintStats(MINISAT::Solver& stats); + void printCacheStatus(); + //from v8 int TopLevelSATAux(const ASTNode& query); @@ -1678,23 +1695,18 @@ private: ASTNodeSet _introduced_symbols; - /*Memoization map for TransformFormula/TransformTerm/TransformArray function - */ - ASTNodeMap TransformMap; - //count to keep track of new symbolic constants introduced //corresponding to Array Reads unsigned int _symbol_count; //Formula/Term Transformers. Let Expr Manager, Type Checker public: - //Functions that Transform ASTNodes - ASTNode TransformFormula(const ASTNode& query); - ASTNode TransformTerm(const ASTNode& term); + //Functions that Transform ASTNodes. TransformArray should be a non-member function, + // but it accesses private elements. Move it later. + ASTNode TransformFormula_TopLevel(const ASTNode& form); ASTNode TransformArray(const ASTNode& term); ASTNode TransformFiniteFor(const ASTNode& form); - ASTNode TranslateSignedDivModRem(const ASTNode& term); - void assertTransformPostConditions(const ASTNode & term); + //LET Management private: @@ -1931,6 +1943,7 @@ public: SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); _letid_expr_map = new ASTNodeMap(INITIAL_INTRODUCED_SYMBOLS_SIZE); + ReferenceCount = new ASTNodeCountMap(INITIAL_SIMPLIFY_MAP_SIZE); } ; diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 5d1d0bc..84bdde3 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -1101,6 +1101,23 @@ ASTNode BeevMgr::GetCounterExample(bool t, const ASTNode& expr) //################################################## //################################################## + +void BeevMgr::printCacheStatus() +{ + cerr << SimplifyMap->size() << endl; + cerr << SimplifyNegMap->size() << endl; + cerr << ReferenceCount->size() << endl; + cerr << TermsAlreadySeenMap.size() << endl; + + cerr << SimplifyMap->bucket_count() << endl; + cerr << SimplifyNegMap->bucket_count() << endl; + cerr << ReferenceCount->bucket_count() << endl; + cerr << TermsAlreadySeenMap.bucket_count() << endl; + + + +} + // FIXME: Don't use numeric codes. Use an enum type! //Acceps a query, calls the SAT solver and generates Valid/InValid. //if returned 0 then input is INVALID @@ -1179,12 +1196,13 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) SimplifyWrites_InPlace_Flag = false; Begin_RemoveWrites = false; - newq = TransformFormula(newq); - if (false) - assertTransformPostConditions(newq); + newq = TransformFormula_TopLevel(newq); ASTNodeStats("after transformation: ", newq); TermsAlreadySeenMap.clear(); + //if(stats_flag) + // printCacheStatus(); + int res; //solver instantiated here MINISAT::Solver newS; @@ -1369,12 +1387,12 @@ int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& writeAxiom = Create_ArrayWriteAxioms(it->first, it->second); if (ASTFalse == ComputeFormulaUsingModel(writeAxiom)) { - writeAxiom = TransformFormula(writeAxiom); + writeAxiom = TransformFormula_TopLevel(writeAxiom); FalseAxioms.push_back(writeAxiom); } else { - writeAxiom = TransformFormula(writeAxiom); + writeAxiom = TransformFormula_TopLevel(writeAxiom); RemainingAxioms.push_back(writeAxiom); } } diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index 459f0ed..84b3988 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -8,52 +8,78 @@ // -*- c++ -*- -/* Transform: +/* Transform: * * Converts signed Div/signed remainder/signed modulus into their * unsigned counterparts. Removes array selects and stores from * formula. Arrays are replaced by equivalent bit-vector variables */ + #include "AST.h" #include #include namespace BEEV { +ASTNode TransformFormula(const ASTNode& form); +ASTNode TranslateSignedDivModRem(const ASTNode& in); +ASTNode TransformTerm(const ASTNode& inputterm); +void assertTransformPostConditions(const ASTNode & term); + +ASTNodeMap* TransformMap; + +const bool debug_transform = false; + +// NB: This is the only function that should be called externally. It sets +// up the cache that the others use. +ASTNode BeevMgr::TransformFormula_TopLevel(const ASTNode& form) +{ + assert(TransformMap == NULL); + TransformMap = new ASTNodeMap(100); + ASTNode result = TransformFormula(form); + if (debug_transform) + assertTransformPostConditions(result); + TransformMap->clear(); + delete TransformMap; + TransformMap = NULL; + return result; +} + //Translates signed BVDIV,BVMOD and BVREM into unsigned variety -ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) +ASTNode TranslateSignedDivModRem(const ASTNode& in) { + BeevMgr& bm = in.GetBeevMgr(); assert(in.GetChildren().size() ==2); ASTNode dividend = in[0]; ASTNode divisor = in[1]; unsigned len = in.GetValueWidth(); - ASTNode hi1 = CreateBVConst(32, len - 1); - ASTNode one = CreateOneConst(1); - ASTNode zero = CreateZeroConst(1); + ASTNode hi1 = bm.CreateBVConst(32, len - 1); + ASTNode one = bm.CreateOneConst(1); + ASTNode zero = bm.CreateZeroConst(1); // create the condition for the dividend - ASTNode cond_dividend = CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)); + ASTNode cond_dividend = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)); // create the condition for the divisor - ASTNode cond_divisor = CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1)); + ASTNode cond_divisor = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1)); if (SBVREM == in.GetKind()) { //BVMOD is an expensive operation. So have the fewest bvmods possible. Just one. //Take absolute value. - ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend); - ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); + ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor); //create the modulus term - ASTNode modnode = CreateTerm(BVMOD, len, pos_dividend, pos_divisor); + ASTNode modnode = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor); //If the dividend is <0 take the unary minus. - ASTNode n = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, modnode), modnode); + ASTNode n = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, modnode), modnode); //put everything together, simplify, and return - return SimplifyTerm_TopLevel(n); + return bm.SimplifyTerm_TopLevel(n); } // This is the modulus of dividing rounding to -infinity. @@ -72,19 +98,19 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) // (bvneg (bvurem (bvneg s) (bvneg t))))))) //Take absolute value. - ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend); - ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); + ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor); - ASTNode urem_node = CreateTerm(BVMOD, len, pos_dividend, pos_divisor); + ASTNode urem_node = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor); // If the dividend is <0, then we negate the whole thing. - ASTNode rev_node = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node); + ASTNode rev_node = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, urem_node), urem_node); // if It's XOR <0 then add t (not its absolute value). - ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor); - ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); + ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); - return SimplifyTerm_TopLevel(n); + return bm.SimplifyTerm_TopLevel(n); } else if (SBVDIV == in.GetKind()) { @@ -104,25 +130,25 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) //else simply output BVDIV(dividend,divisor) //Take absolute value. - ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend); - ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); + ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor); - ASTNode divnode = CreateTerm(BVDIV, len, pos_dividend, pos_divisor); + ASTNode divnode = bm.CreateTerm(BVDIV, len, pos_dividend, pos_divisor); // A little confusing. Only negate the result if they are XOR <0. - ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor); - ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVUMINUS, len, divnode), divnode); + ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVUMINUS, len, divnode), divnode); - return SimplifyTerm_TopLevel(n); + return bm.SimplifyTerm_TopLevel(n); } FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in); - return ASTUndefined; + return bm.CreateNode(UNDEFINED); }//end of TranslateSignedDivModRem() // Check that the transformations have occurred. -void BeevMgr::assertTransformPostConditions(const ASTNode & term) +void assertTransformPostConditions(const ASTNode & term) { const Kind k = term.GetKind(); @@ -148,8 +174,12 @@ void BeevMgr::assertTransformPostConditions(const ASTNode & term) } } -ASTNode BeevMgr::TransformFormula(const ASTNode& form) +ASTNode TransformFormula(const ASTNode& form) { + BeevMgr& bm = form.GetBeevMgr(); + + assert(TransformMap != null); + ASTNode result; ASTNode simpleForm = form; @@ -161,7 +191,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) } ASTNodeMap::iterator iter; - if ((iter = TransformMap.find(simpleForm)) != TransformMap.end()) + if ((iter = TransformMap->find(simpleForm)) != TransformMap->end()) return iter->second; switch (k) @@ -176,7 +206,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) { ASTVec c; c.push_back(TransformFormula(simpleForm[0])); - result = CreateNode(NOT, c); + result = bm.CreateNode(NOT, c); break; } case BVLT: @@ -192,14 +222,14 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) ASTVec c; c.push_back(TransformTerm(simpleForm[0])); c.push_back(TransformTerm(simpleForm[1])); - result = CreateNode(k, c); + result = bm.CreateNode(k, c); break; } case EQ: { ASTNode term1 = TransformTerm(simpleForm[0]); ASTNode term2 = TransformTerm(simpleForm[1]); - result = CreateSimplifiedEQ(term1, term2); + result = bm.CreateSimplifiedEQ(term1, term2); break; } case AND: @@ -219,7 +249,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) vec.push_back(o); } - result = CreateNode(k, vec); + result = bm.CreateNode(k, vec); break; } default: @@ -229,17 +259,22 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) { cerr << "The input is: " << simpleForm << endl; cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl; - FatalError("TransformFormula: Illegal kind: ", ASTUndefined, k); + FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k); } break; } - //assert(BVTypeCheckRecursive(result)); - TransformMap[simpleForm] = result; + + if (simpleForm.GetChildren().size() > 0) + (*TransformMap)[simpleForm] = result; return result; } //End of TransformFormula -ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) +ASTNode TransformTerm(const ASTNode& inputterm) { + assert(TransformMap != null); + + BeevMgr& bm = inputterm.GetBeevMgr(); + ASTNode result; ASTNode term = inputterm; @@ -247,7 +282,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) if (!is_Term_kind(k)) FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k); ASTNodeMap::iterator iter; - if ((iter = TransformMap.find(term)) != TransformMap.end()) + if ((iter = TransformMap->find(term)) != TransformMap->end()) return iter->second; switch (k) { @@ -267,7 +302,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) FatalError("TransformTerm: this kind is not supported", term); break; case READ: - result = TransformArray(term); + result = bm.TransformArray(term); break; case ITE: { @@ -278,7 +313,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) thn = TransformTerm(thn); els = TransformTerm(els); //result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els); - result = CreateSimplifiedTermITE(cond, thn, els); + result = bm.CreateSimplifiedTermITE(cond, thn, els); result.SetIndexWidth(term.GetIndexWidth()); break; } @@ -295,7 +330,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) o.push_back(TransformTerm(*it)); } - result = CreateTerm(k, width, o); + result = bm.CreateTerm(k, width, o); result.SetIndexWidth(indexwidth); Kind k = result.GetKind(); @@ -315,9 +350,9 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) // result is embedded unchanged inside the result. unsigned inputValueWidth = result.GetValueWidth(); - ASTNode zero = CreateZeroConst(inputValueWidth); - ASTNode one = CreateOneConst(inputValueWidth); - result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result); + ASTNode zero = bm.CreateZeroConst(inputValueWidth); + ASTNode one = bm.CreateOneConst(inputValueWidth); + result = bm.CreateTerm(ITE, inputValueWidth, bm.CreateNode(EQ, zero, bottom), one, result); } } } @@ -327,7 +362,8 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) break; } - TransformMap[term] = result; + if (term.GetChildren().size() > 0) + (*TransformMap)[term] = result; if (term.GetValueWidth() != result.GetValueWidth()) FatalError("TransformTerm: result and input terms are of different length", result); if (term.GetIndexWidth() != result.GetIndexWidth()) @@ -351,6 +387,8 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) */ ASTNode BeevMgr::TransformArray(const ASTNode& term) { + assert(TransformMap != null); + ASTNode result = term; const unsigned int width = term.GetValueWidth(); @@ -359,7 +397,7 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term) FatalError("TransformArray: input term is of wrong kind: ", ASTUndefined); ASTNodeMap::iterator iter; - if ((iter = TransformMap.find(term)) != TransformMap.end()) + if ((iter = TransformMap->find(term)) != TransformMap->end()) return iter->second; //'term' is of the form READ(arrName, readIndex) @@ -574,7 +612,7 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term) break; } - TransformMap[term] = result; + (*TransformMap)[term] = result; return result; } //end of TransformArray() diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y index 36f84f5..c8b3359 100644 --- a/src/parser/smtlib.y +++ b/src/parser/smtlib.y @@ -776,7 +776,7 @@ an_nonbvconst_term: BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3); BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); BEEV::ASTNode output = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$7,hi,low); - BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(output)); + BEEV::ASTNode * n = new BEEV::ASTNode(output); BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); $$ = n; delete $7; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index ba81303..6e73afc 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1,4 +1,4 @@ -/******************************************************************** + /******************************************************************** * AUTHORS: Vijay Ganesh * * BEGIN DATE: November, 2005 @@ -35,8 +35,22 @@ bool BeevMgr::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg return false; } +// Push any reference count used by the key to the value. void BeevMgr::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg) { + // If there are references to the key, add them to the references of the value. + ASTNodeCountMap::const_iterator itKey, itValue; + itKey = ReferenceCount->find(key); + if (itKey != ReferenceCount->end()) + { + itValue = ReferenceCount->find(value); + if (itValue != ReferenceCount->end()) + (*ReferenceCount)[value] = itValue->second + itKey->second; + else + (*ReferenceCount)[value] = itKey->second; + } + + if (pushNeg) (*SimplifyNegMap)[key] = value; else @@ -138,10 +152,9 @@ int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b) //a is of the form READ(Arr,const), and b is const, or //a is of the form var, and b is const - if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && - (k2 == BVCONST))) - // || -// k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST))) + if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST))) + // || + // k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST))) return 1; if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2)) @@ -199,9 +212,37 @@ ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg) return out; } +void BeevMgr::BuildReferenceCountMap(const ASTNode& b) +{ + if (b.GetChildren().size() == 0) + return; + + ASTNodeCountMap::iterator it, itend; + + it = ReferenceCount->find(b); + if (it == ReferenceCount->end()) + { + (*ReferenceCount)[b] = 1; + } + else + { + (*ReferenceCount)[b] = it->second + 1; + return; + } + + const ASTVec& c = b.GetChildren(); + ASTVec::const_iterator itC = c.begin(); + ASTVec::const_iterator itendC = c.end(); + for (; itC != itendC; itC++) + { + BuildReferenceCountMap(*itC); + } +} + ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) { ResetSimplifyMaps(); + BuildReferenceCountMap(b); ASTNode out = SimplifyFormula(b, pushNeg); ResetSimplifyMaps(); return out; @@ -209,8 +250,8 @@ ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) { - if (!optimize_flag) - return b; + if (!optimize_flag) + return b; Kind kind = b.GetKind(); if (BOOLEAN_TYPE != b.GetType()) @@ -283,8 +324,7 @@ ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg) { ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) { if (!optimize_flag) - return a; - + return a; ASTNode output; if (CheckSimplifyMap(a, output, pushNeg)) @@ -554,7 +594,6 @@ ASTNode BeevMgr::PullUpITE(const ASTNode& in) return result; } - //takes care of some simple ITE Optimizations in the context of equations ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) { @@ -653,9 +692,9 @@ ASTNode BeevMgr::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2) Kind k2 = in2.GetKind(); // if (!optimize_flag) -// { -// return CreateNode(EQ, in1, in2); -// } + // { + // return CreateNode(EQ, in1, in2); + // } if (in1 == in2) //terms are syntactically the same @@ -1117,7 +1156,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg) { if (!optimize_flag) - return b; + return b; ASTNode output; if (CheckSimplifyMap(b, output, pushNeg)) @@ -1253,10 +1292,9 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) //cout << "SimplifyTerm: input: " << a << endl; if (!optimize_flag) { - return inputterm; + return inputterm; } - ASTNode output; assert(BVTypeCheck(inputterm)); //######################################## @@ -2921,6 +2959,14 @@ ASTNode BeevMgr::LhsMinusRhs(const ASTNode& eq) swap_flag = true; } + ASTNodeCountMap::const_iterator it; + it = ReferenceCount->find(lhs); + if (it != ReferenceCount->end()) + { + if (it->second > 1) + return eq; + } + unsigned int len = lhs.GetValueWidth(); ASTNode zero = CreateZeroConst(len); //right is -1*(rhs): Simplify(-1*rhs) @@ -3518,8 +3564,8 @@ bool BeevMgr::BVConstIsOdd(const ASTNode& c) //The big substitution function ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a) { - if (!wordlevel_solve_flag) - return a; + if (!wordlevel_solve_flag) + return a; ASTNode output = a; //if the variable has been solved for, then simply return it @@ -3656,11 +3702,17 @@ bool BeevMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term) // clears() in particular. void BeevMgr::ResetSimplifyMaps() { + SimplifyMap->clear(); delete SimplifyMap; SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); + SimplifyNegMap->clear(); delete SimplifyNegMap; SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE); + + ReferenceCount->clear(); + delete ReferenceCount; + ReferenceCount = new ASTNodeCountMap(INITIAL_SIMPLIFY_MAP_SIZE); } }