mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

track pvar_kind

Browse source
This commit is contained in:
Jakob Rath 2023-08-04 10:12:50 +02:00
parent 63e81e2bb0
commit d62aa82762
7 changed files with 32 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -401,8 +401,8 @@ namespace polysat {
if (it != m_dedup.m_quot_rem_expr.end())
return { m.mk_var(it->m_value.first), m.mk_var(it->m_value.second) };
pdd q = m.mk_var(s.add_var(sz)); // quotient
pdd r = m.mk_var(s.add_var(sz)); // remainder
pdd q = m.mk_var(s.add_var(sz, pvar_kind::internal)); // quotient
pdd r = m.mk_var(s.add_var(sz, pvar_kind::internal)); // remainder
m_dedup.m_quot_rem_expr.insert(args, { q.var(), r.var() });
m_dedup.m_div_rem_list.push_back({ a, b, q.var(), r.var() });
@ -467,7 +467,7 @@ namespace polysat {
if (it != m_dedup.op_constraint_expr.end())
return m.mk_var(it->m_value);
pdd r = m.mk_var(s.add_var(sz));
pdd r = m.mk_var(s.add_var(sz, pvar_kind::op));
m_dedup.op_constraint_expr.insert(args, r.var());
signed_constraint c = mk_op_constraint(op, p, q, r);
@ -644,7 +644,7 @@ namespace polysat {
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
if (it != m_dedup.m_bv_ext_expr.end())
return s.var(it->m_value);
pvar const v = s.add_var(v_sz);
pvar const v = s.add_var(v_sz, pvar_kind::internal);
pdd const V = s.var(v);
m_dedup.m_bv_ext_expr.insert(args, v);
// (1) v[|p|-1:0] = p
@ -665,7 +665,7 @@ namespace polysat {
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
if (it != m_dedup.m_bv_ext_expr.end())
return s.var(it->m_value);
pdd const v = s.var(s.add_var(v_sz));
pdd const v = s.var(s.add_var(v_sz, pvar_kind::internal));
m_dedup.m_bv_ext_expr.insert(args, v.var());
// (1) v[|p|-1:0] = p
s.add_eq(q, extract(v, p_sz - 1, 0));

3
src/math/polysat/naming.cpp
View file

@ -40,6 +40,7 @@ namespace polysat {
SASSERT(!m_names.contains(key));
m_names.insert(key, v);
m_terms[v] = t;
LOG("set_name v" << v << " := " << t);
}
pvar name_manager::get_name(pdd const& t) const {
@ -57,7 +58,7 @@ namespace polysat {
pvar v = get_name(t);
if (v != null_var)
return v;
v = s.add_var(t.power_of_2());
v = s.add_var(t.power_of_2(), pvar_kind::name);
s.add_eq(s.var(v), t);
set_name(v, t);
return v;

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

@ -943,7 +943,7 @@ namespace polysat {
}
// allocate new variable if we cannot reuse it
if (v == null_var) {
v = m_solver.add_var(hi - lo + 1);
v = m_solver.add_var(hi - lo + 1, pvar_kind::internal);
#if 1
// slice didn't have a variable yet; so we can re-use it for the new variable
// (we end up with a "phantom" enode that was first created for the variable)
@ -984,6 +984,7 @@ namespace polysat {
m_extract_dedup.insert(args, v);
m_extract_trail.push_back(args);
m_trail.push_back(trail_item::mk_extract);
LOG("mk_extract: v" << src << "[" << hi << ":" << lo << "] = v" << v);
return v;
}
@ -1020,7 +1021,7 @@ namespace polysat {
v = replay_var;
}
else
v = m_solver.add_var(total_width);
v = m_solver.add_var(total_width, pvar_kind::internal);
enode* sv = var2slice(v);
VERIFY(merge(slices, sv, dep_t()));
// NOTE: add_concat_node must be done after merge to preserve the invariant: "a base slice is never equivalent to a congruence node".

15
src/math/polysat/solver.cpp
View file

@ -168,12 +168,16 @@ namespace polysat {
return sz2pdd(size(v));
}
unsigned solver::add_var(unsigned sz) {
unsigned solver::add_var(unsigned sz, pvar_kind k) {
#ifndef NDEBUG
if (m_is_solving) {
SASSERT(k != pvar_kind::external); // NOTE: if this assertion fails, most likely pvar_kind wasn't set for some internal variable.
}
#endif
pvar const v = m_value.size();
m_kind.push_back(k);
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push_var(sz);
m_viable_fallback.push_var(sz);
m_pwatch.push_back({});
m_activity.push_back(0);
m_vars.push_back(sz2pdd(sz).mk_var(v));
@ -182,6 +186,8 @@ namespace polysat {
m_free_pvars.mk_var_eh(v);
m_names.push_var(var(v)); // needs m_vars
m_slicing.add_var(sz);
m_viable.push_var(sz);
m_viable_fallback.push_var(sz);
return v;
}
@ -195,6 +201,8 @@ namespace polysat {
pvar v = m_value.size() - 1;
m_viable.pop_var();
m_viable_fallback.pop_var();
m_names.pop_var();
m_kind.pop_back();
m_value.pop_back();
m_justification.pop_back();
m_pwatch.pop_back();
@ -202,7 +210,6 @@ namespace polysat {
m_vars.pop_back();
m_size.pop_back();
m_free_pvars.del_var_eh(v);
m_names.pop_var();
}
void solver::assign_eh(signed_constraint c, dependency dep) {

4
src/math/polysat/solver.h
View file

@ -173,6 +173,7 @@ namespace polysat {
slicing m_slicing;
// Per variable information
svector<pvar_kind> m_kind;
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
vector<constraints> m_pwatch; // watch list datastructure into constraints.
@ -240,6 +241,7 @@ namespace polysat {
* Each struct is a subclass of trail and implements undo().
*/
pvar add_var(unsigned sz, pvar_kind k);
void del_var();
dd::pdd_manager& sz2pdd(unsigned sz) const;
@ -409,7 +411,7 @@ namespace polysat {
/**
* Add variable with bit-size.
*/
pvar add_var(unsigned sz);
pvar add_var(unsigned sz) { return add_var(sz, pvar_kind::external); }
/**
* Create polynomial terms

3
src/math/polysat/types.h
View file

@ -44,8 +44,7 @@ namespace polysat {
external, // regular variables (from the input formula)
name, // name for a polynomial term
op, // result of an op_constraint
extract, // result of an extract operation
concat, // result of a concat operation
internal, // other internal variable
};
class dependency {

14
src/math/polysat/variable_elimination.cpp
View file

@ -98,7 +98,7 @@ namespace polysat {
pdd power = get_dyadic_valuation(p).second;
pvar rest = s.add_var(p.power_of_2());
pvar rest = s.add_var(p.power_of_2(), pvar_kind::internal);
pdd rest_pdd = m.mk_var(rest);
m_rest_constants.setx(v, rest, -1);
s.add_clause(s.eq(power * rest_pdd, p), false);
@ -119,7 +119,7 @@ namespace polysat {
if (m_inverse_constants.size() > v && m_inverse_constants[v] != -1)
return optional<pdd>(s.var(m_inverse_constants[v]));
pvar inv = s.add_var(p.power_of_2());
pvar inv = s.add_var(p.power_of_2(), pvar_kind::internal);
pdd inv_pdd = m.mk_var(inv);
m_inverse_constants.setx(v, inv, -1);
s.add_clause(s.eq(inv_pdd * p, m.one()), false);
@ -138,8 +138,8 @@ namespace polysat {
pvar pv2;
bool new_var = false;
if (m_pv_constants.size() <= v || m_pv_constants[v] == -1) {
pv = s.add_var(m.power_of_2()); // TODO: What's a good value? Unfortunately we cannot use an integer
pv2 = s.add_var(m.power_of_2());
pv = s.add_var(m.power_of_2(), pvar_kind::internal); // TODO: What's a good value? Unfortunately we cannot use an integer
pv2 = s.add_var(m.power_of_2(), pvar_kind::internal);
m_pv_constants.setx(v, pv, -1);
m_pv_power_constants.setx(v, pv2, -1);
// [nsb cr]: why these calls to m.mk_var()?
@ -586,7 +586,7 @@ namespace polysat {
pvar p_inv = m_pseudo_inverse[v][parity];
if (p_inv == -1) {
p_inv = s.add_var(p.power_of_2());
p_inv = s.add_var(p.power_of_2(), pvar_kind::internal);
m_pseudo_inverse[v][parity] = p_inv;
// NB: Strictly speaking this condition does not say that "p_inv" is the pseudo-inverse.
// However, the variable elimination lemma stays valid even if "p_inv" is not really the pseudo-inverse anymore (e.g., because of parity was reduced)
@ -608,7 +608,7 @@ namespace polysat {
if (m_inverse.size() > v && m_inverse[v] != -1)
return s.var(m_inverse[v]);
pvar inv = s.add_var(p.power_of_2());
pvar inv = s.add_var(p.power_of_2(), pvar_kind::internal);
pdd inv_pdd = s.var(inv);
m_inverse.setx(v, inv, -1);
s.add_clause(s.eq(inv_pdd * p, p.manager().one()), false);
@ -634,7 +634,7 @@ namespace polysat {
needs_propagate = !tuple.second[parity];
}
else {
odd_v = s.add_var(p.power_of_2());
odd_v = s.add_var(p.power_of_2(), pvar_kind::internal);
verbose_stream() << "Odd part v" << odd_v << " of " << p << " introduced\n";
m_odd.setx(v, optional<std::pair<pvar, bool_vector>>({ odd_v, bool_vector(p.power_of_2(), false) }), optional<std::pair<pvar, bool_vector>>::undef());
}