From b00d21e47d15b9715e6cc2e1a41d20665e01891d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 11 Jun 2010 15:23:04 +0000 Subject: [PATCH] Remove the experimental bvsolver. I've copied its changes into the main bvsolver. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@833 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/bvsolver.cpp | 183 ++++++-- src/simplifier/bvsolverExp.cpp | 831 --------------------------------- src/simplifier/bvsolverExp.h | 152 ------ 3 files changed, 136 insertions(+), 1030 deletions(-) delete mode 100644 src/simplifier/bvsolverExp.cpp delete mode 100644 src/simplifier/bvsolverExp.h diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 95d5400..4bdc3cd 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -38,11 +38,14 @@ //4. Outside the solver, Substitute and Re-normalize the input DAG namespace BEEV { + const bool flatten_ands = false; + const bool sort_extracts_last = false; + //check the solver map for 'key'. If key is present, then return the //value by reference in the argument 'output' bool BVSolver::CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output) { - ASTNodeMap::iterator it; + ASTNodeMap::const_iterator it; if ((it = FormulasAlreadySolvedMap.find(key)) != FormulasAlreadySolvedMap.end()) { @@ -108,6 +111,7 @@ namespace BEEV return div_by_2; } //end of SplitEven_into_Oddnum_PowerOf2() +#if 0 //Checks if there are any ARRAYREADS in the term, after the //alreadyseenmap is cleared, i.e. traversing a new term altogether bool BVSolver::CheckForArrayReads_TopLevel(const ASTNode& term) @@ -163,6 +167,7 @@ namespace BEEV TermsAlreadySeenMap[term] = ASTFalse; return false; } //end of CheckForArrayReads() +#endif bool BVSolver::DoNotSolveThis(const ASTNode& var) { @@ -181,24 +186,22 @@ namespace BEEV FatalError("ChooseMonom: input must be a EQ", eq); } - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(32); + const ASTNode& lhs = eq[0]; + const ASTNode& rhs = eq[1]; //collect all the vars in the lhs and rhs CountOfSymbols count(lhs); //handle BVPLUS case - ASTVec c = lhs.GetChildren(); + const ASTVec& c = lhs.GetChildren(); ASTVec o; ASTNode outmonom = ASTUndefined; bool chosen_symbol = false; - bool chosen_odd = false; //choose variables with no coeffs - for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode monom = *it; + const ASTNode& monom = *it; if (SYMBOL == monom.GetKind() && !chosen_symbol && !DoNotSolveThis(monom) @@ -230,15 +233,18 @@ namespace BEEV //try to choose only odd coeffed variables first if (!chosen_symbol) { - o.clear(); - for (ASTVec::iterator + ASTNode zero = _bm->CreateZeroConst(32); + bool chosen_odd = false; + + o.clear(); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode monom = *it; + const ASTNode& monom = *it; ASTNode var = (BVMULT == monom.GetKind()) ? monom[1] : - _bm->CreateNode(UNDEFINED); + ASTUndefined; if (BVMULT == monom.GetKind() && BVCONST == monom[0].GetKind() @@ -285,23 +291,34 @@ namespace BEEV } ASTNode output = input; - if (CheckAlreadySolvedMap(input, output)) - { - return output; - } //get the lhs and the rhs, and case-split on the lhs kind ASTNode lhs = eq[0]; ASTNode rhs = eq[1]; + + // if only one side is a constant, it should be on the RHS. + if (((BVCONST == lhs.GetKind()) ^ (BVCONST == rhs.GetKind())) + && (lhs.GetKind() == BVCONST)) { + lhs = eq[1]; + rhs = eq[0]; + eq = _bm->CreateNode(EQ, lhs, rhs); // If "return eq" is called, return the arguments in the correct order. + } + + if (CheckAlreadySolvedMap(eq, output)) + { + return output; + } + + if (BVPLUS == lhs.GetKind()) { - ASTNode chosen_monom = _bm->CreateNode(UNDEFINED); + ASTNode chosen_monom = ASTUndefined; ASTNode leftover_lhs; //choose monom makes sure that it gets only those vars that //occur exactly once in lhs and rhs put together chosen_monom = ChooseMonom(eq, leftover_lhs); - if (chosen_monom == _bm->CreateNode(UNDEFINED)) + if (chosen_monom == ASTUndefined) { //no monomial was chosen return eq; @@ -314,10 +331,9 @@ namespace BEEV leftover_lhs = _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, len, leftover_lhs)); - ASTNode newrhs = + rhs = _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs)); lhs = chosen_monom; - rhs = newrhs; } //end of if(BVPLUS ...) if (BVUMINUS == lhs.GetKind()) @@ -380,7 +396,7 @@ namespace BEEV // } case BVEXTRACT: { - ASTNode zero = _bm->CreateZeroConst(32); + const ASTNode zero = _bm->CreateZeroConst(32); if (!(SYMBOL == lhs[0].GetKind() && BVCONST == lhs[1].GetKind() @@ -438,7 +454,7 @@ namespace BEEV } bool ChosenVar_Is_Extract = - (BVEXTRACT == lhs[1].GetKind()) ? true : false; + (BVEXTRACT == lhs[1].GetKind()); //if coeff is even, then we know that all the coeffs in the eqn //are even. Simply return the eqn @@ -449,7 +465,7 @@ namespace BEEV ASTNode a = _simp->MultiplicativeInverse(lhs[0]); ASTNode chosenvar = - (BVEXTRACT == lhs[1].GetKind()) ? lhs[1][0] : lhs[1]; + ChosenVar_Is_Extract ? lhs[1][0] : lhs[1]; ASTNode chosenvar_value = _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, rhs.GetValueWidth(), @@ -479,7 +495,7 @@ namespace BEEV if (ChosenVar_Is_Extract) { - ASTNode var = lhs[1][0]; + const ASTNode& var = lhs[1][0]; ASTNode newvar = _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth()); newvar = @@ -500,15 +516,66 @@ namespace BEEV return output; } //end of BVSolve_Odd() + bool containsExtract(const ASTNode& n, ASTNodeSet& visited) { + if (visited.find(n) != visited.end()) + return false; + + if (BVEXTRACT == n.GetKind()) + return true; + + for (unsigned i = 0; i < n.Degree(); i++) { + if (containsExtract(n[i], visited)) + return true; + } + visited.insert(n); + return false; + } + + // The order that monomials are chosen in from the system of equations is important. + // In particular if a symbol is chosen that is extracted over, and that symbol + // appears elsewhere in the system. Then those other positions will be replaced by + // an equation that contains a concatenation. + // For example, given: + // 5x[5:1] + 4y[5:1] = 6 + // 3x + 2y = 5 + // + // If the x that is extracted over is selected as the monomial, then the later eqn. will be + // rewritten as: + // 3(concat (1/5)(6-4y[5:1]) v) + 2y =5 + // where v is a fresh one-bit variable. + // What's particularly bad about this is that the "y" appears now in two places in the eqn. + // Because it appears in two places it can't be simplified by this algorithm + // This sorting function is a partial solution. Ideally the "best" monomial should be + // chosen from the system of equations. + void specialSort(ASTVec& c) { + // Place equations that don't contain extracts before those that do. + deque extracts; + ASTNodeSet v; + + for (unsigned i = 0; i < c.size(); i++) { + if (containsExtract(c[i], v)) + extracts.push_back(c[i]); + else + extracts.push_front(c[i]); + } + + c.clear(); + deque::iterator it = extracts.begin(); + while (it != extracts.end()) { + c.push_back(*it++); + } + } + //The toplevel bvsolver(). Checks if the formula has already been //solved. If not, the solver() is invoked. If yes, then simply drop //the formula - ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input) + ASTNode BVSolver::TopLevelBVSolve(const ASTNode& _input) { // if (!wordlevel_solve_flag) // { // return input; // } + ASTNode input = _input; Kind k = input.GetKind(); if (!(EQ == k || AND == k)) @@ -523,6 +590,27 @@ namespace BEEV return output; } + if (flatten_ands && AND == k) + { + ASTNode n = input; + while (true) { + ASTNode nold = n; + n = _simp->FlattenOneLevel(n); + if ((n == nold)) + break; + } + + input = n; + + // When flattening simplifications will be applied to the node, potentially changing it's type: + // (AND x (ANY (not x) y)) gives us FALSE. + if (!(EQ == n.GetKind() || AND == n.GetKind())) { + { + return n; + } + } + } + _bm->GetRunTimes()->start(RunTimes::BVSolver); ASTVec o; ASTVec c; @@ -530,6 +618,10 @@ namespace BEEV c.push_back(input); else c = input.GetChildren(); + + if (sort_extracts_last) + specialSort(c); + ASTVec eveneqns; bool any_solved = false; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) @@ -592,7 +684,7 @@ namespace BEEV ASTTrue; output = _bm->CreateNode(AND, output, evens); - UpdateAlreadySolvedMap(input, output); + UpdateAlreadySolvedMap(_input, output); _bm->GetRunTimes()->stop(RunTimes::BVSolver); return output; } //end of TopLevelBVSolve() @@ -609,7 +701,7 @@ namespace BEEV ASTNode lhs = eq[0]; ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); + const ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); //lhs must be a BVPLUS, and rhs must be a BVCONST if (!(BVPLUS == lhs.GetKind() && zero == rhs)) { @@ -617,13 +709,13 @@ namespace BEEV return eq; } - ASTVec lhs_c = lhs.GetChildren(); + const ASTVec& lhs_c = lhs.GetChildren(); ASTNode savetheconst = rhs; - for (ASTVec::iterator + for (ASTVec::const_iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++) { - ASTNode aaa = *it; - Kind itk = aaa.GetKind(); + const ASTNode aaa = *it; + const Kind itk = aaa.GetKind(); if (BVCONST == itk) { @@ -690,14 +782,15 @@ namespace BEEV //power_of_2 holds the exponent of 2 in the coeff unsigned int power_of_2 = 0; //we need this additional variable to find the lowest power of 2 - unsigned int power_of_2_lowest = 0xffffffff; + unsigned int power_of_2_lowest = ~0; //the monom which has the least power of 2 in the coeff - ASTNode monom_with_best_coeff; + //ASTNode monom_with_best_coeff; for (ASTVec::iterator jt = input_c.begin(), jtend = input_c.end(); jt != jtend; jt++) { ASTNode eq = *jt; + assert(EQ == eq.GetKind()); ASTNode lhs = eq[0]; ASTNode rhs = eq[1]; ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); @@ -707,14 +800,13 @@ namespace BEEV return input; } - ASTVec lhs_c = lhs.GetChildren(); - //ASTNode odd; - for (ASTVec::iterator + const ASTVec& lhs_c = lhs.GetChildren(); + for (ASTVec::const_iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++) { - ASTNode aaa = *it; - Kind itk = aaa.GetKind(); + const ASTNode aaa = *it; + const Kind itk = aaa.GetKind(); if (!(BVCONST == itk && !_simp->BVConstIsOdd(aaa)) && !(BVMULT == itk @@ -734,7 +826,7 @@ namespace BEEV if (power_of_2 < power_of_2_lowest) { power_of_2_lowest = power_of_2; - monom_with_best_coeff = aaa; + //monom_with_best_coeff = aaa; } power_of_2 = 0; }//end of inner for loop @@ -742,6 +834,7 @@ namespace BEEV //get the exponent power_of_2 = power_of_2_lowest; + assert(power_of_2 > 0); //if control is here, we are gauranteed that we have chosen a //monomial with fewest powers of 2 @@ -777,14 +870,14 @@ namespace BEEV two_const, two)); } - ASTVec lhs_c = lhs.GetChildren(); + const ASTVec& lhs_c = lhs.GetChildren(); ASTVec lhs_out; - for (ASTVec::iterator + for (ASTVec::const_iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++) { ASTNode aaa = *it; - Kind itk = aaa.GetKind(); + const Kind itk = aaa.GetKind(); if (BVCONST == itk) { aaa = @@ -811,11 +904,7 @@ namespace BEEV coeff, low_minus_one, low_zero)); - ASTNode upper_x, lower_x; - //upper_x = - //_simp->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, - //power_of_2, aaa[1], hi, low)); - lower_x = + ASTNode lower_x = _simp->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, newlen, aaa[1], diff --git a/src/simplifier/bvsolverExp.cpp b/src/simplifier/bvsolverExp.cpp deleted file mode 100644 index cc1f6a1..0000000 --- a/src/simplifier/bvsolverExp.cpp +++ /dev/null @@ -1,831 +0,0 @@ -// Experimental bvsolver. - - -/******************************************************************** - * AUTHORS: Vijay Ganesh, Trevor Hansen - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -#include "../AST/AST.h" -#include "bvsolverExp.h" -#include -#include "simplifier.h" -#include "CountOfSymbols.h" - -//This file contains the implementation of member functions of -//bvsolver class, which represents the bitvector arithmetic linear -//solver. Please also refer the STP's CAV 2007 paper for the -//complete description of the linear solver algorithm -// -//The bitvector solver is a partial solver, i.e. it does not solve -//for all variables in the system of equations. it is -//best-effort. it relies on the SAT solver to be complete. -// -//The BVSolver assumes that the input equations are normalized, and -//have liketerms combined etc. -// -//0. Traverse top-down over the input DAG, looking for a conjunction -//0. of equations. if you find one, then for each equation in the -//0. conjunction, do the following steps. -// -//1. check for Linearity of the input equation -// -//2. Solve for a "chosen" variable. The variable should occur -//2. exactly once and must have an odd coeff. Refer STP's CAV 2007 -//2. paper for actual solving procedure -// -//4. Outside the solver, Substitute and Re-normalize the input DAG -namespace BEEV { -const bool bv_debug = false; - -//check the solver map for 'key'. If key is present, then return the -//value by reference in the argument 'output' -bool BVSolverExp::CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output) { - ASTNodeMap::const_iterator it; - if ((it = FormulasAlreadySolvedMap.find(key)) - != FormulasAlreadySolvedMap.end()) { - output = it->second; - return true; - } - return false; -} //CheckAlreadySolvedMap() - -void BVSolverExp::UpdateAlreadySolvedMap(const ASTNode& key, - const ASTNode& value) { - FormulasAlreadySolvedMap[key] = value; -} //end of UpdateAlreadySolvedMap() - -//Accepts an even number "in", and splits it into an odd number and -//a power of 2. i.e " in = b.(2^k) ". returns the odd number, and -//the power of two by reference. -//An "in" of zero returns a large shift. -void BVSolverExp::SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, - unsigned int& number_shifts) { - if (BVCONST != in.GetKind() || simplifier->BVConstIsOdd(in)) { - FatalError( - "BVSolver:SplitNum_Odd_PowerOf2: input must be a BVCONST and even\n", - in); - } - - for (number_shifts = 0; number_shifts < in.GetValueWidth() - && !CONSTANTBV::BitVector_bit_test(in.GetBVConst(), number_shifts); number_shifts++) { - }; - assert(number_shifts >0); -} -#if 0 -ASTNode OLDSplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts) -{ - if (BVCONST != in.GetKind() || simplifier->BVConstIsOdd(in)) - { - FatalError("BVSolver:SplitNum_Odd_PowerOf2: input must be a BVCONST and even\n", in); - } - - unsigned int len = in.GetValueWidth(); - ASTNode zero = _bm->CreateZeroConst(len); - ASTNode two = _bm->CreateTwoConst(len); - ASTNode div_by_2 = in; - ASTNode mod_by_2 = _bm->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two)); - while (mod_by_2 == zero) - { - div_by_2 = _bm->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, div_by_2, two)); - number_shifts++; - mod_by_2 = _bm->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two)); - } - return div_by_2; -} //end of SplitEven_into_Oddnum_PowerOf2() - -//Checks if there are any ARRAYREADS in the term, after the -//alreadyseenmap is cleared, i.e. traversing a new term altogether - - -bool BVSolver::CheckForArrayReads_TopLevel(const ASTNode& term) -{ - TermsAlreadySeenMap.clear(); - return CheckForArrayReads(term); -} - -//Checks if there are any ARRAYREADS in the term -bool BVSolver::CheckForArrayReads(const ASTNode& term) -{ - ASTNode a = term; - ASTNodeMap::iterator it; - if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) - { - //if the term has been seen, then simply return true, else - //return false - if (ASTTrue == (it->second)) - { - return true; - } - else - { - return false; - } - } - - switch (term.GetKind()) - { - case READ: - //an array read has been seen. Make an entry in the map and - //return true - TermsAlreadySeenMap[term] = ASTTrue; - return true; - default: - { - ASTVec c = term.GetChildren(); - for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) - { - if (CheckForArrayReads(*it)) - { - return true; - } - } - break; - } - } - - //If control is here, then it means that no arrayread was seen for - //the input 'term'. Make an entry in the map with the term as key - //and FALSE as value. - TermsAlreadySeenMap[term] = ASTFalse; - return false; -} //end of CheckForArrayReads() -#endif - -bool BVSolverExp::DoNotSolveThis(const ASTNode& var) { - if (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end()) { - if (bv_debug) { - cerr << "DoNotSolveThis. Do Not Solve for:" << var; - } - return true; - } - return false; -} - -//chooses a variable in the lhs and returns the chosen variable -ASTNode BVSolverExp::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs) { - if (!(EQ == eq.GetKind() && BVPLUS == eq[0].GetKind())) { - FatalError("ChooseMonom: input must be a EQ", eq); - } - - const ASTNode& lhs = eq[0]; - const ASTNode& rhs = eq[1]; - - assert(lhs.Degree() > 1); - - CountOfSymbols Vars(eq); - - const ASTVec& c = lhs.GetChildren(); - ASTVec o; - ASTNode outmonom = _bm->CreateNode(UNDEFINED); - bool chosen_symbol = false; - - //choose variables with no coeffs. - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - const ASTNode& monom = *it; - if (SYMBOL == monom.GetKind() && !DoNotSolveThis(monom) - && !chosen_symbol && Vars.single(monom)) { - outmonom = monom; - chosen_symbol = true; - } else if (BVUMINUS == monom.GetKind() && SYMBOL == monom[0].GetKind() - && !DoNotSolveThis(monom[0]) && !chosen_symbol && Vars.single( - monom[0])) { - //cerr << "Chosen Monom: " << monom << endl; - outmonom = monom; - chosen_symbol = true; - } else { - o.push_back(monom); - } - } - - //try to choose only odd coeffed variables. - if (!chosen_symbol) { - bool chosen_odd = false; - const ASTNode& zero = _bm->CreateZeroConst(32); - o.clear(); - - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it - != itend; it++) { - const ASTNode& monom = *it; - ASTNode var = (BVMULT == monom.GetKind()) ? monom[1] - : _bm->CreateNode(UNDEFINED); - - if (BVMULT == monom.GetKind() && BVCONST == monom[0].GetKind() - && simplifier->BVConstIsOdd(monom[0]) && ((SYMBOL == var.GetKind() - && Vars.single(var)) || (BVEXTRACT == var.GetKind() - && SYMBOL == var[0].GetKind() && BVCONST - == var[1].GetKind() && zero == var[2] - && Vars.single(var[0]) && !DoNotSolveThis(var[0]))) - && !DoNotSolveThis(var) && !_bm->VarSeenInTerm(var, rhs) - && !chosen_odd && Vars.single(var)) { - //monom[0] is odd. - outmonom = monom; - chosen_odd = true; - } else { - o.push_back(monom); - } - } - } - - modifiedlhs = (o.size() > 1) ? _bm->CreateTerm(BVPLUS, lhs.GetValueWidth(), - o) : o[0]; - return outmonom; -} //end of choosemonom() - -//solver function which solves for variables with odd coefficient -ASTNode BVSolverExp::BVSolve_Odd(const ASTNode& eq_original) { - ASTNode eq = eq_original; - - if (!(EQ == eq.GetKind())) { - return eq; - } - - //get the lhs and the rhs, and case-split on the lhs kind - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - - // if only one side is a constant, it should be on the RHS. - if (((BVCONST == lhs.GetKind()) ^ (BVCONST == rhs.GetKind())) - && (lhs.GetKind() == BVCONST)) { - lhs = eq[1]; - rhs = eq[0]; - eq = _bm->CreateNode(EQ, lhs, rhs); // If "return eq" is called, return the arguments in the correct order. - } - - ASTNode output = eq; - if (CheckAlreadySolvedMap(eq, output)) { - return output; - } - - if (BVPLUS == lhs.GetKind()) { - ASTNode chosen_monom = _bm->CreateNode(UNDEFINED); - ASTNode leftover_lhs; - - //choose monom makes sure that it gets only those vars that - //occur exactly once in lhs and rhs put together - chosen_monom = ChooseMonom(eq, leftover_lhs); - if (chosen_monom == _bm->CreateNode(UNDEFINED)) { - //no monomial was chosen - return eq; - } - - if (bv_debug) - cerr << "Chosen monomial:" << chosen_monom; - - //if control is here then it means that a monom was chosen - // - //construct: rhs - (lhs without the chosen monom) - unsigned int len = lhs.GetValueWidth(); - leftover_lhs = simplifier->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, - len, leftover_lhs)); - rhs - = simplifier->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, - leftover_lhs)); - lhs = chosen_monom; - } //end of if(BVPLUS ...) - - if (BVUMINUS == lhs.GetKind()) { - //equation is of the form (-lhs0) = rhs - ASTNode lhs0 = lhs[0]; - rhs = simplifier->SimplifyTerm(_bm->CreateTerm(BVUMINUS, rhs.GetValueWidth(), - rhs)); - lhs = lhs0; - } - - switch (lhs.GetKind()) { - case SYMBOL: { - //input is of the form x = rhs first make sure that the lhs - //symbol does not occur on the rhs or that it has not been - //solved for - if (_bm->VarSeenInTerm(lhs, rhs)) { - //found the lhs in the rhs. Abort! - DoNotSolve_TheseVars.insert(lhs); - return eq; - } - - //rhs should not have arrayreads in it. it complicates matters - //during transformation - // if(CheckForArrayReads_TopLevel(rhs)) { - // return eq; - // } - - DoNotSolve_TheseVars.insert(lhs); - if (simplifier->UpdateSolverMap(lhs, rhs)) { - return eq; - } - - output = ASTTrue; - break; - } - // case READ: - // { - // if(BVCONST != lhs[1].GetKind() || READ != rhs.GetKind() || - // BVCONST != rhs[1].GetKind() || lhs == rhs) - // { - // return eq; - // } - // else - // { - // DoNotSolve_TheseVars.insert(lhs); - // if (!_bm->UpdateSolverMap(lhs, rhs)) - // { - // return eq; - // } - - // output = ASTTrue; - // break; - // } - // } - case BVEXTRACT: { - const ASTNode zero = _bm->CreateZeroConst(32); - - if (!(SYMBOL == lhs[0].GetKind() && BVCONST == lhs[1].GetKind() && zero - == lhs[2] && !_bm->VarSeenInTerm(lhs[0], rhs) - && !DoNotSolveThis(lhs[0]))) { - return eq; - } - - if (_bm->VarSeenInTerm(lhs[0], rhs)) { - DoNotSolve_TheseVars.insert(lhs[0]); - return eq; - } - - DoNotSolve_TheseVars.insert(lhs[0]); - if (!simplifier->UpdateSolverMap(lhs, rhs)) { - return eq; - } - - //if the extract of x[i:0] = t is entered into the solvermap, - //then also add another entry for x = x1@t - ASTNode var = lhs[0]; - ASTNode newvar = NewVar(var.GetValueWidth() - lhs.GetValueWidth()); - newvar = _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs); - simplifier->UpdateSolverMap(var, newvar); - output = ASTTrue; - break; - } - case BVMULT: { - //the input is of the form a*x = t. If 'a' is odd, then compute - //its multiplicative inverse a^-1, multiply 't' with it, and - //update the solver map - if (BVCONST != lhs[0].GetKind()) { - return eq; - } - - if (!(SYMBOL == lhs[1].GetKind() || (BVEXTRACT == lhs[1].GetKind() - && SYMBOL == lhs[1][0].GetKind()))) { - return eq; - } - - bool ChosenVar_Is_Extract = (BVEXTRACT == lhs[1].GetKind()) ? true - : false; - - //if coeff is even, then we know that all the coeffs in the eqn - //are even. Simply return the eqn - if (simplifier->BVConstIsOdd(lhs[0])) { - return eq; - } - - ASTNode a = simplifier->MultiplicativeInverse(lhs[0]); - ASTNode chosenvar = ChosenVar_Is_Extract ? lhs[1][0] : lhs[1]; - ASTNode chosenvar_value = simplifier->SimplifyTerm(_bm->CreateTerm(BVMULT, - rhs.GetValueWidth(), a, rhs)); - - //if chosenvar is seen in chosenvar_value then abort - if (_bm->VarSeenInTerm(chosenvar, chosenvar_value)) { - //abort solving - if (bv_debug) - cerr << "The chosen variable appears elsewhere:" << chosenvar; - - DoNotSolve_TheseVars.insert(lhs); // this could be an extract?? - return eq; - } - - //rhs should not have arrayreads in it. it complicates matters - //during transformation - // if(CheckForArrayReads_TopLevel(chosenvar_value)) { - // return eq; - // } - - //found a variable to solve - DoNotSolve_TheseVars.insert(chosenvar); - chosenvar = lhs[1]; - if (!simplifier->UpdateSolverMap(chosenvar, chosenvar_value)) { - return eq; - } - - // can we be sure that the extract is from zero? - if (ChosenVar_Is_Extract) { - const ASTNode& var = lhs[1][0]; - ASTNode newvar = NewVar(var.GetValueWidth() - - lhs[1].GetValueWidth()); - newvar = _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, - chosenvar_value); - simplifier->UpdateSolverMap(var, newvar); - } - - output = ASTTrue; - break; - } - default: - output = eq; - break; - } - - assert(!output.IsNull()); - UpdateAlreadySolvedMap(eq, output); - return output; -} //end of BVSolve_Odd() - -//Create a new variable of ValueWidth 'n' -ASTNode BVSolverExp::NewVar(unsigned int n) { - std::string c("v"); - char d[32]; - sprintf(d, "%d", _symbol_count++); - std::string ccc(d); - c += "_solver_" + ccc; - - ASTNode CurrentSymbol = _bm->CreateSymbol(c.c_str()); - CurrentSymbol.SetValueWidth(n); - CurrentSymbol.SetIndexWidth(0); - return CurrentSymbol; -} //end of NewVar() - - -bool containsExtract(const ASTNode& n, ASTNodeSet& visited) { - if (visited.find(n) != visited.end()) - return false; - - if (BVEXTRACT == n.GetKind()) - return true; - - for (unsigned i = 0; i < n.Degree(); i++) { - if (containsExtract(n[i], visited)) - return true; - } - visited.insert(n); - return false; -} - -// The order that monomials are chosen in from the system of equations is important. -// In particular if a symbol is chosen that is extracted over, and that symbol -// appears elsewhere in the system. Then those other positions will be replaced by -// an equation that contains a concatenation. -// For example, given: -// 5x[5:1] + 4y[5:1] = 6 -// 3x + 2y = 5 -// -// If the x that is extracted over is selected as the monomial, then the later eqn. will be -// rewritten as: -// 3(concat (1/5)(6-4y[5:1]) v) + 2y =5 -// where v is a fresh one-bit variable. -// What's particularly bad about this is that the "y" appears now in two places in the eqn. -// Because it appears in two places it can't be simplified by this algorithm -// This sorting function is a partial solution. Ideally the "best" monomial should be -// chosen from the system of equations. -void specialSort(ASTVec& c) { - // Place equations that don't contain extracts before those that do. - deque extracts; - ASTNodeSet v; - - for (unsigned i = 0; i < c.size(); i++) { - if (containsExtract(c[i], v)) - extracts.push_back(c[i]); - else - extracts.push_front(c[i]); - } - - c.clear(); - deque::iterator it = extracts.begin(); - while (it != extracts.end()) { - c.push_back(*it++); - } -} - -//The toplevel bvsolver(). Checks if the formula has already been -//solved. If not, the solver() is invoked. If yes, then simply drop -//the formula -ASTNode BVSolverExp::TopLevelBVSolve(const ASTNode& input) { - assert(_bm->UserFlags.wordlevel_solve_flag); - return input; - - if (bv_debug) { - cerr << "input to bvSolver"; - cerr << input; - } - - const Kind k = input.GetKind(); - if (!(EQ == k || AND == k)) { - return input; - } - - ASTNode output = input; - if (CheckAlreadySolvedMap(input, output)) { - //output is TRUE. The formula is thus dropped - return output; - } - - _bm->GetRunTimes()->start(RunTimes::BVSolver); - ASTVec o; - ASTVec c; - if (EQ == k) - c.push_back(input); - else { - // Flatten the AND, this may flatten BVPLUS (say) which we don't really want. - ASTNode n = input; - while (true) { - ASTNode nold = n; - n = simplifier->FlattenOneLevel(n); - if ((n == nold)) - break; - } - - // When flattening simplifications will be applied to the node, potentially changing it's type: - // (AND x (ANY (not x) y)) gives us FALSE. - if (!(EQ == n.GetKind() || AND == n.GetKind())) { - { - _bm->GetRunTimes()->stop(RunTimes::BVSolver); - return n; - } - } - - c = n.GetChildren(); - specialSort(c); - } - - assert(c.size()> 0); - - ASTVec eveneqns; - bool substitution = false; - for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { - assert(it->GetKind() != AND); // These should have been flattened. - - // If there has been a prior substitution we need to be careful that the newly encountered equations - // don't have the substituted variable on the rhs. For example, say we have the substitution already: - // v1 = (concat v2 v3). - // Next, say we encounter the equation: - // v2 = (concat v1 v3). - // if the v1 in the second equation is not substituted, then we will create a circular reference in the - // substitution map. We use simplify to perform the substitutions. - ASTNode aaa = - (substitution && EQ == it->GetKind()) ? simplifier->SimplifyFormula( - *it, false) : *it; - aaa = BVSolve_Odd(aaa); - bool even = false; - aaa = CheckEvenEqn(aaa, even); - if (even) { - eveneqns.push_back(aaa); - } else { - if (ASTTrue != aaa) { - o.push_back(aaa); - } else { - substitution = true; - } - } - } - - ASTNode evens; - if (eveneqns.size() > 0) { - //if there is a system of even equations then solve them - evens = (eveneqns.size() > 1) ? _bm->CreateNode(AND, eveneqns) - : eveneqns[0]; - //evens = _bm->SimplifyFormula(evens,false); - evens = BVSolve_Even(evens); - _bm->ASTNodeStats("Printing after evensolver:", evens); - } else { - evens = ASTTrue; - } - output = (o.size() > 0) ? ((o.size() > 1) ? _bm->CreateNode(AND, o) : o[0]) - : ASTTrue; - output = _bm->CreateNode(AND, evens, output); - - UpdateAlreadySolvedMap(input, output); - - if (bv_debug) { - cerr << "output from bvSolver"; - cerr << output; - } - - _bm->GetRunTimes()->stop(RunTimes::BVSolver); - return output; -} //end of TopLevelBVSolve() - - -ASTNode BVSolverExp::CheckEvenEqn(const ASTNode& input, bool& evenflag) { - ASTNode eq = input; - //cerr << "Input to BVSolve_Odd()" << eq << endl; - if (!(EQ == eq.GetKind())) { - evenflag = false; - return eq; - } - - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); - //lhs must be a BVPLUS, and rhs must be a BVCONST - assert(!(BVPLUS == rhs.GetKind() && zero == lhs)); // shouldn't be swapped. - if (!(BVPLUS == lhs.GetKind() && zero == rhs)) { - evenflag = false; - return eq; - } - - const ASTVec lhs_c = lhs.GetChildren(); - ASTNode savetheconst = rhs; - bool first = true; - for (ASTVec::const_iterator it = lhs_c.begin(), itend = lhs_c.end(); it - != itend; it++) { - ASTNode aaa = *it; - const Kind itk = aaa.GetKind(); - - if (BVCONST == itk) { - //check later if the constant is even or not - savetheconst = aaa; - assert(first); // atmost a single constant in the expression. - first = false; - continue; - } - - if (!(BVMULT == itk && BVCONST == aaa[0].GetKind() && SYMBOL - == aaa[1].GetKind() && !simplifier->BVConstIsOdd(aaa[0]))) { - //If the monomials of the lhs are NOT of the form 'a*x' where - //'a' is even, then return the false - evenflag = false; - return eq; - } - }//end of for loop - - //if control is here then it means that all coeffs are even. the - //only remaining thing is to check if the constant is even or not - if (simplifier->BVConstIsOdd(savetheconst)) { - //the constant turned out to be odd. we have UNSAT eqn - evenflag = false; - return ASTFalse; - } - - //all is clear. the eqn in even, through and through - evenflag = true; - return eq; -} //end of CheckEvenEqn - -//solve an eqn whose monomials have only even coefficients -//The input should have already been checked with "checkeveneqn" -// Given an input of "2x + 6y + 12 = 0", -// it will divide by the smallest co-efficient, giving: "x[?:1] + 3y[?:1] + 6 = 0" -ASTNode BVSolverExp::BVSolve_Even(const ASTNode& input) { - assert(_bm->UserFlags.wordlevel_solve_flag); - - assert((EQ == input.GetKind() || AND == input.GetKind())); - if (!(EQ == input.GetKind() || AND == input.GetKind())) { - return input; - } - - { - ASTNode output; - if (CheckAlreadySolvedMap(input, output)) { - return output; - } - } - - ASTVec input_c; - if (EQ == input.GetKind()) { - input_c.push_back(input); - } else { - input_c = input.GetChildren(); - } - - //power_of_2 holds the exponent of 2 in the coeff - unsigned int power_of_2 = 0; - //we need this additional variable to find the lowest power of 2 - unsigned int power_of_2_lowest = ~0; - //the monom which has the least power of 2 in the coeff - for (ASTVec::iterator jt = input_c.begin(), jtend = input_c.end(); jt - != jtend; jt++) { - ASTNode eq = *jt; - assert(EQ ==eq.GetKind()); - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); - - //lhs must be a BVPLUS, and rhs must be zero - assert ((BVPLUS == lhs.GetKind() && zero == rhs)); - if (!(BVPLUS == lhs.GetKind() && zero == rhs)) { - return input; - } - - const ASTVec& lhs_c = lhs.GetChildren(); - for (ASTVec::const_iterator it = lhs_c.begin(), itend = lhs_c.end(); it - != itend; it++) { - ASTNode aaa = *it; - const Kind itk = aaa.GetKind(); - - //If the monomials of the lhs are NOT of the form 'a*x' or 'a' - //where 'a' is even, then return the eqn - - assert ((BVCONST == itk && !simplifier->BVConstIsOdd(aaa)) || - (BVMULT == itk && BVCONST == aaa[0].GetKind() && SYMBOL == aaa[1].GetKind() && !simplifier->BVConstIsOdd(aaa[0]))); - - if (!(BVCONST == itk && !simplifier->BVConstIsOdd(aaa)) && !(BVMULT == itk - && BVCONST == aaa[0].GetKind() && SYMBOL - == aaa[1].GetKind() && !simplifier->BVConstIsOdd(aaa[0]))) { - return input; - } - - //we are gauranteed that if control is here then the monomial is - //of the form 'a*x' or 'a', where 'a' is even - ASTNode coeff = (BVCONST == itk) ? aaa : aaa[0]; - SplitEven_into_Oddnum_PowerOf2(coeff, power_of_2); - if (power_of_2 < power_of_2_lowest) { - power_of_2_lowest = power_of_2; - } - power_of_2 = 0; - }//end of inner for loop - } //end of outer for loop - - //get the exponent - power_of_2 = power_of_2_lowest; - assert(power_of_2 > 0); - - if (bv_debug) - cerr << "Shifting all by:" << power_of_2 << endl; - - //if control is here, we are gauranteed that we have chosen a - //monomial with fewest powers of 2 - //Go through all the formulae, dividing the co-efficients. - ASTVec formula_out; - for (ASTVec::iterator jt = input_c.begin(), jtend = input_c.end(); jt - != jtend; jt++) { - const ASTNode eq = *jt; - assert(EQ == eq.GetKind()); - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - unsigned len = lhs.GetValueWidth(); - const ASTNode zero = _bm->CreateZeroConst(len); - - //lhs must be a BVPLUS, and rhs must be a BVCONST - assert((BVPLUS == lhs.GetKind() && zero == rhs)); - if (!(BVPLUS == lhs.GetKind() && zero == rhs)) { - return input; - } - - const unsigned newlen = len - power_of_2; - const ASTNode start = _bm->CreateBVConst(32, newlen - 1); - ASTNode end = _bm->CreateZeroConst(32); - const ASTNode two_const = _bm->CreateTwoConst(len); - - unsigned count = power_of_2; - ASTNode two = two_const; - while (--count) { - two = simplifier->BVConstEvaluator(_bm->CreateTerm(BVMULT, len, two_const, - two)); - } - const ASTVec& lhs_c = lhs.GetChildren(); - ASTVec lhs_out; - for (ASTVec::const_iterator it = lhs_c.begin(), itend = lhs_c.end(); it - != itend; it++) { - ASTNode aaa = *it; - const Kind itk = aaa.GetKind(); - if (BVCONST == itk) { - aaa = simplifier->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, aaa, - two)); - aaa = simplifier->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT, newlen, - aaa, start, end)); - } else { - //it must be of the form a*x - ASTNode coeff = simplifier->BVConstEvaluator(_bm->CreateTerm(BVDIV, - len, aaa[0], two)); - coeff = simplifier->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT, - newlen, coeff, start, end)); - ASTNode lower_x = simplifier->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, - newlen, aaa[1], start, end)); - aaa = _bm->CreateTerm(BVMULT, newlen, coeff, lower_x); - } - lhs_out.push_back(aaa); - }//end of inner forloop() - rhs = _bm->CreateZeroConst(newlen); - lhs = _bm->CreateTerm(BVPLUS, newlen, lhs_out); - formula_out.push_back(_bm->CreateNode(EQ, lhs, rhs)); - } //end of outer forloop() - - ASTNode - output = - (formula_out.size() > 0) ? (formula_out.size() > 1) ? _bm->CreateNode( - AND, formula_out) - : formula_out[0] - : ASTTrue; - - if (bv_debug) { - cerr << "Even has been solved"; - cerr << input; - cerr << output; - } - - UpdateAlreadySolvedMap(input, output); - - return output; -} //end of BVSolve_Even() -} -;//end of namespace BEEV diff --git a/src/simplifier/bvsolverExp.h b/src/simplifier/bvsolverExp.h deleted file mode 100644 index a4b24b2..0000000 --- a/src/simplifier/bvsolverExp.h +++ /dev/null @@ -1,152 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, Trevor Hansen - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - - -// This is an experimental BVSOLVER> I find the bvsolver difficult to work -// with. Do something and it doesn't break, STP just runs very slowly. - - -#include "simplifier.h" - -namespace BEEV -{ -class Simplifier; - - //This class represents the bitvector arithmetic linear solver. - // - //The bitvector solver is a partial solver, i.e. it does not solve - //for all variables in the system of equations. it is - //best-effort. it relies on the SAT solver to be complete. - // - //The BVSolver assumes that the input equations are normalized, and - //have liketerms combined etc. - // - //0. Traverse top-down over the input DAG, looking for a conjunction - //0. of equations. if you find one, then for each equation in the - //0. conjunction, do the following steps. - // - //1. check for Linearity of the input equation - // - //2. Solve for a "chosen" variable. The variable should occur - //2. exactly once and must have an odd coeff. Refer STP's CAV 2007 - //2. paper for actual solving procedure - // - //4. Outside the solver, Substitute and Re-normalize the input DAG - class BVSolverExp - { - //Ptr to toplevel manager that manages bit-vector expressions - //(i.e. construct various kinds of expressions), and also has - //member functions that simplify bit-vector expressions - STPMgr * _bm; - ASTNode ASTTrue, ASTFalse; - Simplifier *simplifier; - - //Those formulas which have already been solved. If the same - //formula occurs twice then do not solve the second occurence, and - //instead drop it - ASTNodeMap FormulasAlreadySolvedMap; - - //this map is useful while traversing terms and uniquely - //identifying variables in the those terms. Prevents double - //counting. - ASTNodeMap TermsAlreadySeenMap; - ASTNodeMap TermsAlreadySeenMap_ForArrays; - - //count is used in the creation of new variables - unsigned int _symbol_count; - NodeFactory * _nf; - - //solved variables list: If a variable has been solved for then do - //not solve for it again - ASTNodeSet DoNotSolve_TheseVars; - - //checks if var has been solved for or not. if yes, then return - //true else return false - bool DoNotSolveThis(const ASTNode& var); - - //traverses a term, and creates a multiset of all variables in the - //term. Does memoization to avoid double counting. - void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v); - void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v); - - //choose a suitable var from the term - ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm); - //accepts an equation and solves for a variable or a monom in it - ASTNode BVSolve_Odd(const ASTNode& eq); - - //solves equations of the form a*x=t where 'a' is even. Has a - //return value, unlike the normal BVSolve() - ASTNode BVSolve_Even(const ASTNode& eq); - ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag); - - //Checks for arrayreads in a term. if yes then returns true, else - //return false - bool CheckForArrayReads(const ASTNode& term); - bool CheckForArrayReads_TopLevel(const ASTNode& term); - - //Creates new variables used in solving - ASTNode NewVar(unsigned int n); - - //this function return true if the var occurs in term, else the - //function returns false - bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); - - //takes an even number "in" as input, and returns an odd number - //(return value) and a power of 2 (as number_shifts by reference), - //such that in = (odd_number * power_of_2). - // - //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on - //bit-vector arithmetic published in DAC 1998) paper for precise - //understanding of the algorithm - void SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts); - - //Once a formula has been solved, then update the alreadysolvedmap - //with the formula, and the solved value. The solved value can be - //described using the following example: Suppose input to the - //solver is - // - // input key: x = 2 AND y = x + t - // - // output value: y = 2 + t - void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value); - - //This function checks if the key (formula) has already been - //solved for. - // - //If yes it returns TRUE and fills the "output" with the - //solved-value (call by reference argument), - // - //else returns FALSE - bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output); - public: - //constructor - BVSolverExp(STPMgr * bm,Simplifier *simpl, NodeFactory *nf) : - _bm(bm), _symbol_count(0), _nf(nf) - { - ASTTrue = _bm->CreateNode(TRUE); - ASTFalse = _bm->CreateNode(FALSE); - simplifier = simpl; - } - ; - - //Destructor - ~BVSolverExp() - { - TermsAlreadySeenMap.clear(); - DoNotSolve_TheseVars.clear(); - FormulasAlreadySolvedMap.clear(); - TermsAlreadySeenMap_ForArrays.clear(); - } - - //Top Level Solver: Goes over the input DAG, identifies the - //equation to be solved, solves them, - ASTNode TopLevelBVSolve(const ASTNode& a); - }; //end of class bvsolver -} -;//end of namespace BEEV -- 2.47.3