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

track refinement source

Browse source
This commit is contained in:
Jakob Rath 2022-12-15 13:08:13 +01:00
parent e978e4fc8e
commit 3d06a90e7f
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/viable.cpp
View file

@ -70,6 +70,7 @@ namespace polysat {
auto* e = m_alloc.back();
e->side_cond.reset();
e->coeff = 1;
e->refined = nullptr;
m_alloc.pop_back();
return e;
}
@ -348,6 +349,7 @@ namespace polysat {
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->refined = e;
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;
@ -384,6 +386,7 @@ namespace polysat {
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->refined = e;
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;
@ -471,6 +474,7 @@ namespace polysat {
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->refined = e;
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;

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

@ -38,7 +38,9 @@ namespace polysat {
solver& s;
forbidden_intervals m_forbidden_intervals;
struct entry final : public dll_base<entry>, public fi_record {};
struct entry final : public dll_base<entry>, public fi_record {
entry const* refined = nullptr;
};
enum class entry_kind { unit_e, equal_e, diseq_e };
ptr_vector<entry> m_alloc;