mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix eval justifications

Browse source
This commit is contained in:
Jakob Rath 2023-03-15 11:33:20 +01:00
parent 5eb9fb2eb1
commit 03a6d74c58
3 changed files with 26 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -380,8 +380,9 @@ namespace polysat {
#endif
if (!has_decision) {
unsigned const eval_idx = s.m_search.get_bool_index(lit);
for (pvar v : c->vars()) {
if (s.is_assigned(v) && s.get_level(v) <= lvl) {
if (s.is_assigned(v) && s.m_search.get_pvar_index(v) <= eval_idx) {
m_vars.insert(v);
// TODO - figure out what to do with constraints from conflict lemma that disappear here.
// if (s.m_bvars.is_false(lit))

18
src/math/polysat/search_state.cpp
View file

@ -101,15 +101,27 @@ namespace polysat {
return false;
}
void search_state::push_assignment(pvar p, rational const& r) {
m_items.push_back(search_item::assignment(p));
m_assignment.push(p, r);
void search_state::push_assignment(pvar v, rational const& r) {
m_pvar_to_idx.setx(v, m_items.size(), UINT_MAX);
m_items.push_back(search_item::assignment(v));
m_assignment.push(v, r);
}
void search_state::push_boolean(sat::literal lit) {
m_bool_to_idx.setx(lit.var(), m_items.size(), UINT_MAX);
m_items.push_back(search_item::boolean(lit));
}
unsigned search_state::get_pvar_index(pvar v) const {
SASSERT(s.is_assigned(v));
return m_pvar_to_idx[v];
}
unsigned search_state::get_bool_index(sat::bool_var var) const {
SASSERT(s.m_bvars.is_assigned(var));
return m_bool_to_idx[var];
}
void search_state::pop() {
auto const& item = m_items.back();
if (item.is_assignment()) {

10
src/math/polysat/search_state.h
View file

@ -51,6 +51,10 @@ namespace polysat {
vector<search_item> m_items;
assignment m_assignment;
// store index into m_items
unsigned_vector m_pvar_to_idx;
unsigned_vector m_bool_to_idx;
bool value(pvar v, rational& r) const;
public:
@ -67,10 +71,14 @@ namespace polysat {
// (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop)
substitution const& unresolved_assignment(unsigned sz) const;
void push_assignment(pvar p, rational const& r);
void push_assignment(pvar v, rational const& r);
void push_boolean(sat::literal lit);
void pop();
unsigned get_pvar_index(pvar v) const;
unsigned get_bool_index(sat::bool_var var) const;
unsigned get_bool_index(sat::literal lit) const { return get_bool_index(lit.var()); }
void set_resolved(unsigned i) { m_items[i].set_resolved(); }
using const_iterator = decltype(m_items)::const_iterator;