mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

remove unused variables

Browse source
This commit is contained in:
Jakob Rath 2023-08-01 13:42:02 +02:00
parent d943eb4787
commit 8b90a45233
4 changed files with 1 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/constraint_manager.cpp
View file

@ -613,7 +613,6 @@ namespace polysat {
// v[|q|:] = q // v[|q|:] = q
unsigned const p_sz = p.power_of_2(); unsigned const p_sz = p.power_of_2();
unsigned const q_sz = q.power_of_2(); unsigned const q_sz = q.power_of_2();
unsigned const v_sz = p_sz + q_sz;
if (p.is_val() || q.is_val()) if (p.is_val() || q.is_val())
return zero_ext(p, q_sz) * rational::power_of_two(q_sz) + zero_ext(q, p_sz); return zero_ext(p, q_sz) * rational::power_of_two(q_sz) + zero_ext(q, p_sz);
pvar const v = s.m_slicing.mk_concat({s.m_names.mk_name(p), s.m_names.mk_name(q)}); pvar const v = s.m_slicing.mk_concat({s.m_names.mk_name(p), s.m_names.mk_name(q)});

2
src/math/polysat/op_constraint.cpp
View file

@ -629,7 +629,6 @@ namespace polysat {
* q = 1 ==> r = p * q = 1 ==> r = p
*/ */
clause_ref op_constraint::lemma_udiv(solver& s, assignment const& a) { clause_ref op_constraint::lemma_udiv(solver& s, assignment const& a) {
auto& m = p().manager();
auto pv = a.apply_to(p()); auto pv = a.apply_to(p());
auto qv = a.apply_to(q()); auto qv = a.apply_to(q());
auto rv = a.apply_to(r()); auto rv = a.apply_to(r());
@ -679,7 +678,6 @@ namespace polysat {
* q = 0 ==> r = p * q = 0 ==> r = p
*/ */
clause_ref op_constraint::lemma_urem(solver& s, assignment const& a) { clause_ref op_constraint::lemma_urem(solver& s, assignment const& a) {
auto& m = p().manager();
auto pv = a.apply_to(p()); auto pv = a.apply_to(p());
auto qv = a.apply_to(q()); auto qv = a.apply_to(q());
auto rv = a.apply_to(r()); auto rv = a.apply_to(r());

1
src/math/polysat/polysat_ast.cpp
View file

@ -165,7 +165,6 @@ namespace polysat {
template <typename Fn> template <typename Fn>
expr* polysat_ast::mk_bin(char const* name, pdd const& p, pdd const& q, pdd const& r, Fn mk_bin_expr) { expr* polysat_ast::mk_bin(char const* name, pdd const& p, pdd const& q, pdd const& r, Fn mk_bin_expr) {
unsigned const N = p.power_of_2();
// r = p OP q // r = p OP q
expr* definition = m().mk_eq(mk_poly(r), mk_bin_expr(mk_poly(p), mk_poly(q))); expr* definition = m().mk_eq(mk_poly(r), mk_bin_expr(mk_poly(p), mk_poly(q)));
// b <=> definition // b <=> definition

5
src/math/polysat/saturation.cpp
View file

@ -1359,11 +1359,9 @@ namespace polysat {
if (!is_AxB_eq_0(x, a_l_b, a, b, y)) // TODO: Is the restriction to linear "x" too restrictive? if (!is_AxB_eq_0(x, a_l_b, a, b, y)) // TODO: Is the restriction to linear "x" too restrictive?
return false; return false;
bool change = false;
bool prop = false; bool prop = false;
for (auto c : core) { for (auto c : core) {
change = false;
if (c == a_l_b) if (c == a_l_b)
continue; continue;
LOG("Trying to eliminate v" << x << " in " << c << " by using equation " << a_l_b.as_signed_constraint()); LOG("Trying to eliminate v" << x << " in " << c << " by using equation " << a_l_b.as_signed_constraint());
@ -1448,7 +1446,6 @@ namespace polysat {
* -x < -x - y * -x < -x - y
*/ */
bool saturation::is_add_overflow(pvar x, inequality const& i, pdd& y, bool& is_minus) { bool saturation::is_add_overflow(pvar x, inequality const& i, pdd& y, bool& is_minus) {
auto& m = s.var2pdd(x);
pdd const X = s.var(x); pdd const X = s.var(x);
pdd a = X; pdd a = X;
if (i.lhs().degree(x) != 1 || i.rhs().degree(x) != 1) if (i.lhs().degree(x) != 1 || i.rhs().degree(x) != 1)
@ -1950,7 +1947,7 @@ namespace polysat {
* Values of x1, y1, q1 have to be available for the rule to apply. * Values of x1, y1, q1 have to be available for the rule to apply.
* If not all values are present, the rule isn't going to be used. * If not all values are present, the rule isn't going to be used.
* The arithmetic solver uses complete assignments because it * The arithmetic solver uses complete assignments because it
* builds on top of an integer feasiable state (or feasible over rationals) * builds on top of an integer feasible state (or feasible over rationals)
* Lemmas are false under that assignment. They don't necessarily propagate, though. * Lemmas are false under that assignment. They don't necessarily propagate, though.
* PolySAT isn't (yet) set up to work with complete assignments and thereforce misses such lemmas. * PolySAT isn't (yet) set up to work with complete assignments and thereforce misses such lemmas.
* - should we force complete assignments by computing first a model that is feasible modulo linear constraints * - should we force complete assignments by computing first a model that is feasible modulo linear constraints