//if the variables are not cnf variables then add
//them to the counterexample
if (0 != strncmp("cnf", zz, 3)
- && 0 != strcmp("*TrueDummy*", zz))
+ && 0 != strcmp("*TrueDummy*", zz))
{
if (newS.model[i] == MINISAT::l_True)
CounterExampleMap[s] = ASTTrue;
int seed = 10000;
srand(seed);
CounterExampleMap[s] =
- (rand() > seed) ? ASTFalse : ASTTrue;
+ (rand() > seed) ? ASTFalse : ASTTrue;
}
}
}
{
FatalError("ConstructCounterExample:"\
"error while constructing counterexample: "\
- "not a variable: ", var);
+ "not a variable: ", var);
}
//construct the bitvector value
HASHMAP<unsigned, bool> * w = it->second;
if (!is_Term_kind(k))
{
FatalError("TermToConstTermUsingModel: "\
- "The input is not a term: ",
- term);
+ "The input is not a term: ",
+ term);
}
if (k == WRITE)
{
FatalError("TermToConstTermUsingModel: "\
- "The input has wrong kind: WRITE : ",
- term);
+ "The input has wrong kind: WRITE : ",
+ term);
}
if (k == SYMBOL && BOOLEAN_TYPE == term.GetType())
{
FatalError("TermToConstTermUsingModel: "\
- "The input has wrong kind: Propositional variable : ",
- term);
+ "The input has wrong kind: Propositional variable : ",
+ term);
}
ASTNodeMap::iterator it1;
if (term == val)
{
FatalError("TermToConstTermUsingModel: "\
- "The input term is stored as-is "
+ "The input term is stored as-is "
"in the CounterExample: Not ok: ",
- term);
+ term);
}
return TermToConstTermUsingModel(val, ArrayReadFlag);
}
if (0 == arrName.GetIndexWidth())
{
FatalError("TermToConstTermUsingModel: "\
- "array has 0 index width: ", arrName);
+ "array has 0 index width: ", arrName);
}
if (WRITE == arrName.GetKind()) //READ over a WRITE
{
ASTNode wrtterm =
- Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag);
+ Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag);
if (wrtterm == term)
{
FatalError("TermToConstTermUsingModel: "\
- "Read_Over_Write term must be expanded "\
- "into an ITE", term);
+ "Read_Over_Write term must be expanded "\
+ "into an ITE", term);
}
ASTNode rtterm =
- TermToConstTermUsingModel(wrtterm, ArrayReadFlag);
+ TermToConstTermUsingModel(wrtterm, ArrayReadFlag);
assert(ArrayReadFlag || (BVCONST == rtterm.GetKind()));
return rtterm;
}
{
// The "then" and "else" branch are arrays.
ASTNode indexVal =
- TermToConstTermUsingModel(index, ArrayReadFlag);
+ TermToConstTermUsingModel(index, ArrayReadFlag);
ASTNode condcompute =
- ComputeFormulaUsingModel(arrName[0]); // Get the truth value.
- unsigned int wid = arrName.GetValueWidth();
+ ComputeFormulaUsingModel(arrName[0]); // Get the truth value.
+ unsigned int wid = arrName.GetValueWidth();
if (ASTTrue == condcompute)
{
const ASTNode & result =
- TermToConstTermUsingModel(bm->CreateTerm(READ,
- wid,
- arrName[1],
- indexVal),
- ArrayReadFlag);
+ TermToConstTermUsingModel(bm->CreateTerm(READ,
+ wid,
+ arrName[1],
+ indexVal),
+ ArrayReadFlag);
assert(ArrayReadFlag || (BVCONST == result.GetKind()));
return result;
}
else if (ASTFalse == condcompute)
{
const ASTNode & result =
- TermToConstTermUsingModel(bm->CreateTerm(READ,
- wid,
- arrName[2],
- indexVal),
- ArrayReadFlag);
+ TermToConstTermUsingModel(bm->CreateTerm(READ,
+ wid,
+ arrName[2],
+ indexVal),
+ ArrayReadFlag);
assert(ArrayReadFlag || (BVCONST == result.GetKind()));
return result;
}
else
{
cerr << "TermToConstTermUsingModel: termITE: "\
- "value of conditional is wrong: " << condcompute << endl;
+ "value of conditional is wrong: " << condcompute << endl;
FatalError(" TermToConstTermUsingModel: termITE: "\
- "cannot compute ITE conditional against model: ",
- term);
+ "cannot compute ITE conditional against model: ",
+ term);
}
FatalError("bn23143 Never Here");
}
//index has a const value in the CounterExampleMap
//ASTNode indexVal = CounterExampleMap[index];
ASTNode indexVal =
- TermToConstTermUsingModel(CounterExampleMap[index],
- ArrayReadFlag);
+ TermToConstTermUsingModel(CounterExampleMap[index],
+ ArrayReadFlag);
modelentry =
- bm->CreateTerm(READ, arrName.GetValueWidth(),
- arrName, indexVal);
+ bm->CreateTerm(READ, arrName.GetValueWidth(),
+ arrName, indexVal);
}
else
{
//index does not have a const value in the
//CounterExampleMap. compute it.
ASTNode indexconstval =
- TermToConstTermUsingModel(index, ArrayReadFlag);
+ TermToConstTermUsingModel(index, ArrayReadFlag);
//update model with value of the index
//CounterExampleMap[index] = indexconstval;
modelentry =
- bm->CreateTerm(READ, arrName.GetValueWidth(),
- arrName, indexconstval);
+ bm->CreateTerm(READ, arrName.GetValueWidth(),
+ arrName, indexconstval);
}
//modelentry is now an arrayread over a constant index
BVTypeCheck(modelentry);
if (CounterExampleMap.find(modelentry) != CounterExampleMap.end())
{
output =
- TermToConstTermUsingModel(CounterExampleMap[modelentry],
- ArrayReadFlag);
+ TermToConstTermUsingModel(CounterExampleMap[modelentry],
+ ArrayReadFlag);
}
else if (ArrayReadFlag)
{
else
{
cerr << "TermToConstTermUsingModel: termITE: "
- << "value of conditional is wrong: "
- << condcompute << endl;
+ << "value of conditional is wrong: "
+ << condcompute << endl;
FatalError(" TermToConstTermUsingModel: termITE: cannot "\
- "compute ITE conditional against model: ", term);
+ "compute ITE conditional against model: ", term);
}
break;
}
ASTVec c = term.GetChildren();
ASTVec o;
for (ASTVec::iterator
- it = c.begin(), itend = c.end(); it != itend; it++)
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag);
o.push_back(ff);
Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool arrayread_flag)
{
if (READ != term.GetKind()
- && WRITE != term[0].GetKind())
+ && WRITE != term[0].GetKind())
{
FatalError("RemovesWrites: Input must be a READ over a WRITE", term);
}
if (term == val)
{
FatalError("TermToConstTermUsingModel: The input term is "\
- "stored as-is "
+ "stored as-is "
"in the CounterExample: Not ok: ", term);
}
return TermToConstTermUsingModel(val, arrayread_flag);
ASTNode cond =
ComputeFormulaUsingModel(simp->CreateSimplifiedEQ(writeIndex,
- readIndex));
+ readIndex));
if (ASTTrue == cond)
{
//found the write-value. return it
if (!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType()))
{
FatalError(" ComputeConstFormUsingModel: "\
- "The input is a non-formula: ", form);
+ "The input is a non-formula: ", form);
}
//cerr << "Input to ComputeFormulaUsingModel:" << form << endl;
else
{
FatalError("ComputeFormulaUsingModel: "\
- "The value of a formula must be TRUE or FALSE:", form);
+ "The value of a formula must be TRUE or FALSE:", form);
}
}
case SYMBOL:
if (BOOLEAN_TYPE != form.GetType())
FatalError(" ComputeFormulaUsingModel: "\
- "Non-Boolean variables are not formulas", form);
+ "Non-Boolean variables are not formulas", form);
if (CounterExampleMap.find(form) != CounterExampleMap.end())
{
ASTNode counterexample_val = CounterExampleMap[form];
{
ASTNode o = ASTTrue;
for (ASTVec::const_iterator
- it = form.begin(), itend = form.end(); it != itend; it++)
+ it = form.begin(), itend = form.end(); it != itend; it++)
if (ASTFalse == ComputeFormulaUsingModel(*it))
{
o = ASTFalse;
{
ASTNode o = ASTFalse;
for (ASTVec::const_iterator
- it = form.begin(), itend = form.end(); it != itend; it++)
+ it = form.begin(), itend = form.end(); it != itend; it++)
if (ASTTrue == ComputeFormulaUsingModel(*it))
{
o = ASTTrue;
break;
case OR:
for (ASTVec::const_iterator
- it = form.begin(), itend = form.end(); it != itend; it++)
+ it = form.begin(), itend = form.end(); it != itend; it++)
if (ASTTrue == ComputeFormulaUsingModel(*it))
output = ASTTrue;
break;
case AND:
output = ASTTrue;
for (ASTVec::const_iterator
- it = form.begin(), itend = form.end(); it != itend; it++)
+ it = form.begin(), itend = form.end(); it != itend; it++)
{
if (ASTFalse == ComputeFormulaUsingModel(*it))
{
t0 = ComputeFormulaUsingModel(form[0]);
t1 = ComputeFormulaUsingModel(form[1]);
if ((ASTTrue == t0
- && ASTTrue == t1)
- || (ASTFalse == t0 && ASTFalse == t1))
+ && ASTTrue == t1)
+ || (ASTFalse == t0 && ASTFalse == t1))
output = ASTFalse;
else
output = ASTTrue;
t0 = ComputeFormulaUsingModel(form[0]);
t1 = ComputeFormulaUsingModel(form[1]);
if ((ASTTrue == t0 && ASTTrue == t1)
- || (ASTFalse == t0 && ASTFalse == t1))
+ || (ASTFalse == t0 && ASTFalse == t1))
output = ASTTrue;
else
output = ASTFalse;
//t is true if SAT solver generated a counterexample, else it is false
if (!t)
FatalError("CheckCounterExample: "\
- "No CounterExample to check", ASTUndefined);
+ "No CounterExample to check", ASTUndefined);
const ASTVec c = bm->GetAsserts();
for (ASTVec::const_iterator
- it = c.begin(), itend = c.end(); it != itend; it++)
+ it = c.begin(), itend = c.end(); it != itend; it++)
if (ASTFalse == ComputeFormulaUsingModel(*it))
FatalError("CheckCounterExample:counterexample bogus:"
"assert evaluates to FALSE under counterexample: "\
- "NOT OK", *it);
+ "NOT OK", *it);
if (ASTTrue == ComputeFormulaUsingModel(bm->GetQuery()))
FatalError("CheckCounterExample:counterexample bogus:"
"query evaluates to TRUE under counterexample: "\
- "NOT OK", bm->GetQuery());
+ "NOT OK", bm->GetQuery());
}
/* FUNCTION: queries the CounterExampleMap object with 'expr' and
for (int j = 0; j < n; j++)
{
ASTNode index =
- bm->CreateBVConst(it->GetIndexWidth(), j);
+ bm->CreateBVConst(it->GetIndexWidth(), j);
ASTNode readexpr =
- bm->CreateTerm(READ, it->GetValueWidth(), *it, index);
+ bm->CreateTerm(READ, it->GetValueWidth(), *it, index);
ASTNode val =
- GetCounterExample(t, readexpr);
+ GetCounterExample(t, readexpr);
//cout << "ASSERT( ";
//cout << " = ";
out_int.push_back(GetUnsignedConst(val));
if (l < len)
FatalError("BoolVectorBVConst : "
"length of bitvector does not match HASHMAP size:",
- ASTUndefined, l);
+ ASTUndefined, l);
std::string cc;
for (unsigned int jj = 0; jj < l; jj++)
{
bool BVSolver::CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output)
{
ASTNodeMap::iterator it;
- if ((it = FormulasAlreadySolvedMap.find(key)) != FormulasAlreadySolvedMap.end())
+ if ((it = FormulasAlreadySolvedMap.find(key))
+ != FormulasAlreadySolvedMap.end())
{
output = it->second;
return true;
return false;
} //CheckAlreadySolvedMap()
- void BVSolver::UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value)
+ void BVSolver::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
- ASTNode BVSolver::SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts)
+ ASTNode BVSolver::SplitEven_into_Oddnum_PowerOf2(const ASTNode& in,
+ unsigned int& number_shifts)
{
if (BVCONST != in.GetKind() || _simp->BVConstIsOdd(in))
{
- FatalError("BVSolver:SplitNum_Odd_PowerOf2: input must be a BVCONST and even\n", 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 = _simp->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two));
+ ASTNode mod_by_2 =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two));
while (mod_by_2 == zero)
{
- div_by_2 = _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, div_by_2, two));
+ div_by_2 =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, div_by_2, two));
number_shifts++;
- mod_by_2 = _simp->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two));
+ mod_by_2 =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVMOD, len, div_by_2, two));
}
return div_by_2;
} //end of SplitEven_into_Oddnum_PowerOf2()
default:
{
ASTVec c = term.GetChildren();
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
if (CheckForArrayReads(*it))
{
} //end of UpdateSolverMap()
//collects the vars in the term 'lhs' into the multiset Vars
- void BVSolver::VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& Vars)
+ void BVSolver::VarsInTheTerm_TopLevel(const ASTNode& lhs,
+ ASTNodeMultiSet& Vars)
{
TermsAlreadySeenMap.clear();
VarsInTheTerm(lhs, Vars);
default:
{
ASTVec c = term.GetChildren();
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
VarsInTheTerm(*it, Vars);
}
if (!chosen_symbol)
{
o.clear();
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
ASTNode monom = *it;
ASTNode var =
//construct: rhs - (lhs without the chosen monom)
unsigned int len = lhs.GetValueWidth();
leftover_lhs =
- _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, len, leftover_lhs));
+ _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS,
+ len, leftover_lhs));
ASTNode newrhs =
_simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
lhs = chosen_monom;
{
//equation is of the form (-lhs0) = rhs
ASTNode lhs0 = lhs[0];
- rhs = _simp->SimplifyTerm(_bm->CreateTerm(BVUMINUS, rhs.GetValueWidth(), rhs));
+ rhs = _simp->SimplifyTerm(_bm->CreateTerm(BVUMINUS,
+ rhs.GetValueWidth(), rhs));
lhs = lhs0;
}
}
// case READ:
// {
- // if(BVCONST != lhs[1].GetKind() || READ != rhs.GetKind() ||
+ // if(BVCONST != lhs[1].GetKind()
+ // || READ != rhs.GetKind() ||
// BVCONST != rhs[1].GetKind() || lhs == rhs)
// {
// return eq;
return eq;
}
- if (!(SYMBOL == lhs[1].GetKind() || (BVEXTRACT == lhs[1].GetKind() && SYMBOL == lhs[1][0].GetKind())))
+ 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;
+ 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
}
ASTNode a = _simp->MultiplicativeInverse(lhs[0]);
- ASTNode chosenvar = (BVEXTRACT == lhs[1].GetKind()) ? lhs[1][0] : lhs[1];
+ ASTNode chosenvar =
+ (BVEXTRACT == lhs[1].GetKind()) ? lhs[1][0] : lhs[1];
ASTNode chosenvar_value =
- _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, rhs.GetValueWidth(), a, rhs));
+ _simp->SimplifyTerm(_bm->CreateTerm(BVMULT,
+ rhs.GetValueWidth(),
+ a, rhs));
//if chosenvar is seen in chosenvar_value then abort
if (VarSeenInTerm(chosenvar, chosenvar_value))
ASTNode solved = ASTFalse;
for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
{
- //_bm->ASTNodeStats("Printing before calling simplifyformula inside the solver:", *it);
- ASTNode aaa = (ASTTrue == solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(*it, false) : *it;
- //_bm->ASTNodeStats("Printing after calling simplifyformula inside the solver:", aaa);
+ //_bm->ASTNodeStats("Printing before calling simplifyformula
+ //inside the solver:", *it);
+ ASTNode aaa =
+ (ASTTrue == solved
+ && EQ == it->GetKind()) ?
+ _simp->SimplifyFormula(*it, false) :
+ *it;
+ //_bm->ASTNodeStats("Printing after calling simplifyformula
+ //inside the solver:", aaa);
aaa = BVSolve_Odd(aaa);
//_bm->ASTNodeStats("Printing after oddsolver:", aaa);
bool even = false;
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 =
+ (eveneqns.size() > 1) ?
+ _bm->CreateNode(AND, eveneqns) :
+ eveneqns[0];
//evens = _simp->SimplifyFormula(evens,false);
evens = BVSolve_Even(evens);
_bm->ASTNodeStats("Printing after evensolver:", evens);
{
evens = ASTTrue;
}
- output = (o.size() > 0) ? ((o.size() > 1) ? _bm->CreateNode(AND, o) : o[0]) : ASTTrue;
+ output =
+ (o.size() > 0) ?
+ ((o.size() > 1) ?
+ _bm->CreateNode(AND, o) :
+ o[0]) :
+ ASTTrue;
output = _bm->CreateNode(AND, output, evens);
UpdateAlreadySolvedMap(input, output);
ASTVec lhs_c = lhs.GetChildren();
ASTNode savetheconst = rhs;
- for (ASTVec::iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++)
{
ASTNode aaa = *it;
Kind itk = aaa.GetKind();
continue;
}
- if (!(BVMULT == itk && BVCONST == aaa[0].GetKind() && SYMBOL == aaa[1].GetKind() && !_simp->BVConstIsOdd(aaa[0])))
+ if (!(BVMULT == itk
+ && BVCONST == aaa[0].GetKind()
+ && SYMBOL == aaa[1].GetKind()
+ && !_simp->BVConstIsOdd(aaa[0])))
{
//If the monomials of the lhs are NOT of the form 'a*x' where
//'a' is even, then return the false
unsigned int power_of_2_lowest = 0xffffffff;
//the monom which has the least power of 2 in the coeff
ASTNode monom_with_best_coeff;
- for (ASTVec::iterator jt = input_c.begin(), jtend = input_c.end(); jt != jtend; jt++)
+ for (ASTVec::iterator
+ jt = input_c.begin(), jtend = input_c.end();
+ jt != jtend; jt++)
{
ASTNode eq = *jt;
ASTNode lhs = eq[0];
ASTVec lhs_c = lhs.GetChildren();
ASTNode odd;
- for (ASTVec::iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = lhs_c.begin(), itend = lhs_c.end();
+ it != itend; it++)
{
ASTNode aaa = *it;
Kind itk = aaa.GetKind();
- if (!(BVCONST == itk && !_simp->BVConstIsOdd(aaa)) && !(BVMULT == itk && BVCONST == aaa[0].GetKind() && SYMBOL == aaa[1].GetKind()
- && !_simp->BVConstIsOdd(aaa[0])))
+ if (!(BVCONST == itk
+ && !_simp->BVConstIsOdd(aaa))
+ && !(BVMULT == itk
+ && BVCONST == aaa[0].GetKind()
+ && SYMBOL == aaa[1].GetKind()
+ && !_simp->BVConstIsOdd(aaa[0])))
{
//If the monomials of the lhs are NOT of the form 'a*x' or 'a'
//where 'a' is even, then return the eqn
//if control is here, we are gauranteed that we have chosen a
//monomial with fewest powers of 2
ASTVec formula_out;
- for (ASTVec::iterator jt = input_c.begin(), jtend = input_c.end(); jt != jtend; jt++)
+ for (ASTVec::iterator
+ jt = input_c.begin(), jtend = input_c.end(); jt != jtend; jt++)
{
ASTNode eq = *jt;
ASTNode lhs = eq[0];
ASTNode two = two_const;
while (--count)
{
- two = _simp->BVConstEvaluator(_bm->CreateTerm(BVMULT, len, two_const, two));
+ two =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVMULT,
+ len,
+ two_const,
+ two));
}
ASTVec lhs_c = lhs.GetChildren();
ASTVec lhs_out;
- for (ASTVec::iterator it = lhs_c.begin(), itend = lhs_c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = lhs_c.begin(), itend = lhs_c.end();
+ it != itend; it++)
{
ASTNode aaa = *it;
Kind itk = aaa.GetKind();
if (BVCONST == itk)
{
- aaa = _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, aaa, two));
- aaa = _simp->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT, newlen, aaa, low_minus_one, low_zero));
+ aaa =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV,
+ len,
+ aaa, two));
+ aaa =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT,
+ newlen,
+ aaa,
+ low_minus_one,
+ low_zero));
}
else
{
//it must be of the form a*x
- ASTNode coeff = _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV, len, aaa[0], two));
- coeff = _simp->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT, newlen, coeff, low_minus_one, low_zero));
+ ASTNode coeff =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVDIV,
+ len,
+ aaa[0], two));
+ coeff =
+ _simp->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT,
+ newlen,
+ 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 = _simp->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, newlen, aaa[1], low_minus_one, low_zero));
+ //upper_x =
+ //_simp->SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ //power_of_2, aaa[1], hi, low));
+ lower_x =
+ _simp->SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ newlen,
+ aaa[1],
+ low_minus_one,
+ low_zero));
aaa = _bm->CreateTerm(BVMULT, newlen, coeff, lower_x);
}
lhs_out.push_back(aaa);
formula_out.push_back(_simp->CreateSimplifiedEQ(lhs, rhs));
} //end of outer forloop()
- output = (formula_out.size() > 0) ? (formula_out.size() > 1) ? _bm->CreateNode(AND, formula_out) : formula_out[0] : ASTTrue;
+ output =
+ (formula_out.size() > 0) ?
+ (formula_out.size() > 1) ?
+ _bm->CreateNode(AND, formula_out) :
+ formula_out[0] :
+ ASTTrue;
UpdateAlreadySolvedMap(input, output);
return output;
return true;
}
- for (ASTVec::const_iterator it = term.begin(), itend = term.end(); it != itend; it++)
+ for (ASTVec::const_iterator
+ it = term.begin(), itend = term.end();
+ it != itend; it++)
{
if (VarSeenInTerm(var, *it))
{
if (0 == key.Degree())
return;
- // If there are references to the key, add them to the references of the value.
+ // 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())
return false;
}
- void Simplifier::UpdateMultInverseMap(const ASTNode& key, const ASTNode& value)
+ void Simplifier::UpdateMultInverseMap(const ASTNode& key,
+ const ASTNode& value)
{
MultInverseMap[key] = value;
}
ASTNode
Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
_bm->Begin_RemoveWrites = false;
ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
}
}
- // The SimplifyMaps on entry to the topLevel functions may contain useful entries.
- // E.g. The BVSolver calls SimplifyTerm()
+ // The SimplifyMaps on entry to the topLevel functions may contain
+ // useful entries. E.g. The BVSolver calls SimplifyTerm()
ASTNode Simplifier::SimplifyFormula_TopLevel(const ASTNode& b,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
_bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
if (_bm->UserFlags.smtlib_parser_flag)
ASTNode zero = _bm->CreateZeroConst(1);
ASTNode one = _bm->CreateOneConst(1);
ASTNode getthebit =
- SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), VarConstMap);
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 1, term, thebit, thebit),
+ VarConstMap);
if (getthebit == zero)
output = pushNeg ? ASTTrue : ASTFalse;
else if (getthebit == one)
}
else
{
- l1 = _bm->CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][1], in[1][1]);
- l2 = _bm->CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][2], in[1][2]);
- result = _bm->CreateTerm(ITE, in.GetValueWidth(), in[0][0], l1, l2);
+ l1 =
+ _bm->CreateTerm(in.GetKind(),
+ in.GetValueWidth(), in[0][1], in[1][1]);
+ l2 =
+ _bm->CreateTerm(in.GetKind(),
+ in.GetValueWidth(), in[0][2], in[1][2]);
+ result =
+ _bm->CreateTerm(ITE,
+ in.GetValueWidth(), in[0][0], l1, l2);
}
assert(result.GetType() == in.GetType());
{
return t1;
}
- if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, t0)) || (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
+ if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, t0))
+ || (NOT == t0.GetKind()
+ && CheckAlwaysTrueFormMap(t0[0])))
{
return t2;
}
{
return t1;
}
- if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, t0)) || (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
+ if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, t0))
+ || (NOT == t0.GetKind()
+ && CheckAlwaysTrueFormMap(t0[0])))
{
return t2;
}
return result;
}
- ASTNode Simplifier::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyAndOrFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
ASTNode output;
//cerr << "input:\n" << a << endl;
Kind k = a.GetKind();
bool isAnd = (k == AND) ? true : false;
- ASTNode annihilator = isAnd ? (pushNeg ? ASTTrue : ASTFalse) : (pushNeg ? ASTFalse : ASTTrue);
+ ASTNode annihilator =
+ isAnd ?
+ (pushNeg ? ASTTrue : ASTFalse) :
+ (pushNeg ? ASTFalse : ASTTrue);
- ASTNode identity = isAnd ? (pushNeg ? ASTFalse : ASTTrue) : (pushNeg ? ASTTrue : ASTFalse);
+ ASTNode identity =
+ isAnd ?
+ (pushNeg ? ASTFalse : ASTTrue) :
+ (pushNeg ? ASTTrue : ASTFalse);
//do the work
ASTVec::const_iterator next_it;
default:
{
output =
- (isAnd) ? (pushNeg ?
- _bm->CreateNode(OR, outvec) :
- _bm->CreateNode(AND, outvec)) :
- (pushNeg ? _bm->CreateNode(AND, outvec) : _bm->CreateNode(OR,outvec));
+ (isAnd) ?
+ (pushNeg ?
+ _bm->CreateNode(OR, outvec) :
+ _bm->CreateNode(AND, outvec)) :
+ (pushNeg ?
+ _bm->CreateNode(AND, outvec) :
+ _bm->CreateNode(OR,outvec));
//output = FlattenOneLevel(output);
break;
}
return output;
if (!(a.Degree() == 1 && NOT == a.GetKind()))
- FatalError("SimplifyNotFormula: input vector with more than 1 node", ASTUndefined);
+ FatalError("SimplifyNotFormula: input vector with more than 1 node",
+ ASTUndefined);
//if pushNeg is set then there is NOT on top
unsigned int NotCount = pushNeg ? 1 : 0;
return output;
}
- ASTNode Simplifier::SimplifyXorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyXorFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
ASTNode output;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
ASTNode a0 = SimplifyFormula(a[0], false, VarConstMap);
ASTNode a1 = SimplifyFormula(a[1], false, VarConstMap);
- output = pushNeg ? _bm->CreateNode(IFF, a0, a1) : _bm->CreateNode(XOR, a0, a1);
+ output =
+ pushNeg ?
+ _bm->CreateNode(IFF, a0, a1) :
+ _bm->CreateNode(XOR, a0, a1);
if (XOR == output.GetKind())
{
a1 = output[1];
if (a0 == a1)
output = ASTFalse;
- else if ((a0 == ASTTrue && a1 == ASTFalse) || (a0 == ASTFalse && a1 == ASTTrue))
+ else if ((a0 == ASTTrue
+ && a1 == ASTFalse)
+ || (a0 == ASTFalse
+ && a1 == ASTTrue))
output = ASTTrue;
}
return output;
}
- ASTNode Simplifier::SimplifyNandFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyNandFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
ASTNode output, a0, a1;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
}
- ASTNode Simplifier::SimplifyNorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyNorFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
ASTNode output, a0, a1;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
}
- ASTNode Simplifier::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyImpliesFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
ASTNode output;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
if (!(a.Degree() == 2 && IMPLIES == a.GetKind()))
- FatalError("SimplifyImpliesFormula: vector with wrong num of nodes", ASTUndefined);
+ FatalError("SimplifyImpliesFormula: vector with wrong num of nodes",
+ ASTUndefined);
ASTNode c0, c1;
if (pushNeg)
return output;
}
- ASTNode Simplifier::SimplifyIffFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyIffFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
ASTNode output;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
if (!(a.Degree() == 2 && IFF == a.GetKind()))
- FatalError("SimplifyIffFormula: vector with wrong num of nodes", ASTUndefined);
+ FatalError("SimplifyIffFormula: vector with wrong num of nodes",
+ ASTUndefined);
ASTNode c0 = a[0];
ASTNode c1 = SimplifyFormula(a[1], false, VarConstMap);
{
output = ASTTrue;
}
- else if ((NOT == c0.GetKind() && c0[0] == c1) || (NOT == c1.GetKind() && c0 == c1[0]))
+ else if ((NOT == c0.GetKind()
+ && c0[0] == c1)
+ || (NOT == c1.GetKind()
+ && c0 == c1[0]))
{
output = ASTFalse;
}
return output;
}
- ASTNode Simplifier::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyIteFormula(const ASTNode& b,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap)
{
// if (!optimize_flag)
// return b;
return output;
if (!(b.Degree() == 3 && ITE == b.GetKind()))
- FatalError("SimplifyIteFormula: vector with wrong num of nodes", ASTUndefined);
+ FatalError("SimplifyIteFormula: vector with wrong num of nodes",
+ ASTUndefined);
ASTNode a = b;
ASTNode t0 = SimplifyFormula(a[0], false, VarConstMap);
//This function simplifies terms based on their kind
ASTNode
- Simplifier::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap)
+ Simplifier::SimplifyTerm(const ASTNode& actualInputterm,
+ ASTNodeMap* VarConstMap)
{
ASTNode inputterm(actualInputterm); // mutable local copy.
if (CheckSimplifyMap(inputterm, output, false, VarConstMap))
{
- //cerr << "SimplifierMap:" << inputterm << " output: " << output << endl;
+ //cerr << "SimplifierMap:" << inputterm << " output: " <<
+ //output << endl;
return output;
}
//########################################
{
if (2 != inputterm.Degree())
{
- FatalError("SimplifyTerm: We assume that BVMULT is binary", inputterm);
+ FatalError("SimplifyTerm: We assume that BVMULT is binary",
+ inputterm);
}
// Described nicely by Warren, Hacker's Delight pg 135.
- // Turn sequences of one bits into subtractions.
- // 28*x == 32x - 4x (two instructions), rather than 16x+ 8x+ 4x.
- // When fully implemented. I.e. supporting sequences of 1 anywhere.
- // Other simplifications will try to fold these back in. So need to be careful
- // about when the simplifications are applied. But in this version it won't
+ // Turn sequences of one bits into subtractions. 28*x ==
+ // 32x - 4x (two instructions), rather than 16x+ 8x+ 4x.
+ // When fully implemented. I.e. supporting sequences of 1
+ // anywhere. Other simplifications will try to fold these
+ // back in. So need to be careful about when the
+ // simplifications are applied. But in this version it won't
// be simplified down by anything else.
- // This (temporary) version only simplifies if all the left most bits are set.
- // All the leftmost bits being set simplifies very nicely down.
+ // This (temporary) version only simplifies if all the left
+ // most bits are set. All the leftmost bits being set
+ // simplifies very nicely down.
const ASTNode& n0 = inputterm.GetChildren()[0];
const ASTNode& n1 = inputterm.GetChildren()[1];
- // This implementation has two problems.
- // 1) It causes a segfault for cmu-model15,16,17
- // 2) It doesn't count the number of bits saved, so if there is a single
- // leading bit it will invert it. Even though that will take more shifts
+ // This implementation has two problems. 1) It causes a
+ // segfault for cmu-model15,16,17 2) It doesn't count the
+ // number of bits saved, so if there is a single leading bit
+ // it will invert it. Even though that will take more shifts
// and adds when it's finally done.
// disabled.
- if (false && (BVCONST == n0.GetKind()) ^ (BVCONST == n1.GetKind()))
+ if (false
+ && (BVCONST == n0.GetKind())
+ ^ (BVCONST == n1.GetKind()))
{
- CBV constant = (BVCONST == n0.GetKind()) ? n0.GetBVConst() : n1.GetBVConst();
- ASTNode other = (BVCONST == n0.GetKind()) ? n1 : n0;
+ CBV constant =
+ (BVCONST == n0.GetKind()) ?
+ n0.GetBVConst() :
+ n1.GetBVConst();
+ ASTNode other =
+ (BVCONST == n0.GetKind()) ?
+ n1 :
+ n0;
int startSequence = 0;
for (unsigned int i = 0; i < inputValueWidth; i++)
if ((inputValueWidth - startSequence) > 3)
{
- // turn off all bits from "startSequence to the end", then add one.
- CBV maskedPlusOne = CONSTANTBV::BitVector_Create(inputValueWidth, true);
+ // turn off all bits from "startSequence to the
+ // end", then add one.
+ CBV maskedPlusOne =
+ CONSTANTBV::BitVector_Create(inputValueWidth, true);
for (int i = 0; i < startSequence; i++)
{
if (!CONSTANTBV::BitVector_bit_test(constant, i)) // swap
CONSTANTBV::BitVector_increment(maskedPlusOne);
ASTNode temp =
_bm->CreateTerm(BVMULT, inputValueWidth,
- _bm->CreateBVConst(maskedPlusOne, inputValueWidth), other);
+ _bm->CreateBVConst(maskedPlusOne,
+ inputValueWidth),
+ other);
output = _bm->CreateTerm(BVNEG, inputValueWidth, temp);
}
}
//BVPLUS, then ignore it (similarily for 1 and BVMULT). else,
//add the computed constant to the nonconst vector, flatten,
//sort, and create BVPLUS/BVMULT and return
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end();
+ it != itend; it++)
{
ASTNode aaa = SimplifyTerm(*it, VarConstMap);
if (BVCONST == aaa.GetKind())
else if (1 < constkids.size())
{
//many elements in constkids. simplify it
- constoutput = _bm->CreateTerm(k, inputterm.GetValueWidth(), constkids);
+ constoutput =
+ _bm->CreateTerm(k, inputterm.GetValueWidth(), constkids);
constoutput = BVConstEvaluator(constoutput);
}
- if (BVMULT == k && zero == constoutput)
+ if (BVMULT == k
+ && zero == constoutput)
{
output = zero;
}
- else if (BVMULT == k && 1 == nonconstkids.size() && constoutput == max)
+ else if (BVMULT == k
+ && 1 == nonconstkids.size()
+ && constoutput == max)
{
//useful special case opt: when input is BVMULT(max_const,t),
//then output = BVUMINUS(t). this is easier on the bitblaster
- output = _bm->CreateTerm(BVUMINUS, inputValueWidth, nonconstkids);
+ output =
+ _bm->CreateTerm(BVUMINUS, inputValueWidth, nonconstkids);
}
else
{
{
//more than 1 element in nonconstkids. create BVPLUS term
SortByArith(nonconstkids);
- output = _bm->CreateTerm(k, inputValueWidth, nonconstkids);
+ output =
+ _bm->CreateTerm(k, inputValueWidth, nonconstkids);
output = Flatten(output);
output = DistributeMultOverPlus(output, true);
output = CombineLikeTerms(output);
output = _bm->CreateTerm(BVMULT, output.GetValueWidth(), d);
if ((uminus & 0x1) != 0) // odd, pull up the uminus.
{
- output = _bm->CreateTerm(BVUMINUS, output.GetValueWidth(), output);
+ output =
+ _bm->CreateTerm(BVUMINUS,
+ output.GetValueWidth(),
+ output);
}
}
}
{
ASTVec d = output.GetChildren();
SortByArith(d);
- output = _bm->CreateTerm(output.GetKind(), output.GetValueWidth(), d);
+ output =
+ _bm->CreateTerm(output.GetKind(),
+ output.GetValueWidth(), d);
}
//covert x-y into x+(-y) and simplify. this transformation
//triggers more simplifications
//
- a1 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a1), VarConstMap);
- output = SimplifyTerm(_bm->CreateTerm(BVPLUS, l, a0, a1), VarConstMap);
+ a1 =
+ SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a1),
+ VarConstMap);
+ output =
+ SimplifyTerm(_bm->CreateTerm(BVPLUS, l, a0, a1),
+ VarConstMap);
}
break;
}
}
case BVNEG:
{
- output = SimplifyTerm(_bm->CreateTerm(BVPLUS, l, a0[0], one), VarConstMap);
+ output =
+ SimplifyTerm(_bm->CreateTerm(BVPLUS, l, a0[0], one),
+ VarConstMap);
break;
}
case BVMULT:
}
else
{
- // If the first argument to the multiply is a constant, push it through.
- // Without regard for the splitting of nodes (hmm.)
- // This is necessary because the bitvector solver can process -3*x, but
- // not -(3*x).
+ // If the first argument to the multiply is a
+ // constant, push it through. Without regard for
+ // the splitting of nodes (hmm.) This is
+ // necessary because the bitvector solver can
+ // process -3*x, but not -(3*x).
if (BVCONST == a0[0].GetKind())
{
- ASTNode a00 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[0]), VarConstMap);
+ ASTNode a00 =
+ SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[0]),
+ VarConstMap);
output = _bm->CreateTerm(BVMULT, l, a00, a0[1]);
}
else
//BVUMINUS(a2x2) + ...
ASTVec c = a0.GetChildren();
ASTVec o;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
//Simplify(BVUMINUS(a1x1))
- ASTNode aaa = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, *it), VarConstMap);
+ ASTNode aaa =
+ SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, *it),
+ VarConstMap);
o.push_back(aaa);
}
//simplify the bvplus
- output = SimplifyTerm(_bm->CreateTerm(BVPLUS, l, o), VarConstMap);
+ output =
+ SimplifyTerm(_bm->CreateTerm(BVPLUS, l, o),
+ VarConstMap);
break;
}
case BVSUB:
{
//BVUMINUS(BVSUB(x,y)) <=> BVSUB(y,x)
- output = SimplifyTerm(_bm->CreateTerm(BVSUB, l, a0[1], a0[0]), VarConstMap);
+ output =
+ SimplifyTerm(_bm->CreateTerm(BVSUB, l, a0[1], a0[0]),
+ VarConstMap);
break;
}
case ITE:
{
//BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2))
ASTNode c = a0[0];
- ASTNode t1 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[1]), VarConstMap);
- ASTNode t2 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[2]), VarConstMap);
+ ASTNode t1 =
+ SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[1]),
+ VarConstMap);
+ ASTNode t2 =
+ SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[2]),
+ VarConstMap);
output = CreateSimplifiedTermITE(c, t1, t2);
break;
}
case BVCONST:
{
//extract the constant
- output = BVConstEvaluator(_bm->CreateTerm(BVEXTRACT, a_len, a0, i, j));
+ output =
+ BVConstEvaluator(_bm->CreateTerm(BVEXTRACT,
+ a_len, a0, i, j));
break;
}
case BVCONCAT:
//Apply the following rule:
// (t@u)[i:j] <==> u[i:j], if len(u) > i
//
- output = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, u, i, j), VarConstMap);
+ output =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, u, i, j),
+ VarConstMap);
}
else if (len_a0 > i_val && j_val >= len_u)
{
- //Apply the rule:
- // (t@u)[i:j] <==> t[i-len_u:j-len_u], if len(t@u) > i >= j >= len(u)
+ //Apply the rule: (t@u)[i:j] <==>
+ // t[i-len_u:j-len_u], if len(t@u) > i >= j >=
+ // len(u)
i = _bm->CreateBVConst(32, i_val - len_u);
j = _bm->CreateBVConst(32, j_val - len_u);
- output = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap);
+ output =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, t, i, j),
+ VarConstMap);
}
else
{
// (t@u)[i:j] <==> t[i-len_u:0] @ u[len_u-1:j]
i = _bm->CreateBVConst(32, i_val - len_u);
ASTNode m = _bm->CreateBVConst(32, len_u - 1);
- t = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero), VarConstMap);
- u = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, len_u - j_val, u, m, j), VarConstMap);
+ t =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ i_val - len_u + 1,
+ t, i, zero),
+ VarConstMap);
+ u =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ len_u - j_val,
+ u, m, j),
+ VarConstMap);
output = _bm->CreateTerm(BVCONCAT, a_len, t, u);
}
break;
//similar rule for BVPLUS
ASTVec c = a0.GetChildren();
ASTVec o;
- for (ASTVec::iterator jt = c.begin(), jtend = c.end(); jt != jtend; jt++)
+ for (ASTVec::iterator
+ jt = c.begin(), jtend = c.end();
+ jt != jtend; jt++)
{
ASTNode aaa = *jt;
- aaa = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero), VarConstMap);
+ aaa =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ i_val + 1,
+ aaa, i, zero),
+ VarConstMap);
o.push_back(aaa);
}
output = _bm->CreateTerm(a0.GetKind(), i_val + 1, o);
// (t op u)[i:j] <==> t[i:j] op u[i:j]
ASTNode t = a0[0];
ASTNode u = a0[1];
- t = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap);
- u = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, u, i, j), VarConstMap);
+ t =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ a_len, t, i, j),
+ VarConstMap);
+ u =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ a_len, u, i, j),
+ VarConstMap);
BVTypeCheck(t);
BVTypeCheck(u);
output = _bm->CreateTerm(k1, a_len, t, u);
{
// (~t)[i:j] <==> ~(t[i:j])
ASTNode t = a0[0];
- t = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap);
+ t =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, t, i, j),
+ VarConstMap);
output = _bm->CreateTerm(BVNEG, a_len, t);
break;
}
- // case BVSX:{
- // //(BVSX(t,n)[i:j] <==> BVSX(t,i+1), if n >= i+1 and j=0
- // ASTNode t = a0[0];
- // unsigned int bvsx_len = a0.GetValueWidth();
- // if(bvsx_len < a_len) {
- // FatalError("SimplifyTerm: BVEXTRACT over BVSX:"
- // "the length of BVSX term must be greater than extract-len",inputterm);
- // }
- // if(j != zero) {
- // output = _bm->CreateTerm(BVEXTRACT,a_len,a0,i,j);
- // }
- // else {
- // output = _bm->CreateTerm(BVSX,a_len,t,_bm->CreateBVConst(32,a_len));
- // }
- // break;
- // }
+ // case BVSX:{ //(BVSX(t,n)[i:j] <==> BVSX(t,i+1), if n
+ // >= i+1 and j=0 ASTNode t = a0[0]; unsigned int
+ // bvsx_len = a0.GetValueWidth(); if(bvsx_len <
+ // a_len) { FatalError("SimplifyTerm: BVEXTRACT
+ // over BVSX:" "the length of BVSX term must be
+ // greater than extract-len",inputterm); } if(j
+ // != zero) { output =
+ // _bm->CreateTerm(BVEXTRACT,a_len,a0,i,j); }
+ // else { output =
+ // _bm->CreateTerm(BVSX,a_len,t,
+ // _bm->CreateBVConst(32,a_len));
+ // } break; }
case ITE:
{
ASTNode t0 = a0[0];
- ASTNode t1 = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, a0[1], i, j), VarConstMap);
- ASTNode t2 = SimplifyTerm(_bm->CreateTerm(BVEXTRACT, a_len, a0[2], i, j), VarConstMap);
+ ASTNode t1 =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ a_len, a0[1], i, j),
+ VarConstMap);
+ ASTNode t2 =
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT,
+ a_len, a0[2], i, j),
+ VarConstMap);
output = CreateSimplifiedTermITE(t0, t1, t2);
break;
}
case BVNEG:
output = a0[0];
break;
- // case ITE: {
- // ASTNode cond = a0[0];
- // ASTNode thenpart = SimplifyTerm(_bm->CreateTerm(BVNEG,len,a0[1]), VarConstMap);
- // ASTNode elsepart = SimplifyTerm(_bm->CreateTerm(BVNEG,len,a0[2]), VarConstMap);
- // output = _bm->CreateSimplifiedTermITE(cond,thenpart,elsepart);
- // break;
- // }
+ // case ITE: { ASTNode cond = a0[0]; ASTNode thenpart =
+ // SimplifyTerm(_bm->CreateTerm(BVNEG,len,a0[1]),
+ // VarConstMap); ASTNode elsepart =
+ // SimplifyTerm(_bm->CreateTerm(BVNEG,len,a0[2]),
+ // VarConstMap); output =
+ // _bm->CreateSimplifiedTermITE(cond,thenpart,elsepart);
+ // break; }
default:
output = _bm->CreateTerm(BVNEG, len, a0);
break;
output = BVConstEvaluator(_bm->CreateTerm(BVSX, len, a0, a1));
break;
case BVNEG:
- output = _bm->CreateTerm(a0.GetKind(), len, _bm->CreateTerm(BVSX, len, a0[0], a1));
+ output =
+ _bm->CreateTerm(a0.GetKind(), len,
+ _bm->CreateTerm(BVSX, len, a0[0], a1));
break;
case BVAND:
case BVOR:
//assuming BVAND and BVOR are binary
- output = _bm->CreateTerm(a0.GetKind(), len, _bm->CreateTerm(BVSX, len, a0[0], a1), _bm->CreateTerm(BVSX, len, a0[1], a1));
+ output =
+ _bm->CreateTerm(a0.GetKind(), len,
+ _bm->CreateTerm(BVSX, len, a0[0], a1),
+ _bm->CreateTerm(BVSX, len, a0[1], a1));
break;
case BVPLUS:
{
- //BVSX(m,BVPLUS(n,BVSX(t1),BVSX(t2))) <==> BVPLUS(m,BVSX(m,t1),BVSX(m,t2))
+ //BVSX(m,BVPLUS(n,BVSX(t1),BVSX(t2))) <==>
+ //BVPLUS(m,BVSX(m,t1),BVSX(m,t2))
ASTVec c = a0.GetChildren();
bool returnflag = false;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
if (BVSX != it->GetKind())
{
else
{
ASTVec o;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
- ASTNode aaa = SimplifyTerm(_bm->CreateTerm(BVSX, len, *it, a1), VarConstMap);
+ ASTNode aaa =
+ SimplifyTerm(_bm->CreateTerm(BVSX, len, *it, a1),
+ VarConstMap);
o.push_back(aaa);
}
output = _bm->CreateTerm(a0.GetKind(), len, o);
case ITE:
{
ASTNode cond = a0[0];
- ASTNode thenpart = SimplifyTerm(_bm->CreateTerm(BVSX, len, a0[1], a1), VarConstMap);
- ASTNode elsepart = SimplifyTerm(_bm->CreateTerm(BVSX, len, a0[2], a1), VarConstMap);
+ ASTNode thenpart =
+ SimplifyTerm(_bm->CreateTerm(BVSX, len, a0[1], a1),
+ VarConstMap);
+ ASTNode elsepart =
+ SimplifyTerm(_bm->CreateTerm(BVSX, len, a0[2], a1),
+ VarConstMap);
output = CreateSimplifiedTermITE(cond, thenpart, elsepart);
break;
}
SortByArith(c);
ASTVec o;
bool constant = true;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
ASTNode aaa = SimplifyTerm(*it, VarConstMap);
if (BVCONST != aaa.GetKind())
if (BVCONST == tkind && BVCONST == ukind)
{
- output = BVConstEvaluator(_bm->CreateTerm(BVCONCAT, inputValueWidth, t, u));
+ output =
+ BVConstEvaluator(_bm->CreateTerm(BVCONCAT,
+ inputValueWidth, t, u));
}
- else if (BVEXTRACT == tkind && BVEXTRACT == ukind && t[0] == u[0])
+ else if (BVEXTRACT == tkind
+ && BVEXTRACT == ukind
+ && t[0] == u[0])
{
//to handle the case x[m:n]@x[n-1:k] <==> x[m:k]
ASTNode t_hi = t[1];
ASTNode t_low = t[2];
ASTNode u_hi = u[1];
ASTNode u_low = u[2];
- ASTNode c = BVConstEvaluator(_bm->CreateTerm(BVPLUS, 32, u_hi, _bm->CreateOneConst(32)));
+ ASTNode c =
+ BVConstEvaluator(_bm->CreateTerm(BVPLUS, 32,
+ u_hi,
+ _bm->CreateOneConst(32)));
if (t_low == c)
{
- output = _bm->CreateTerm(BVEXTRACT, inputValueWidth, t[0], t_hi, u_low);
+ output =
+ _bm->CreateTerm(BVEXTRACT,
+ inputValueWidth, t[0], t_hi, u_low);
}
else
{
{
if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
{
- // Intended to remove shifts by very large amounts that don't fit into the unsigned.
- // at thhe start of the "else" branch.
+ // Intended to remove shifts by very large amounts
+ // that don't fit into the unsigned. at thhe start
+ // of the "else" branch.
output = _bm->CreateZeroConst(width);
}
else
ASTNode zero = _bm->CreateZeroConst(shift);
ASTNode hi = _bm->CreateBVConst(32, width - shift -1);
ASTNode low = _bm->CreateBVConst(32, 0);
- ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low);
+ ASTNode extract =
+ _bm->CreateTerm(BVEXTRACT, width - shift,
+ a, hi, low);
BVTypeCheck(extract);
- output = _bm->CreateTerm(BVCONCAT, width, extract, zero);
+ output =
+ _bm->CreateTerm(BVCONCAT, width,
+ extract, zero);
BVTypeCheck(output);
}
else if (k == BVRIGHTSHIFT)
ASTNode zero = _bm->CreateZeroConst(shift);
ASTNode hi = _bm->CreateBVConst(32, width -1);
ASTNode low = _bm->CreateBVConst(32, shift);
- ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low);
+ ASTNode extract =
+ _bm->CreateTerm(BVEXTRACT, width - shift,
+ a, hi, low);
BVTypeCheck(extract);
- output = _bm->CreateTerm(BVCONCAT, width, zero, extract);
+ output =
+ _bm->CreateTerm(BVCONCAT, width, zero, extract);
BVTypeCheck(output);
}
else
ASTVec c = inputterm.GetChildren();
ASTVec o;
bool constant = true;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
ASTNode aaa = SimplifyTerm(*it, VarConstMap);
if (BVCONST != aaa.GetKind())
}
else if (ITE == inputterm[0].GetKind())
{
- ASTNode cond = SimplifyFormula(inputterm[0][0], false, VarConstMap);
- ASTNode index = SimplifyTerm(inputterm[1], VarConstMap);
-
- ASTNode read1 = _bm->CreateTerm(READ, inputValueWidth, inputterm[0][1], index);
- ASTNode read2 = _bm->CreateTerm(READ, inputValueWidth, inputterm[0][2], index);
-
+ ASTNode cond =
+ SimplifyFormula(inputterm[0][0], false, VarConstMap);
+ ASTNode index =
+ SimplifyTerm(inputterm[1], VarConstMap);
+ ASTNode read1 =
+ _bm->CreateTerm(READ,
+ inputValueWidth,
+ inputterm[0][1], index);
+ ASTNode read2 =
+ _bm->CreateTerm(READ,
+ inputValueWidth,
+ inputterm[0][2], index);
read1 = SimplifyTerm(read1, VarConstMap);
read2 = SimplifyTerm(read2, VarConstMap);
out1 = CreateSimplifiedTermITE(cond, read1, read2);
{
ASTVec c = inputterm.GetChildren();
ASTVec o;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
ASTNode aaa = SimplifyTerm(*it, VarConstMap);
o.push_back(aaa);
}
case WRITE:
default:
- FatalError("SimplifyTerm: Control should never reach here:", inputterm, k);
+ FatalError("SimplifyTerm: Control should never reach here:",
+ inputterm, k);
return inputterm;
break;
}
//At the end of each simplification call, we want the output to be
//always smaller or equal to the input in size.
- void Simplifier::CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output)
+ void Simplifier::CheckSimplifyInvariant(const ASTNode& a,
+ const ASTNode& output)
{
if (_bm->NodeSize(a, true) + 1 < _bm->NodeSize(output, true))
{
cerr << "lhs := " << a << endl;
- cerr << "NodeSize of lhs is: " << _bm->NodeSize(a, true) << endl;
+ cerr << "NodeSize of lhs is: "
+ << _bm->NodeSize(a, true) << endl;
cerr << endl;
cerr << "rhs := " << output << endl;
- cerr << "NodeSize of rhs is: " << _bm->NodeSize(output, true) << endl;
- // FatalError("SimplifyFormula: The nodesize shoudl decrease from lhs to rhs: ",ASTUndefined);
+ cerr << "NodeSize of rhs is: "
+ << _bm->NodeSize(output, true) << endl;
+ // FatalError("SimplifyFormula: The nodesize shoudl decrease
+ // from lhs to rhs: ",ASTUndefined);
}
}
//go over the childnodes of the input bvplus, and collect like
//terms in a map. the key of the map are the variables, and the
//values are stored in a ASTVec
- for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::const_iterator
+ it = c.begin(), itend = c.end(); it != itend; it++)
{
ASTNode aaa = *it;
if (SYMBOL == aaa.GetKind())
{
vars_to_consts[aaa].push_back(one);
}
- else if (BVMULT == aaa.GetKind() && BVUMINUS == aaa[0].GetKind() && BVCONST == aaa[0][0].GetKind())
+ else if (BVMULT == aaa.GetKind()
+ && BVUMINUS == aaa[0].GetKind()
+ && BVCONST == aaa[0][0].GetKind())
{
//(BVUMINUS(c))*(y) <==> compute(BVUMINUS(c))*y
ASTNode compute_const = BVConstEvaluator(aaa[0]);
vars_to_consts[aaa[1]].push_back(compute_const);
}
- else if (BVMULT == aaa.GetKind() && BVUMINUS == aaa[1].GetKind() && BVCONST == aaa[0].GetKind())
+ else if (BVMULT == aaa.GetKind()
+ && BVUMINUS == aaa[1].GetKind()
+ && BVCONST == aaa[0].GetKind())
{
//c*(BVUMINUS(y)) <==> compute(BVUMINUS(c))*y
- ASTNode cccc = BVConstEvaluator(_bm->CreateTerm(BVUMINUS, len, aaa[0]));
+ ASTNode cccc =
+ BVConstEvaluator(_bm->CreateTerm(BVUMINUS, len, aaa[0]));
vars_to_consts[aaa[1][0]].push_back(cccc);
}
else if (BVMULT == aaa.GetKind() && BVCONST == aaa[0].GetKind())
//go over the map from variables to vector of values. combine the
//vector of values, multiply to the variable, and put the
//resultant monomial in the output BVPLUS.
- for (ASTNodeToVecMap::iterator it = vars_to_consts.begin(), itend = vars_to_consts.end(); it != itend; it++)
+ for (ASTNodeToVecMap::iterator
+ it = vars_to_consts.begin(), itend = vars_to_consts.end();
+ it != itend; it++)
{
ASTVec ccc = it->second;
monom = it->first;
else
{
- monom = SimplifyTerm(_bm->CreateTerm(BVMULT, constant.GetValueWidth(), constant, it->first));
+ monom =
+ SimplifyTerm(_bm->CreateTerm(BVMULT,
+ constant.GetValueWidth(),
+ constant, it->first));
}
if (zero != monom)
{
if (constkids.size() > 1)
{
- ASTNode output = _bm->CreateTerm(BVPLUS, constkids[0].GetValueWidth(), constkids);
+ ASTNode output =
+ _bm->CreateTerm(BVPLUS,
+ constkids[0].GetValueWidth(), constkids);
output = BVConstEvaluator(output);
if (output != zero)
outputvec.push_back(output);
Kind k_rhs = rhs.GetKind();
//either the lhs has to be a BVPLUS or the rhs has to be a
//BVPLUS
- if (!(BVPLUS == k_lhs || BVPLUS == k_rhs || (BVMULT == k_lhs && BVMULT == k_rhs)))
+ if (!(BVPLUS == k_lhs
+ || BVPLUS == k_rhs
+ || (BVMULT == k_lhs
+ && BVMULT == k_rhs)))
{
return eq;
}
// (y1 + y2 + ...+ yn)*x <==> x*y1 + x*y2 + ... + x*yn
//
// The function assumes that the BVPLUSes have been flattened
- ASTNode Simplifier::DistributeMultOverPlus(const ASTNode& a, bool startdistribution)
+ ASTNode Simplifier::DistributeMultOverPlus(const ASTNode& a,
+ bool startdistribution)
{
if (!startdistribution)
return a;
}
//special case optimization: c1*(c2*t1) <==> (c1*c2)*t1
- if (BVCONST == left_kind && BVMULT == right_kind && BVCONST == right[0].GetKind())
- {
- ASTNode c = BVConstEvaluator(_bm->CreateTerm(BVMULT, a.GetValueWidth(), left, right[0]));
+ if (BVCONST == left_kind
+ && BVMULT == right_kind
+ && BVCONST == right[0].GetKind())
+ {
+ ASTNode c =
+ BVConstEvaluator(_bm->CreateTerm(BVMULT,
+ a.GetValueWidth(),
+ left, right[0]));
c = _bm->CreateTerm(BVMULT, a.GetValueWidth(), c, right[1]);
return c;
left = c[0];
}
//special case optimization: c1*(t1*c2) <==> (c1*c2)*t1
- if (BVCONST == left_kind && BVMULT == right_kind && BVCONST == right[1].GetKind())
- {
- ASTNode c = BVConstEvaluator(_bm->CreateTerm(BVMULT, a.GetValueWidth(), left, right[1]));
+ if (BVCONST == left_kind
+ && BVMULT == right_kind
+ && BVCONST == right[1].GetKind())
+ {
+ ASTNode c =
+ BVConstEvaluator(_bm->CreateTerm(BVMULT,
+ a.GetValueWidth(),
+ left, right[1]));
c = _bm->CreateTerm(BVMULT, a.GetValueWidth(), c, right[0]);
return c;
left = c[0];
}
else
{
- for (ASTVec::iterator j = rightnodes.begin(), jend = rightnodes.end(); j != jend; j++)
+ for (ASTVec::iterator
+ j = rightnodes.begin(), jend = rightnodes.end();
+ j != jend; j++)
{
- ASTNode out = SimplifyTerm(_bm->CreateTerm(BVMULT, len, left, *j));
+ ASTNode out =
+ SimplifyTerm(_bm->CreateTerm(BVMULT, len, left, *j));
outputvec.push_back(out);
}
}
ASTVec leftnodes = left.GetChildren();
// (x1 + x2 + ... + xm)*(y1 + y2 + ...+ yn) <==> x1*y1 + x1*y2 +
// ... + x2*y1 + ... + xm*yn
- for (ASTVec::iterator i = leftnodes.begin(), iend = leftnodes.end(); i != iend; i++)
+ for (ASTVec::iterator
+ i = leftnodes.begin(), iend = leftnodes.end();
+ i != iend; i++)
{
ASTNode multiplier = *i;
- for (ASTVec::iterator j = rightnodes.begin(), jend = rightnodes.end(); j != jend; j++)
+ for (ASTVec::iterator
+ j = rightnodes.begin(), jend = rightnodes.end();
+ j != jend; j++)
{
- ASTNode out = SimplifyTerm(_bm->CreateTerm(BVMULT, len, multiplier, *j));
+ ASTNode out =
+ SimplifyTerm(_bm->CreateTerm(BVMULT, len, multiplier, *j));
outputvec.push_back(out);
}
}
if (a0_len > a_len)
{
FatalError("Trying to sign_extend a larger BV into a smaller BV");
- return ASTUndefined; //to stop the compiler from producing bogus warnings
+ return ASTUndefined;
}
//sign extend
BEEV::ASTNode BVZeros = _bm->CreateBVConst(zeros.c_str(), 2);
//string of ones BVCONCAT a0
- BEEV::ASTNode concatOnes = _bm->CreateTerm(BEEV::BVCONCAT, a_len, BVOnes, a0);
+ BEEV::ASTNode concatOnes =
+ _bm->CreateTerm(BEEV::BVCONCAT, a_len, BVOnes, a0);
//string of zeros BVCONCAT a0
- BEEV::ASTNode concatZeros = _bm->CreateTerm(BEEV::BVCONCAT, a_len, BVZeros, a0);
+ BEEV::ASTNode concatZeros =
+ _bm->CreateTerm(BEEV::BVCONCAT, a_len, BVZeros, a0);
//extract top bit of a0
BEEV::ASTNode hi = _bm->CreateBVConst(32, a0_len - 1);
BEEV::ASTNode topBit = _bm->CreateTerm(BEEV::BVEXTRACT, 1, a0, hi, low);
//compare topBit of a0 with 0bin1
- BEEV::ASTNode condition = CreateSimplifiedEQ(_bm->CreateBVConst(1, 1), topBit);
+ BEEV::ASTNode condition =
+ CreateSimplifiedEQ(_bm->CreateBVConst(1, 1), topBit);
//ITE(topbit = 0bin1, 0bin1111...a0, 0bin000...a0)
output = CreateSimplifiedTermITE(condition, concatOnes, concatZeros);
}
} //end of RemoveWrites_TopLevel()
- ASTNode Simplifier::SimplifyWrites_InPlace(const ASTNode& term, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::SimplifyWrites_InPlace(const ASTNode& term,
+ ASTNodeMap* VarConstMap)
{
ASTNodeMultiSet WriteIndicesSeenSoFar;
bool SeenNonConstWriteIndex = false;
- if ((READ != term.GetKind()) || (WRITE != term[0].GetKind()))
+ if ((READ != term.GetKind())
+ || (WRITE != term[0].GetKind()))
{
FatalError("RemovesWrites: Input must be a READ over a WRITE", term);
}
//compare the readIndex and the current writeIndex and see if they
//simplify to TRUE or FALSE or UNDETERMINABLE at this stage
- ASTNode compare_readwrite_indices = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false, VarConstMap);
+ ASTNode compare_readwrite_indices =
+ SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex),
+ false, VarConstMap);
//if readIndex and writeIndex are equal
if (ASTTrue == compare_readwrite_indices && !SeenNonConstWriteIndex)
return writeVal;
}
- if (!(ASTTrue == compare_readwrite_indices || ASTFalse == compare_readwrite_indices))
+ if (!(ASTTrue == compare_readwrite_indices
+ || ASTFalse == compare_readwrite_indices))
{
SeenNonConstWriteIndex = true;
}
//if (readIndex=writeIndex <=> FALSE)
- if (ASTFalse == compare_readwrite_indices || (WriteIndicesSeenSoFar.find(writeIndex) != WriteIndicesSeenSoFar.end()))
+ if (ASTFalse == compare_readwrite_indices
+ || (WriteIndicesSeenSoFar.find(writeIndex)
+ != WriteIndicesSeenSoFar.end()))
{
//drop the current level write
//do nothing
NewName_ReadOverWrite_Map[newVar] = input;
UpdateSimplifyMap(input, newVar, false);
- _bm->ASTNodeStats("New Var Name which replace Read_Over_Write: ", newVar);
+ _bm->ASTNodeStats("New Var Name which replace Read_Over_Write: ",
+ newVar);
}
output = newVar;
} //end of start_abstracting if condition
return output;
} //end of RemoveWrites()
- ASTNode Simplifier::ReadOverWrite_To_ITE(const ASTNode& term, ASTNodeMap* VarConstMap)
+ ASTNode Simplifier::ReadOverWrite_To_ITE(const ASTNode& term,
+ ASTNodeMap* VarConstMap)
{
unsigned int width = term.GetValueWidth();
ASTNode input = term;
ASTNode writeIndex = SimplifyTerm(write[1]);
ASTNode writeVal = SimplifyTerm(write[2]);
- ASTNode cond = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false, VarConstMap);
+ ASTNode cond =
+ SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex),
+ false,
+ VarConstMap);
ASTNode newRead = _bm->CreateTerm(READ, width, writeA, readIndex);
ASTNode newRead_memoized = newRead;
if (CheckSimplifyMap(newRead, newRead_memoized, false))
newRead = newRead_memoized;
}
- if (ASTTrue == cond && (term == partialITE))
+ if (ASTTrue == cond
+ && (term == partialITE))
{
- //found the write-value in the first iteration itself. return
- //it
+ //found the write-value in the first iteration
+ //itself. return it
output = writeVal;
UpdateSimplifyMap(term, output, false);
return output;
}
- if (READ == partialITE.GetKind() && WRITE == partialITE[0].GetKind())
+ if (READ == partialITE.GetKind()
+ && WRITE == partialITE[0].GetKind())
{
- //first iteration or (previous cond==ASTFALSE and partialITE is a "READ over WRITE")
- partialITE = CreateSimplifiedTermITE(cond, writeVal, newRead);
+ //first iteration or (previous cond==ASTFALSE and
+ //partialITE is a "READ over WRITE")
+ partialITE =
+ CreateSimplifiedTermITE(cond, writeVal, newRead);
}
else if (ITE == partialITE.GetKind())
{
//ITE(i1 = j, v1, R(A,j))
- ASTNode ElseITE = CreateSimplifiedTermITE(cond, writeVal, newRead);
+ ASTNode ElseITE =
+ CreateSimplifiedTermITE(cond, writeVal, newRead);
//R(W(A,i1,v1),j) <==> ITE(i1 = j, v1, R(A,j))
UpdateSimplifyMap(oldRead, ElseITE, false);
- //ITE(i2 = j, v2, R(W(A,i1,v1),j)) <==> ITE(i2 = j, v2, ITE(i1 = j, v1, R(A,j)))
+ //ITE(i2 = j, v2, R(W(A,i1,v1),j)) <==> ITE(i2 = j, v2,
+ //ITE(i1 = j, v1, R(A,j)))
partialITE = SimplifyTerm(partialITE);
}
else
ASTNode inverse;
if (CheckMultInverseMap(d, inverse))
{
- //cerr << "found the inverse of: " << d << "and it is: " << inverse << endl;
+ //cerr << "found the inverse of: " << d << "and it is: " <<
+ //inverse << endl;
return inverse;
}
//create a '0' which is 1 bit long
ASTNode onebit_zero = _bm->CreateZeroConst(1);
//zero pad t0, i.e. 0 @ t0
- c = BVConstEvaluator(_bm->CreateTerm(BVCONCAT, inputwidth + 1, onebit_zero, c));
+ c =
+ BVConstEvaluator(_bm->CreateTerm(BVCONCAT,
+ inputwidth + 1, onebit_zero, c));
//construct 2^(inputwidth), i.e. a bitvector of length
//'inputwidth+1', which is max(inputwidth)+1
//all 1's
ASTNode max = _bm->CreateMaxConst(inputwidth);
//zero pad max
- max = BVConstEvaluator(_bm->CreateTerm(BVCONCAT, inputwidth + 1, onebit_zero, max));
+ max =
+ BVConstEvaluator(_bm->CreateTerm(BVCONCAT,
+ inputwidth + 1, onebit_zero, max));
//_bm->Create a '1' which has leading zeros of length 'inputwidth'
- ASTNode inputwidthplusone_one = _bm->CreateOneConst(inputwidth + 1);
+ ASTNode inputwidthplusone_one =
+ _bm->CreateOneConst(inputwidth + 1);
//add 1 to max
- max = _bm->CreateTerm(BVPLUS, inputwidth + 1, max, inputwidthplusone_one);
- max = BVConstEvaluator(max);
-
+ max =
+ _bm->CreateTerm(BVPLUS, inputwidth + 1, max, inputwidthplusone_one);
+ max =
+ BVConstEvaluator(max);
ASTNode zero = _bm->CreateZeroConst(inputwidth + 1);
ASTNode max_bvgt_0 = _bm->CreateNode(BVGT, max, zero);
ASTNode quotient, remainder;
while (ASTTrue == BVConstEvaluator(max_bvgt_0))
{
//quotient = (c divided by max)
- quotient = BVConstEvaluator(_bm->CreateTerm(BVDIV, inputwidth + 1, c, max));
+ quotient =
+ BVConstEvaluator(_bm->CreateTerm(BVDIV,
+ inputwidth + 1, c, max));
//remainder of (c divided by max)
- remainder = BVConstEvaluator(_bm->CreateTerm(BVMOD, inputwidth + 1, c, max));
+ remainder =
+ BVConstEvaluator(_bm->CreateTerm(BVMOD,
+ inputwidth + 1, c, max));
//x = x2 - q*x1
- x = _bm->CreateTerm(BVSUB, inputwidth + 1, x2, _bm->CreateTerm(BVMULT, inputwidth + 1, quotient, x1));
+ x =
+ _bm->CreateTerm(BVSUB,
+ inputwidth + 1, x2,
+ _bm->CreateTerm(BVMULT,
+ inputwidth + 1,
+ quotient, x1));
x = BVConstEvaluator(x);
//fix the inputs to the extended euclidian algo
projects / francis / stp.git / commitdiff