mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

use phase

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-07 19:50:45 -08:00
parent b3ebce3966
commit a8335f2d5e
2 changed files with 8 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/sat/smt/euf_local_search.cpp
View file

@ -22,8 +22,6 @@ Author:
namespace euf { namespace euf {
void solver::local_search(bool_vector& phase) { void solver::local_search(bool_vector& phase) {
scoped_limits scoped_rl(m.limit()); scoped_limits scoped_rl(m.limit());
sat::ddfw bool_search; sat::ddfw bool_search;
bool_search.add(s()); bool_search.add(s());
@ -31,23 +29,17 @@ namespace euf {
bool_search.set_seed(rand()); bool_search.set_seed(rand());
scoped_rl.push_child(&(bool_search.rlimit())); scoped_rl.push_child(&(bool_search.rlimit()));
unsigned rounds = 0;
unsigned max_rounds = 30; unsigned max_rounds = 30;
sat::model mdl(s().num_vars()); for (unsigned rounds = 0; m.inc() && rounds < max_rounds; ++rounds) {
for (unsigned v = 0; v < s().num_vars(); ++v) setup_bounds(phase);
mdl[v] = s().value(v);
while (m.inc() && rounds < max_rounds) {
setup_bounds(mdl);
bool_search.reinit(s(), phase); bool_search.reinit(s(), phase);
// Non-boolean literals are assumptions to Boolean search // Non-boolean literals are assumptions to Boolean search
literal_vector _lits; literal_vector _lits;
for (unsigned v = 0; v < mdl.size(); ++v) for (unsigned v = 0; v < phase.size(); ++v)
if (!is_propositional(literal(v))) if (!is_propositional(literal(v)))
_lits.push_back(literal(v, mdl[v] == l_false)); _lits.push_back(literal(v, !phase[v]));
bool_search.rlimit().push(m_max_bool_steps); bool_search.rlimit().push(m_max_bool_steps);
@ -60,7 +52,6 @@ namespace euf {
for (auto* th : m_solvers) for (auto* th : m_solvers)
th->local_search(phase); th->local_search(phase);
++rounds;
// if is_sat break; // if is_sat break;
} }
@ -68,14 +59,10 @@ namespace euf {
bool solver::is_propositional(sat::literal lit) { bool solver::is_propositional(sat::literal lit) {
expr* e = m_bool_var2expr.get(lit.var(), nullptr); expr* e = m_bool_var2expr.get(lit.var(), nullptr);
if (!e) return !e || is_uninterp_const(e) || !m_egraph.find(e);
return true;
if (is_uninterp_const(e))
return true;
return !m_egraph.find(e);
} }
void solver::setup_bounds(sat::model const& mdl) { void solver::setup_bounds(bool_vector const& phase) {
unsigned num_literals = 0; unsigned num_literals = 0;
unsigned num_bool = 0; unsigned num_bool = 0;
for (auto* th : m_solvers) for (auto* th : m_solvers)
@ -95,7 +82,7 @@ namespace euf {
}; };
auto is_true = [&](auto lit) { auto is_true = [&](auto lit) {
return mdl[lit.var()] == to_lbool(!lit.sign()); return phase[lit.var()] == !lit.sign();
}; };
svector<sat::solver::bin_clause> bin_clauses; svector<sat::solver::bin_clause> bin_clauses;

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

@ -265,7 +265,7 @@ namespace euf {
// local search // local search
unsigned m_max_bool_steps = 10; unsigned m_max_bool_steps = 10;
bool is_propositional(sat::literal lit); bool is_propositional(sat::literal lit);
void setup_bounds(sat::model const& mdl); void setup_bounds(bool_vector const& mdl);
// user propagator // user propagator
void check_for_user_propagator() { void check_for_user_propagator() {