mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

porting viable

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-08 14:50:33 -08:00
parent c11f558451
commit d14ab3d707
3 changed files with 71 additions and 327 deletions
Download patch file Download diff file Expand all files Collapse all files

276
src/sat/smt/polysat_core.cpp
View file

@ -1,276 +0,0 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
polysat_core.cpp
Abstract:
PolySAT core functionality
Author:
Nikolaj Bjorner (nbjorner) 2022-01-26
Jakob Rath 2021-04-06
Notes:
polysat::solver
- adds assignments
- calls propagation and check
polysat::core
- propagates literals
- crates case splits by value assignment (equalities)
- detects conflicts based on Literal assignmets
- adds lemmas based on projections
--*/
#include "params/bv_rewriter_params.hpp"
#include "sat/smt/polysat_solver.h"
#include "sat/smt/euf_solver.h"
namespace polysat {
class core::mk_assign_var : public trail {
pvar m_var;
core& c;
public:
mk_assign_var(pvar v, core& c) : m_var(v), c(c) {}
void undo() {
c.m_justification[m_var] = nullptr;
c.m_assignment.pop();
}
};
class core::mk_dqueue_var : public trail {
pvar m_var;
core& c;
public:
mk_dqueue_var(pvar v, core& c) : m_var(v), c(c) {}
void undo() {
c.m_var_queue.unassign_var_eh(m_var);
}
};
class core::mk_add_var : public trail {
core& c;
public:
mk_add_var(core& c) : c(c) {}
void undo() override {
c.del_var();
}
};
class core::mk_add_watch : public trail {
core& c;
unsigned m_idx;
public:
mk_add_watch(core& c, unsigned idx) : c(c), m_idx(idx) {}
void undo() override {
auto& sc = c.m_prop_queue[m_idx].first;
auto& vars = sc.vars();
if (vars.size() > 0)
c.m_watch[vars[0]].pop_back();
if (vars.size() > 1)
c.m_watch[vars[1]].pop_back();
}
};
core::core(solver& s) :
s(s),
m_viable(*this),
m_constraints(s.get_trail_stack()),
m_assignment(*this),
m_dep(s.get_region()),
m_var_queue(m_activity)
{}
pdd core::value(rational const& v, unsigned sz) {
return sz2pdd(sz).mk_val(v);
}
dd::pdd_manager& core::sz2pdd(unsigned sz) const {
m_pdd.reserve(sz + 1);
if (!m_pdd[sz])
m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
return *m_pdd[sz];
}
dd::pdd_manager& core::var2pdd(pvar v) const {
return sz2pdd(size(v));
}
pvar core::add_var(unsigned sz) {
unsigned v = m_vars.size();
m_vars.push_back(sz2pdd(sz).mk_var(v));
m_activity.push_back({ sz, 0 });
m_justification.push_back(nullptr);
m_watch.push_back({});
m_var_queue.mk_var_eh(v);
s.ctx.push(mk_add_var(*this));
return v;
}
void core::del_var() {
unsigned v = m_vars.size() - 1;
m_vars.pop_back();
m_activity.pop_back();
m_justification.pop_back();
m_watch.pop_back();
m_var_queue.del_var_eh(v);
}
// case split on unassigned variables until all are assigned values.
// create equality literal for unassigned variable.
// return new_eq if there is a new literal.
sat::check_result core::check() {
if (m_var_queue.empty())
return sat::check_result::CR_DONE;
m_var = m_var_queue.next_var();
s.ctx.push(mk_dqueue_var(m_var, *this));
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
m_unsat_core = 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());
return sat::check_result::CR_CONTINUE;
case find_t::multiple:
return sat::check_result::CR_CONTINUE;
case find_t::resource_out:
return sat::check_result::CR_GIVEUP;
}
UNREACHABLE();
return sat::check_result::CR_GIVEUP;
}
// First propagate Boolean assignment, then propagate value assignment
bool core::propagate() {
if (m_qhead == m_prop_queue.size() && m_vqhead == m_prop_queue.size())
return false;
s.ctx.push(value_trail(m_qhead));
for (; m_qhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_qhead)
propagate_constraint(m_qhead, m_prop_queue[m_qhead]);
s.ctx.push(value_trail(m_vqhead));
for (; m_vqhead < m_prop_queue.size() && !s.ctx.inconsistent(); ++m_vqhead)
propagate_value(m_vqhead, m_prop_queue[m_vqhead]);
return true;
}
void core::propagate_constraint(unsigned idx, dependent_constraint& dc) {
auto [sc, dep] = dc;
if (sc.is_eq(m_var, m_value)) {
propagate_assignment(m_var, m_value, dep);
return;
}
add_watch(idx, sc);
}
void core::add_watch(unsigned idx, signed_constraint& sc) {
auto& vars = sc.vars();
unsigned i = 0, j = 0, sz = vars.size();
for (; i < sz && j < 2; ++i)
if (!is_assigned(vars[i]))
std::swap(vars[i], vars[j++]);
if (vars.size() > 0)
add_watch(idx, vars[0]);
if (vars.size() > 1)
add_watch(idx, vars[1]);
s.ctx.push(mk_add_watch(*this, idx));
}
void core::add_watch(unsigned idx, unsigned var) {
m_watch[var].push_back(idx);
}
void core::propagate_assignment(pvar v, rational const& value, stacked_dependency* dep) {
if (is_assigned(v))
return;
if (m_var_queue.contains(v)) {
m_var_queue.del_var_eh(v);
s.ctx.push(mk_dqueue_var(v, *this));
}
m_values[v] = value;
m_justification[v] = dep;
m_assignment.push(v , value);
s.ctx.push(mk_assign_var(v, *this));
// update the watch lists for pvars
// remove constraints from m_watch[v] that have more than 2 free variables.
// for entries where there is only one free variable left add to viable set
unsigned j = 0;
for (auto idx : m_watch[v]) {
auto [sc, dep] = m_prop_queue[idx];
auto& vars = sc.vars();
if (vars[0] != v)
std::swap(vars[0], vars[1]);
SASSERT(vars[0] == v);
bool swapped = false;
for (unsigned i = vars.size(); i-- > 2; ) {
if (!is_assigned(vars[i])) {
add_watch(idx, vars[i]);
std::swap(vars[i], vars[0]);
swapped = true;
break;
}
}
if (!swapped) {
m_watch[v][j++] = idx;
}
// constraint is unitary, add to viable set
if (vars.size() >= 2 && is_assigned(vars[0]) && !is_assigned(vars[1])) {
// m_viable.add_unitary(vars[1], idx);
}
}
m_watch[v].shrink(j);
}
void core::propagate_value(unsigned idx, dependent_constraint const& dc) {
auto [sc, dep] = dc;
// check if sc evaluates to false
switch (eval(sc)) {
case l_true:
return;
case l_false:
m_unsat_core = explain_eval(dc);
propagate_unsat_core();
return;
default:
break;
}
// if sc is v == value, then check the watch list for v if they evaluate to false.
if (sc.is_eq(m_var, m_value)) {
for (auto idx : m_watch[m_var]) {
auto [sc, dep] = m_prop_queue[idx];
if (eval(sc) == l_false) {
m_unsat_core = explain_eval({ sc, dep });
propagate_unsat_core();
return;
}
}
}
throw default_exception("nyi");
}
bool core::propagate_unsat_core() {
// default is to use unsat core:
s.set_conflict(m_unsat_core);
// if core is based on viable, use s.set_lemma();
throw default_exception("nyi");
}
void core::assign_eh(signed_constraint const& sc, dependency const& dep) {
m_prop_queue.push_back({ sc, m_dep.mk_leaf(dep) });
s.ctx.push(push_back_vector(m_prop_queue));
}
}

