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

find_op_by_result_var

Browse source
This commit is contained in:
Jakob Rath 2023-03-12 16:14:12 +01:00
parent 9a061d8f4a
commit be72a37440
2 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -431,6 +431,13 @@ namespace polysat {
return { dedup_find(&tmp), true };
}
signed_constraint constraint_manager::find_op_by_result_var(pvar r) const {
auto it = m_dedup.op_constraint_by_result_var.find_iterator(r);
if (it == m_dedup.op_constraint_by_result_var.end())
return {};
return it->m_value;
}
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();
@ -443,7 +450,11 @@ namespace polysat {
pdd r = m.mk_var(s.add_var(sz));
m_dedup.op_constraint_expr.insert(args, r.var());
s.add_clause(mk_op_constraint(op, p, q, r), false);
signed_constraint c = mk_op_constraint(op, p, q, r);
SASSERT(!m_dedup.op_constraint_by_result_var.contains(r.var()));
m_dedup.op_constraint_by_result_var.insert(r.var(), c);
s.add_clause(c, false);
return r;
}

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

@ -29,6 +29,7 @@ namespace polysat {
using op_constraint_args_hash = obj_hash<op_constraint_args>;
using op_constraint_expr_map = map<op_constraint_args, pvar, op_constraint_args_hash, op_constraint_args_eq>;
op_constraint_expr_map op_constraint_expr;
u_map<signed_constraint> op_constraint_by_result_var;
using quot_rem_args = std::optional<std::pair<pdd, pdd>>; // NOTE: this is only wrapped in optional because table2map requires a default constructor
using quot_rem_args_eq = default_eq<quot_rem_args>;
@ -111,6 +112,7 @@ namespace polysat {
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_by_result_var(pvar r) const;
signed_constraint find_op_pseudo_inv(pdd const& p) const;
signed_constraint eq(pdd const& p);