mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

enable sat.euf in opt, enable smt legacy for lns

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-02 06:21:14 -08:00
parent db04ccb137
commit 56478f917b
4 changed files with 38 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/maxres.cpp
View file

@ -869,7 +869,7 @@ public:
m_pivot_on_cs = p.maxres_pivot_on_correction_set();
m_wmax = p.maxres_wmax();
m_dump_benchmarks = p.dump_benchmarks();
m_enable_lns = p.enable_lns() && m_c.sat_enabled();
m_enable_lns = p.enable_lns();
m_lns_conflicts = p.lns_conflicts();
}

51
src/opt/opt_context.cpp
View file

@ -41,7 +41,7 @@ Notes:
#include "tactic/generic_model_converter.h"
#include "ackermannization/ackermannize_bv_tactic.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "qe/qsat.h"
#include "sat/sat_params.hpp"
#include "opt/opt_context.h"
#include "opt/opt_solver.h"
#include "opt/opt_params.hpp"
@ -680,20 +680,23 @@ namespace opt {
}
void context::update_solver() {
if (!m_enable_sat || !probe_bv()) {
return;
}
if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("pd-maxres") &&
m_maxsat_engine != symbol("bcd2") &&
m_maxsat_engine != symbol("sls")) {
return;
}
if (opt_params(m_params).priority() == symbol("pareto")) {
return;
}
if (m.proofs_enabled()) {
return;
sat_params p(m_params);
if (!p.euf()) {
if (!m_enable_sat || !probe_fd()) {
return;
}
if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("pd-maxres") &&
m_maxsat_engine != symbol("bcd2") &&
m_maxsat_engine != symbol("sls")) {
return;
}
if (opt_params(m_params).priority() == symbol("pareto")) {
return;
}
if (m.proofs_enabled()) {
return;
}
}
m_params.set_bool("minimize_core_partial", true);
m_params.set_bool("minimize_core", true);
@ -711,28 +714,28 @@ namespace opt {
}
}
struct context::is_bv {
struct found {};
struct context::is_fd {
struct found_fd {};
ast_manager& m;
pb_util pb;
bv_util bv;
is_bv(ast_manager& m): m(m), pb(m), bv(m) {}
void operator()(var *) { throw found(); }
void operator()(quantifier *) { throw found(); }
is_fd(ast_manager& m): m(m), pb(m), bv(m) {}
void operator()(var *) { throw found_fd(); }
void operator()(quantifier *) { throw found_fd(); }
void operator()(app *n) {
family_id fid = n->get_family_id();
if (fid != m.get_basic_family_id() &&
fid != pb.get_family_id() &&
fid != bv.get_family_id() &&
(!is_uninterp_const(n) || (!m.is_bool(n) && !bv.is_bv(n)))) {
throw found();
throw found_fd();
}
}
};
bool context::probe_bv() {
bool context::probe_fd() {
expr_fast_mark1 visited;
is_bv proc(m);
is_fd proc(m);
try {
for (objective& obj : m_objectives) {
if (obj.m_type != O_MAXSMT) return false;
@ -749,7 +752,7 @@ namespace opt {
quick_for_each_expr(proc, visited, f);
}
}
catch (const is_bv::found &) {
catch (const is_fd::found_fd &) {
return false;
}
return true;

4
src/opt/opt_context.h
View file

@ -302,8 +302,8 @@ namespace opt {
inf_eps get_upper_as_num(unsigned idx);
struct is_bv;
bool probe_bv();
struct is_fd;
bool probe_fd();
struct is_propositional_fn;
bool is_propositional(expr* e);

12
src/smt/smt_kernel.h
View file

@ -150,10 +150,14 @@ namespace smt {
*/
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
void set_phase(expr * e) { NOT_IMPLEMENTED_YET(); }
solver::phase* get_phase() { NOT_IMPLEMENTED_YET(); return nullptr; }
void set_phase(solver::phase* p) { NOT_IMPLEMENTED_YET(); }
void move_to_front(expr* e) { NOT_IMPLEMENTED_YET(); }
/**
\brief control phase selection and variable ordering.
Base implementation is a no-op.
*/
void set_phase(expr * e) { }
solver::phase* get_phase() { return nullptr; }
void set_phase(solver::phase* p) { }
void move_to_front(expr* e) { }
/**
\brief Return the model associated with the last check command.