mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
enable generic parameters with smt-tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
284436aa5a
commit
74ac58de2b
|
|
@ -21,6 +21,7 @@ Notes:
|
|||
#include"smt_kernel.h"
|
||||
#include"smt_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
#include"lp_params.hpp"
|
||||
#include"rewriter_types.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"ast_util.h"
|
||||
|
|
@ -64,6 +65,10 @@ public:
|
|||
return m_params;
|
||||
}
|
||||
|
||||
params_ref & params() {
|
||||
return m_params_ref;
|
||||
}
|
||||
|
||||
void updt_params_core(params_ref const & p) {
|
||||
m_candidate_models = p.get_bool("candidate_models", false);
|
||||
m_fail_if_inconclusive = p.get_bool("fail_if_inconclusive", true);
|
||||
|
|
@ -73,6 +78,7 @@ public:
|
|||
TRACE("smt_tactic", tout << "updt_params: " << p << "\n";);
|
||||
updt_params_core(p);
|
||||
fparams().updt_params(p);
|
||||
m_params_ref.copy(p);
|
||||
m_logic = p.get_sym(symbol("logic"), m_logic);
|
||||
if (m_logic != symbol::null && m_ctx) {
|
||||
m_ctx->set_logic(m_logic);
|
||||
|
|
@ -84,6 +90,7 @@ public:
|
|||
r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete.");
|
||||
r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal.");
|
||||
smt_params_helper::collect_param_descrs(r);
|
||||
lp_params::collect_param_descrs(r);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -112,10 +119,12 @@ public:
|
|||
struct scoped_init_ctx {
|
||||
smt_tactic & m_owner;
|
||||
smt_params m_params; // smt-setup overwrites parameters depending on the current assertions.
|
||||
params_ref m_params_ref;
|
||||
|
||||
scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
|
||||
m_params = o.fparams();
|
||||
smt::kernel * new_ctx = alloc(smt::kernel, m, m_params);
|
||||
m_params_ref = o.params();
|
||||
smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref);
|
||||
TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
|
||||
new_ctx->set_logic(o.m_logic);
|
||||
if (o.m_callback) {
|
||||
|
|
|
|||
|
|
@ -143,7 +143,6 @@ namespace smt {
|
|||
theory_lra& th;
|
||||
ast_manager& m;
|
||||
theory_arith_params& m_arith_params;
|
||||
lp_params m_lp_params; // seeded from global parameters.
|
||||
arith_util a;
|
||||
|
||||
arith_eq_adapter m_arith_eq_adapter;
|
||||
|
|
@ -282,14 +281,16 @@ namespace smt {
|
|||
expr* get_owner(theory_var v) const { return get_enode(v)->get_owner(); }
|
||||
|
||||
void init_solver() {
|
||||
if (m_solver) return;
|
||||
lp_params lp(ctx().get_params());
|
||||
m_solver = alloc(lean::lar_solver);
|
||||
m_theory_var2var_index.reset();
|
||||
m_solver->settings().set_resource_limit(m_resource_limit);
|
||||
m_solver->settings().simplex_strategy() = static_cast<lean::simplex_strategy_enum>(m_lp_params.simplex_strategy());
|
||||
m_solver->settings().presolve_with_double_solver_for_lar = m_lp_params.presolve_with_dbl();
|
||||
m_solver->settings().simplex_strategy() = static_cast<lean::simplex_strategy_enum>(lp.simplex_strategy());
|
||||
m_solver->settings().presolve_with_double_solver_for_lar = lp.presolve_with_dbl();
|
||||
reset_variable_values();
|
||||
m_solver->settings().bound_propagation() = BP_NONE != propagation_mode();
|
||||
m_solver->set_propagate_bounds_on_pivoted_rows_mode(m_lp_params.bprop_on_pivoted_rows());
|
||||
m_solver->set_propagate_bounds_on_pivoted_rows_mode(lp.bprop_on_pivoted_rows());
|
||||
//m_solver->settings().set_ostream(0);
|
||||
}
|
||||
|
||||
|
|
@ -646,9 +647,11 @@ namespace smt {
|
|||
|
||||
|
||||
public:
|
||||
imp(theory_lra& th, ast_manager& m, theory_arith_params& p):
|
||||
th(th), m(m), m_arith_params(p), a(m),
|
||||
m_arith_eq_adapter(th, p, a),
|
||||
imp(theory_lra& th, ast_manager& m, theory_arith_params& ap):
|
||||
th(th), m(m),
|
||||
m_arith_params(ap),
|
||||
a(m),
|
||||
m_arith_eq_adapter(th, ap, a),
|
||||
m_internalize_head(0),
|
||||
m_delay_constraints(false),
|
||||
m_delayed_terms(m),
|
||||
|
|
@ -656,15 +659,19 @@ namespace smt {
|
|||
m_asserted_qhead(0),
|
||||
m_assume_eq_head(0),
|
||||
m_num_conflicts(0),
|
||||
m_solver(0),
|
||||
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
|
||||
m_resource_limit(*this) {
|
||||
init_solver();
|
||||
}
|
||||
|
||||
~imp() {
|
||||
del_bounds(0);
|
||||
std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc<internalize_state>());
|
||||
}
|
||||
|
||||
void init(context* ctx) {
|
||||
init_solver();
|
||||
}
|
||||
|
||||
bool internalize_atom(app * atom, bool gate_ctx) {
|
||||
if (m_delay_constraints) {
|
||||
|
|
@ -2008,7 +2015,7 @@ namespace smt {
|
|||
|
||||
bool proofs_enabled() const { return m.proofs_enabled(); }
|
||||
|
||||
bool use_tableau() const { return m_lp_params.simplex_strategy() < 2; }
|
||||
bool use_tableau() const { return lp_params(ctx().get_params()).simplex_strategy() < 2; }
|
||||
|
||||
void set_upper_bound(lean::var_index vi, lean::constraint_index ci, rational const& v) { set_bound(vi, ci, v, false); }
|
||||
|
||||
|
|
@ -2517,9 +2524,9 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
theory_lra::theory_lra(ast_manager& m, theory_arith_params& p):
|
||||
theory_lra::theory_lra(ast_manager& m, theory_arith_params& ap):
|
||||
theory(m.get_family_id("arith")) {
|
||||
m_imp = alloc(imp, *this, m, p);
|
||||
m_imp = alloc(imp, *this, m, ap);
|
||||
}
|
||||
theory_lra::~theory_lra() {
|
||||
dealloc(m_imp);
|
||||
|
|
@ -2529,6 +2536,7 @@ namespace smt {
|
|||
}
|
||||
void theory_lra::init(context * ctx) {
|
||||
theory::init(ctx);
|
||||
m_imp->init(ctx);
|
||||
}
|
||||
bool theory_lra::internalize_atom(app * atom, bool gate_ctx) {
|
||||
return m_imp->internalize_atom(atom, gate_ctx);
|
||||
|
|
|
|||
|
|
@ -26,8 +26,9 @@ namespace smt {
|
|||
class theory_lra : public theory, public theory_opt {
|
||||
class imp;
|
||||
imp* m_imp;
|
||||
|
||||
public:
|
||||
theory_lra(ast_manager& m, theory_arith_params& params);
|
||||
theory_lra(ast_manager& m, theory_arith_params& ap);
|
||||
virtual ~theory_lra();
|
||||
virtual theory* mk_fresh(context* new_ctx);
|
||||
virtual char const* get_name() const { return "lra"; }
|
||||
|
|
|
|||
|
|
@ -423,7 +423,7 @@ public:
|
|||
|
||||
void find_feasible_solution();
|
||||
|
||||
bool is_tiny() const {return this->m_m < 10 && this->m_n < 20;}
|
||||
// bool is_tiny() const {return this->m_m < 10 && this->m_n < 20;}
|
||||
|
||||
void one_iteration();
|
||||
void one_iteration_tableau();
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@
|
|||
#include "util/lp/lp_primal_core_solver.hpp"
|
||||
#include "util/lp/lp_primal_core_solver_tableau.hpp"
|
||||
namespace lean {
|
||||
|
||||
template void lp_primal_core_solver<double, double>::find_feasible_solution();
|
||||
template void lean::lp_primal_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::find_feasible_solution();
|
||||
|
||||
|
|
@ -22,4 +23,5 @@ template void lean::lp_primal_core_solver<double, double>::clear_breakpoints();
|
|||
template bool lean::lp_primal_core_solver<lean::mpq, lean::mpq>::update_basis_and_x_tableau(int, int, lean::mpq const&);
|
||||
template bool lean::lp_primal_core_solver<double, double>::update_basis_and_x_tableau(int, int, double const&);
|
||||
template bool lean::lp_primal_core_solver<lean::mpq, lean::numeric_pair<lean::mpq> >::update_basis_and_x_tableau(int, int, lean::numeric_pair<lean::mpq> const&);
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue