}
//chooses a variable in the lhs and returns the chosen variable
- ASTNode BVSolver::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs)
+ ASTNode BVSolver::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs, ASTNodeSet& checked)
{
assert(EQ == eq.GetKind());
assert(BVPLUS == eq[0].GetKind() || BVPLUS== eq[1].GetKind());
SYMBOL == monom.GetKind()
&& !chosen_symbol
&& !DoNotSolveThis(monom)
+ && checked.find(monom)==checked.end()
&& !vars.VarSeenInTerm(monom,rhs)
)
||
&& SYMBOL == monom[0].GetKind()
&& !chosen_symbol
&& !DoNotSolveThis(monom[0])
+ && checked.find(monom[0])==checked.end()
&& !vars.VarSeenInTerm(monom[0],rhs)
)
)
{
outmonom = monom; //nb. monom not var.
chosen_symbol = true;
+ checked.insert(var);
}
else
o.push_back(monom);
&& _simp->BVConstIsOdd(monom[0])
&& !chosen_symbol
&& !DoNotSolveThis(var)
+ && checked.find(var)==checked.end()
&& ((SYMBOL == var.GetKind()
&& !vars.VarSeenInTerm(var,rhs)
)
//monom[0] is odd.
outmonom = monom;
chosen_symbol = true;
+ checked.insert(var);
}
else if (
!chosen_symbol
&& BVCONST == monom[1].GetKind()
&& zero == monom[2]
&& !DoNotSolveThis(monom[0])
+ && checked.find(monom[0])==checked.end()
&& !vars.VarSeenInTerm(monom[0],rhs)
)
{
outmonom = monom;
chosen_symbol = true;
+ checked.insert(monom[0]);
}
else if (
!chosen_symbol
&& BVCONST == monom[0][1].GetKind()
&& zero == monom[0][2]
&& !DoNotSolveThis(monom[0][0])
+ && checked.find(monom[0][0])==checked.end()
&& !vars.VarSeenInTerm(monom[0][0],rhs)
)
{
outmonom = monom;
chosen_symbol = true;
+ checked.insert(monom[0][0]);
}
else
return outmonom;
} //end of choosemonom()
+ // Manipulate the lhs and rhs to get just a variable on the lhs (if possible). Then add to the
+ // substitution map.
+ ASTNode BVSolver::substitute(const ASTNode& eq, const ASTNode& lhs, const ASTNode& rhs, const bool single)
+ {
+
+ ASTNode output;
+
+ switch (lhs.GetKind())
+ {
+ case SYMBOL:
+ {
+ DoNotSolve_TheseVars.insert(lhs);
+
+ //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 (!single && vars.VarSeenInTerm(lhs, rhs))
+ {
+ //found the lhs in the rhs. Abort!
+ return eq;
+ }
+
+ if (!_simp->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]
+ && !vars.VarSeenInTerm(lhs[0], rhs)
+ && !DoNotSolveThis(lhs[0])))
+ {
+ return eq;
+ }
+
+ if (vars.VarSeenInTerm(lhs[0], rhs))
+ {
+ DoNotSolve_TheseVars.insert(lhs[0]);
+ return eq;
+ }
+
+ DoNotSolve_TheseVars.insert(lhs[0]);
+ if (!_simp->UpdateSolverMap(lhs, rhs))
+ {
+ return eq;
+ }
+
+ if (lhs[0].GetValueWidth() != lhs.GetValueWidth())
+ {
+ //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 =
+ _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs.GetValueWidth(), "v_solver");
+ newvar =
+ _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs);
+ assert(BVTypeCheck(newvar));
+ _simp->UpdateSolverMap(var, newvar);
+ }
+ else
+ _simp->UpdateSolverMap(lhs[0], rhs);
+ 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());
+
+ //if coeff is even, then we know that all the coeffs in the eqn
+ //are even. Simply return the eqn
+ if (!_simp->BVConstIsOdd(lhs[0]))
+ {
+ return eq;
+ }
+
+ ASTNode a = _simp->MultiplicativeInverse(lhs[0]);
+ ASTNode chosenvar =
+ ChosenVar_Is_Extract ? lhs[1][0] : lhs[1];
+ ASTNode chosenvar_value =
+ simplifyNode(_bm->CreateTerm(BVMULT,
+ rhs.GetValueWidth(),
+ a, rhs));
+
+ //if chosenvar is seen in chosenvar_value then abort
+ if (vars.VarSeenInTerm(chosenvar, chosenvar_value))
+ {
+ //abort solving
+ DoNotSolve_TheseVars.insert(lhs);
+ return eq;
+ }
+
+ // It fails if it's a full-bitwidth extract. These are rare, and won't be
+ // present after simplification. So ignore them for now.
+ if (ChosenVar_Is_Extract && lhs[0].GetValueWidth() == lhs.GetValueWidth())
+ return eq;
+
+ //found a variable to solve
+ DoNotSolve_TheseVars.insert(chosenvar);
+ chosenvar = lhs[1];
+ if (!_simp->UpdateSolverMap(chosenvar, chosenvar_value))
+ {
+ return eq;
+ }
+
+ if (ChosenVar_Is_Extract)
+ {
+ const ASTNode& var = lhs[1][0];
+
+ ASTNode newvar =
+ _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs[1].GetValueWidth(), "v_solver");
+ newvar =
+ _bm->CreateTerm(BVCONCAT,
+ var.GetValueWidth(),
+ newvar, chosenvar_value);
+ assert(BVTypeCheck(newvar));
+ _simp->UpdateSolverMap(var, newvar);
+
+ }
+ output = ASTTrue;
+ break;
+ }
+ default:
+ output = eq;
+ break;
+ }
+ return output;
+ }
+
//solver function which solves for variables with odd coefficient
ASTNode BVSolver::BVSolve_Odd(const ASTNode& input)
{
if (BVPLUS == lhs.GetKind())
{
- 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 == ASTUndefined)
- {
- //no monomial was chosen
- return eq;
- }
-
- //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 =
- simplifyNode(_bm->CreateTerm(BVUMINUS,
- len, leftover_lhs));
- assert(BVTypeCheck(leftover_lhs));
- rhs =
- simplifyNode(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
- assert(BVTypeCheck(rhs));
- lhs = chosen_monom;
- single = true;
- } //end of if(BVPLUS ...)
-
- if (BVUMINUS == lhs.GetKind())
- {
- //equation is of the form (-lhs0) = rhs
- ASTNode lhs0 = lhs[0];
- rhs = simplifyNode(_bm->CreateTerm(BVUMINUS,
- rhs.GetValueWidth(), rhs));
- assert(BVTypeCheck(rhs));
- lhs = lhs0;
- }
- switch (lhs.GetKind())
- {
- case SYMBOL:
+ ASTNodeSet checked;
+ do
{
- DoNotSolve_TheseVars.insert(lhs);
+ ASTNode chosen_monom = ASTUndefined;
+ ASTNode leftover_lhs;
- //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 (!single && vars.VarSeenInTerm(lhs, rhs))
+ //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,checked);
+ if (chosen_monom == ASTUndefined)
{
- //found the lhs in the rhs. Abort!
+ //no monomial was chosen
return eq;
}
- if (!_simp->UpdateSolverMap(lhs, rhs))
- {
- return eq;
- }
-
- output = ASTTrue;
- break;
+ //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 = simplifyNode(_bm->CreateTerm(BVUMINUS,len, leftover_lhs));
+ assert(BVTypeCheck(leftover_lhs));
+ rhs = simplifyNode(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
+ assert(BVTypeCheck(rhs));
+ lhs = chosen_monom;
+ single = true;
+ //This tries to substitute it.. But it might not work, in which case it will return eq.
+ output = substitute(eq, lhs, rhs,single);
}
+ while (output == eq);
- case BVEXTRACT:
- {
- const ASTNode zero = _bm->CreateZeroConst(32);
-
- if (!(SYMBOL == lhs[0].GetKind()
- && BVCONST == lhs[1].GetKind()
- && zero == lhs[2]
- && !vars.VarSeenInTerm(lhs[0], rhs)
- && !DoNotSolveThis(lhs[0])))
- {
- return eq;
- }
-
- if (vars.VarSeenInTerm(lhs[0], rhs))
- {
- DoNotSolve_TheseVars.insert(lhs[0]);
- return eq;
- }
-
- DoNotSolve_TheseVars.insert(lhs[0]);
- if (!_simp->UpdateSolverMap(lhs, rhs))
- {
- return eq;
- }
-
- if (lhs[0].GetValueWidth() != lhs.GetValueWidth())
- {
- //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 =
- _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs.GetValueWidth(), "v_solver");
- newvar =
- _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs);
- assert(BVTypeCheck(newvar));
- _simp->UpdateSolverMap(var, newvar);
- }
- else
- _simp->UpdateSolverMap(lhs[0], rhs);
- 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());
-
- //if coeff is even, then we know that all the coeffs in the eqn
- //are even. Simply return the eqn
- if (!_simp->BVConstIsOdd(lhs[0]))
- {
- return eq;
- }
-
- ASTNode a = _simp->MultiplicativeInverse(lhs[0]);
- ASTNode chosenvar =
- ChosenVar_Is_Extract ? lhs[1][0] : lhs[1];
- ASTNode chosenvar_value =
- simplifyNode(_bm->CreateTerm(BVMULT,
- rhs.GetValueWidth(),
- a, rhs));
-
- //if chosenvar is seen in chosenvar_value then abort
- if (vars.VarSeenInTerm(chosenvar, chosenvar_value))
- {
- //abort solving
- DoNotSolve_TheseVars.insert(lhs);
- return eq;
- }
-
- // It fails if it's a full-bitwidth extract. These are rare, and won't be
- // present after simplification. So ignore them for now.
- if (ChosenVar_Is_Extract && lhs[0].GetValueWidth() == lhs.GetValueWidth())
- return eq;
-
- //found a variable to solve
- DoNotSolve_TheseVars.insert(chosenvar);
- chosenvar = lhs[1];
- if (!_simp->UpdateSolverMap(chosenvar, chosenvar_value))
- {
- return eq;
- }
-
- if (ChosenVar_Is_Extract)
- {
- const ASTNode& var = lhs[1][0];
-
- ASTNode newvar =
- _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs[1].GetValueWidth(), "v_solver");
- newvar =
- _bm->CreateTerm(BVCONCAT,
- var.GetValueWidth(),
- newvar, chosenvar_value);
- assert(BVTypeCheck(newvar));
- _simp->UpdateSolverMap(var, newvar);
+ } //end of if(BVPLUS ...)
- }
- output = ASTTrue;
- break;
- }
- default:
- output = eq;
- break;
+ else if (BVUMINUS == lhs.GetKind())
+ {
+ //equation is of the form (-lhs0) = rhs
+ ASTNode lhs0 = lhs[0];
+ rhs = simplifyNode(_bm->CreateTerm(BVUMINUS, rhs.GetValueWidth(), rhs));
+ assert(BVTypeCheck(rhs));
+ lhs = lhs0;
+ output = substitute(eq, lhs, rhs,single);
}
+ else
+ output = substitute(eq, lhs, rhs,single);
UpdateAlreadySolvedMap(input, output);
return output;
projects / francis / stp.git / commitdiff