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

find_op

Browse source
This commit is contained in:
Jakob Rath 2023-03-12 15:59:44 +01:00
parent 9f7c9dfb17
commit 9a061d8f4a
2 changed files with 25 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -417,6 +417,20 @@ namespace polysat {
return -p - 1;
}
signed_constraint constraint_manager::find_op(op_constraint::code op, pdd const& p, pdd const& q) const {
auto& m = p.manager();
unsigned sz = m.power_of_2();
op_constraint_args const args(op, p, q);
auto it = m_dedup.op_constraint_expr.find_iterator(args);
if (it == m_dedup.op_constraint_expr.end())
return {};
pdd r = m.mk_var(it->m_value);
op_constraint tmp(op, p, q, r); // TODO: this still allocates op_constraint::m_vars
return { dedup_find(&tmp), true };
}
pdd constraint_manager::mk_op_term(op_constraint::code op, pdd const& p, pdd const& q) {
auto& m = p.manager();
unsigned sz = m.power_of_2();
@ -516,14 +530,18 @@ namespace polysat {
pdd constraint_manager::bxnor(pdd const& p, pdd const& q) {
return bnot(bxor(p, q));
}
pdd constraint_manager::pseudo_inv(pdd const& p) {
auto& m = p.manager();
if (p.is_val())
return m.mk_val(p.val().pseudo_inverse(m.power_of_2()));
return mk_op_term(op_constraint::code::inv_op, p, m.zero());
}
signed_constraint constraint_manager::find_op_pseudo_inv(pdd const& p) const {
return find_op(op_constraint::code::inv_op, p, p.manager().zero());
}
pdd constraint_manager::udiv(pdd const& p, pdd const& q) {
return div_rem_op_constraint(p, q).first;
}

6
src/math/polysat/constraint_manager.h
View file

@ -107,7 +107,11 @@ namespace polysat {
/** Find constraint p == 0; returns null if it doesn't exist yet */
signed_constraint find_eq(pdd const& p) const;
signed_constraint find_ule(pdd const& a, pdd const& b) const;
/** Find constraint p <= q; returns null if it doesn't exist yet */
signed_constraint find_ule(pdd const& p, pdd const& q) const;
/** Find op_constraint; returns null if it doesn't exist yet */
signed_constraint find_op(op_constraint::code op, pdd const& p, pdd const& q) const;
signed_constraint find_op_pseudo_inv(pdd const& p) const;
signed_constraint eq(pdd const& p);
signed_constraint ule(pdd const& a, pdd const& b);