From 622d8c951cdef6b7abf61579db8dc3f41c304db7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 May 2017 14:40:42 -0700 Subject: [PATCH 01/12] remove redundant data-type function declarations from pretty-printed output. #1034 Signed-off-by: Nikolaj Bjorner --- src/ast/ast_pp_util.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index f953dbf0e..3021b702b 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -44,8 +44,11 @@ void ast_pp_util::display_decls(std::ostream& out) { } n = coll.get_num_decls(); for (unsigned i = 0; i < n; ++i) { - ast_smt2_pp(out, coll.get_func_decls()[i], env); - out << "\n"; + func_decl* f = coll.get_func_decls()[i]; + if (f->get_family_id() == null_family_id) { + ast_smt2_pp(out, f, env); + out << "\n"; + } } } From 2cbeedec690fbd89da1a4154ae96708af77cfe65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 May 2017 19:32:43 -0700 Subject: [PATCH 02/12] accept hereditarily finite sorts in datalog engine Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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); } } From 8e9739d3b0b231c499e4429b59c5d02b8690458d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 08:51:26 -0700 Subject: [PATCH 03/12] work around crash #1039 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 94cb17526..8b94ec967 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7292,7 +7292,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 @@ -7339,7 +7339,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)); From 2834fea9b3977f2988c528e221ff51fa12bfbe52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 08:58:21 -0700 Subject: [PATCH 04/12] fix x64 warnings Signed-off-by: Nikolaj Bjorner --- src/util/lp/matrix.hpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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; From af4346f16a0c5b3aacb2b502b8e83cc32f799137 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 10:04:29 -0700 Subject: [PATCH 05/12] expose arith reflection, get rid of long m_manager attribute in asserted fromulas Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.h | 1 + src/smt/asserted_formulas.cpp | 270 ++++++++++++------------- src/smt/asserted_formulas.h | 6 +- src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_arith_params.cpp | 3 +- 5 files changed, 142 insertions(+), 139 deletions(-) diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8885bc5d6..5867b9825 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -161,6 +161,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/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 26395f9ab..8c8743eec 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_IVERBOSE(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, @@ -424,27 +424,27 @@ void asserted_formulas::apply_quasi_macros() { void asserted_formulas::nnf_cnf() { IF_IVERBOSE(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 +456,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 +476,23 @@ void asserted_formulas::NAME() { IF_IVERBOSE(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 +505,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, *m_bsimp), "distribute_forall", "distribute-forall"); void asserted_formulas::reduce_and_solve() { IF_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";); @@ -516,22 +516,22 @@ void asserted_formulas::reduce_and_solve() { void asserted_formulas::infer_patterns() { IF_IVERBOSE(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 +554,16 @@ void asserted_formulas::commit(unsigned new_qhead) { void asserted_formulas::eliminate_term_ite() { IF_IVERBOSE(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 +574,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 +602,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 +634,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 +646,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); } } @@ -680,22 +680,22 @@ void asserted_formulas::propagate_booleans() { #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); \ + 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_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); \ } \ 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)); \ + 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_manager.mk_true(), m_manager.mk_iff_true(new_pr)); \ + m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \ } for (; i < sz; i++) { PROCESS(); @@ -720,23 +720,23 @@ bool asserted_formulas::NAME() { \ 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); \ + 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); \ 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()) { \ + else if (m.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); \ + 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 { \ @@ -753,19 +753,19 @@ bool asserted_formulas::NAME() { \ 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_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_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", 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 +780,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,11 +797,11 @@ 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() { \ @@ -813,14 +813,14 @@ void asserted_formulas::NAME() { 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); \ functor(n, new_n, new_pr); \ - TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";); \ + TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \ IF_IVERBOSE(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); \ + if (m.proofs_enabled()) { \ + new_pr = m.mk_modus_ponens(pr, new_pr); \ m_asserted_formula_prs.set(i, new_pr); \ } \ } \ @@ -848,12 +848,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..84302a7ae 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, False, '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 +} From edb164587ffde74ae48677ae0c354f7e0f693dac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 10:12:32 -0700 Subject: [PATCH 06/12] get rid of a simplifier dependency Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/ast/rewriter/CMakeLists.txt | 1 + contrib/cmake/src/ast/simplifier/CMakeLists.txt | 1 - .../{simplifier => rewriter}/distribute_forall.cpp | 13 +++++++------ .../{simplifier => rewriter}/distribute_forall.h | 4 +--- src/smt/asserted_formulas.cpp | 2 +- 5 files changed, 10 insertions(+), 11 deletions(-) rename src/ast/{simplifier => rewriter}/distribute_forall.cpp (92%) rename src/ast/{simplifier => rewriter}/distribute_forall.h (90%) 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/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 8c8743eec..6f0190e7a 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -505,7 +505,7 @@ void asserted_formulas::NAME() { TRACE(LABEL, display(tout);); \ } -MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m, *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_IVERBOSE(10, verbose_stream() << "(smt.reducing)\n";); From 23ff580a67518d2ef2d10a0e8c2ca4377f099928 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 12:16:43 -0700 Subject: [PATCH 07/12] get rid of timeb dependencies, pull request #1040 Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 158 +++++++++++++++--------------- src/util/lp/lp_primal_simplex.h | 4 - src/util/lp/lp_primal_simplex.hpp | 2 - src/util/lp/lp_settings.h | 15 ++- src/util/lp/lp_settings.hpp | 13 --- src/util/lp/sparse_matrix.hpp | 6 +- 6 files changed, 88 insertions(+), 110 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6f0190e7a..5c7ed33f8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -677,25 +677,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); \ - 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)); \ +#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,43 +715,43 @@ void asserted_formulas::propagate_booleans() { } #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \ -bool asserted_formulas::NAME() { \ - IF_IVERBOSE(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); \ - 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(); \ + bool asserted_formulas::NAME() { \ + IF_IVERBOSE(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, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false); @@ -803,30 +803,30 @@ MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bo 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_IVERBOSE(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_IVERBOSE(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(); \ -} +#define LIFT_ITE(NAME, FUNCTOR, MSG) \ + void asserted_formulas::NAME() { \ + IF_IVERBOSE(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_IVERBOSE(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"); 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/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)); } } From 3f89c1418be3ef791306a5634b022b32e756b7a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 12:51:14 -0700 Subject: [PATCH 08/12] fix test build Signed-off-by: Nikolaj Bjorner --- src/test/lp.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) 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); From 6f2cd4817b40d57b8ee90afb4216cff8015b34aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 14:09:45 -0700 Subject: [PATCH 09/12] ensure arith.reflect has default true Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 84302a7ae..a501f474a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -44,7 +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, False, 'reflect arithmetical operators to the congruence closure'), + ('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'), From f3a0b7e0cd891c53badfc8c44d5fc2939a61a79d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 May 2017 20:04:27 -0700 Subject: [PATCH 10/12] change command-line experience for pareto fronts. It now requires multiple check-sat calls to loop over the fronts. This allows querying each model in turn. #1008 --- src/cmd_context/cmd_context.cpp | 34 ++++++++++++++++----------------- src/cmd_context/cmd_context.h | 1 - src/opt/opt_context.cpp | 5 ----- src/opt/opt_context.h | 1 - src/opt/opt_params.pyg | 1 - 5 files changed, 17 insertions(+), 25 deletions(-) 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 5867b9825..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; }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1310727aa..54909939f 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -319,11 +319,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'), From 7d245be4e1b464995443ee475b7600729638a46e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 May 2017 17:33:27 -0700 Subject: [PATCH 11/12] enable exposing internal solver state on interrupted solvers Signed-off-by: Nikolaj Bjorner --- src/api/api_model.cpp | 3 +- src/ast/rewriter/pb2bv_rewriter.cpp | 3 +- src/sat/card_extension.h | 11 ++- src/sat/sat_extension.h | 2 +- src/sat/sat_solver.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 58 +++++++++++-- src/sat/tactic/goal2sat.cpp | 83 +++++++++++++++++-- src/solver/solver2tactic.cpp | 16 +++- src/tactic/bv/bit_blaster_model_converter.cpp | 43 +++++++++- src/tactic/goal.cpp | 7 ++ src/tactic/goal.h | 1 + src/tactic/portfolio/default_tactic.cpp | 2 - src/tactic/portfolio/fd_solver.cpp | 6 ++ src/tactic/portfolio/fd_solver.h | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 6 +- 15 files changed, 215 insertions(+), 29 deletions(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 67c0f2f08..d867900e8 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -349,10 +349,10 @@ extern "C" { // // ---------------------------- +#if 0 void Z3_API Z3_del_model(Z3_context c, Z3_model m) { Z3_model_dec_ref(c, m); } - unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m) { return Z3_model_get_num_consts(c, m); } @@ -368,6 +368,7 @@ extern "C" { Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i) { return Z3_model_get_func_decl(c, m, i); } +#endif unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) { diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index aedd62081..bcc050048 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -822,8 +822,7 @@ struct pb2bv_rewriter::imp { p.get_bool("keep_cardinality_constraints", false) || p.get_bool("sat.cardinality.solver", false) || p.get_bool("cardinality.solver", false) || - gparams::get_module("sat").get_bool("cardinality.solver", false) || - keep_pb(); + gparams::get_module("sat").get_bool("cardinality.solver", false); } bool keep_pb() const { diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 41219fae5..fbe1141b1 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -42,7 +42,8 @@ namespace sat { stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; - + + public: class card { unsigned m_index; literal m_lit; @@ -105,6 +106,7 @@ namespace sat { void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); } void negate() { m_lits[0].neg(); } }; + protected: struct ineq { literal_vector m_lits; @@ -304,6 +306,13 @@ namespace sat { void add_at_least(bool_var v, literal_vector const& lits, unsigned k); void add_pb_ge(bool_var v, svector const& wlits, unsigned k); void add_xor(bool_var v, literal_vector const& lits); + unsigned num_pb() const { return m_pbs.size(); } + pb const& get_pb(unsigned i) const { return *m_pbs[i]; } + unsigned num_card() const { return m_cards.size(); } + card const& get_card(unsigned i) const { return *m_cards[i]; } + unsigned num_xor() const { return m_xors.size(); } + xor const& get_xor(unsigned i) const { return *m_xors[i]; } + virtual void propagate(literal l, ext_constraint_idx idx, bool & keep); virtual bool resolve_conflict(); virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r); diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index aae99c28f..a875bad6c 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -46,7 +46,7 @@ namespace sat { virtual std::ostream& display(std::ostream& out) const = 0; virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0; virtual void collect_statistics(statistics& st) const = 0; - virtual extension* copy(solver* s) = 0; + virtual extension* copy(solver* s) = 0; virtual void find_mutexes(literal_vector& lits, vector & mutexes) = 0; }; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c708823dd..c512597b0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -309,7 +309,7 @@ namespace sat { } void set_par(parallel* p, unsigned id); bool canceled() { return !m_rlimit.inc(); } - config const& get_config() { return m_config; } + config const& get_config() const { return m_config; } extension* get_extension() const { return m_ext.get(); } void set_extension(extension* e); typedef std::pair bin_clause; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 0d12c0a94..5016d20cd 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -66,7 +66,11 @@ class inc_sat_solver : public solver { expr_dependency_ref m_dep_core; svector m_weights; std::string m_unknown; - + // access formulas after they have been pre-processed and handled by the sat solver. + // this allows to access the internal state of the SAT solver and carry on partial results. + bool m_internalized; // are formulas internalized? + bool m_internalized_converted; // have internalized formulas been converted back + expr_ref_vector m_internalized_fmls; // formulas in internalized format typedef obj_map dep2asm_t; public: @@ -81,7 +85,10 @@ public: m_map(m), m_num_scopes(0), m_dep_core(m), - m_unknown("no reason given") { + m_unknown("no reason given"), + m_internalized(false), + m_internalized_converted(false), + m_internalized_fmls(m) { updt_params(p); init_preprocess(); } @@ -141,6 +148,8 @@ public: if (r != l_true) return r; r = internalize_assumptions(sz, assumptions, dep2asm); if (r != l_true) return r; + m_internalized = true; + m_internalized_converted = false; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); @@ -170,8 +179,11 @@ public: m_fmls_head_lim.push_back(m_fmls_head); if (m_bb_rewriter) m_bb_rewriter->push(); m_map.push(); + m_internalized = true; + m_internalized_converted = false; } virtual void pop(unsigned n) { + m_internalized = false; if (n > m_num_scopes) { // allow inc_sat_solver to n = m_num_scopes; // take over for another solver. } @@ -204,6 +216,7 @@ public: } virtual ast_manager& get_manager() const { return m; } virtual void assert_expr(expr * t) { + m_internalized = false; TRACE("goal2sat", tout << mk_pp(t, m) << "\n";); m_fmls.push_back(t); } @@ -320,9 +333,18 @@ public: virtual void get_labels(svector & r) { } virtual unsigned get_num_assertions() const { - return m_fmls.size(); + const_cast(this)->convert_internalized(); + if (m_internalized && m_internalized_converted) { + return m_internalized_fmls.size(); + } + else { + return m_fmls.size(); + } } virtual expr * get_assertion(unsigned idx) const { + if (m_internalized && m_internalized_converted) { + return m_internalized_fmls[idx]; + } return m_fmls[idx]; } virtual unsigned get_num_assumptions() const { @@ -332,6 +354,32 @@ public: return m_asmsf[idx]; } + void convert_internalized() { + if (!m_internalized) return; + sat2goal s2g; + model_converter_ref mc; + goal g(m, false, false, false); + s2g(m_solver, m_map, m_params, g, mc); + extract_model(); + if (!m_model) { + m_model = alloc(model, m); + } + model_ref mdl = m_model; + if (m_mc) (*m_mc)(mdl); + for (unsigned i = 0; i < mdl->get_num_constants(); ++i) { + func_decl* c = mdl->get_constant(i); + expr_ref eq(m.mk_eq(m.mk_const(c), mdl->get_const_interp(c)), m); + g.assert_expr(eq); + } + m_internalized_fmls.reset(); + g.get_formulas(m_internalized_fmls); + // g.display(std::cout); + m_internalized_converted = true; + // if (mc) mc->display(std::cout << "mc"); + // if (m_mc) m_mc->display(std::cout << "m_mc\n"); + // if (m_mc0) m_mc0->display(std::cout << "m_mc0\n"); + } + void init_preprocess() { if (m_preprocess) { m_preprocess->reset(); @@ -374,7 +422,7 @@ private: init_preprocess(); SASSERT(g->models_enabled()); SASSERT(!g->proofs_enabled()); - TRACE("goal2sat", g->display(tout);); + TRACE("sat", g->display(tout);); try { (*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core); } @@ -391,7 +439,7 @@ private: } g = m_subgoals[0]; expr_ref_vector atoms(m); - TRACE("goal2sat", g->display_with_dependencies(tout);); + TRACE("sat", g->display_with_dependencies(tout);); m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true); m_goal2sat.get_interpreted_atoms(atoms); if (!atoms.empty()) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 9d07ec3e6..6604bab89 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -137,7 +137,7 @@ struct goal2sat::imp { sat::bool_var v = m_solver.mk_var(ext); m_map.insert(t, v); l = sat::literal(v, sign); - TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";); + TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";); if (ext && !is_uninterp_const(t)) { m_interpreted_atoms.push_back(t); } @@ -993,6 +993,7 @@ struct sat2goal::imp { expr_ref_vector m_lit2expr; unsigned long long m_max_memory; bool m_learned; + unsigned m_glue; imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) { updt_params(p); @@ -1000,6 +1001,7 @@ struct sat2goal::imp { void updt_params(params_ref const & p) { m_learned = p.get_bool("learned", false); + m_glue = p.get_uint("glue", UINT_MAX); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); } @@ -1042,20 +1044,71 @@ struct sat2goal::imp { return m_lit2expr.get(l.index()); } - void assert_clauses(sat::clause * const * begin, sat::clause * const * end, goal & r) { + void assert_pb(goal& r, sat::card_extension::pb const& p) { + pb_util pb(m); + ptr_buffer lits; + vector coeffs; + for (unsigned i = 0; i < p.size(); ++i) { + lits.push_back(lit2expr(p[i].second)); + coeffs.push_back(rational(p[i].first)); + } + rational k(p.k()); + expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m); + + if (p.lit() != sat::null_literal) { + fml = m.mk_eq(lit2expr(p.lit()), fml); + } + r.assert_expr(fml); + } + + void assert_card(goal& r, sat::card_extension::card const& c) { + pb_util pb(m); + ptr_buffer lits; + for (unsigned i = 0; i < c.size(); ++i) { + lits.push_back(lit2expr(c[i])); + } + expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m); + + if (c.lit() != sat::null_literal) { + fml = m.mk_eq(lit2expr(c.lit()), fml); + } + r.assert_expr(fml); + } + + void assert_xor(goal & r, sat::card_extension::xor const& x) { + ptr_buffer lits; + for (unsigned i = 0; i < x.size(); ++i) { + lits.push_back(lit2expr(x[i])); + } + expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m); + + if (x.lit() != sat::null_literal) { + fml = m.mk_eq(lit2expr(x.lit()), fml); + } + r.assert_expr(fml); + } + + void assert_clauses(sat::solver const & s, sat::clause * const * begin, sat::clause * const * end, goal & r, bool asserted) { ptr_buffer lits; for (sat::clause * const * it = begin; it != end; it++) { checkpoint(); lits.reset(); sat::clause const & c = *(*it); unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - lits.push_back(lit2expr(c[i])); + if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) { + for (unsigned i = 0; i < sz; i++) { + lits.push_back(lit2expr(c[i])); + } + r.assert_expr(m.mk_or(lits.size(), lits.c_ptr())); } - r.assert_expr(m.mk_or(lits.size(), lits.c_ptr())); } } + sat::card_extension* get_card_extension(sat::solver const& s) { + sat::extension* ext = s.get_extension(); + return dynamic_cast(ext); + } + void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) { if (s.inconsistent()) { r.assert_expr(m.mk_false()); @@ -1087,9 +1140,22 @@ struct sat2goal::imp { r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second))); } // collect clauses - assert_clauses(s.begin_clauses(), s.end_clauses(), r); - if (m_learned) - assert_clauses(s.begin_learned(), s.end_learned(), r); + assert_clauses(s, s.begin_clauses(), s.end_clauses(), r, true); + assert_clauses(s, s.begin_learned(), s.end_learned(), r, false); + + // TBD: collect assertions from plugin + sat::card_extension* ext = get_card_extension(s); + if (ext) { + for (unsigned i = 0; i < ext->num_pb(); ++i) { + assert_pb(r, ext->get_pb(i)); + } + for (unsigned i = 0; i < ext->num_card(); ++i) { + assert_card(r, ext->get_card(i)); + } + for (unsigned i = 0; i < ext->num_xor(); ++i) { + assert_xor(r, ext->get_xor(i)); + } + } } }; @@ -1100,6 +1166,7 @@ sat2goal::sat2goal():m_imp(0) { void sat2goal::collect_param_descrs(param_descrs & r) { insert_max_memory(r); r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses."); + r.insert("glue", CPK_UINT, "(default: max-int) collect learned clauses with glue level below parameter."); } struct sat2goal::scoped_set_imp { diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 1a02c97e6..4283da50a 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -150,7 +150,21 @@ public: if (m.canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } - throw tactic_exception(local_solver->reason_unknown().c_str()); + if (in->models_enabled()) { + model_ref mdl; + local_solver->get_model(mdl); + if (mdl) { + mc = model2model_converter(mdl.get()); + mc = concat(fmc.get(), mc.get()); + } + } + in->reset(); + unsigned sz = local_solver->get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + in->assert_expr(local_solver->get_assertion(i)); + } + result.push_back(in.get()); + break; } local_solver->collect_statistics(m_st); } diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index a18862ee8..c9ba2f09c 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -117,8 +117,10 @@ struct bit_blaster_model_converter : public model_converter { SASSERT(is_uninterp_const(bit)); func_decl * bit_decl = to_app(bit)->get_decl(); expr * bit_val = old_model->get_const_interp(bit_decl); - // remark: if old_model does not assign bit_val, then assume it is false. - if (bit_val != 0 && m().is_true(bit_val)) + if (bit_val == 0) { + goto bail; + } + if (m().is_true(bit_val)) val++; } } @@ -133,15 +135,50 @@ struct bit_blaster_model_converter : public model_converter { func_decl * bit_decl = to_app(bit)->get_decl(); expr * bit_val = old_model->get_const_interp(bit_decl); // remark: if old_model does not assign bit_val, then assume it is false. - if (bit_val != 0 && !util.is_zero(bit_val)) + if (bit_val == 0) { + goto bail; + } + if (!util.is_zero(bit_val)) val++; } } new_val = util.mk_numeral(val, bv_sz); new_model->register_decl(m_vars.get(i), new_val); + continue; + bail: + new_model->register_decl(m_vars.get(i), mk_bv(bs, *old_model)); } } + app_ref mk_bv(expr* bs, model& old_model) { + bv_util util(m()); + unsigned bv_sz = to_app(bs)->get_num_args(); + expr_ref_vector args(m()); + app_ref result(m()); + for (unsigned j = 0; j < bv_sz; ++j) { + expr * bit = to_app(bs)->get_arg(j); + SASSERT(is_uninterp_const(bit)); + func_decl * bit_decl = to_app(bit)->get_decl(); + expr * bit_val = old_model.get_const_interp(bit_decl); + if (bit_val != 0) { + args.push_back(bit_val); + } + else { + args.push_back(bit); + } + } + + if (TO_BOOL) { + SASSERT(is_app_of(bs, m().get_family_id("bv"), OP_MKBV)); + result = util.mk_bv(bv_sz, args.c_ptr()); + } + else { + SASSERT(is_app_of(bs, m().get_family_id("bv"), OP_CONCAT)); + result = util.mk_concat(bv_sz, args.c_ptr()); + } + return result; + } + virtual void operator()(model_ref & md, unsigned goal_idx) { SASSERT(goal_idx == 0); model * new_model = alloc(model, m()); diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index b14d2676c..af58d8331 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -262,6 +262,13 @@ void goal::get_formulas(ptr_vector & result) { } } +void goal::get_formulas(expr_ref_vector & result) { + unsigned sz = size(); + for (unsigned i = 0; i < sz; i++) { + result.push_back(form(i)); + } +} + void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { // KLM: don't know why this assertion is no longer true // SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); diff --git a/src/tactic/goal.h b/src/tactic/goal.h index ea02dfa17..5ccbd4529 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -120,6 +120,7 @@ public: void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0); void get_formulas(ptr_vector & result); + void get_formulas(expr_ref_vector & result); void elim_true(); void elim_redundancies(); diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 4f5eb5ed0..2052894d2 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -30,7 +30,6 @@ Notes: #include"qffp_tactic.h" #include"qfaufbv_tactic.h" #include"qfauflia_tactic.h" -#include"qfufnra_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), @@ -44,7 +43,6 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), - //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), mk_smt_tactic()))))))))))), p); return st; diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp index a534337bc..12842daac 100644 --- a/src/tactic/portfolio/fd_solver.cpp +++ b/src/tactic/portfolio/fd_solver.cpp @@ -18,11 +18,13 @@ Notes: --*/ #include "fd_solver.h" +#include "fd_tactic.h" #include "tactic.h" #include "inc_sat_solver.h" #include "enum2bv_solver.h" #include "pb2bv_solver.h" #include "bounded_int2bv_solver.h" +#include "solver/solver2tactic.h" solver * mk_fd_solver(ast_manager & m, params_ref const & p) { solver* s = mk_inc_sat_solver(m, p); @@ -31,3 +33,7 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p) { s = mk_bounded_int2bv_solver(m, p, s); return s; } + +tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) { + return mk_solver2tactic(mk_fd_solver(m, p)); +} diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h index 51abb087f..41605c460 100644 --- a/src/tactic/portfolio/fd_solver.h +++ b/src/tactic/portfolio/fd_solver.h @@ -26,4 +26,5 @@ class solver; solver * mk_fd_solver(ast_manager & m, params_ref const & p); + #endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index a4a579ddd..15d2e02c2 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -34,11 +34,11 @@ Notes: #include"default_tactic.h" #include"ufbv_tactic.h" #include"qffp_tactic.h" -#include"qfufnra_tactic.h" #include"horn_tactic.h" #include"smt_solver.h" #include"inc_sat_solver.h" #include"fd_solver.h" +#include"fd_tactic.h" #include"bv_rewriter.h" #include"solver2tactic.h" @@ -91,9 +91,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const else if (logic=="HORN") return mk_horn_tactic(m, p); else if (logic == "QF_FD") - return mk_solver2tactic(mk_fd_solver(m, p)); - //else if (logic=="QF_UFNRA") - // return mk_qfufnra_tactic(m, p); + return mk_fd_tactic(m, p); else return mk_default_tactic(m, p); } From 4e65c13726d2fb95e0fb9826a8c200db0e6d4712 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Jun 2017 14:49:54 -0700 Subject: [PATCH 12/12] adding lookahead and lemmas Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 56 +++++++++++++++++++ src/api/dotnet/Solver.cs | 23 ++++++++ src/api/python/z3/z3.py | 15 +++++ src/api/z3_api.h | 24 ++++++++ src/sat/sat_lookahead.h | 32 ++++++++++- src/sat/sat_solver.cpp | 10 ++++ src/sat/sat_solver.h | 2 + src/sat/sat_solver/inc_sat_solver.cpp | 22 ++++++++ src/solver/solver.cpp | 6 ++ src/solver/solver.h | 11 ++++ .../portfolio/bounded_int2bv_solver.cpp | 1 + src/tactic/portfolio/enum2bv_solver.cpp | 1 + src/tactic/portfolio/pb2bv_solver.cpp | 1 + 13 files changed, 203 insertions(+), 1 deletion(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6dc41efb2..c6eae7488 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -477,4 +477,60 @@ extern "C" { Z3_CATCH_RETURN(Z3_L_UNDEF); } + Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, + Z3_solver s, + Z3_ast_vector candidates) { + Z3_TRY; + LOG_Z3_solver_lookahead(c, s, candidates); + ast_manager& m = mk_c(c)->m(); + expr_ref_vector _candidates(m); + ast_ref_vector const& __candidates = to_ast_vector_ref(candidates); + for (auto & e : __candidates) { + if (!is_expr(e)) { + SET_ERROR_CODE(Z3_INVALID_USAGE); + return 0; + } + _candidates.push_back(to_expr(e)); + } + + expr_ref result(m); + unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); + cancel_eh eh(mk_c(c)->m().limit()); + api::context::set_interruptable si(*(mk_c(c)), eh); + { + scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_timer timer(timeout, &eh); + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + try { + result = to_solver_ref(s)->lookahead(_candidates); + } + catch (z3_exception & ex) { + mk_c(c)->handle_exception(ex); + return 0; + } + } + mk_c(c)->save_ast_trail(result); + RETURN_Z3(of_ast(result)); + Z3_CATCH_RETURN(0); + } + + Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s) { + Z3_TRY; + LOG_Z3_solver_get_lemmas(c, s); + RESET_ERROR_CODE(); + ast_manager& m = mk_c(c)->m(); + init_solver(c, s); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + expr_ref_vector lemmas(m); + to_solver_ref(s)->get_lemmas(lemmas); + for (expr* e : lemmas) { + v->m_ast_vector.push_back(e); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + }; diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index dff2677df..6dd19cddf 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -252,6 +252,29 @@ namespace Microsoft.Z3 return lboolToStatus(r); } + /// + /// Select a lookahead literal from the set of supplied candidates. + /// + public BoolExpr Lookahead(IEnumerable candidates) + { + ASTVector cands = new ASTVector(Context); + foreach (var c in candidates) cands.Push(c); + return (BoolExpr)Expr.Create(Context, Native.Z3_solver_lookahead(Context.nCtx, NativeObject, cands.NativeObject)); + } + + /// + /// Retrieve set of lemmas that have been inferred by solver. + /// + public BoolExpr[] Lemmas + { + get + { + var r = Native.Z3_solver_get_lemmas(Context.nCtx, NativeObject); + var v = new ASTVector(Context, r); + return v.ToBoolExprArray(); + } + } + /// /// The model of the last Check. /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 84a80ddf7..7e93e58ae 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6216,6 +6216,21 @@ class Solver(Z3PPObject): consequences = [ consequences[i] for i in range(sz) ] return CheckSatResult(r), consequences + def lemmas(self): + """Extract auxiliary lemmas produced by solver""" + return AstVector(Z3_solver_get_lemmas(self.ctx.ref(), self.solver), self.ctx) + + def lookahead(self, candidates = None): + """Get lookahead literal""" + if candidates is None: + candidates = AstVector(None, self.ctx) + elif not isinstance(candidates, AstVector): + _cs = AstVector(None, self.ctx) + for c in candidates: + _asms.push(c) + candidates = _cs + return _to_expr_ref(Z3_solver_lookahead(self.ctx.ref(), self.solver, candidates), self.ctx) + def proof(self): """Return a proof for the last `check()`. Proof construction must be enabled.""" return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 45065f856..e3bd942bd 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6023,6 +6023,29 @@ extern "C" { Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences); + + /** + \brief select a literal from the list of candidate propositional variables to split on. + If the candidate list is empty, then the solver chooses a formula based on its internal state. + + def_API('Z3_solver_lookahead', AST, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR))) + */ + + Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, Z3_solver s, Z3_ast_vector candidates); + + + /** + \brief retrieve lemmas from solver state. Lemmas are auxiliary unit literals, + binary clauses and other learned clauses that are below a minimal glue level. + Lemmas that have been retrieved in a previous call may be suppressed from subsequent + calls. + + def_API('Z3_solver_get_lemmas', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) + */ + + Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s); + + /** \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions @@ -6031,6 +6054,7 @@ extern "C" { def_API('Z3_solver_get_model', MODEL, (_in(CONTEXT), _in(SOLVER))) */ + Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s); /** diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 7f01197f2..8f7a7675f 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -384,6 +384,7 @@ namespace sat { candidate(bool_var v, float r): m_var(v), m_rating(r) {} }; svector m_candidates; + uint_set m_select_lookahead_vars; float get_rating(bool_var v) const { return m_rating[v]; } float get_rating(literal l) const { return get_rating(l.var()); } @@ -468,7 +469,11 @@ namespace sat { for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) { SASSERT(is_undef(*it)); bool_var x = *it; - if (newbies || active_prefix(x)) { + if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) { + m_candidates.push_back(candidate(x, m_rating[x])); + sum += m_rating[x]; + } + else if (newbies || active_prefix(x)) { m_candidates.push_back(candidate(x, m_rating[x])); sum += m_rating[x]; } @@ -1853,6 +1858,31 @@ namespace sat { return search(); } + literal select_lookahead(bool_var_vector const& vars) { + m_search_mode = lookahead_mode::searching; + scoped_level _sl(*this, c_fixed_truth); + init(); + if (inconsistent()) return null_literal; + inc_istamp(); + for (auto v : vars) { + m_select_lookahead_vars.insert(v); + } + literal l = choose(); + m_select_lookahead_vars.reset(); + if (inconsistent()) return null_literal; + + // assign unit literals that were found during search for lookahead. + unsigned num_assigned = 0; + for (literal lit : m_trail) { + if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) { + m_s.assign(lit, justification()); + ++num_assigned; + } + } + IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";); + return l; + } + /** \brief simplify set of clauses by extracting units from a lookahead at base level. */ diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 8095ee12d..fd26bdd70 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -809,6 +809,16 @@ namespace sat { return r; } + literal solver::select_lookahead(bool_var_vector const& vars) { + lookahead lh(*this); + literal result = lh.select_lookahead(vars); + if (result == null_literal) { + set_conflict(justification()); + } + // extract unit literals from lh + return result; + } + // ----------------------- // // Search diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c512597b0..54ea360e4 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -352,6 +352,8 @@ namespace sat { model_converter const & get_model_converter() const { return m_mc; } void set_model(model const& mdl); + literal select_lookahead(bool_var_vector const& vars); + protected: unsigned m_conflicts; unsigned m_restarts; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5016d20cd..225fd8d63 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -255,6 +255,28 @@ public: return 0; } + virtual expr_ref lookahead(expr_ref_vector const& candidates) { + sat::bool_var_vector vars; + u_map var2candidate; + for (auto c : candidates) { + // TBD: check membership + sat::bool_var v = m_map.to_bool_var(c); + SASSERT(v != sat::null_bool_var); + vars.push_back(v); + var2candidate.insert(v, c); + } + sat::literal l = m_solver.select_lookahead(vars); + if (l == sat::null_literal) { + return expr_ref(m.mk_true(), m); + } + expr* e; + if (!var2candidate.find(l.var(), e)) { + // TBD: if candidate set is empty, then do something else. + e = m.mk_true(); + } + return expr_ref(l.sign() ? m.mk_not(e) : e, m); + } + virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { init_preprocess(); TRACE("sat", tout << assumptions << "\n" << vars << "\n";); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 9163cfeda..59b950972 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -162,3 +162,9 @@ bool solver::is_literal(ast_manager& m, expr* e) { return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } +expr_ref solver::lookahead(expr_ref_vector const& candidates) { + ast_manager& m = candidates.get_manager(); + return expr_ref(m.mk_true(), m); +} + + diff --git a/src/solver/solver.h b/src/solver/solver.h index 6b9d38f29..51bff08ad 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -172,6 +172,17 @@ public: */ virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); + /** + \brief extract a lookahead candidates for branching. + */ + + virtual expr_ref lookahead(expr_ref_vector const& candidates); + + /** + \brief extract learned lemmas. + */ + virtual void get_lemmas(expr_ref_vector& lemmas) {} + /** \brief Display the content of this solver. */ diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 83693abba..cee8688e5 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -149,6 +149,7 @@ public: virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } + virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { flush_assertions(); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 35601f374..ef7ee6cd8 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -97,6 +97,7 @@ public: virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + virtual expr_ref lookahead(expr_ref_vector& candidates) { return m_solver->lookahead(candidates); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { datatype_util dt(m); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index c8aa82e97..673db03c0 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -93,6 +93,7 @@ public: virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } + virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { flush_assertions();