mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

Missing file

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-01 15:10:47 +01:00
parent fe164c843d
commit 4648c35a35
2 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -373,13 +373,14 @@ namespace polysat {
} }
#endif #endif
constraint_dedup::quot_rem_args args({a, b}); constraint_dedup::quot_rem_args args({a, b});
auto it = m_dedup.quot_rem_expr.find_iterator(args); auto it = m_dedup.m_quot_rem_expr.find_iterator(args);
if (it != m_dedup.quot_rem_expr.end()) if (it != m_dedup.m_quot_rem_expr.end())
return { m.mk_var(it->m_value.first), m.mk_var(it->m_value.second) }; 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 q = m.mk_var(s.add_var(sz)); // quotient
pdd r = m.mk_var(s.add_var(sz)); // remainder pdd r = m.mk_var(s.add_var(sz)); // remainder
m_dedup.quot_rem_expr.insert(args, { q.var(), r.var() }); 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() });
// Axioms for quotient/remainder: // Axioms for quotient/remainder:
// a = b*q + r // a = b*q + r

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

@ -38,7 +38,8 @@ namespace polysat {
} }
}; };
using quot_rem_expr_map = map<quot_rem_args, std::pair<pvar, pvar>, quot_rem_args_hash, quot_rem_args_eq>; using quot_rem_expr_map = map<quot_rem_args, std::pair<pvar, pvar>, quot_rem_args_hash, quot_rem_args_eq>;
quot_rem_expr_map quot_rem_expr; quot_rem_expr_map m_quot_rem_expr;
vector<std::tuple<pdd, pdd, pvar, pvar>> m_div_rem_list;
}; };
// Manage constraint lifetime, deduplication, and connection to boolean variables/literals. // Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
@ -131,6 +132,9 @@ namespace polysat {
constraint* const* begin() const { return m_constraints.data(); } constraint* const* begin() const { return m_constraints.data(); }
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); } constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }
std::tuple<pdd, pdd, pvar, pvar> const* begin_div() const { return m_dedup.m_div_rem_list.data(); }
std::tuple<pdd, pdd, pvar, pvar> const* end_div() const { return m_dedup.m_div_rem_list.data() + m_dedup.m_div_rem_list.size(); }
class clause_iterator { class clause_iterator {
friend class constraint_manager; friend class constraint_manager;
using storage_t = decltype(constraint_manager::m_clauses); using storage_t = decltype(constraint_manager::m_clauses);