mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

remove dual solver approach

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-03 14:08:01 -08:00
parent 1f964eea90
commit 8e3185ffe3
13 changed files with 44 additions and 537 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver.cpp
View file

@ -3009,7 +3009,7 @@ namespace sat {
svector<double> logits(vars.size(), 0.0);
double itau = m_config.m_reorder_itau;
double lse = 0;
double mid = m_rand.max_value()/2;
double mid = (double)(m_rand.max_value()/2);
double max = 0;
for (double& f : logits) {
f = itau * (m_rand() - mid)/mid;

2
src/sat/smt/CMakeLists.txt
View file

@ -21,7 +21,6 @@ z3_add_component(sat_smt
euf_invariant.cpp
euf_model.cpp
euf_proof.cpp
euf_relevancy.cpp
euf_solver.cpp
fpa_solver.cpp
pb_card.cpp
@ -38,7 +37,6 @@ z3_add_component(sat_smt
q_queue.cpp
q_solver.cpp
recfun_solver.cpp
sat_dual_solver.cpp
sat_th.cpp
smt_relevant.cpp
user_solver.cpp

4
src/sat/smt/euf_internalize.cpp
View file

@ -183,8 +183,6 @@ namespace euf {
m_egraph.set_bool_var(n, v);
if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
m_egraph.set_merge_enabled(n, false);
if (!si.is_bool_op(e))
track_relevancy(lit.var());
if (s().value(lit) != l_undef)
m_egraph.set_value(n, s().value(lit));
return lit;
@ -396,7 +394,7 @@ namespace euf {
// Remark: The inconsistency is not going to be detected if they are
// not marked as shared.
for (auto p : euf::enode_th_vars(n))
for (auto const& p : euf::enode_th_vars(n))
if (fid2solver(p.get_id())->is_shared(p.get_var()))
return true;

208
src/sat/smt/euf_relevancy.cpp
View file

@ -1,208 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_relevancy.cpp
Abstract:
Features for relevancy tracking.
A reduced (minimal) implicant is extracted by running a dual solver.
Then the literals in the implicant are used as a basis for marking
subterms relevant.
Author:
Nikolaj Bjorner (nbjorner) 2020-09-22
--*/
#include "sat/smt/euf_solver.h"
namespace euf {
void solver::mark_relevant(sat::literal lit) {
if (m_relevancy.enabled()) {
m_relevancy.mark_relevant(lit);
return;
}
if (!relevancy_enabled())
return;
for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes)
m_auto_relevant_lim.push_back(m_auto_relevant.size());
expr* e = bool_var2expr(lit.var());
m_auto_relevant.push_back(e);
}
void solver::pop_relevant(unsigned n) {
if (m_relevancy.enabled()) {
m_relevancy.pop(n);
return;
}
if (m_auto_relevant_scopes >= n) {
m_auto_relevant_scopes -= n;
return;
}
n -= m_auto_relevant_scopes;
m_auto_relevant_scopes = 0;
unsigned top = m_auto_relevant_lim.size() - n;
unsigned lim = m_auto_relevant_lim[top];
m_auto_relevant_lim.shrink(top);
m_auto_relevant.shrink(lim);
}
void solver::push_relevant() {
if (m_relevancy.enabled()) {
m_relevancy.push();
return;
}
++m_auto_relevant_scopes;
}
bool solver::is_relevant(enode* n) const {
if (m_relevancy.enabled())
return m_relevancy.is_relevant(n);
return m_relevant_expr_ids.get(n->get_expr_id(), true);
}
bool solver::is_relevant(bool_var v) const {
if (m_relevancy.enabled())
return m_relevancy.is_relevant(v);
auto* e = bool_var2enode(v);
return !e || is_relevant(e);
}
void solver::ensure_dual_solver() {
if (m_relevancy.enabled())
return;
if (m_dual_solver)
return;
m_dual_solver = alloc(sat::dual_solver, s(), s().rlimit());
for (unsigned i = s().num_user_scopes(); i-- > 0; )
m_dual_solver->push();
}
/**
* Add a root clause. Root clauses must all be satisfied by the
* final assignment. If a clause is added above search level it
* is subject to removal on backtracking. These clauses are therefore
* not tracked.
*/
void solver::add_root(unsigned n, sat::literal const* lits) {
if (m_relevancy.enabled()) {
m_relevancy.add_root(n, lits);
return;
}
if (!relevancy_enabled())
return;
ensure_dual_solver();
m_dual_solver->add_root(n, lits);
}
void solver::add_aux(unsigned n, sat::literal const* lits) {
if (m_relevancy.enabled()) {
m_relevancy.add_def(n, lits);
return;
}
if (!relevancy_enabled())
return;
ensure_dual_solver();
m_dual_solver->add_aux(n, lits);
}
void solver::track_relevancy(sat::bool_var v) {
if (m_relevancy.enabled())
return;
ensure_dual_solver();
m_dual_solver->track_relevancy(v);
}
bool solver::init_relevancy() {
if (m_relevancy.enabled())
return true;
m_relevant_expr_ids.reset();
if (!relevancy_enabled())
return true;
if (!m_dual_solver)
return true;
if (!(*m_dual_solver)())
return false;
init_relevant_expr_ids();
for (auto lit : m_dual_solver->core())
push_relevant(lit.var());
relevant_subterms();
return true;
}
void solver::push_relevant(sat::bool_var v) {
SASSERT(!m_relevancy.enabled());
expr* e = m_bool_var2expr.get(v, nullptr);
if (e)
m_relevant_todo.push_back(e);
}
bool solver::is_propagated(sat::literal lit) {
SASSERT(!m_relevancy.enabled());
return s().value(lit) == l_true && !s().get_justification(lit.var()).is_none();
}
void solver::init_relevant_expr_ids() {
SASSERT(!m_relevancy.enabled());
unsigned max_id = 0;
for (enode* n : m_egraph.nodes())
max_id = std::max(max_id, n->get_expr_id());
m_relevant_expr_ids.resize(max_id + 1, false);
m_relevant_todo.reset();
m_relevant_todo.append(m_auto_relevant);
}
void solver::relevant_subterms() {
SASSERT(!m_relevancy.enabled());
ptr_vector<expr>& todo = m_relevant_todo;
bool_vector& visited = m_relevant_visited;
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (visited.get(e->get_id(), false))
continue;
visited.setx(e->get_id(), true, false);
if (si.is_bool_op(e))
continue;
else
m_relevant_expr_ids.setx(e->get_id(), true, false);
if (!is_app(e))
continue;
expr* c = nullptr, *th = nullptr, *el = nullptr;
if (m.is_ite(e, c, th, el) && get_enode(c)) {
sat::literal lit = expr2literal(c);
todo.push_back(c);
switch (s().value(lit)) {
case l_true:
todo.push_back(th);
break;
case l_false:
todo.push_back(el);
break;
default:
todo.push_back(th);
todo.push_back(el);
break;
}
continue;
}
for (expr* arg : *to_app(e))
todo.push_back(arg);
}
for (auto * e : todo)
visited[e->get_id()] = false;
TRACE("euf",
for (enode* n : m_egraph.nodes())
if (is_relevant(n))
tout << "relevant " << n->get_expr_id() << " [r" << n->get_root_id() << "]: " << mk_bounded_pp(n->get_expr(), m) << "\n";);
}
}

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

@ -479,9 +479,6 @@ namespace euf {
if (unit_propagate())
return sat::check_result::CR_CONTINUE;
if (!init_relevancy())
give_up = true;
unsigned num_nodes = m_egraph.num_nodes();
auto apply_solver = [&](th_solver* e) {
@ -546,9 +543,7 @@ namespace euf {
for (auto* e : m_solvers)
e->push();
m_egraph.push();
if (m_dual_solver)
m_dual_solver->push();
push_relevant();
m_relevancy.push();
}
void solver::pop(unsigned n) {
@ -558,7 +553,7 @@ namespace euf {
e->pop(n);
si.pop(n);
m_egraph.pop(n);
pop_relevant(n);
m_relevancy.pop(n);
scope const & sc = m_scopes[m_scopes.size() - n];
for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) {
bool_var v = m_var_trail[i];
@ -567,8 +562,6 @@ namespace euf {
}
m_var_trail.shrink(sc.m_var_lim);
m_scopes.shrink(m_scopes.size() - n);
if (m_dual_solver)
m_dual_solver->pop(n);
SASSERT(m_egraph.num_scopes() == m_scopes.size());
TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
}
@ -741,6 +734,13 @@ namespace euf {
}
}
bool solver::is_relevant(bool_var v) const {
if (m_relevancy.enabled())
return m_relevancy.is_relevant(v);
auto* e = bool_var2enode(v);
return !e || is_relevant(e);
}
void solver::relevant_eh(euf::enode* n) {
if (m_qsolver)
m_qsolver->relevant_eh(n);

27
src/sat/smt/euf_solver.h
View file

@ -25,7 +25,6 @@ Author:
#include "sat/sat_extension.h"
#include "sat/smt/atom2bool_var.h"
#include "sat/smt/sat_th.h"
#include "sat/smt/sat_dual_solver.h"
#include "sat/smt/euf_ackerman.h"
#include "sat/smt/user_solver.h"
#include "sat/smt/smt_relevant.h"
@ -184,14 +183,11 @@ namespace euf {
void init_drat();
// relevancy
bool_vector m_relevant_expr_ids;
bool_vector m_relevant_visited;
ptr_vector<expr> m_relevant_todo;
void ensure_dual_solver();
bool init_relevancy();
void relevant_subterms();
void init_relevant_expr_ids();
void push_relevant(sat::bool_var v);
//bool_vector m_relevant_expr_ids;
//bool_vector m_relevant_visited;
//ptr_vector<expr> m_relevant_todo;
//void init_relevant_expr_ids();
//void push_relevant(sat::bool_var v);
bool is_propagated(sat::literal lit);
// invariant
void check_eqc_bool_assignment() const;
@ -376,29 +372,26 @@ namespace euf {
// relevancy
bool m_relevancy_enabled = true;
scoped_ptr<sat::dual_solver> m_dual_solver;
ptr_vector<expr> m_auto_relevant;
unsigned_vector m_auto_relevant_lim;
unsigned m_auto_relevant_scopes = 0;
bool relevancy_enabled() const { return m_relevancy_enabled && get_config().m_relevancy_lvl > 0; }
void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy_enabled = false; }
void add_root(unsigned n, sat::literal const* lits);
void add_root(unsigned n, sat::literal const* lits) { m_relevancy.add_root(n, lits); }
void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
void add_root(sat::literal lit) { add_root(1, &lit); }
void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
void add_aux(unsigned n, sat::literal const* lits);
void add_aux(unsigned n, sat::literal const* lits) { m_relevancy.add_def(n, lits); }
void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }
void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); }
void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
void track_relevancy(sat::bool_var v);
bool is_relevant(enode* n) const;
void mark_relevant(sat::literal lit) { m_relevancy.mark_relevant(lit); }
bool is_relevant(enode* n) const { return m_relevancy.is_relevant(n); }
bool is_relevant(bool_var v) const;
bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
void mark_relevant(sat::literal lit);
void pop_relevant(unsigned n);
void push_relevant();
void relevant_eh(euf::enode* n);
smt::relevancy& relevancy() { return m_relevancy; }
// model construction

189
src/sat/smt/sat_dual_solver.cpp
View file

@ -1,189 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_dual_solver.cpp
Abstract:
Solver for obtaining implicant.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "sat/smt/sat_dual_solver.h"
namespace sat {
dual_solver::dual_solver(solver& s, reslimit& l):
s(s),
m_solver(m_params, l)
{
SASSERT(!m_solver.get_config().m_drat);
m_solver.set_incremental(true);
}
void dual_solver::flush() {
while (m_num_scopes > 0) {
m_solver.user_push();
m_roots.push_scope();
m_tracked_vars.push_scope();
m_units.push_scope();
m_vars.push_scope();
--m_num_scopes;
}
}
void dual_solver::push() {
++m_num_scopes;
}
void dual_solver::pop(unsigned num_scopes) {
if (m_num_scopes >= num_scopes) {
m_num_scopes -= num_scopes;
return;
}
num_scopes -= m_num_scopes;
m_num_scopes = 0;
m_solver.user_pop(num_scopes);
unsigned old_sz = m_tracked_vars.old_size(num_scopes);
for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
m_is_tracked[m_tracked_vars[i]] = false;
old_sz = m_vars.old_size(num_scopes);
for (unsigned i = m_vars.size(); i-- > old_sz; ) {
unsigned v = m_vars[i];
unsigned w = m_ext2var[v];
m_ext2var[v] = null_bool_var;
m_var2ext[w] = null_bool_var;
}
m_vars.pop_scope(num_scopes);
m_units.pop_scope(num_scopes);
m_roots.pop_scope(num_scopes);
m_tracked_vars.pop_scope(num_scopes);
}
bool_var dual_solver::ext2var(bool_var v) {
bool_var w = m_ext2var.get(v, null_bool_var);
if (null_bool_var == w) {
w = m_solver.mk_var();
m_solver.set_external(w);
s.set_external(v);
m_ext2var.setx(v, w, null_bool_var);
m_var2ext.setx(w, v, null_bool_var);
m_vars.push_back(v);
}
return w;
}
void dual_solver::track_relevancy(bool_var w) {
flush();
bool_var v = ext2var(w);
if (!m_is_tracked.get(v, false)) {
m_is_tracked.setx(v, true, false);
m_tracked_vars.push_back(v);
}
}
literal dual_solver::ext2lit(literal lit) {
return literal(ext2var(lit.var()), lit.sign());
}
literal dual_solver::lit2ext(literal lit) {
return literal(m_var2ext[lit.var()], lit.sign());
}
void dual_solver::add_root(unsigned sz, literal const* clause) {
flush();
if (false && sz == 1) {
TRACE("dual", tout << "unit: " << clause[0] << "\n";);
m_units.push_back(clause[0]);
return;
}
literal root;
if (sz == 1)
root = ext2lit(clause[0]);
else {
root = literal(m_solver.mk_var(), false);
for (unsigned i = 0; i < sz; ++i)
m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
}
m_solver.set_external(root.var());
m_roots.push_back(~root);
TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
}
void dual_solver::add_aux(unsigned sz, literal const* clause) {
flush();
m_lits.reset();
for (unsigned i = 0; i < sz; ++i)
m_lits.push_back(ext2lit(clause[i]));
TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";);
m_solver.mk_clause(sz, m_lits.data(), status::input());
}
void dual_solver::add_assumptions() {
flush();
m_lits.reset();
for (bool_var v : m_tracked_vars)
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
for (auto lit : m_units) {
bool_var w = m_ext2var.get(lit.var(), null_bool_var);
if (w != null_bool_var)
m_lits.push_back(ext2lit(lit));
}
}
bool dual_solver::operator()() {
m_core.reset();
m_core.append(m_units);
if (m_roots.empty())
return true;
m_solver.user_push();
m_solver.add_clause(m_roots.size(), m_roots.data(), status::input());
add_assumptions();
lbool is_sat = m_solver.check(m_lits.size(), m_lits.data());
if (is_sat == l_false)
for (literal lit : m_solver.get_core())
m_core.push_back(lit2ext(lit));
if (is_sat == l_true) {
TRACE("dual", display(tout); s.display(tout););
IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
IF_VERBOSE(0, verbose_stream() << "assumptions: " << m_lits << "\n");
IF_VERBOSE(0, display(verbose_stream()); s.display(verbose_stream()););
UNREACHABLE();
return false;
}
TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
m_solver.user_pop(1);
return is_sat == l_false;
}
std::ostream& dual_solver::display(std::ostream& out) const {
for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
bool_var w = m_var2ext.get(v, null_bool_var);
if (w == null_bool_var)
continue;
lbool v1 = m_solver.value(v);
lbool v2 = s.value(w);
if (v1 == v2 || v2 == l_undef)
continue;
out << "ext: " << w << " " << v2 << "\n";
out << "int: " << v << " " << v1 << "\n";
}
literal_vector lits;
for (bool_var v : m_tracked_vars)
lits.push_back(literal(m_var2ext[v], l_false == s.value(m_var2ext[v])));
out << "tracked: " << lits << "\n";
lits.reset();
for (literal r : m_roots)
if (m_solver.value(r) == l_true)
lits.push_back(r);
out << "roots: " << lits << "\n";
m_solver.display(out);
return out;
}
}

84
src/sat/smt/sat_dual_solver.h
View file

@ -1,84 +0,0 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_dual_solver.h
Abstract:
Solver for obtaining implicant.
Based on an idea by Armin Biere to use dual propagation
for representation of negated goal.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#pragma once
#include "util/lim_vector.h"
#include "sat/sat_solver.h"
namespace sat {
class dual_solver {
class dual_params : public no_drat_params {
public:
dual_params() {
set_bool("core.minimize", false);
}
};
solver& s;
dual_params m_params;
solver m_solver;
lim_svector<literal> m_units, m_roots;
lim_svector<bool_var> m_tracked_vars;
literal_vector m_lits, m_core;
bool_var_vector m_is_tracked;
unsigned_vector m_ext2var;
unsigned_vector m_var2ext;
lim_svector<unsigned> m_vars;
unsigned m_num_scopes = 0;
void add_literal(literal lit);
bool_var ext2var(bool_var v);
bool_var var2ext(bool_var v);
literal ext2lit(literal lit);
literal lit2ext(literal lit);
void add_assumptions();
std::ostream& display(std::ostream& out) const;
void flush();
public:
dual_solver(solver& s, reslimit& l);
void push();
void pop(unsigned num_scopes);
/*
* track model relevancy for variable
*/
void track_relevancy(bool_var v);
/*
* Add a root clause from the input problem.
* At least one literal has to be satisfied in every root.
*/
void add_root(unsigned sz, literal const* clause);
/*
* Add auxiliary clauses that originate from compiling definitions.
*/
void add_aux(unsigned sz, literal const* clause);
/*
* Extract a minimized subset of relevant literals from a model for s.
*/
bool operator()();
literal_vector const& core() const { return m_core; }
};
}

6
src/sat/smt/smt_relevant.cpp
View file

@ -44,6 +44,8 @@ namespace smt {
}
void relevancy::pop(unsigned n) {
if (!m_enabled)
return;
if (n <= m_num_scopes) {
m_num_scopes -= n;
return;
@ -55,7 +57,7 @@ namespace smt {
SASSERT(n > 0);
unsigned sz = m_lim[m_lim.size() - n];
for (unsigned i = m_trail.size(); i-- > sz; ) {
auto [u, idx] = m_trail[i];
auto const& [u, idx] = m_trail[i];
switch (u) {
case update::relevant_var:
m_relevant_var_ids[idx] = false;
@ -168,7 +170,7 @@ namespace smt {
return;
m_trail.push_back(std::make_pair(update::set_qhead, m_qhead));
while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) {
auto [lit, n] = m_queue[m_qhead++];
auto const& [lit, n] = m_queue[m_qhead++];
SASSERT(n || lit != sat::null_literal);
SASSERT(!n || lit == sat::null_literal);
if (n)

2
src/sat/smt/smt_relevant.h
View file

@ -137,7 +137,7 @@ namespace smt {
public:
relevancy(euf::solver& ctx);
void push() { ++m_num_scopes; }
void push() { if (m_enabled) ++m_num_scopes; }
void pop(unsigned n);
void add_root(unsigned n, sat::literal const* lits);

8
src/sat/tactic/goal2sat.cpp
View file

@ -186,8 +186,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
return v;
v = m_solver.add_var(is_ext);
log_def(v, n);
if (top_level_relevant() && !is_bool_op(n))
ensure_euf()->track_relevancy(v);
return v;
}
@ -216,10 +214,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))
v = add_var(true, t);
m_map.insert(t, v);
if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) {
add_dual_root(sat::literal(v, m.is_false(t)));
ensure_euf()->track_relevancy(v);
}
return v;
}
@ -678,8 +672,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
if (lit == sat::null_literal)
return;
if (top_level_relevant())
euf->track_relevancy(lit.var());
if (root)
mk_root_clause(lit);
else

1
src/sat/tactic/sat_tactic.cpp
View file

@ -135,6 +135,7 @@ class sat_tactic : public tactic {
ref<sat2goal::mc> mc;
m_sat2goal(*m_solver, map, m_params, *(g.get()), mc);
g->add(mc.get());
g->display(std::cout);
if (produce_core || m_goal2sat.has_interpreted_funs()) {
// sat2goal does not preseve assumptions or assignments to interpreted atoms
g->updt_prec(goal::OVER);