mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

refactor for handling cores

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-15 16:28:59 -08:00
parent c6d3b7ec5d
commit 5098d5bbfe
5 changed files with 44 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/sat/smt/polysat/core.cpp
View file

@ -38,7 +38,7 @@ namespace polysat {
public:
mk_assign_var(pvar v, core& c) : m_var(v), c(c) {}
void undo() {
c.m_justification[m_var] = null_dependency;
c.m_justification[m_var] = constraint_id::null();
c.m_assignment.pop();
}
};
@ -123,7 +123,7 @@ namespace polysat {
unsigned v = m_vars.size();
m_vars.push_back(sz2pdd(sz).mk_var(v));
m_activity.push_back({ sz, 0 });
m_justification.push_back(null_dependency);
m_justification.push_back(constraint_id::null());
m_watch.push_back({});
m_var_queue.mk_var_eh(v);
m_viable.ensure_var(v);
@ -174,11 +174,11 @@ namespace polysat {
s.trail().push(mk_dqueue_var(m_var, *this));
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
s.set_lemma(m_viable.get_core(), m_viable.explain());
s.set_lemma(m_viable.get_core(), get_dependencies(m_viable.explain()));
// propagate_unsat_core();
return sat::check_result::CR_CONTINUE;
case find_t::singleton:
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), get_dependencies(m_viable.explain()));
return sat::check_result::CR_CONTINUE;
case find_t::multiple:
s.add_eq_literal(m_var, m_value);
@ -210,7 +210,7 @@ namespace polysat {
if (value == l_false)
sc = ~sc;
if (sc.is_eq(m_var, m_value))
propagate_assignment(m_var, m_value, dep);
propagate_assignment(m_var, m_value, idx);
else
sc.activate(*this, dep);
}
@ -219,7 +219,7 @@ namespace polysat {
m_watch[var].push_back(idx);
}
void core::propagate_assignment(pvar v, rational const& value, dependency dep) {
void core::propagate_assignment(pvar v, rational const& value, constraint_id dep) {
if (is_assigned(v))
return;
if (m_var_queue.contains(v)) {
@ -255,7 +255,7 @@ namespace polysat {
// this can create fresh literals and update m_watch, but
// will not update m_watch[v] (other than copy constructor for m_watch)
// because v has been assigned a value.
propagate(sc, value, dep);
propagate({ idx }, sc, value, dep);
if (s.inconsistent())
return;
@ -280,7 +280,7 @@ namespace polysat {
void core::propagate_value(constraint_id idx) {
auto [sc, d, value] = m_constraint_index[idx.id];
// propagate current assignment for sc
propagate(sc, value, d);
propagate(idx, sc, value, d);
if (s.inconsistent())
return;
@ -292,10 +292,10 @@ namespace polysat {
auto [sc, d, value] = m_constraint_index[idx1];
switch (eval(sc)) {
case l_false:
s.propagate(d, true, explain_eval(sc));
s.propagate(d, true, get_dependencies(explain_eval(sc)));
break;
case l_true:
s.propagate(d, false, explain_eval(sc));
s.propagate(d, false, get_dependencies(explain_eval(sc)));
break;
default:
break;
@ -304,15 +304,25 @@ namespace polysat {
}
}
void core::propagate(signed_constraint& sc, lbool value, dependency const& d) {
dependency_vector core::get_dependencies(constraint_id_vector const& cc) {
dependency_vector result;
for (auto idx : cc) {
auto [sc, d, value] = m_constraint_index[idx.id];
SASSERT(value != l_undef);
result.push_back(value == l_false ? ~d : d);
}
return result;
}
void core::propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d) {
lbool eval_value = eval(sc);
if (eval_value == l_undef)
sc.propagate(*this, value, d);
else if (value == l_undef)
s.propagate(d, eval_value != l_true, explain_eval(sc));
s.propagate(d, eval_value != l_true, get_dependencies(explain_eval(sc)));
else if (value != eval_value) {
m_unsat_core = explain_eval(sc);
m_unsat_core.push_back(value == l_false ? ~d : d);
m_unsat_core.push_back(id);
propagate_unsat_core();
}
}
@ -333,7 +343,7 @@ namespace polysat {
// default is to use unsat core:
// if core is based on viable, use s.set_lemma();
s.set_conflict(m_unsat_core);
s.set_conflict(get_dependencies(m_unsat_core));
}
void core::assign_eh(constraint_id index, bool sign, unsigned level) {
@ -352,8 +362,8 @@ namespace polysat {
s.trail().push(unassign(*this, index.id));
}
dependency_vector core::explain_eval(signed_constraint const& sc) {
dependency_vector deps;
constraint_id_vector core::explain_eval(signed_constraint const& sc) {
constraint_id_vector deps;
for (auto v : sc.vars())
if (is_assigned(v))
deps.push_back(m_justification[v]);
@ -379,7 +389,7 @@ namespace polysat {
for (auto const& [sc, d, value] : m_constraint_index)
out << sc << " " << d << " := " << value << "\n";
for (unsigned i = 0; i < m_vars.size(); ++i)
out << m_vars[i] << " := " << m_values[i] << " " << m_justification[i] << "\n";
out << m_vars[i] << " := " << m_values[i] << " " << m_constraint_index[m_justification[i].id].d << "\n";
m_var_queue.display(out << "vars ") << "\n";
return out;
}

13
src/sat/smt/polysat/core.h
View file

@ -31,6 +31,8 @@ namespace polysat {
class core;
class solver_interface;
class core {
class mk_add_var;
class mk_dqueue_var;
@ -54,13 +56,13 @@ namespace polysat {
unsigned m_qhead = 0, m_vqhead = 0;
svector<constraint_id> m_prop_queue;
svector<constraint_info> m_constraint_index; // index of constraints
dependency_vector m_unsat_core;
constraint_id_vector m_unsat_core;
// attributes associated with variables
vector<pdd> m_vars; // for each variable a pdd
vector<rational> m_values; // current value of assigned variable
svector<dependency> m_justification; // justification for assignment
svector<constraint_id> m_justification; // justification for assignment
activity m_activity; // activity of variables
var_queue<activity> m_var_queue; // priority queue of variables to assign
vector<unsigned_vector> m_watch; // watch lists for variables for constraints on m_prop_queue where they occur
@ -77,9 +79,9 @@ namespace polysat {
bool is_assigned(pvar v) { return !m_justification[v].is_null(); }
void propagate_value(constraint_id idx);
void propagate_assignment(constraint_id idx);
void propagate_assignment(pvar v, rational const& value, dependency dep);
void propagate_assignment(pvar v, rational const& value, constraint_id dep);
void propagate_unsat_core();
void propagate(signed_constraint& sc, lbool value, dependency const& d);
void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
void get_bitvector_prefixes(pvar v, pvar_vector& out);
void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits);
@ -88,7 +90,8 @@ namespace polysat {
void add_watch(unsigned idx, unsigned var);
lbool eval(signed_constraint const& sc);
dependency_vector explain_eval(signed_constraint const& sc);
constraint_id_vector explain_eval(signed_constraint const& sc);
dependency_vector get_dependencies(constraint_id_vector const& cc);
void add_axiom(signed_constraint sc);

7
src/sat/smt/polysat/types.h
View file

@ -22,7 +22,10 @@ namespace polysat {
using pdd = dd::pdd;
using pvar = unsigned;
using theory_var = unsigned;
struct constraint_id { unsigned id; };
struct constraint_id {
unsigned id; bool is_null() const { return id == UINT_MAX; }
static constraint_id null() { return constraint_id{ UINT_MAX }; }
};
using pvar_vector = unsigned_vector;
inline const pvar null_var = UINT_MAX;
@ -80,7 +83,7 @@ namespace polysat {
using dependency_vector = vector<dependency>;
using core_vector = std::initializer_list<std::variant<signed_constraint, dependency>>;
using constraint_id_vector = svector<constraint_id>;
//

6
src/sat/smt/polysat/viable.cpp
View file

@ -809,12 +809,12 @@ namespace polysat {
/*
* Explain why the current variable is not viable or signleton.
*/
dependency_vector viable::explain() {
dependency_vector result;
constraint_id_vector viable::explain() {
constraint_id_vector result;
for (auto e : m_explain) {
auto index = e->constraint_index;
auto const& [sc, d, value] = c.m_constraint_index[index];
result.push_back(d);
result.push_back({ index });
result.append(c.explain_eval(sc));
}
// TODO: explaination for fixed bits

2
src/sat/smt/polysat/viable.h
View file

@ -253,7 +253,7 @@ namespace polysat {
/*
* Explain why the current variable is not viable or signleton.
*/
dependency_vector explain();
constraint_id_vector explain();
/*
* flag whether there is a forbidden interval core