45
src/sat/smt/polysat_types.h
View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-06
--*/
#pragma once
#include "math/dd/dd_pdd.h"
#include "util/sat_literal.h"
#include "util/dependency.h"
namespace polysat {
using pdd = dd::pdd;
using pvar = unsigned;
class dependency {
unsigned m_index;
unsigned m_level;
public:
dependency(sat::literal lit, unsigned level) : m_index(2 * lit.index()), m_level(level) {}
dependency(unsigned var_idx, unsigned level) : m_index(1 + 2 * var_idx), m_level(level) {}
bool is_literal() const { return m_index % 2 == 0; }
sat::literal literal() const { SASSERT(is_literal()); return sat::to_literal(m_index / 2); }
unsigned index() const { SASSERT(!is_literal()); return (m_index - 1) / 2; }
unsigned level() const { return m_level; }
};
using stacked_dependency = stacked_dependency_manager<dependency>::dependency;
inline std::ostream& operator<<(std::ostream& out, dependency d) {
if (d.is_literal())
return out << d.literal() << "@" << d.level();
else
return out << "v" << d.index() << "@" << d.level();
}
using dependency_vector = vector<dependency>;
}

77
src/sat/smt/polysat_viable.h
View file

@ -17,7 +17,12 @@ Author:
#pragma once
#include "util/rational.h"
#include "util/dlist.h"
#include "util/map.h"
#include "util/small_object_allocator.h"
#include "sat/smt/polysat_types.h"
#include "sat/smt/polysat_fi.h"
namespace polysat {
@ -29,26 +34,86 @@ namespace polysat {
};
class core;
class constraints;
class viable {
core& c;
public:
viable(core& c) : c(c) {}
constraints& cs;
forbidden_intervals m_forbidden_intervals;
/**
struct entry final : public dll_base<entry>, public fi_record {
/// whether the entry has been created by refinement (from constraints in 'fi_record::src')
bool refined = false;
/// whether the entry is part of the current set of intervals, or stashed away for backtracking
bool active = true;
bool valid_for_lemma = true;
pvar var = null_var;
void reset() {
// dll_base<entry>::init(this); // we never did this in alloc_entry either
fi_record::reset();
refined = false;
active = true;
valid_for_lemma = true;
var = null_var;
}
};
enum class entry_kind { unit_e, equal_e, diseq_e };
struct layer final {
entry* entries = nullptr;
unsigned bit_width = 0;
layer(unsigned bw) : bit_width(bw) {}
};
class layers final {
svector<layer> m_layers;
public:
svector<layer> const& get_layers() const { return m_layers; }
layer& ensure_layer(unsigned bit_width);
layer* get_layer(unsigned bit_width);
layer* get_layer(entry* e) { return get_layer(e->bit_width); }
layer const* get_layer(unsigned bit_width) const;
layer const* get_layer(entry* e) const { return get_layer(e->bit_width); }
entry* get_entries(unsigned bit_width) const { layer const* l = get_layer(bit_width); return l ? l->entries : nullptr; }
};
ptr_vector<entry> m_alloc;
vector<layers> m_units; // set of viable values based on unit multipliers, layered by bit-width in descending order
ptr_vector<entry> m_equal_lin; // entries that have non-unit multipliers, but are equal
ptr_vector<entry> m_diseq_lin; // entries that have distinct non-zero multipliers
entry* alloc_entry(pvar v);
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
void log();
void log(pvar v);
void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
void intersect(pvar v, entry* e);
public:
viable(core& c);
~viable();
/**
* Find a next viable value for variable.
*/
find_t find_viable(pvar v, rational& out_val) { throw default_exception("nyi"); }
find_t find_viable(pvar v, rational& out_val);
/*
* Explain why the current variable is not viable or signleton.
*/
dependency_vector explain() { throw default_exception("nyi"); }
dependency_vector explain();
/*
* Register constraint at index 'idx' as unitary in v.
*/
void add_unitary(pvar v, unsigned idx) { throw default_exception("nyi"); }
void add_unitary(pvar v, unsigned idx);
};