From 8412ecbdbf74e638960ba96f387866933f02760b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Mar 2021 13:57:04 -0700 Subject: [PATCH] fixes to new solver, add mode for using nlsat solver eagerly from nla_core --- scripts/mk_project.py | 2 +- src/CMakeLists.txt | 2 +- src/api/api_solver.cpp | 4 +- src/cmd_context/cmd_context.cpp | 4 +- src/math/lp/CMakeLists.txt | 1 + src/math/lp/lar_solver.cpp | 10 ++ src/math/lp/lar_solver.h | 1 + src/math/lp/lp_settings.cpp | 11 ++ src/math/lp/lp_settings.h | 151 +++++++++------------------ src/math/lp/nla_core.cpp | 44 ++++++-- src/math/lp/nla_core.h | 5 + src/params/context_params.cpp | 6 +- src/params/context_params.h | 2 +- src/sat/smt/arith_solver.cpp | 12 +-- src/sat/smt/bv_internalize.cpp | 16 ++- src/sat/smt/bv_invariant.cpp | 8 +- src/sat/smt/bv_solver.cpp | 17 --- src/sat/smt/bv_solver.h | 2 + src/sat/smt/euf_solver.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 8 +- src/smt/params/smt_params_helper.pyg | 3 +- src/smt/theory_lra.cpp | 9 +- 22 files changed, 156 insertions(+), 164 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 28413965a..6d739e4e2 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -28,6 +28,7 @@ def init_project_def(): add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') add_lib('sat', ['util', 'dd', 'grobner']) add_lib('nlsat', ['polynomial', 'sat']) + add_lib('smt_params', ['ast', 'params'], 'smt/params') add_lib('lp', ['util', 'nlsat', 'grobner', 'interval'], 'math/lp') add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter') add_lib('macros', ['rewriter'], 'ast/macros') @@ -45,7 +46,6 @@ def init_project_def(): add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa') add_lib('bit_blaster', ['rewriter', 'params'], 'ast/rewriter/bit_blaster') add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern') - add_lib('smt_params', ['ast', 'params'], 'smt/params') add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') add_lib('mbp', ['model', 'simplex'], 'qe/mbp') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a453fcb3b..e100a1f77 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -56,7 +56,6 @@ add_subdirectory(parsers/util) add_subdirectory(math/grobner) add_subdirectory(sat) add_subdirectory(nlsat) -add_subdirectory(math/lp) add_subdirectory(tactic/core) add_subdirectory(math/subpaving/tactic) add_subdirectory(tactic/aig) @@ -68,6 +67,7 @@ add_subdirectory(parsers/smt2) add_subdirectory(ast/pattern) add_subdirectory(ast/rewriter/bit_blaster) add_subdirectory(smt/params) +add_subdirectory(math/lp) add_subdirectory(qe/mbp) add_subdirectory(sat/smt) add_subdirectory(sat/tactic) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index fd8997a2c..b84970155 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -140,9 +140,9 @@ extern "C" { static void init_solver_core(Z3_context c, Z3_solver _s) { Z3_solver_ref * s = to_solver(_s); - bool proofs_enabled, models_enabled, unsat_core_enabled; + bool proofs_enabled = true, models_enabled = true, unsat_core_enabled = false; params_ref p = s->m_params; - mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); + mk_c(c)->params().get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); param_descrs r; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index e7d382953..90f7191dd 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1992,9 +1992,9 @@ void cmd_context::display_detailed_analysis(std::ostream& out, model_evaluator& } void cmd_context::mk_solver() { - bool proofs_enabled, models_enabled, unsat_core_enabled; + bool proofs_enabled = m().proofs_enabled(), models_enabled = true, unsat_core_enabled = true; params_ref p; - m_params.get_solver_params(m(), p, proofs_enabled, models_enabled, unsat_core_enabled); + m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); } diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index f40ae6038..ad21bea37 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -51,6 +51,7 @@ z3_add_component(lp util polynomial nlsat + smt_params ) include_directories(${src_SOURCE_DIR}) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index dba380010..6a799b1ff 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1,4 +1,6 @@ #include "math/lp/lar_solver.h" +#include "smt/params/smt_params_helper.hpp" + /* Copyright (c) 2017 Microsoft Corporation Author: Nikolaj Bjorner, Lev Nachmanson @@ -14,6 +16,14 @@ namespace lp { lp_settings const& lar_solver::settings() const { return m_settings; } + void lar_solver::updt_params(params_ref const& _p) { + smt_params_helper p(_p); + set_track_pivoted_rows(p.arith_bprop_on_pivoted_rows()); + set_cut_strategy(p.arith_branch_cut_ratio()); + m_settings.updt_params(_p); + } + + void clear() { lp_assert(false); // not implemented } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 36908a05d..420a41d16 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -515,6 +515,7 @@ public: unsigned column_to_reported_index(unsigned j) const; lp_settings & settings(); lp_settings const & settings() const; + void updt_params(params_ref const& p); column_type get_column_type(unsigned j) const { return m_mpq_lar_core_solver.m_column_types()[j]; } const impq & get_lower_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_lower_bounds()[j]; } const impq & get_upper_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_upper_bounds()[j]; } diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index fa5570538..ce6edcfd5 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -19,7 +19,18 @@ Revision History: --*/ #include #include "util/vector.h" +#include "smt/params/smt_params_helper.hpp" #include "math/lp/lp_settings_def.h" template bool lp::vectors_are_equal(vector const&, vector const&); template bool lp::vectors_are_equal(vector const&, vector const&); +void lp::lp_settings::updt_params(params_ref const& _p) { + smt_params_helper p(_p); + m_enable_hnf = p.arith_enable_hnf(); + m_cheap_eqs = p.arith_propagate_eqs(); + print_statistics = p.arith_print_stats(); + m_print_external_var_name = p.arith_print_ext_var_names(); + report_frequency = p.arith_rep_freq(); + m_simplex_strategy = static_cast(p.arith_simplex_strategy()); + m_nlsat_delay = p.arith_nl_delay(); +} diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 05ce8cdb8..b850be15b 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -25,9 +25,10 @@ Revision History: #include #include #include -#include "math/lp/lp_utils.h" #include "util/stopwatch.h" #include "util/statistics.h" +#include "util/params.h" +#include "math/lp/lp_utils.h" #include "math/lp/lp_types.h" namespace lp { @@ -174,141 +175,93 @@ private: random_gen m_rand; public: + void updt_params(params_ref const& p); bool enable_hnf() const { return m_enable_hnf; } - bool& enable_hnf() { return m_enable_hnf; } + unsigned nlsat_delay() const { return m_nlsat_delay; } bool int_run_gcd_test() const { return m_int_run_gcd_test; } bool& int_run_gcd_test() { return m_int_run_gcd_test; } - unsigned reps_in_scaler; + unsigned reps_in_scaler { 20 }; // when the absolute value of an element is less than pivot_epsilon // in pivoting, we treat it as a zero - double pivot_epsilon; + double pivot_epsilon { 0.00000001 }; // see Chatal, page 115 - double positive_price_epsilon; + double positive_price_epsilon { 1e-7 }; // a quotation "if some choice of the entering variable leads to an eta matrix // whose diagonal element in the eta column is less than e2 (entering_diag_epsilon) in magnitude, the this choice is rejected ... - double entering_diag_epsilon; - int c_partial_pivoting; // this is the constant c from page 410 - unsigned depth_of_rook_search; - bool using_partial_pivoting; + double entering_diag_epsilon { 1e-8 }; + int c_partial_pivoting { 10 }; // this is the constant c from page 410 + unsigned depth_of_rook_search { 4 }; + bool using_partial_pivoting { true }; // dissertation of Achim Koberstein // if Bx - b is different at any component more that refactor_epsilon then we refactor - double refactor_tolerance; - double pivot_tolerance; - double zero_tolerance; - double drop_tolerance; - double tolerance_for_artificials; - double can_be_taken_to_basis_tolerance; + double refactor_tolerance { 1e-4 }; + double pivot_tolerance { 1e-6 }; + double zero_tolerance { 1e-12 }; + double drop_tolerance { 1e-14 }; + double tolerance_for_artificials { 1e-4 }; + double can_be_taken_to_basis_tolerance { 0.00001 }; - unsigned percent_of_entering_to_check; // we try to find a profitable column in a percentage of the columns - bool use_scaling; - double scaling_maximum; - double scaling_minimum; - double harris_feasibility_tolerance; // page 179 of Istvan Maros - double ignore_epsilon_of_harris; - unsigned max_number_of_iterations_with_no_improvements; - unsigned max_total_number_of_iterations; + unsigned percent_of_entering_to_check { 5 }; // we try to find a profitable column in a percentage of the columns + bool use_scaling { true }; + double scaling_maximum { 1.0 }; + double scaling_minimum { 0.5 }; + double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros + double ignore_epsilon_of_harris { 10e-5 }; + unsigned max_number_of_iterations_with_no_improvements { 2000000 }; + unsigned max_total_number_of_iterations { 2000000 }; double time_limit; // the maximum time limit of the total run time in seconds // dual section - double dual_feasibility_tolerance; // // page 71 of the PhD thesis of Achim Koberstein - double primal_feasibility_tolerance; // page 71 of the PhD thesis of Achim Koberstein - double relative_primal_feasibility_tolerance; // page 71 of the PhD thesis of Achim Koberstein + double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein + double primal_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein + double relative_primal_feasibility_tolerance { 1e-9 }; // page 71 of the PhD thesis of Achim Koberstein // end of dual section - bool m_bound_propagation; - bool presolve_with_double_solver_for_lar; + bool m_bound_propagation { true }; + bool presolve_with_double_solver_for_lar { true }; simplex_strategy_enum m_simplex_strategy; - int report_frequency; - bool print_statistics; - unsigned column_norms_update_frequency; - bool scale_with_ratio; - double density_threshold; - bool use_breakpoints_in_feasibility_search; - unsigned max_row_length_for_bound_propagation; - bool backup_costs; - unsigned column_number_threshold_for_using_lu_in_lar_solver; - unsigned m_int_gomory_cut_period; - unsigned m_int_find_cube_period; + int report_frequency { 1000 }; + bool print_statistics { false }; + unsigned column_norms_update_frequency { 12000 }; + bool scale_with_ratio { true }; + double density_threshold { 0.7 }; + bool use_breakpoints_in_feasibility_search { false }; + unsigned max_row_length_for_bound_propagation { 300 }; + bool backup_costs { true }; + unsigned column_number_threshold_for_using_lu_in_lar_solver { 4000 }; + unsigned m_int_gomory_cut_period { 4 }; + unsigned m_int_find_cube_period { 4 }; private: - unsigned m_hnf_cut_period; - bool m_int_run_gcd_test; + unsigned m_hnf_cut_period { 4 }; + bool m_int_run_gcd_test { true }; public: - unsigned limit_on_rows_for_hnf_cutter; - unsigned limit_on_columns_for_hnf_cutter; + unsigned limit_on_rows_for_hnf_cutter { 75 }; + unsigned limit_on_columns_for_hnf_cutter { 150 }; private: - bool m_enable_hnf; - bool m_print_external_var_name; - bool m_cheap_eqs; + unsigned m_nlsat_delay; + bool m_enable_hnf { true }; + bool m_print_external_var_name { false }; + bool m_cheap_eqs { false }; public: bool print_external_var_name() const { return m_print_external_var_name; } - bool& print_external_var_name() { return m_print_external_var_name; } bool cheap_eqs() const { return m_cheap_eqs;} - bool& cheap_eqs() { return m_cheap_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; } void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; } unsigned random_next() { return m_rand(); } void set_random_seed(unsigned s) { m_rand.set_seed(s); } - bool bound_progation() const { + bool bound_progation() const { return m_bound_propagation; } - bool& bound_propagation() { - return m_bound_propagation; - } + bool& bound_propagation() { return m_bound_propagation; } lp_settings() : m_default_resource_limit(*this), m_resource_limit(&m_default_resource_limit), m_debug_out(&std::cout), m_message_out(&std::cout), - reps_in_scaler(20), - pivot_epsilon(0.00000001), - positive_price_epsilon(1e-7), - entering_diag_epsilon (1e-8), - c_partial_pivoting (10), // this is the constant c from page 410 - depth_of_rook_search (4), - using_partial_pivoting (true), - // dissertation of Achim Koberstein - // if Bx - b is different at any component more that refactor_epsilon then we refactor - refactor_tolerance ( 1e-4), - pivot_tolerance ( 1e-6), - zero_tolerance ( 1e-12), - drop_tolerance ( 1e-14), - tolerance_for_artificials ( 1e-4), - can_be_taken_to_basis_tolerance ( 0.00001), - percent_of_entering_to_check ( 5),// we try to find a profitable column in a percentage of the columns - use_scaling ( true), - scaling_maximum ( 1), - scaling_minimum ( 0.5), - harris_feasibility_tolerance ( 1e-7), // page 179 of Istvan Maros - ignore_epsilon_of_harris ( 10e-5), - max_number_of_iterations_with_no_improvements ( 2000000), - max_total_number_of_iterations ( 20000000), time_limit ( std::numeric_limits::max()), // the maximum time limit of the total run time in seconds // dual section - dual_feasibility_tolerance ( 1e-7), // // page 71 of the PhD thesis of Achim Koberstein - primal_feasibility_tolerance ( 1e-7), // page 71 of the PhD thesis of Achim Koberstein - relative_primal_feasibility_tolerance ( 1e-9), // page 71 of the PhD thesis of Achim Koberstein - m_bound_propagation ( true), - presolve_with_double_solver_for_lar(true), - m_simplex_strategy(simplex_strategy_enum::tableau_rows), - report_frequency(1000), - print_statistics(false), - column_norms_update_frequency(12000), - scale_with_ratio(true), - density_threshold(0.7), - use_breakpoints_in_feasibility_search(false), - max_row_length_for_bound_propagation(300), - backup_costs(true), - column_number_threshold_for_using_lu_in_lar_solver(4000), - m_int_gomory_cut_period(4), - m_int_find_cube_period(4), - m_hnf_cut_period(4), - m_int_run_gcd_test(true), - limit_on_rows_for_hnf_cutter(75), - limit_on_columns_for_hnf_cutter(150), - m_enable_hnf(true), - m_print_external_var_name(false) - + m_simplex_strategy(simplex_strategy_enum::tableau_rows) {} void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 88db78d85..05cacf720 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -37,7 +37,9 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_reslim(lim), m_use_nra_model(false), m_nra(s, lim, *this) -{} +{ + m_nlsat_delay = lp_settings().nlsat_delay(); +} bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const { switch(cmp) { @@ -1507,11 +1509,15 @@ lbool core::check(vector& l_vec) { run_grobner(); if (l_vec.empty() && !done()) - m_basics.basic_lemma(true); + m_basics.basic_lemma(true); if (l_vec.empty() && !done()) m_basics.basic_lemma(false); + if (!conflict_found() && !done() && should_run_bounded_nlsat()) + ret = bounded_nlsat(); + + if (l_vec.empty() && !done()) { std::function check1 = [&]() { m_order.order_lemma(); }; std::function check2 = [&]() { m_monotone.monotonicity_lemma(); }; @@ -1523,15 +1529,9 @@ lbool core::check(vector& l_vec) { { 1, check3 }}; check_weighted(3, checks); - if (!conflict_found() && m_nla_settings.run_nra() && random() % 50 == 0 && + if (!conflict_found() && m_nla_settings.run_nra() && should_run_bounded_nlsat() && lp_settings().stats().m_nla_calls > 500) { - params_ref p; - p.set_uint("max_conflicts", 100); - m_nra.updt_params(p); - ret = m_nra.check(); - p.set_uint("max_conflicts", UINT_MAX); - m_nra.updt_params(p); - m_stats.m_nra_calls++; + ret = bounded_nlsat(); } } @@ -1554,6 +1554,30 @@ lbool core::check(vector& l_vec) { return ret; } +bool core::should_run_bounded_nlsat() { + if (m_nlsat_delay > m_nlsat_fails) + ++m_nlsat_fails; + return m_nlsat_delay <= m_nlsat_fails; +} + +lbool core::bounded_nlsat() { + params_ref p; + p.set_uint("max_conflicts", 100); + scoped_rlimit sr(m_reslim, 100000); + m_nra.updt_params(p); + lbool ret = m_nra.check(); + p.set_uint("max_conflicts", UINT_MAX); + m_nra.updt_params(p); + m_stats.m_nra_calls++; + if (ret == l_undef) + ++m_nlsat_delay; + else { + m_nlsat_fails = 0; + m_nlsat_delay /= 2; + } + return ret; +} + bool core::no_lemmas_hold() const { for (auto & l : * m_lemma_vec) { if (lemma_holds(l)) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 8b4f1bcfe..18baa0847 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -150,6 +150,11 @@ class core { }; stats m_stats; friend class new_lemma; + + unsigned m_nlsat_delay { 50 }; + unsigned m_nlsat_fails { 0 }; + bool should_run_bounded_nlsat(); + lbool bounded_nlsat(); public: var_eqs m_evars; lp::lar_solver& m_lar_solver; diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 95e612512..eadbd278e 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -187,9 +187,9 @@ params_ref context_params::merge_default_params(params_ref const & p) { } } -void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) { - proofs_enabled = m.proofs_enabled() && p.get_bool("proof", m_proof); - models_enabled = p.get_bool("model", m_model); +void context_params::get_solver_params(params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) { + proofs_enabled &= p.get_bool("proof", m_proof); + models_enabled &= p.get_bool("model", m_model); unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false); p = merge_default_params(p); } diff --git a/src/params/context_params.h b/src/params/context_params.h index f90aa1b86..b0ed71c1f 100644 --- a/src/params/context_params.h +++ b/src/params/context_params.h @@ -60,7 +60,7 @@ public: /** \brief Goodies for extracting parameters for creating a solver object. */ - void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled); + void get_solver_params(params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled); static void collect_solver_param_descrs(param_descrs & d); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index daa4bee48..3469bd846 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -32,20 +32,12 @@ namespace arith { { m_solver = alloc(lp::lar_solver); - smt_params_helper lpar(ctx.s().params()); + lp().updt_params(ctx.s().params()); lp().settings().set_resource_limit(m_resource_limit); - lp().settings().simplex_strategy() = static_cast(lpar.arith_simplex_strategy()); lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); - lp().settings().enable_hnf() = lpar.arith_enable_hnf(); - lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names(); - lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows()); - lp().settings().report_frequency = lpar.arith_rep_freq(); - lp().settings().print_statistics = lpar.arith_print_stats(); - lp().settings().cheap_eqs() = lpar.arith_propagate_eqs(); - lp().set_cut_strategy(get_config().m_arith_branch_cut_ratio); lp().settings().int_run_gcd_test() = get_config().m_arith_gcd_test; lp().settings().set_random_seed(get_config().m_random_seed); - + m_lia = alloc(lp::int_solver, *m_solver.get()); } diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 893d3c616..0b225ab30 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -276,7 +276,9 @@ namespace bv { void solver::register_true_false_bit(theory_var v, unsigned idx) { SASSERT(s().value(m_bits[v][idx]) != l_undef); - bool is_true = (s().value(m_bits[v][idx]) == l_true); + sat::literal l = m_bits[v][idx]; + SASSERT(l == mk_true() || ~l == mk_true()); + bool is_true = l == mk_true(); zero_one_bits& bits = m_zero_one_bits[v]; bits.push_back(zero_one_bit(v, idx, is_true)); } @@ -309,7 +311,7 @@ namespace bv { void solver::set_bit_eh(theory_var v, literal l, unsigned idx) { SASSERT(m_bits[v][idx] == l); - if (s().value(l) != l_undef && s().lvl(l) == 0) + if (l.var() == mk_true().var()) register_true_false_bit(v, idx); else { atom* b = mk_atom(l.var()); @@ -354,6 +356,14 @@ namespace bv { return get_bv_size(var2enode(v)); } + sat::literal solver::mk_true() { + if (m_true == sat::null_literal) { + ctx.push(value_trail(m_true)); + m_true = ctx.internalize(m.mk_true(), false, false, false); + } + return m_true; + } + void solver::internalize_num(app* a) { numeral val; unsigned sz = 0; @@ -365,7 +375,7 @@ namespace bv { m_bb.num2bits(val, sz, bits); SASSERT(bits.size() == sz); SASSERT(m_bits[v].empty()); - sat::literal true_literal = ctx.internalize(m.mk_true(), false, false, false); + sat::literal true_literal = mk_true(); for (unsigned i = 0; i < sz; i++) { expr* l = bits.get(i); SASSERT(m.is_true(l) || m.is_false(l)); diff --git a/src/sat/smt/bv_invariant.cpp b/src/sat/smt/bv_invariant.cpp index 4af785460..1178ed105 100644 --- a/src/sat/smt/bv_invariant.cpp +++ b/src/sat/smt/bv_invariant.cpp @@ -70,12 +70,14 @@ namespace bv { bits[0].resize(bv_sz, false); bits[1].resize(bv_sz, false); + sat::literal_vector assigned; theory_var curr = v; do { literal_vector const& lits = m_bits[curr]; for (unsigned i = 0; i < lits.size(); i++) { literal l = lits[i]; - if (s().value(l) != l_undef) { + if (l.var() == mk_true().var()) { + assigned.push_back(l); unsigned is_true = s().value(l) == l_true; if (bits[!is_true][i]) { // expect a conflict later on. @@ -91,7 +93,9 @@ namespace bv { } while (curr != v); zero_one_bits const& _bits = m_zero_one_bits[v]; - SASSERT(_bits.size() == num_bits); + if (_bits.size() != num_bits) + std::cout << v << " " << _bits.size() << " " << num_bits << "\n"; + VERIFY(_bits.size() == num_bits); bool_vector already_found; already_found.resize(bv_sz, false); for (auto& zo : _bits) { diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index e1d52ca36..c216530af 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -354,23 +354,6 @@ namespace bv { sat::literal_vector lits; switch (c.m_kind) { case bv_justification::kind_t::eq2bit: - ++s_count; -// std::cout << "eq2bit " << s_count << "\n"; -#if 0 - if (s_count == 1899) { - std::cout << "eq2bit " << mk_bounded_pp(var2expr(c.m_v1), m) << " == " << mk_bounded_pp(var2expr(c.m_v2), m) << "\n"; - std::cout << mk_bounded_pp(literal2expr(~c.m_antecedent), m, 4) << "\n"; - std::cout << mk_bounded_pp(literal2expr(c.m_consequent), m, 4) << "\n"; - std::cout << literal2expr(c.m_consequent) << "\n"; -#if 0 - solver_ref slv = mk_smt2_solver(m, ctx.s().params()); - slv->assert_expr(eq); - slv->assert_expr(literal2expr(c.m_antecedent)); - slv->assert_expr(literal2expr(~c.m_consequent)); - slv->display(std::cout) << "(check-sat)\n"; -#endif - } -#endif lits.push_back(~leq); lits.push_back(~c.m_antecedent); lits.push_back(c.m_consequent); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index b7bd11591..17e199448 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -204,6 +204,7 @@ namespace bv { svector m_prop_queue; unsigned_vector m_prop_queue_lim; unsigned m_prop_queue_head { 0 }; + sat::literal m_true { sat::null_literal }; // internalize void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); } @@ -294,6 +295,7 @@ namespace bv { bool propagate_bits(var_pos entry); bool propagate_eq_occurs(eq_occurs const& occ); numeral const& power2(unsigned i) const; + sat::literal mk_true(); // invariants diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 0430ead12..7c73631ab 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -308,7 +308,7 @@ namespace euf { euf::enode* nb = n->get_arg(1); m_egraph.merge(na, nb, c); } - else if (n->merge_enabled()) { + else if (n->merge_enabled() && n->num_parents() > 0) { euf::enode* nb = sign ? mk_false() : mk_true(); m_egraph.merge(n, nb, c); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7d5d91248..32d880024 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -63,7 +63,7 @@ struct goal2sat::imp : public sat::sat_internalizer { obj_map m_app2lit; u_map m_lit2app; unsigned_vector m_cache_lim; - ptr_vector m_cache_trail; + app_ref_vector m_cache_trail; obj_hashtable m_interface_vars; sat::solver_core & m_solver; atom2bool_var & m_map; @@ -85,6 +85,7 @@ struct goal2sat::imp : public sat::sat_internalizer { imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): m(_m), pb(m), + m_cache_trail(m), m_solver(s), m_map(map), m_dep2asm(dep2asm), @@ -95,7 +96,8 @@ struct goal2sat::imp : public sat::sat_internalizer { m_true = sat::null_literal; } - ~imp() override {} + ~imp() override { + } sat::cut_simplifier* aig() { @@ -258,7 +260,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_map.pop(n); unsigned k = m_cache_lim[m_cache_lim.size() - n]; for (unsigned i = m_cache_trail.size(); i-- > k; ) { - app* t = m_cache_trail[i]; + app* t = m_cache_trail.get(i); sat::literal lit; if (m_app2lit.find(t, lit)) { m_app2lit.remove(t); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index b139ec744..55d4f9f9e 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -70,7 +70,8 @@ def_module_params(module_name='smt', ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), - ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), + ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), + ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c045c98f4..d050fcb77 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -879,16 +879,9 @@ public: get_zero(true); get_zero(false); - smt_params_helper lpar(ctx().get_params()); + lp().updt_params(ctx().get_params()); lp().settings().set_resource_limit(m_resource_limit); - lp().settings().simplex_strategy() = static_cast(lpar.arith_simplex_strategy()); lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); - lp().settings().enable_hnf() = lpar.arith_enable_hnf(); - lp().settings().print_external_var_name() = lpar.arith_print_ext_var_names(); - lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows()); - lp().settings().report_frequency = lpar.arith_rep_freq(); - lp().settings().print_statistics = lpar.arith_print_stats(); - lp().settings().cheap_eqs() = lpar.arith_propagate_eqs(); // todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;