diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index 74fddd2bb..abf09ff0c 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(rewriter bv_rewriter.cpp datatype_rewriter.cpp der.cpp + distribute_forall.cpp dl_rewriter.cpp enum2bv_rewriter.cpp expr_replacer.cpp diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/contrib/cmake/src/ast/simplifier/CMakeLists.txt index 7597374a6..9575c5c89 100644 --- a/contrib/cmake/src/ast/simplifier/CMakeLists.txt +++ b/contrib/cmake/src/ast/simplifier/CMakeLists.txt @@ -10,7 +10,6 @@ z3_add_component(simplifier bv_simplifier_params.cpp bv_simplifier_plugin.cpp datatype_simplifier_plugin.cpp - distribute_forall.cpp elim_bounds.cpp fpa_simplifier_plugin.cpp inj_axiom.cpp diff --git a/src/ast/simplifier/distribute_forall.cpp b/src/ast/rewriter/distribute_forall.cpp similarity index 92% rename from src/ast/simplifier/distribute_forall.cpp rename to src/ast/rewriter/distribute_forall.cpp index 78e5d5ded..c64c0f089 100644 --- a/src/ast/simplifier/distribute_forall.cpp +++ b/src/ast/rewriter/distribute_forall.cpp @@ -20,12 +20,12 @@ Revision History: --*/ #include"var_subst.h" #include"ast_ll_pp.h" - +#include"ast_util.h" #include"distribute_forall.h" +#include"bool_rewriter.h" -distribute_forall::distribute_forall(ast_manager & m, basic_simplifier_plugin & p) : +distribute_forall::distribute_forall(ast_manager & m) : m_manager(m), - m_bsimp(p), m_cache(m) { } @@ -109,6 +109,8 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { expr * e = get_cached(q->get_expr()); if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) { + bool_rewriter br(m_manager); + // found target for simplification // (forall X (not (or F1 ... Fn))) // --> @@ -121,8 +123,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { for (unsigned i = 0; i < num_args; i++) { expr * arg = or_e->get_arg(i); expr_ref not_arg(m_manager); - // m_bsimp.mk_not applies basic simplifications. For example, if arg is of the form (not a), then it will return a. - m_bsimp.mk_not(arg, not_arg); + br.mk_not(arg, not_arg); quantifier_ref tmp_q(m_manager); tmp_q = m_manager.update_quantifier(q, not_arg); expr_ref new_q(m_manager); @@ -132,7 +133,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { expr_ref result(m_manager); // m_bsimp.mk_and actually constructs a (not (or ...)) formula, // it will also apply basic simplifications. - m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result); + br.mk_and(new_args.size(), new_args.c_ptr(), result); cache_result(q, result); } else { diff --git a/src/ast/simplifier/distribute_forall.h b/src/ast/rewriter/distribute_forall.h similarity index 90% rename from src/ast/simplifier/distribute_forall.h rename to src/ast/rewriter/distribute_forall.h index 4c2eefb56..b2c239239 100644 --- a/src/ast/simplifier/distribute_forall.h +++ b/src/ast/rewriter/distribute_forall.h @@ -22,7 +22,6 @@ Revision History: #define DISTRIBUTE_FORALL_H_ #include"ast.h" -#include"basic_simplifier_plugin.h" #include"act_cache.h" /** @@ -47,7 +46,6 @@ Revision History: class distribute_forall { typedef act_cache expr_map; ast_manager & m_manager; - basic_simplifier_plugin & m_bsimp; // useful for constructing formulas and/or/not in simplified form. ptr_vector m_todo; expr_map m_cache; ptr_vector m_new_args; @@ -57,7 +55,7 @@ class distribute_forall { public: - distribute_forall(ast_manager & m, basic_simplifier_plugin & p); + distribute_forall(ast_manager & m); /** \brief Apply the distribute_forall transformation (when possible) to all universal quantifiers in \c f. diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f590725a7..36afeb87d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -326,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_numeral_as_real(false), m_ignore_check(false), m_exit_on_error(false), + m_processing_pareto(false), m_manager(m), m_own_manager(m == 0), m_manager_initialized(false), @@ -1130,6 +1131,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) { } void cmd_context::reset(bool finalize) { + m_processing_pareto = false; m_logic = symbol::null; m_check_sat_result = 0; m_numeral_as_real = false; @@ -1174,6 +1176,7 @@ void cmd_context::reset(bool finalize) { } void cmd_context::assert_expr(expr * t) { + m_processing_pareto = false; if (!m_check_logic(t)) throw cmd_exception(m_check_logic.get_last_error()); m_check_sat_result = 0; @@ -1186,6 +1189,7 @@ void cmd_context::assert_expr(expr * t) { } void cmd_context::assert_expr(symbol const & name, expr * t) { + m_processing_pareto = false; if (!m_check_logic(t)) throw cmd_exception(m_check_logic.get_last_error()); if (!produce_unsat_cores() || name == symbol::null) { @@ -1286,6 +1290,7 @@ static void restore(ast_manager & m, ptr_vector & c, unsigned old_sz) { } void cmd_context::restore_assertions(unsigned old_sz) { + m_processing_pareto = false; if (!has_manager()) { // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one. SASSERT(old_sz == m_assertions.size()); @@ -1303,6 +1308,7 @@ void cmd_context::restore_assertions(unsigned old_sz) { void cmd_context::pop(unsigned n) { m_check_sat_result = 0; + m_processing_pareto = false; if (n == 0) return; unsigned lvl = m_scopes.size(); @@ -1333,7 +1339,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions unsigned rlimit = m_params.m_rlimit; scoped_watch sw(*this); lbool r; - bool was_pareto = false, was_opt = false; + bool was_opt = false; if (m_opt && !m_opt->empty()) { was_opt = true; @@ -1342,21 +1348,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m().limit(), rlimit); - ptr_vector cnstr(m_assertions); - cnstr.append(num_assumptions, assumptions); - get_opt()->set_hard_constraints(cnstr); + if (!m_processing_pareto) { + ptr_vector cnstr(m_assertions); + cnstr.append(num_assumptions, assumptions); + get_opt()->set_hard_constraints(cnstr); + } try { r = get_opt()->optimize(); - while (r == l_true && get_opt()->is_pareto()) { - was_pareto = true; - get_opt()->display_assignment(regular_stream()); - regular_stream() << "\n"; - if (get_opt()->print_model()) { - model_ref mdl; - get_opt()->get_model(mdl); - display_model(mdl); - } - r = get_opt()->optimize(); + if (r == l_true && get_opt()->is_pareto()) { + m_processing_pareto = true; } } catch (z3_error & ex) { @@ -1366,8 +1366,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions get_opt()->display_assignment(regular_stream()); throw cmd_exception(ex.msg()); } - if (was_pareto && r == l_false) { - r = l_true; + if (m_processing_pareto && r != l_true) { + m_processing_pareto = false; } get_opt()->set_status(r); } @@ -1400,7 +1400,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions validate_model(); } validate_check_sat_result(r); - if (was_opt && r != l_false && !was_pareto) { + if (was_opt && r != l_false && !m_processing_pareto) { get_opt()->display_assignment(regular_stream()); } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8885bc5d6..c72e2ac0e 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -123,7 +123,6 @@ public: virtual void display_assignment(std::ostream& out) = 0; virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; - virtual bool print_model() const = 0; virtual void get_box_model(model_ref& mdl, unsigned index) = 0; virtual void updt_params(params_ref const& p) = 0; }; @@ -161,6 +160,7 @@ protected: status m_status; bool m_numeral_as_real; bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. + bool m_processing_pareto; // used when re-entering check-sat for pareto front. bool m_exit_on_error; static std::ostringstream g_error_stream; diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 619f88e3b..518e848c4 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -50,7 +50,8 @@ void rule_properties::collect(rule_set const& rules) { } for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) { sort* d = r->get_decl()->get_domain(i); - if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) { + sort_size sz = d->get_num_elements(); + if (!sz.is_finite()) { m_inf_sort.push_back(m_rule); } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 834f4fa81..94313b13b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -318,11 +318,6 @@ namespace opt { return r; } - bool context::print_model() const { - opt_params optp(m_params); - return optp.print_model(); - } - void context::get_base_model(model_ref& mdl) { mdl = m_model; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 53bfc19c5..66f0ef015 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -183,7 +183,6 @@ namespace opt { virtual bool empty() { return m_scoped_state.m_objectives.empty(); } virtual void set_hard_constraints(ptr_vector & hard); virtual lbool optimize(); - virtual bool print_model() const; virtual void set_model(model_ref& _m) { m_model = _m; } virtual void get_model(model_ref& _m); virtual void get_box_model(model_ref& _m, unsigned index); diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 51f58396c..13bf51313 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -7,7 +7,6 @@ def_module_params('opt', ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), - ('print_model', BOOL, False, 'display model for satisfiable constraints'), ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 9d81ce886..3d803d164 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -126,6 +126,27 @@ namespace sat { m_drat_file = p.drat_file(); m_drat = (m_drat_check || m_drat_file != symbol("")) && p.threads() == 1; m_dyn_sub_res = p.dyn_sub_res(); + + // Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016. + m_branching_heuristic = BH_VSIDS; + if (p.branching_heuristic() == symbol("vsids")) { + m_branching_heuristic = BH_VSIDS; + } + else if (p.branching_heuristic() == symbol("chb")) { + m_branching_heuristic = BH_CHB; + } + else if (p.branching_heuristic() == symbol("lrb")) { + m_branching_heuristic = BH_LRB; + } + else { + throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'"); + } + m_anti_exploration = m_branching_heuristic != BH_VSIDS; + m_step_size_init = 0.40; + m_step_size_dec = 0.000001; + m_step_size_min = 0.06; + m_reward_multiplier = 0.9; + m_reward_offset = 1000000.0; } void config::collect_param_descrs(param_descrs & r) { diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index a34384e87..d8b0bc7d2 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -44,6 +44,12 @@ namespace sat { GC_PSM_GLUE }; + enum branching_heuristic { + BH_VSIDS, + BH_CHB, + BH_LRB + }; + struct config { unsigned long long m_max_memory; phase_selection m_phase; @@ -95,6 +101,14 @@ namespace sat { symbol m_glue_psm; symbol m_psm_glue; + // branching heuristic settings. + branching_heuristic m_branching_heuristic; + bool m_anti_exploration; + double m_step_size_init; + double m_step_size_dec; + double m_step_size_min; + double m_reward_multiplier; + double m_reward_offset; config(params_ref const & p); void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 2c09ecdc1..c60ceee07 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -9,6 +9,7 @@ def_module_params('sat', ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), + ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), ('random_seed', UINT, 0, 'random seed'), ('burst_search', UINT, 100, 'number of conflicts before first global simplification'), @@ -21,8 +22,7 @@ def_module_params('sat', ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('core.minimize', BOOL, False, 'minimize computed core'), - ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), - ('threads', UINT, 1, 'number of parallel threads to use'), + ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), ('drat.check', BOOL, False, 'build up internal proof and check'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index ac491d6c2..8095ee12d 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -174,6 +174,11 @@ namespace sat { m_phase.push_back(PHASE_NOT_AVAILABLE); m_prev_phase.push_back(PHASE_NOT_AVAILABLE); m_assigned_since_gc.push_back(false); + m_last_conflict.push_back(0); + m_last_propagation.push_back(0); + m_participated.push_back(0); + m_canceled.push_back(0); + m_reasoned.push_back(0); m_case_split_queue.mk_var_eh(v); m_simplifier.insert_elim_todo(v); SASSERT(!was_eliminated(v)); @@ -580,6 +585,29 @@ namespace sat { if (m_ext && m_external[v]) m_ext->asserted(l); + switch (m_config.m_branching_heuristic) { + case BH_VSIDS: + break; + case BH_CHB: + m_last_propagation[v] = m_stats.m_conflict; + break; + case BH_LRB: + m_participated[v] = 0; + m_reasoned[v] = 0; + break; + } + if (m_config.m_anti_exploration) { + uint64 age = m_stats.m_conflict - m_canceled[v]; + if (age > 0) { + double decay = pow(0.95, age); + m_activity[v] = static_cast(m_activity[v] * decay); + // NB. MapleSAT does not update canceled. + m_canceled[v] = m_stats.m_conflict; + m_case_split_queue.activity_changed_eh(v, false); + } + } + + SASSERT(!l.sign() || m_phase[v] == NEG_PHASE); SASSERT(l.sign() || m_phase[v] == POS_PHASE); @@ -771,7 +799,11 @@ namespace sat { } bool solver::propagate(bool update) { + unsigned qhead = m_qhead; bool r = propagate_core(update); + if (m_config.m_branching_heuristic == BH_CHB) { + update_chb_activity(r, qhead); + } CASSERT("sat_propagate", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); return r; @@ -1064,6 +1096,18 @@ namespace sat { } while (!m_case_split_queue.empty()) { + if (m_config.m_anti_exploration) { + next = m_case_split_queue.min_var(); + auto age = m_stats.m_conflict - m_canceled[next]; + while (age > 0) { + double decay = pow(0.95, age); + m_activity[next] = static_cast(m_activity[next] * pow(0.95, age)); + m_case_split_queue.activity_changed_eh(next, false); + m_canceled[next] = m_stats.m_conflict; + next = m_case_split_queue.min_var(); + age = m_stats.m_conflict - m_canceled[next]; + } + } next = m_case_split_queue.next_var(); if (value(next) == l_undef && !was_eliminated(next)) return next; @@ -1828,6 +1872,9 @@ namespace sat { m_conflicts_since_restart++; m_conflicts_since_gc++; m_stats.m_conflict++; + if (m_step_size > m_config.m_step_size_min) { + m_step_size -= m_config.m_step_size_dec; + } m_conflict_lvl = get_max_lvl(m_not_l, m_conflict); TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for "; @@ -2175,7 +2222,16 @@ namespace sat { SASSERT(var < num_vars()); if (!is_marked(var) && var_lvl > 0) { mark(var); - inc_activity(var); + switch (m_config.m_branching_heuristic) { + case BH_VSIDS: + inc_activity(var); + break; + case BH_CHB: + m_last_conflict[var] = m_stats.m_conflict; + break; + default: + break; + } if (var_lvl == m_conflict_lvl) num_marks++; else @@ -2431,6 +2487,9 @@ namespace sat { \brief Reset the mark of the variables in the current lemma. */ void solver::reset_lemma_var_marks() { + if (m_config.m_branching_heuristic == BH_LRB) { + update_lrb_reasoned(); + } literal_vector::iterator it = m_lemma.begin(); literal_vector::iterator end = m_lemma.end(); SASSERT(!is_marked((*it).var())); @@ -2441,6 +2500,58 @@ namespace sat { } } + void solver::update_lrb_reasoned() { + unsigned sz = m_lemma.size(); + SASSERT(!is_marked(m_lemma[0].var())); + mark(m_lemma[0].var()); + for (unsigned i = m_lemma.size(); i > 0; ) { + --i; + justification js = m_justification[m_lemma[i].var()]; + switch (js.get_kind()) { + case justification::NONE: + break; + case justification::BINARY: + update_lrb_reasoned(js.get_literal()); + break; + case justification::TERNARY: + update_lrb_reasoned(js.get_literal1()); + update_lrb_reasoned(js.get_literal2()); + break; + case justification::CLAUSE: { + clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); + for (unsigned i = 0; i < c.size(); ++i) { + update_lrb_reasoned(c[i]); + } + break; + } + case justification::EXT_JUSTIFICATION: { + fill_ext_antecedents(m_lemma[i], js); + literal_vector::iterator it = m_ext_antecedents.begin(); + literal_vector::iterator end = m_ext_antecedents.end(); + for (; it != end; ++it) { + update_lrb_reasoned(*it); + } + break; + } + } + } + reset_mark(m_lemma[0].var()); + for (unsigned i = m_lemma.size(); i > sz; ) { + --i; + reset_mark(m_lemma[i].var()); + } + m_lemma.shrink(sz); + } + + void solver::update_lrb_reasoned(literal lit) { + bool_var v = lit.var(); + if (!is_marked(v)) { + mark(v); + m_reasoned[v]++; + m_lemma.push_back(lit); + } + } + /** \brief Apply dynamic subsumption resolution to new lemma. Only binary and ternary clauses are used. @@ -2617,6 +2728,18 @@ namespace sat { bool_var v = l.var(); SASSERT(value(v) == l_undef); m_case_split_queue.unassign_var_eh(v); + if (m_config.m_branching_heuristic == BH_LRB) { + uint64 interval = m_stats.m_conflict - m_last_propagation[v]; + if (interval > 0) { + auto activity = m_activity[v]; + auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval; + m_activity[v] = static_cast(m_step_size * reward + ((1 - m_step_size) * activity)); + m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity); + } + } + if (m_config.m_anti_exploration) { + m_canceled[v] = m_stats.m_conflict; + } } m_trail.shrink(old_sz); m_qhead = old_sz; @@ -2799,6 +2922,8 @@ namespace sat { m_probing.updt_params(p); m_scc.updt_params(p); m_rand.set_seed(m_config.m_random_seed); + + m_step_size = m_config.m_step_size_init; } void solver::collect_param_descrs(param_descrs & d) { @@ -2836,6 +2961,7 @@ namespace sat { // ----------------------- void solver::rescale_activity() { + SASSERT(m_config.m_branching_heuristic == BH_VSIDS); svector::iterator it = m_activity.begin(); svector::iterator end = m_activity.end(); for (; it != end; ++it) { @@ -2844,6 +2970,18 @@ namespace sat { m_activity_inc >>= 14; } + void solver::update_chb_activity(bool is_sat, unsigned qhead) { + SASSERT(m_config.m_branching_heuristic == BH_CHB); + double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0); + for (unsigned i = qhead; i < m_trail.size(); ++i) { + auto v = m_trail[i].var(); + auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1); + auto activity = m_activity[v]; + m_activity[v] = static_cast(m_step_size * reward + ((1.0 - m_step_size) * activity)); + m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity); + } + } + // ----------------------- // // Iterators diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 0429fe624..c708823dd 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -110,8 +110,17 @@ namespace sat { svector m_eliminated; svector m_external; svector m_level; + // branch variable selection: svector m_activity; unsigned m_activity_inc; + svector m_last_conflict; + svector m_last_propagation; + svector m_participated; + svector m_canceled; + svector m_reasoned; + int m_action; + double m_step_size; + // phase svector m_phase; svector m_prev_phase; svector m_assigned_since_gc; @@ -555,6 +564,12 @@ namespace sat { private: void rescale_activity(); + void update_chb_activity(bool is_sat, unsigned qhead); + + void update_lrb_reasoned(); + + void update_lrb_reasoned(literal lit); + // ----------------------- // // Iterators diff --git a/src/sat/sat_var_queue.h b/src/sat/sat_var_queue.h index f008fbb88..97e7b64f0 100644 --- a/src/sat/sat_var_queue.h +++ b/src/sat/sat_var_queue.h @@ -39,6 +39,15 @@ namespace sat { m_queue.decreased(v); } + void activity_changed_eh(bool_var v, bool up) { + if (m_queue.contains(v)) { + if (up) + m_queue.decreased(v); + else + m_queue.increased(v); + } + } + void mk_var_eh(bool_var v) { m_queue.reserve(v+1); m_queue.insert(v); @@ -61,6 +70,8 @@ namespace sat { bool empty() const { return m_queue.empty(); } bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); } + + bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); } }; }; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6598c3a05..b329a4cd8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -43,7 +43,7 @@ Revision History: #include"quasi_macros.h" asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): - m_manager(m), + m(m), m_params(p), m_pre_simplifier(m), m_simplifier(m), @@ -63,7 +63,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp); SASSERT(m_bsimp != 0); SASSERT(arith_simp != 0); - m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager); + m_macro_finder = alloc(macro_finder, m, m_macro_manager); basic_simplifier_plugin * basic_simp = 0; bv_simplifier_plugin * bv_simp = 0; @@ -90,16 +90,16 @@ void asserted_formulas::setup() { } void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) { - bsimp = alloc(basic_simplifier_plugin, m_manager); + bsimp = alloc(basic_simplifier_plugin, m); s.register_plugin(bsimp); - asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, m_params); + asimp = alloc(arith_simplifier_plugin, m, *bsimp, m_params); s.register_plugin(asimp); - s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params)); - bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params); + s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params)); + bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params); s.register_plugin(bvsimp); - s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp)); - s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp)); - s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp)); + s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp)); + s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp)); + s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp)); } void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) { @@ -108,7 +108,7 @@ void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, pro SASSERT(!m_inconsistent); SASSERT(m_scopes.empty()); m_asserted_formulas.append(num_formulas, formulas); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) m_asserted_formula_prs.append(num_formulas, prs); } @@ -125,9 +125,9 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, expr_ref_vector & r SASSERT(!result.empty()); return; } - if (m_manager.is_false(e)) + if (m.is_false(e)) m_inconsistent = true; - ::push_assertion(m_manager, e, pr, result, result_prs); + ::push_assertion(m, e, pr, result, result_prs); } void asserted_formulas::set_eliminate_and(bool flag) { @@ -145,13 +145,13 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs); return; } - proof_ref in_pr(_in_pr, m_manager); - expr_ref r1(m_manager); - proof_ref pr1(m_manager); - expr_ref r2(m_manager); - proof_ref pr2(m_manager); - TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";); - TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";); + proof_ref in_pr(_in_pr, m); + expr_ref r1(m); + proof_ref pr1(m); + expr_ref r2(m); + proof_ref pr2(m); + TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m) << "\n";); + TRACE("assert_expr_bug", tout << mk_pp(e, m) << "\n";); if (m_params.m_pre_simplifier) { m_pre_simplifier(e, r1, pr1); } @@ -161,14 +161,14 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { } set_eliminate_and(false); // do not eliminate and before nnf. m_simplifier(r1, r2, pr2); - TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";); - if (m_manager.proofs_enabled()) { + TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";); + if (m.proofs_enabled()) { if (e == r2) pr2 = in_pr; else - pr2 = m_manager.mk_modus_ponens(in_pr, m_manager.mk_transitivity(pr1, pr2)); + pr2 = m.mk_modus_ponens(in_pr, m.mk_transitivity(pr1, pr2)); } - TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m_manager) << "\n";); + TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m) << "\n";); push_assertion(r2, pr2, m_asserted_formulas, m_asserted_formula_prs); TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout);); } @@ -176,7 +176,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { void asserted_formulas::assert_expr(expr * e) { if (inconsistent()) return; - assert_expr(e, m_manager.mk_asserted(e)); + assert_expr(e, m.mk_asserted(e)); } void asserted_formulas::get_assertions(ptr_vector & result) { @@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector & result) { } void asserted_formulas::push_scope() { - SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled()); + SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m.canceled()); TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); m_scopes.push_back(scope()); m_macro_manager.push_scope(); scope & s = m_scopes.back(); s.m_asserted_formulas_lim = m_asserted_formulas.size(); - SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled()); + SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m.canceled()); s.m_inconsistent_old = m_inconsistent; m_defined_names.push(); m_bv_sharing.push_scope(); @@ -206,7 +206,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { m_inconsistent = s.m_inconsistent_old; m_defined_names.pop(num_scopes); m_asserted_formulas.shrink(s.m_asserted_formulas_lim); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim); m_asserted_qhead = s.m_asserted_formulas_lim; m_scopes.shrink(new_lvl); @@ -228,7 +228,7 @@ void asserted_formulas::reset() { #ifdef Z3DEBUG bool asserted_formulas::check_well_sorted() const { for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { - if (!is_well_sorted(m_manager, m_asserted_formulas.get(i))) return false; + if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; } return true; } @@ -322,7 +322,7 @@ void asserted_formulas::display(std::ostream & out) const { for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { if (i == m_asserted_qhead) out << "[HEAD] ==>\n"; - out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n"; + out << mk_pp(m_asserted_formulas.get(i), m) << "\n"; } out << "inconsistent: " << inconsistent() << "\n"; } @@ -331,7 +331,7 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co if (!m_asserted_formulas.empty()) { unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) - ast_def_ll_pp(out, m_manager, m_asserted_formulas.get(i), pp_visited, true, false); + ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false); out << "asserted formulas:\n"; for (unsigned i = 0; i < sz; i++) out << "#" << m_asserted_formulas[i]->get_id() << " "; @@ -346,23 +346,23 @@ void asserted_formulas::reduce_asserted_formulas() { if (inconsistent()) { return; } - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz && !inconsistent(); i++) { expr * n = m_asserted_formulas.get(i); SASSERT(n != 0); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); m_simplifier(n, new_n, new_pr); - TRACE("reduce_asserted_formulas", tout << mk_pp(n, m_manager) << " -> " << mk_pp(new_n, m_manager) << "\n";); + TRACE("reduce_asserted_formulas", tout << mk_pp(n, m) << " -> " << mk_pp(new_n, m) << "\n";); if (n == new_n.get()) { push_assertion(n, pr, new_exprs, new_prs); } else { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs, new_prs); } if (canceled()) { @@ -376,15 +376,15 @@ void asserted_formulas::swap_asserted_formulas(expr_ref_vector & new_exprs, proo SASSERT(!inconsistent() || !new_exprs.empty()); m_asserted_formulas.shrink(m_asserted_qhead); m_asserted_formulas.append(new_exprs); - if (m_manager.proofs_enabled()) { + if (m.proofs_enabled()) { m_asserted_formula_prs.shrink(m_asserted_qhead); m_asserted_formula_prs.append(new_prs); } } void asserted_formulas::find_macros_core() { - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned sz = m_asserted_formulas.size(); m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs); @@ -407,9 +407,9 @@ void asserted_formulas::expand_macros() { void asserted_formulas::apply_quasi_macros() { IF_VERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";); TRACE("before_quasi_macros", display(tout);); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); - quasi_macros proc(m_manager, m_macro_manager, m_simplifier); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); + quasi_macros proc(m, m_macro_manager, m_simplifier); while (proc(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, @@ -423,28 +423,29 @@ void asserted_formulas::apply_quasi_macros() { } void asserted_formulas::nnf_cnf() { + IF_VERBOSE(10, verbose_stream() << "(smt.nnf)\n";); - nnf apply_nnf(m_manager, m_defined_names); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); - expr_ref_vector push_todo(m_manager); - proof_ref_vector push_todo_prs(m_manager); + nnf apply_nnf(m, m_defined_names); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); + expr_ref_vector push_todo(m); + proof_ref_vector push_todo_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); - TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m_manager) << "\n";); + TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref r1(m_manager); - proof_ref pr1(m_manager); - CASSERT("well_sorted",is_well_sorted(m_manager, n)); + expr_ref r1(m); + proof_ref pr1(m); + CASSERT("well_sorted",is_well_sorted(m, n)); push_todo.reset(); push_todo_prs.reset(); apply_nnf(n, push_todo, push_todo_prs, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m_manager, r1)); - pr = m_manager.mk_modus_ponens(pr, pr1); + CASSERT("well_sorted",is_well_sorted(m, r1)); + pr = m.mk_modus_ponens(pr, pr1); push_todo.push_back(r1); push_todo_prs.push_back(pr); @@ -456,13 +457,13 @@ void asserted_formulas::nnf_cnf() { expr * n = push_todo.get(k); proof * pr = 0; m_simplifier(n, r1, pr1); - CASSERT("well_sorted",is_well_sorted(m_manager, r1)); + CASSERT("well_sorted",is_well_sorted(m, r1)); if (canceled()) { return; } - if (m_manager.proofs_enabled()) - pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1); + if (m.proofs_enabled()) + pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1); else pr = 0; push_assertion(r1, pr, new_exprs, new_prs); @@ -476,23 +477,23 @@ void asserted_formulas::NAME() { IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(LABEL, tout << "before:\n"; display(tout);); \ FUNCTOR_DEF; \ - expr_ref_vector new_exprs(m_manager); \ - proof_ref_vector new_prs(m_manager); \ + expr_ref_vector new_exprs(m); \ + proof_ref_vector new_prs(m); \ unsigned i = m_asserted_qhead; \ unsigned sz = m_asserted_formulas.size(); \ for (; i < sz; i++) { \ expr * n = m_asserted_formulas.get(i); \ proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ + expr_ref new_n(m); \ functor(n, new_n); \ - TRACE("simplifier_simple_step", tout << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";); \ + TRACE("simplifier_simple_step", tout << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); \ if (n == new_n.get()) { \ push_assertion(n, pr, new_exprs, new_prs); \ } \ - else if (m_manager.proofs_enabled()) { \ - proof_ref new_pr(m_manager); \ - new_pr = m_manager.mk_rewrite_star(n, new_n, 0, 0); \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ + else if (m.proofs_enabled()) { \ + proof_ref new_pr(m); \ + new_pr = m.mk_rewrite_star(n, new_n, 0, 0); \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ push_assertion(new_n, new_pr, new_exprs, new_prs); \ } \ else { \ @@ -505,7 +506,7 @@ void asserted_formulas::NAME() { TRACE(LABEL, display(tout);); \ } -MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall"); +MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall"); void asserted_formulas::reduce_and_solve() { IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";); @@ -516,22 +517,22 @@ void asserted_formulas::reduce_and_solve() { void asserted_formulas::infer_patterns() { IF_VERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";); TRACE("before_pattern_inference", display(tout);); - pattern_inference infer(m_manager, m_params); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + pattern_inference infer(m, m_params); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); infer(n, new_n, new_pr); if (n == new_n.get()) { push_assertion(n, pr, new_exprs, new_prs); } - else if (m_manager.proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + else if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs, new_prs); } else { @@ -554,16 +555,16 @@ void asserted_formulas::commit(unsigned new_qhead) { void asserted_formulas::eliminate_term_ite() { IF_VERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";); TRACE("before_elim_term_ite", display(tout);); - elim_term_ite elim(m_manager, m_defined_names); - expr_ref_vector new_exprs(m_manager); - proof_ref_vector new_prs(m_manager); + elim_term_ite elim(m, m_defined_names); + expr_ref_vector new_exprs(m); + proof_ref_vector new_prs(m); unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); elim(n, new_exprs, new_prs, new_n, new_pr); SASSERT(new_n.get() != 0); DEBUG_CODE({ @@ -574,8 +575,8 @@ void asserted_formulas::eliminate_term_ite() { if (n == new_n.get()) { push_assertion(n, pr, new_exprs, new_prs); } - else if (m_manager.proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + else if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs, new_prs); } else { @@ -602,31 +603,31 @@ void asserted_formulas::propagate_values() { // - new_exprs2 is the set R // // The loop also updates the m_cache. It adds the entries x -> n to it. - expr_ref_vector new_exprs1(m_manager); - proof_ref_vector new_prs1(m_manager); - expr_ref_vector new_exprs2(m_manager); - proof_ref_vector new_prs2(m_manager); + expr_ref_vector new_exprs1(m); + proof_ref_vector new_prs1(m); + expr_ref_vector new_exprs2(m); + proof_ref_vector new_prs2(m); unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) { - expr_ref n(m_asserted_formulas.get(i), m_manager); - proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager); - TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";); + expr_ref n(m_asserted_formulas.get(i), m); + proof_ref pr(m_asserted_formula_prs.get(i, 0), m); + TRACE("simplifier", tout << mk_pp(n, m) << "\n";); expr* lhs, *rhs; - if (m_manager.is_eq(n, lhs, rhs) && - (m_manager.is_value(lhs) || m_manager.is_value(rhs))) { - if (m_manager.is_value(lhs)) { + if (m.is_eq(n, lhs, rhs) && + (m.is_value(lhs) || m.is_value(rhs))) { + if (m.is_value(lhs)) { std::swap(lhs, rhs); - n = m_manager.mk_eq(lhs, rhs); - pr = m_manager.mk_symmetry(pr); + n = m.mk_eq(lhs, rhs); + pr = m.mk_symmetry(pr); } - if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) { + if (!m.is_value(lhs) && !m_simplifier.is_cached(lhs)) { if (i >= m_asserted_qhead) { new_exprs1.push_back(n); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) new_prs1.push_back(pr); } - TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n"; - if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";); + TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m) << "\n->\n" << mk_pp(rhs, m) << "\n"; + if (pr) tout << "proof: " << mk_pp(pr, m) << "\n";); m_simplifier.cache_result(lhs, rhs, pr); found = true; continue; @@ -634,7 +635,7 @@ void asserted_formulas::propagate_values() { } if (i >= m_asserted_qhead) { new_exprs2.push_back(n); - if (m_manager.proofs_enabled()) + if (m.proofs_enabled()) new_prs2.push_back(pr); } } @@ -646,14 +647,14 @@ void asserted_formulas::propagate_values() { for (unsigned i = 0; i < sz; i++) { expr * n = new_exprs2.get(i); proof * pr = new_prs2.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); m_simplifier(n, new_n, new_pr); if (n == new_n.get()) { push_assertion(n, pr, new_exprs1, new_prs1); } else { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + new_pr = m.mk_modus_ponens(pr, new_pr); push_assertion(new_n, new_pr, new_exprs1, new_prs1); } } @@ -677,25 +678,25 @@ void asserted_formulas::propagate_booleans() { cont = false; unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); -#define PROCESS() { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ - proof_ref new_pr(m_manager); \ - m_simplifier(n, new_n, new_pr); \ - m_asserted_formulas.set(i, new_n); \ - if (m_manager.proofs_enabled()) { \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - if (n != new_n) { \ - cont = true; \ - modified = true; \ - } \ - if (m_manager.is_not(new_n)) \ - m_simplifier.cache_result(to_app(new_n)->get_arg(0), m_manager.mk_false(), m_manager.mk_iff_false(new_pr)); \ - else \ - m_simplifier.cache_result(new_n, m_manager.mk_true(), m_manager.mk_iff_true(new_pr)); \ +#define PROCESS() { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + m_simplifier(n, new_n, new_pr); \ + m_asserted_formulas.set(i, new_n); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + m_asserted_formula_prs.set(i, new_pr); \ + } \ + if (n != new_n) { \ + cont = true; \ + modified = true; \ + } \ + if (m.is_not(new_n)) \ + m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \ + else \ + m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \ } for (; i < sz; i++) { PROCESS(); @@ -715,57 +716,58 @@ void asserted_formulas::propagate_booleans() { } #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \ -bool asserted_formulas::NAME() { \ - IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - FUNCTOR; \ - bool changed = false; \ - expr_ref_vector new_exprs(m_manager); \ - proof_ref_vector new_prs(m_manager); \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ - proof_ref new_pr(m_manager); \ - functor(n, new_n, new_pr); \ - if (n == new_n.get()) { \ - push_assertion(n, pr, new_exprs, new_prs); \ - } \ - else if (m_manager.proofs_enabled()) { \ - changed = true; \ - if (!new_pr) new_pr = m_manager.mk_rewrite(n, new_n); \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ - push_assertion(new_n, new_pr, new_exprs, new_prs); \ - } \ - else { \ - changed = true; \ - push_assertion(new_n, 0, new_exprs, new_prs); \ - } \ - } \ - swap_asserted_formulas(new_exprs, new_prs); \ - TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - if (changed && REDUCE) { \ - reduce_and_solve(); \ + bool asserted_formulas::NAME() { \ + IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ - } \ - return changed; \ -} + FUNCTOR; \ + bool changed = false; \ + expr_ref_vector new_exprs(m); \ + proof_ref_vector new_prs(m); \ + unsigned i = m_asserted_qhead; \ + unsigned sz = m_asserted_formulas.size(); \ + for (; i < sz; i++) { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + functor(n, new_n, new_pr); \ + if (n == new_n.get()) { \ + push_assertion(n, pr, new_exprs, new_prs); \ + } \ + else if (m.proofs_enabled()) { \ + changed = true; \ + if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + push_assertion(new_n, new_pr, new_exprs, new_prs); \ + } \ + else { \ + changed = true; \ + push_assertion(new_n, 0, new_exprs, new_prs); \ + } \ + } \ + swap_asserted_formulas(new_exprs, new_prs); \ + TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ + if (changed && REDUCE) { \ + reduce_and_solve(); \ + TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \ + } \ + return changed; \ + } -MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); -MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false); +MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); + +MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false); proof * asserted_formulas::get_inconsistency_proof() const { if (!inconsistent()) return 0; - if (!m_manager.proofs_enabled()) + if (!m.proofs_enabled()) return 0; unsigned sz = m_asserted_formulas.size(); for (unsigned i = 0; i < sz; i++) { expr * f = m_asserted_formulas.get(i); - if (m_manager.is_false(f)) + if (m.is_false(f)) return m_asserted_formula_prs.get(i); } UNREACHABLE(); @@ -780,14 +782,14 @@ void asserted_formulas::refine_inj_axiom() { for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - if (is_quantifier(n) && simplify_inj_axiom(m_manager, to_quantifier(n), new_n)) { - TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";); + expr_ref new_n(m); + if (is_quantifier(n) && simplify_inj_axiom(m, to_quantifier(n), new_n)) { + TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); m_asserted_formulas.set(i, new_n); - if (m_manager.proofs_enabled()) { - proof_ref new_pr(m_manager); - new_pr = m_manager.mk_rewrite(n, new_n); - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + if (m.proofs_enabled()) { + proof_ref new_pr(m); + new_pr = m.mk_rewrite(n, new_n); + new_pr = m.mk_modus_ponens(pr, new_pr); m_asserted_formula_prs.set(i, new_pr); } } @@ -797,36 +799,36 @@ void asserted_formulas::refine_inj_axiom() { MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true); -MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true); +MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bounds", "cheap-fourier-motzkin", true); -MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); +MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true); -#define LIFT_ITE(NAME, FUNCTOR, MSG) \ -void asserted_formulas::NAME() { \ - IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ - TRACE("lift_ite", display(tout);); \ - FUNCTOR; \ - unsigned i = m_asserted_qhead; \ - unsigned sz = m_asserted_formulas.size(); \ - for (; i < sz; i++) { \ - expr * n = m_asserted_formulas.get(i); \ - proof * pr = m_asserted_formula_prs.get(i, 0); \ - expr_ref new_n(m_manager); \ - proof_ref new_pr(m_manager); \ - functor(n, new_n, new_pr); \ - TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";); \ - IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ - m_asserted_formulas.set(i, new_n); \ - if (m_manager.proofs_enabled()) { \ - new_pr = m_manager.mk_modus_ponens(pr, new_pr); \ - m_asserted_formula_prs.set(i, new_pr); \ - } \ - } \ - TRACE("lift_ite", display(tout);); \ - reduce_and_solve(); \ -} +#define LIFT_ITE(NAME, FUNCTOR, MSG) \ + void asserted_formulas::NAME() { \ + IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \ + TRACE("lift_ite", display(tout);); \ + FUNCTOR; \ + unsigned i = m_asserted_qhead; \ + unsigned sz = m_asserted_formulas.size(); \ + for (; i < sz; i++) { \ + expr * n = m_asserted_formulas.get(i); \ + proof * pr = m_asserted_formula_prs.get(i, 0); \ + expr_ref new_n(m); \ + proof_ref new_pr(m); \ + functor(n, new_n, new_pr); \ + TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \ + IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \ + m_asserted_formulas.set(i, new_n); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ + m_asserted_formula_prs.set(i, new_pr); \ + } \ + } \ + TRACE("lift_ite", display(tout);); \ + reduce_and_solve(); \ + } LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite"); LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite"); @@ -848,12 +850,12 @@ void asserted_formulas::max_bv_sharing() { for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); proof * pr = m_asserted_formula_prs.get(i, 0); - expr_ref new_n(m_manager); - proof_ref new_pr(m_manager); + expr_ref new_n(m); + proof_ref new_pr(m); m_bv_sharing(n, new_n, new_pr); m_asserted_formulas.set(i, new_n); - if (m_manager.proofs_enabled()) { - new_pr = m_manager.mk_modus_ponens(pr, new_pr); + if (m.proofs_enabled()) { + new_pr = m.mk_modus_ponens(pr, new_pr); m_asserted_formula_prs.set(i, new_pr); } } diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 9e9ecf33a..6ad36cc70 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -35,7 +35,7 @@ class arith_simplifier_plugin; class bv_simplifier_plugin; class asserted_formulas { - ast_manager & m_manager; + ast_manager & m; smt_params & m_params; simplifier m_pre_simplifier; simplifier m_simplifier; @@ -94,7 +94,7 @@ class asserted_formulas { unsigned get_total_size() const; bool has_bv() const; void max_bv_sharing(); - bool canceled() { return m_manager.canceled(); } + bool canceled() { return m.canceled(); } public: asserted_formulas(ast_manager & m, smt_params & p); @@ -115,7 +115,7 @@ public: void commit(); void commit(unsigned new_qhead); expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); } - proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } + proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); } proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); } void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6c2ff4962..a501f474a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -44,6 +44,7 @@ def_module_params(module_name='smt', ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), + ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 1e3f29142..944911f9b 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -35,6 +35,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); m_arith_dump_lemmas = p.arith_dump_lemmas(); + m_arith_reflect = p.arith_reflect(); } @@ -85,4 +86,4 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_branching); DISPLAY_PARAM(m_nl_arith_rounds); DISPLAY_PARAM(m_arith_euclidean_solver); -} \ No newline at end of file +} diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 62846e709..63f0a88bd 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7304,7 +7304,7 @@ namespace smt { TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;); } } - } else if (ex_sort == bool_sort) { + } else if (ex_sort == bool_sort && !is_quantifier(ex)) { TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of sort Bool" << std::endl;); // set up axioms for boolean terms @@ -7351,7 +7351,7 @@ namespace smt { // if expr is an application, recursively inspect all arguments if (is_app(ex)) { - app * term = (app*)ex; + app * term = to_app(ex); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { set_up_axioms(term->get_arg(i)); diff --git a/src/test/lp.cpp b/src/test/lp.cpp index 235dab960..9e05112f5 100644 --- a/src/test/lp.cpp +++ b/src/test/lp.cpp @@ -1159,12 +1159,14 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite lp_solver * solver = reader.create_solver(dual); setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); - int begin = get_millisecond_count(); + stopwatch sw; + sw.start(); if (dual) { std::cout << "solving for dual" << std::endl; } solver->find_maximal_solution(); - int span = get_millisecond_span(begin); + sw.stop(); + double span = sw.get_seconds(); std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl; if (solver->get_status() == lp_status::OPTIMAL) { if (reader.column_names().size() < 20) { @@ -1213,7 +1215,8 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i if (reader.is_ok()) { auto * solver = reader.create_solver(dual); setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); - int begin = get_millisecond_count(); + stopwatch sw; + sw.start(); solver->find_maximal_solution(); std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl; @@ -1227,7 +1230,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i } std::cout << "cost = " << cost.get_double() << std::endl; } - std::cout << "processed in " << get_millisecond_span(begin) / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl; + std::cout << "processed in " << sw.get_current_seconds() / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl; delete solver; } else { std::cout << "cannot process " << file_name << std::endl; @@ -2426,9 +2429,10 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read std::cout << "status = " << lp_status_to_string(solver->get_status()) << std::endl; return; } - int begin = get_millisecond_count(); + stopwatch sw; + sw.start(); lp_status status = solver->solve(); - std::cout << "status is " << lp_status_to_string(status) << ", processed for " << get_millisecond_span(begin) / 1000.0 <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl; + std::cout << "status is " << lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl; if (solver->get_status() == INFEASIBLE) { vector> evidence; solver->get_infeasibility_explanation(evidence); diff --git a/src/util/lp/lp_primal_simplex.h b/src/util/lp/lp_primal_simplex.h index fcddb4eb1..715d76408 100644 --- a/src/util/lp/lp_primal_simplex.h +++ b/src/util/lp/lp_primal_simplex.h @@ -55,10 +55,6 @@ public: void set_core_solver_bounds(); - void update_time_limit_from_starting_time(int start_time) { - this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.); - } - void find_maximal_solution(); void fill_A_x_and_basis_for_stage_one_total_inf(); diff --git a/src/util/lp/lp_primal_simplex.hpp b/src/util/lp/lp_primal_simplex.hpp index 9e1af2bbe..b6b6006e5 100644 --- a/src/util/lp/lp_primal_simplex.hpp +++ b/src/util/lp/lp_primal_simplex.hpp @@ -152,7 +152,6 @@ template void lp_primal_simplex::set_core_solver_ template void lp_primal_simplex::find_maximal_solution() { - int preprocessing_start_time = get_millisecond_count(); if (this->problem_is_empty()) { this->m_status = lp_status::EMPTY; return; @@ -169,7 +168,6 @@ template void lp_primal_simplex::find_maximal_sol fill_acceptable_values_for_x(); this->count_slacks_and_artificials(); set_core_solver_bounds(); - update_time_limit_from_starting_time(preprocessing_start_time); solve_with_total_inf(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 6b6aba2ad..aac3692f9 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -8,9 +8,9 @@ #include #include #include -#include #include #include "util/lp/lp_utils.h" +#include "util/stopwatch.h" namespace lean { typedef unsigned var_index; @@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f template bool is_epsilon_small(const X & v, const double& eps); // forward definition -int get_millisecond_count(); -int get_millisecond_span(int start_time); - - class lp_resource_limit { public: virtual bool get_cancel_flag() = 0; @@ -92,12 +88,13 @@ struct lp_settings { private: class default_lp_resource_limit : public lp_resource_limit { lp_settings& m_settings; - int m_start_time; + stopwatch m_sw; public: - default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {} + default_lp_resource_limit(lp_settings& s): m_settings(s) { + m_sw.start(); + } virtual bool get_cancel_flag() { - int span_in_mills = get_millisecond_span(m_start_time); - return (span_in_mills / 1000.0 > m_settings.time_limit); + return (m_sw.get_current_seconds() > m_settings.time_limit); } }; diff --git a/src/util/lp/lp_settings.hpp b/src/util/lp/lp_settings.hpp index b57a3acda..b27d837e0 100644 --- a/src/util/lp/lp_settings.hpp +++ b/src/util/lp/lp_settings.hpp @@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) { lean_unreachable(); return lp_status::UNKNOWN; // it is unreachable } -int get_millisecond_count() { - timeb tb; - ftime(&tb); - return tb.millitm + (tb.time & 0xfffff) * 1000; -} - -int get_millisecond_span(int start_time) { - int span = get_millisecond_count() - start_time; - if (span < 0) - span += 0x100000 * 1000; - return span; -} - template diff --git a/src/util/lp/matrix.hpp b/src/util/lp/matrix.hpp index 27cdabd3e..d032cab8c 100644 --- a/src/util/lp/matrix.hpp +++ b/src/util/lp/matrix.hpp @@ -58,8 +58,8 @@ unsigned get_width_of_column(unsigned j, vector> & A) { unsigned r = 0; for (unsigned i = 0; i < A.size(); i++) { vector & t = A[i]; - std::string str= t[j]; - unsigned s = str.size(); + std::string str = t[j]; + unsigned s = static_cast(str.size()); if (r < s) { r = s; } @@ -69,8 +69,8 @@ unsigned get_width_of_column(unsigned j, vector> & A) { void print_matrix_with_widths(vector> & A, vector & ws, std::ostream & out) { for (unsigned i = 0; i < A.size(); i++) { - for (unsigned j = 0; j < A[i].size(); j++) { - print_blanks(ws[j] - A[i][j].size(), out); + for (unsigned j = 0; j < static_cast(A[i].size()); j++) { + print_blanks(ws[j] - static_cast(A[i][j].size()), out); out << A[i][j] << " "; } out << std::endl; diff --git a/src/util/lp/sparse_matrix.hpp b/src/util/lp/sparse_matrix.hpp index ff6ac9997..32bb8ed4e 100644 --- a/src/util/lp/sparse_matrix.hpp +++ b/src/util/lp/sparse_matrix.hpp @@ -1050,8 +1050,8 @@ bool sparse_matrix::get_pivot_for_column(unsigned &i, unsigned &j, int c_p if (i_inv < k) continue; unsigned j_inv = adjust_column_inverse(j); if (j_inv < k) continue; - int small = elem_is_too_small(i, j, c_partial_pivoting); - if (!small) { + int _small = elem_is_too_small(i, j, c_partial_pivoting); + if (!_small) { #ifdef LEAN_DEBUG // if (!really_best_pivot(i, j, c_partial_pivoting, k)) { // print_active_matrix(k); @@ -1063,7 +1063,7 @@ bool sparse_matrix::get_pivot_for_column(unsigned &i, unsigned &j, int c_p j = j_inv; return true; } - if (small != 2) { // 2 means that the pair is not in the matrix + if (_small != 2) { // 2 means that the pair is not in the matrix pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j)); } }