diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index eef22fe06..9e3eddafa 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -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) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 12d34c516..4a602f808 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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(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(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()); } + + 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); diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h index c91363848..beb5c8387 100644 --- a/src/smt/theory_lra.h +++ b/src/smt/theory_lra.h @@ -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"; } diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h index f05f88db6..62464ca8b 100644 --- a/src/util/lp/lp_primal_core_solver.h +++ b/src/util/lp/lp_primal_core_solver.h @@ -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(); diff --git a/src/util/lp/lp_primal_core_solver_instances.cpp b/src/util/lp/lp_primal_core_solver_instances.cpp index 32364a963..ca231fd34 100644 --- a/src/util/lp/lp_primal_core_solver_instances.cpp +++ b/src/util/lp/lp_primal_core_solver_instances.cpp @@ -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::find_feasible_solution(); template void lean::lp_primal_core_solver >::find_feasible_solution(); @@ -22,4 +23,5 @@ template void lean::lp_primal_core_solver::clear_breakpoints(); template bool lean::lp_primal_core_solver::update_basis_and_x_tableau(int, int, lean::mpq const&); template bool lean::lp_primal_core_solver::update_basis_and_x_tableau(int, int, double const&); template bool lean::lp_primal_core_solver >::update_basis_and_x_tableau(int, int, lean::numeric_pair const&); + }