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

fix missing propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-14 13:10:35 -08:00
parent 05d61ed090
commit ff637a3989
4 changed files with 23 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -369,6 +369,9 @@ namespace polysat {
s.set_conflict(deps, "non-viable assignment");
return;
}
s.propagate_eq(v, value, dep);
if (s.inconsistent())
return;
m_values[v] = value;
m_justification[v] = dep;
m_assignment.push(v , value);

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

@ -141,6 +141,7 @@ namespace polysat {
virtual void set_conflict(dependency_vector const& core, char const* hint) = 0;
virtual dependency propagate(signed_constraint sc, dependency_vector const& deps, char const* hint) = 0;
virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint) = 0;
virtual void propagate_eq(pvar v, rational const& val, dependency const& d) = 0;
virtual trail_stack& trail() = 0;
virtual bool inconsistent() const = 0;
virtual void get_bitvector_suffixes(pvar v, offset_slices& out) = 0;

18
src/sat/smt/polysat_solver.cpp
View file

@ -268,6 +268,24 @@ namespace polysat {
return dependency(lit.var());
}
void solver::propagate_eq(pvar pv, rational const& val, dependency const& d) {
auto v = m_pddvar2var[pv];
auto a = var2enode(v);
auto bval = bv.mk_numeral(val, get_bv_size(v));
ctx.internalize(bval);
auto b = ctx.get_enode(bval);
if (a->get_root() == b->get_root())
return;
proof_hint* hint = nullptr;
sat::literal_vector core;
euf::enode_pair_vector eqs;
explain_dep(d, eqs, core);
if (ctx.use_drat())
hint = mk_proof_hint("propagate-eq", core, eqs);
auto exp = euf::th_explain::propagate(*this, core, eqs, a, b, hint);
ctx.propagate(a, b, exp);
}
unsigned solver::level(dependency const& d) {
if (d.is_bool_var())
return s().lvl(d.bool_var());

1
src/sat/smt/polysat_solver.h
View file

@ -215,6 +215,7 @@ namespace polysat {
bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) override;
dependency propagate(signed_constraint sc, dependency_vector const& deps, char const* hint) override;
void propagate(dependency const& d, bool sign, dependency_vector const& deps, char const* hint) override;
void propagate_eq(pvar v, rational const& val, dependency const& d) override;
trail_stack& trail() override;
bool inconsistent() const override;
void get_bitvector_sub_slices(pvar v, offset_slices& out) override;