From 6bd87f837a143ec5321d598202591d6ae84d432f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Jan 2019 14:14:26 -0800 Subject: [PATCH 01/12] fix Boolean argument Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 4ee93ff37..5fccadcbd 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -213,7 +213,7 @@ class parallel_tactic : public tactic { solver_state* clone() { SASSERT(!m_cubes.empty()); ast_manager& m = m_solver->get_manager(); - ast_manager* new_m = alloc(ast_manager, m, m.proof_mode()); + ast_manager* new_m = alloc(ast_manager, m, true); ast_translation tr(m, *new_m); solver* s = m_solver.get()->translate(*new_m, m_params); solver_state* st = alloc(solver_state, new_m, s, m_params); From 49a51a075776cd37126bf868cd92184e484752a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jan 2019 07:06:40 -0800 Subject: [PATCH 02/12] fix #2096, introduced when fixing #2082 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d56d37041..21707d3c2 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -907,7 +907,7 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { m_util.mk_idiv(zero, zero), m().mk_ite(m_util.mk_ge(arg, zero), d, - m_util.mk_uminus(nd))), + nd)), m()); } From f9195c77a7ac88fea0bde163bf04256b969619f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jan 2019 09:46:04 -0800 Subject: [PATCH 03/12] remove not-handled clause from mod with non-numerals Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c9db3f6b0..01330269c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -483,22 +483,6 @@ class theory_lra::imp { if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod); } else if (a.is_mod(n, n1, n2)) { - bool is_num = a.is_numeral(n2, r) && !r.is_zero(); - if (!is_num) { - found_not_handled(n); - } -#if 0 - else { - app_ref div(a.mk_idiv(n1, n2), m); - mk_enode(div); - theory_var w = mk_var(div); - theory_var u = mk_var(n1); - // add axioms: - // u = v + r*w - // abs(r) > v >= 0 - assert_idiv_mod_axioms(u, v, w, r); - } -#endif if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2); } else if (a.is_rem(n, n1, n2)) { From 412eee0dace45c2d7c13a6fbdc0a6d83e7a021d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jan 2019 18:12:39 -0800 Subject: [PATCH 04/12] throttle number of rounds of ba simplification Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 47fc2c27f..7315f913b 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2837,7 +2837,7 @@ namespace sat { void ba_solver::simplify() { if (!s().at_base_lvl()) s().pop_to_base_level(); - unsigned trail_sz; + unsigned trail_sz, count = 0; do { trail_sz = s().init_trail_size(); m_simplify_change = false; @@ -2855,8 +2855,9 @@ namespace sat { cleanup_clauses(); cleanup_constraints(); update_pure(); + ++count; } - while (m_simplify_change || trail_sz < s().init_trail_size()); + while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size())); IF_VERBOSE(1, verbose_stream() << "(ba.simplify" << " :vars " << s().num_vars() - trail_sz From 8e5c1fcfd150e6b51040f1802f86e831e674f134 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Jan 2019 16:06:25 -0800 Subject: [PATCH 05/12] make context_solve configurable and exposed as top-level tactic parameter Signed-off-by: Nikolaj Bjorner --- src/tactic/CMakeLists.txt | 2 ++ src/tactic/core/blast_term_ite_tactic.cpp | 13 ++++----- src/tactic/core/propagate_values_tactic.cpp | 6 +++-- src/tactic/core/solve_eqs_tactic.cpp | 29 ++++++++++----------- 4 files changed, 27 insertions(+), 23 deletions(-) diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt index c9554b76a..495078afc 100644 --- a/src/tactic/CMakeLists.txt +++ b/src/tactic/CMakeLists.txt @@ -22,4 +22,6 @@ z3_add_component(tactic probe.h sine_filter.h tactic.h + PYG_FILES + tactic_params.pyg ) diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index eefb9418e..259b479c5 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -16,11 +16,12 @@ Author: Notes: --*/ -#include "tactic/tactical.h" +#include "util/cooperate.h" #include "ast/normal_forms/defined_names.h" #include "ast/rewriter/rewriter_def.h" -#include "util/cooperate.h" #include "ast/scoped_proof.h" +#include "tactic/tactical.h" +#include "tactic/tactic_params.hpp" @@ -50,9 +51,10 @@ class blast_term_ite_tactic : public tactic { } void updt_params(params_ref const & p) { + tactic_params tp(p); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - m_max_inflation = p.get_uint("max_inflation", UINT_MAX); // multiplicative factor of initial term size. + m_max_steps = p.get_uint("max_steps", tp.blast_term_ite_max_steps()); + m_max_inflation = p.get_uint("max_inflation", tp.blast_term_ite_max_inflation()); // multiplicative factor of initial term size. } @@ -182,8 +184,7 @@ public: void collect_param_descrs(param_descrs & r) override { insert_max_memory(r); insert_max_steps(r); - r.insert("max_args", CPK_UINT, - "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); + r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size."); } void operator()(goal_ref const & in, goal_ref_buffer & result) override { diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index f9712120f..351b606e6 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -23,6 +23,7 @@ Revision History: #include "ast/ast_smt2_pp.h" #include "ast/expr_substitution.h" #include "tactic/goal_shared_occs.h" +#include "tactic/tactic_params.hpp" namespace { class propagate_values_tactic : public tactic { @@ -37,7 +38,8 @@ class propagate_values_tactic : public tactic { params_ref m_params; void updt_params_core(params_ref const & p) { - m_max_rounds = p.get_uint("max_rounds", 4); + tactic_params tp(p); + m_max_rounds = p.get_uint("max_rounds", tp.propagate_values_max_rounds()); } bool is_shared(expr * t) { @@ -215,7 +217,7 @@ public: void collect_param_descrs(param_descrs & r) override { th_rewriter::get_param_descrs(r); - r.insert("max_rounds", CPK_UINT, "(default: 2) maximum number of rounds."); + r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds."); } void operator()(goal_ref const & in, goal_ref_buffer & result) override { diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 1ed230886..623f83db4 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -25,6 +25,7 @@ Revision History: #include "tactic/goal_shared_occs.h" #include "tactic/tactical.h" #include "tactic/generic_model_converter.h" +#include "tactic/tactic_params.hpp" class solve_eqs_tactic : public tactic { struct imp { @@ -40,6 +41,7 @@ class solve_eqs_tactic : public tactic { bool m_theory_solver; bool m_ite_solver; unsigned m_max_occs; + bool m_context_solve; scoped_ptr m_subst; scoped_ptr m_norm_subst; expr_sparse_mark m_candidate_vars; @@ -72,9 +74,11 @@ class solve_eqs_tactic : public tactic { ast_manager & m() const { return m_manager; } void updt_params(params_ref const & p) { - m_ite_solver = p.get_bool("ite_solver", true); - m_theory_solver = p.get_bool("theory_solver", true); - m_max_occs = p.get_uint("solve_eqs_max_occs", UINT_MAX); + tactic_params tp(p); + m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver()); + m_theory_solver = p.get_bool("theory_solver", tp.solve_eqs_theory_solver()); + m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs()); + m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve()); } void checkpoint() { @@ -555,7 +559,7 @@ class solve_eqs_tactic : public tactic { insert_solution(g, idx, arg, var, def, pr); } else { - IF_VERBOSE(0, + IF_VERBOSE(10000, verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n"; verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " " << !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";); @@ -726,7 +730,7 @@ class solve_eqs_tactic : public tactic { ++idx; } - IF_VERBOSE(10, + IF_VERBOSE(10000, verbose_stream() << "ordered vars: "; for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " "; verbose_stream() << "\n";); @@ -811,12 +815,6 @@ class solve_eqs_tactic : public tactic { } m_r->operator()(f, new_f, new_pr, new_dep); -#if 0 - pb_util pb(m()); - if (pb.is_ge(f) && f != new_f) { - IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n"); - } -#endif TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";); m_num_steps += m_r->get_num_steps() + 1; @@ -922,8 +920,9 @@ class solve_eqs_tactic : public tactic { while (true) { collect_num_occs(*g); collect(*g); - // TBD Disabled until tested more: - // collect_hoist(*g); + if (m_context_solve) { + collect_hoist(*g); + } if (m_subst->empty()) break; sort_vars(); @@ -941,7 +940,6 @@ class solve_eqs_tactic : public tactic { g->inc_depth(); g->add(mc.get()); result.push_back(g.get()); - //IF_VERBOSE(0, g->display(verbose_stream())); TRACE("solve_eqs", g->display(tout);); SASSERT(g->is_well_sorted()); } @@ -968,10 +966,11 @@ public: m_imp->updt_params(p); } - void collect_param_descrs(param_descrs & r) override { + void collect_param_descrs(param_descrs & r) override { r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations."); r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers."); r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver."); + r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions."); } void operator()(goal_ref const & in, From 9c07167ff8b1a60b3a990ed6666f725c9176f508 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Jan 2019 16:06:44 -0800 Subject: [PATCH 06/12] add new pyg file Signed-off-by: Nikolaj Bjorner --- src/tactic/tactic_params.pyg | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 src/tactic/tactic_params.pyg diff --git a/src/tactic/tactic_params.pyg b/src/tactic/tactic_params.pyg new file mode 100644 index 000000000..5dfc6e5e8 --- /dev/null +++ b/src/tactic/tactic_params.pyg @@ -0,0 +1,20 @@ + +def_module_params('tactic', + description='tactic parameters', + export=True, + params=(('solve_eqs.context_solve', BOOL, False, "solve equalities within disjunctions."), + ('solve_eqs.theory_solver', BOOL, True, "use theory solvers."), + ('solve_eqs.ite_solver', BOOL, True, "use if-then-else solvers."), + ('solve_eqs.max_occs', UINT, UINT_MAX, "maximum number of occurrences for considering a variable for gaussian eliminations."), + ('blast_term_ite.max_inflation', UINT, UINT_MAX, "multiplicative factor of initial term size."), + ('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."), + ('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."), + # ('aig.per_assertion', BOOL, True, "process one assertion at a time"), + # ('add_bounds.lower, INT, -2, "lower bound to be added to unbounded variables."), + # ('add_bounds.upper, INT, 2, "upper bound to be added to unbounded variables."), + # ('fm.real_only', BOOL, True, "consider only real variables for FM"), + # ('fm.occ', BOOL, False, "consider inequalities occurring in clauses for FM."), + # ('fm.limit', UINT, 5000000, "maximal number of constraints, monomials, clauses visited during FM."), + # etc: lia2card, factor, nla2bv, normalize_bounds, pb2bv, purify_arith, bit_blaster, bv_bounds + )) + From f7746e22848ea318a8a094e30a002e022aef1d85 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Jan 2019 16:58:00 -0800 Subject: [PATCH 07/12] address perf #2098 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_big.cpp | 22 +++------------------- src/sat/sat_big.h | 2 +- 2 files changed, 4 insertions(+), 20 deletions(-) diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index c1eeecd27..1aa923f1f 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -164,22 +164,22 @@ namespace sat { DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);}); } - // svector> big::s_del_bin; bool big::in_del(literal u, literal v) const { if (u.index() > v.index()) std::swap(u, v); - return m_del_bin.contains(std::make_pair(u, v)); + return m_del_bin[u.index()].contains(v); } void big::add_del(literal u, literal v) { if (u.index() > v.index()) std::swap(u, v); - m_del_bin.push_back(std::make_pair(u, v)); + m_del_bin[u.index()].push_back(v); } unsigned big::reduce_tr(solver& s) { unsigned idx = 0; unsigned elim = 0; m_del_bin.reset(); + m_del_bin.reserve(s.m_watches.size()); for (watch_list & wlist : s.m_watches) { if (s.inconsistent()) break; literal u = to_literal(idx++); @@ -211,22 +211,6 @@ namespace sat { wlist.set_end(itprev); } -#if 0 - s_del_bin.append(m_del_bin); - IF_VERBOSE(1, - display(verbose_stream() << "Learned: " << learned() << ":"); - verbose_stream() << "del-bin\n"; - for (auto p : m_del_bin) { - verbose_stream() << p.first << " " << p.second << "\n"; - if (safe_reach(~p.first, p.second)) { - display_path(verbose_stream(), ~p.first, p.second) << " " << "\n"; - } - else { - display_path(verbose_stream(), ~p.second, p.first) << " " << "\n"; - } - } - ); -#endif s.propagate(false); return elim; } diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 25093fd60..e682f9dfc 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -36,7 +36,7 @@ namespace sat { bool m_learned; bool m_include_cardinality; - svector> m_del_bin; + vector > m_del_bin; void init_dfs_num(); From 498864c582e2897d7246b0124a9b48fb8643d16b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Jan 2019 12:21:23 -0800 Subject: [PATCH 08/12] adding dump facility for cancelation #2095, easing dimacs in/out Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 66 +- src/api/c++/z3++.h | 2 + src/api/python/z3/z3.py | 4 + src/api/z3_api.h | 8 + src/ast/CMakeLists.txt | 1 + src/ast/display_dimacs.cpp | 81 ++ src/ast/display_dimacs.h | 26 + src/muz/spacer/spacer_iuc_solver.cpp | 791 +++++++++--------- src/muz/spacer/spacer_iuc_solver.h | 2 +- src/opt/opt_solver.cpp | 2 +- src/opt/opt_solver.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/smt/smt_solver.cpp | 2 +- src/solver/CMakeLists.txt | 2 + src/solver/combined_solver.cpp | 10 +- src/solver/solver.cpp | 49 +- src/solver/solver.h | 16 +- src/solver/solver_na2as.cpp | 4 +- src/solver/solver_na2as.h | 5 +- src/solver/solver_params.pyg | 8 + src/solver/solver_pool.cpp | 2 +- src/solver/tactic2solver.cpp | 4 +- .../fd_solver/bounded_int2bv_solver.cpp | 4 +- src/tactic/fd_solver/enum2bv_solver.cpp | 4 +- src/tactic/fd_solver/pb2bv_solver.cpp | 4 +- src/tactic/goal.cpp | 65 +- src/tactic/goal.h | 4 +- src/util/chashtable.h | 1 + 28 files changed, 653 insertions(+), 518 deletions(-) create mode 100644 src/ast/display_dimacs.cpp create mode 100644 src/ast/display_dimacs.h create mode 100644 src/solver/solver_params.pyg diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 8f92d5bb4..330d0f2bc 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -163,12 +163,46 @@ extern "C" { to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); } + static void solver_from_dimacs_stream(Z3_context c, Z3_solver s, std::istream& is) { + init_solver(c, s); + ast_manager& m = to_solver_ref(s)->get_manager(); + std::stringstream err; + sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); + if (!parse_dimacs(is, err, solver)) { + SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str()); + return; + } + sat2goal s2g; + ref mc; + atom2bool_var a2b(m); + for (unsigned v = 0; v < solver.num_vars(); ++v) { + a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v); + } + goal g(m); + s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc); + for (unsigned i = 0; i < g.size(); ++i) { + to_solver_ref(s)->assert_expr(g.form(i)); + } + } + + // DIMACS files start with "p cnf" and number of variables/clauses. + // This is not legal SMT syntax, so use the DIMACS parser. + static bool is_dimacs_string(Z3_string c_str) { + std::cout << c_str << "\n"; + return c_str[0] == 'p' && c_str[1] == ' ' && c_str[2] == 'c'; + } + void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) { Z3_TRY; LOG_Z3_solver_from_string(c, s, c_str); std::string str(c_str); std::istringstream is(str); - solver_from_stream(c, s, is); + if (is_dimacs_string(c_str)) { + solver_from_dimacs_stream(c, s, is); + } + else { + solver_from_stream(c, s, is); + } Z3_CATCH; } @@ -182,24 +216,7 @@ extern "C" { SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr); } else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) { - ast_manager& m = to_solver_ref(s)->get_manager(); - std::stringstream err; - sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); - if (!parse_dimacs(is, err, solver)) { - SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str()); - return; - } - sat2goal s2g; - ref mc; - atom2bool_var a2b(m); - for (unsigned v = 0; v < solver.num_vars(); ++v) { - a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v); - } - goal g(m); - s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc); - for (unsigned i = 0; i < g.size(); ++i) { - to_solver_ref(s)->assert_expr(g.form(i)); - } + solver_from_dimacs_stream(c, s, is); } else { solver_from_stream(c, s, is); @@ -532,6 +549,17 @@ extern "C" { Z3_CATCH_RETURN(""); } + Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s) { + Z3_TRY; + LOG_Z3_solver_to_string(c, s); + RESET_ERROR_CODE(); + init_solver(c, s); + std::ostringstream buffer; + to_solver_ref(s)->display_dimacs(buffer); + return mk_c(c)->mk_external_string(buffer.str()); + Z3_CATCH_RETURN(""); + } + Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, Z3_solver s, diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e541080c9..9847e4264 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2240,6 +2240,8 @@ namespace z3 { fml)); } + std::string dimacs() const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver)); } + param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 65f634b6b..1886bc475 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6800,6 +6800,10 @@ class Solver(Z3PPObject): """ return Z3_solver_to_string(self.ctx.ref(), self.solver) + def dimacs(self): + """Return a textual representation of the solver in DIMACS format.""" + return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver) + def to_smt2(self): """return SMTLIB2 formatted benchmark for solver's assertions""" es = self.assertions() diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 5ee7fcb99..cd52d2d86 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6368,6 +6368,14 @@ extern "C" { */ Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s); + /** + \brief Convert a solver into a DIMACS formatted string. + \sa Z3_goal_to_diamcs_string for requirements. + + def_API('Z3_solver_to_dimacs_string', STRING, (_in(CONTEXT), _in(SOLVER))) + */ + Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s); + /*@}*/ /** @name Statistics */ diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index ce2817b58..56ab78b8a 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -17,6 +17,7 @@ z3_add_component(ast csp_decl_plugin.cpp datatype_decl_plugin.cpp decl_collector.cpp + display_dimacs.cpp dl_decl_plugin.cpp expr2polynomial.cpp expr2var.cpp diff --git a/src/ast/display_dimacs.cpp b/src/ast/display_dimacs.cpp new file mode 100644 index 000000000..da39538d9 --- /dev/null +++ b/src/ast/display_dimacs.cpp @@ -0,0 +1,81 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + display_dimacs.h + +Abstract: + + Display expressions in DIMACS format. + +Author: + + Nikolaj Bjorner (nbjorner0 2019-01-24 + +Revision History: + +--*/ + +#include "ast.h" +#include "display_dimacs.h" + +std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) { + ast_manager& m = fmls.m(); + unsigned_vector expr2var; + ptr_vector exprs; + unsigned num_vars = 0; + unsigned num_cls = fmls.size(); + for (expr * f : fmls) { + unsigned num_lits; + expr * const * lits; + if (m.is_or(f)) { + num_lits = to_app(f)->get_num_args(); + lits = to_app(f)->get_args(); + } + else { + num_lits = 1; + lits = &f; + } + for (unsigned j = 0; j < num_lits; j++) { + expr * l = lits[j]; + if (m.is_not(l)) + l = to_app(l)->get_arg(0); + if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { + num_vars++; + expr2var.setx(l->get_id(), num_vars, UINT_MAX); + exprs.setx(l->get_id(), l, nullptr); + } + } + } + out << "p cnf " << num_vars << " " << num_cls << "\n"; + for (expr* f : fmls) { + unsigned num_lits; + expr * const * lits; + if (m.is_or(f)) { + num_lits = to_app(f)->get_num_args(); + lits = to_app(f)->get_args(); + } + else { + num_lits = 1; + lits = &f; + } + for (unsigned j = 0; j < num_lits; j++) { + expr * l = lits[j]; + if (m.is_not(l)) { + out << "-"; + l = to_app(l)->get_arg(0); + } + SASSERT(exprs[l->get_id()]); + out << expr2var[l->get_id()] << " "; + } + out << "0\n"; + } + for (expr* e : exprs) { + if (e && is_app(e)) { + symbol const& n = to_app(e)->get_decl()->get_name(); + out << "c " << expr2var[e->get_id()] << " " << n << "\n"; + } + } + return out; +} diff --git a/src/ast/display_dimacs.h b/src/ast/display_dimacs.h new file mode 100644 index 000000000..91c2386be --- /dev/null +++ b/src/ast/display_dimacs.h @@ -0,0 +1,26 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + display_dimacs.h + +Abstract: + + Display expressions in DIMACS format. + +Author: + + Nikolaj Bjorner (nbjorner0 2019-01-24 + +Revision History: + +--*/ +#ifndef DISPLAY_DIMACS_H_ +#define DISPLAY_DIMACS_H_ + +#include "ast.h" + +std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls); + +#endif /* DISPLAY_DIMACS_H__ */ diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 32f33f773..f28864e27 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -27,443 +27,426 @@ Notes: #include "muz/spacer/spacer_iuc_proof.h" namespace spacer { -void iuc_solver::push () -{ - m_defs.push_back (def_manager (*this)); - m_solver.push (); -} - -void iuc_solver::pop (unsigned n) -{ - m_solver.pop (n); - unsigned lvl = m_defs.size (); - SASSERT (n <= lvl); - unsigned new_lvl = lvl-n; - while (m_defs.size() > new_lvl) { - m_num_proxies -= m_defs.back ().m_defs.size (); - m_defs.pop_back (); + void iuc_solver::push () { + m_defs.push_back (def_manager (*this)); + m_solver.push (); } -} - -app* iuc_solver::fresh_proxy () -{ - if (m_num_proxies == m_proxies.size()) { - std::stringstream name; - name << "spacer_proxy!" << m_proxies.size (); - app_ref res(m); - res = m.mk_const (symbol (name.str ().c_str ()), - m.mk_bool_sort ()); - m_proxies.push_back (res); - - // -- add the new proxy to proxy eliminator - proof_ref pr(m); - pr = m.mk_asserted (m.mk_true ()); - m_elim_proxies_sub.insert (res, m.mk_true (), pr); + void iuc_solver::pop (unsigned n) { + m_solver.pop (n); + unsigned lvl = m_defs.size (); + SASSERT (n <= lvl); + unsigned new_lvl = lvl-n; + while (m_defs.size() > new_lvl) { + m_num_proxies -= m_defs.back ().m_defs.size (); + m_defs.pop_back (); + } } - return m_proxies.get (m_num_proxies++); -} -app* iuc_solver::mk_proxy (expr *v) -{ - { + app* iuc_solver::fresh_proxy () { + if (m_num_proxies == m_proxies.size()) { + std::stringstream name; + name << "spacer_proxy!" << m_proxies.size (); + app_ref res(m); + res = m.mk_const (symbol (name.str ().c_str ()), + m.mk_bool_sort ()); + m_proxies.push_back (res); + + // -- add the new proxy to proxy eliminator + proof_ref pr(m); + pr = m.mk_asserted (m.mk_true ()); + m_elim_proxies_sub.insert (res, m.mk_true (), pr); + + } + return m_proxies.get (m_num_proxies++); + } + + app* iuc_solver::mk_proxy (expr *v) { expr *e = v; m.is_not (v, e); - if (is_uninterp_const(e)) { return to_app(v); } + if (is_uninterp_const(e)) { + return to_app(v); + } + + def_manager &def = !m_defs.empty() ? m_defs.back () : m_base_defs; + return def.mk_proxy (v); } - def_manager &def = !m_defs.empty() ? m_defs.back () : m_base_defs; - return def.mk_proxy (v); -} - -bool iuc_solver::mk_proxies (expr_ref_vector &v, unsigned from) -{ - bool dirty = false; - for (unsigned i = from, sz = v.size(); i < sz; ++i) { - app *p = mk_proxy (v.get (i)); - dirty |= (v.get (i) != p); - v[i] = p; + bool iuc_solver::mk_proxies (expr_ref_vector &v, unsigned from) { + bool dirty = false; + for (unsigned i = from, sz = v.size(); i < sz; ++i) { + app *p = mk_proxy (v.get (i)); + dirty |= (v.get (i) != p); + v[i] = p; + } + return dirty; } - return dirty; -} -void iuc_solver::push_bg (expr *e) -{ - if (m_assumptions.size () > m_first_assumption) - { m_assumptions.shrink(m_first_assumption); } - m_assumptions.push_back (e); - m_first_assumption = m_assumptions.size (); -} - -void iuc_solver::pop_bg (unsigned n) -{ - if (n == 0) { return; } - - if (m_assumptions.size () > m_first_assumption) { + void iuc_solver::push_bg (expr *e) { + if (m_assumptions.size () > m_first_assumption) { + m_assumptions.shrink(m_first_assumption); + } + m_assumptions.push_back (e); + m_first_assumption = m_assumptions.size (); + } + + void iuc_solver::pop_bg (unsigned n) { + if (n == 0) return; + + if (m_assumptions.size () > m_first_assumption) { + m_assumptions.shrink(m_first_assumption); + } + m_first_assumption = m_first_assumption > n ? m_first_assumption - n : 0; + m_assumptions.shrink (m_first_assumption); + } + + unsigned iuc_solver::get_num_bg () { + return m_first_assumption; + } + + lbool iuc_solver::check_sat_core (unsigned num_assumptions, expr * const *assumptions) { + // -- remove any old assumptions m_assumptions.shrink(m_first_assumption); + + // -- replace theory literals in background assumptions with proxies + mk_proxies (m_assumptions); + // -- in case mk_proxies added new literals, they are all background + m_first_assumption = m_assumptions.size (); + + m_assumptions.append (num_assumptions, assumptions); + m_is_proxied = mk_proxies (m_assumptions, m_first_assumption); + + return set_status (m_solver.check_sat (m_assumptions)); } - m_first_assumption = m_first_assumption > n ? m_first_assumption - n : 0; - m_assumptions.shrink (m_first_assumption); -} + + lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube, + vector const & clauses) { + if (clauses.empty()) + return check_sat(cube.size(), cube.c_ptr()); + + // -- remove any old assumptions + m_assumptions.shrink(m_first_assumption); + + // -- replace theory literals in background assumptions with proxies + mk_proxies(m_assumptions); + // -- in case mk_proxies added new literals, they are all background + m_first_assumption = m_assumptions.size(); + + m_assumptions.append(cube); + m_is_proxied = mk_proxies(m_assumptions, m_first_assumption); + + return set_status (m_solver.check_sat_cc(m_assumptions, clauses)); + } + -unsigned iuc_solver::get_num_bg () {return m_first_assumption;} - -lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions) -{ - // -- remove any old assumptions - m_assumptions.shrink(m_first_assumption); - - // -- replace theory literals in background assumptions with proxies - mk_proxies (m_assumptions); - // -- in case mk_proxies added new literals, they are all background - m_first_assumption = m_assumptions.size (); - - m_assumptions.append (num_assumptions, assumptions); - m_is_proxied = mk_proxies (m_assumptions, m_first_assumption); - - return set_status (m_solver.check_sat (m_assumptions)); -} - -lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube, - vector const & clauses) { - if (clauses.empty()) - return check_sat(cube.size(), cube.c_ptr()); - - // -- remove any old assumptions - m_assumptions.shrink(m_first_assumption); - - // -- replace theory literals in background assumptions with proxies - mk_proxies(m_assumptions); - // -- in case mk_proxies added new literals, they are all background - m_first_assumption = m_assumptions.size(); - - m_assumptions.append(cube); - m_is_proxied = mk_proxies(m_assumptions, m_first_assumption); - - return set_status (m_solver.check_sat_cc(m_assumptions, clauses)); -} - - -app* iuc_solver::def_manager::mk_proxy (expr *v) -{ - app* r; - if (m_expr2proxy.find(v, r)) - return r; - - ast_manager &m = m_parent.m; - app* proxy = m_parent.fresh_proxy (); - app* def = m.mk_or (m.mk_not (proxy), v); - m_defs.push_back (def); - m_expr2proxy.insert (v, proxy); - m_proxy2def.insert (proxy, def); - - m_parent.assert_expr (def); - return proxy; -} - -bool iuc_solver::def_manager::is_proxy (app *k, app_ref &def) -{ - app *r = nullptr; - bool found = m_proxy2def.find (k, r); - def = r; - return found; -} - -void iuc_solver::def_manager::reset () -{ - m_expr2proxy.reset (); - m_proxy2def.reset (); - m_defs.reset (); -} - -bool iuc_solver::def_manager::is_proxy_def (expr *v) -{ - // XXX This might not be the most robust way to check - return m_defs.contains (v); -} - -bool iuc_solver::is_proxy(expr *e, app_ref &def) -{ - if (!is_uninterp_const(e)) - return false; - - app* a = to_app (e); - - for (int i = m_defs.size (); i-- > 0; ) - if (m_defs[i].is_proxy (a, def)) - return true; - - return m_base_defs.is_proxy (a, def); -} - -void iuc_solver::collect_statistics (statistics &st) const -{ - m_solver.collect_statistics (st); - st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds()); - st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds()); - st.update ("time.iuc_solver.get_iuc.hyp_reduce2", m_hyp_reduce2_sw.get_seconds()); - st.update ("time.iuc_solver.get_iuc.learn_core", m_learn_core_sw.get_seconds()); - - st.update("iuc_solver.num_proxies", m_proxies.size()); -} - -void iuc_solver::reset_statistics () -{ - m_iuc_sw.reset(); - m_hyp_reduce1_sw.reset(); - m_hyp_reduce2_sw.reset(); - m_learn_core_sw.reset(); -} - -void iuc_solver::get_unsat_core (expr_ref_vector &core) { - m_solver.get_unsat_core (core); - undo_proxies_in_core (core); -} - -void iuc_solver::undo_proxies_in_core (expr_ref_vector &r) -{ - app_ref e(m); - expr_fast_mark1 bg; - for (unsigned i = 0; i < m_first_assumption; ++i) { - bg.mark(m_assumptions.get(i)); + app* iuc_solver::def_manager::mk_proxy (expr *v) { + app* r; + if (m_expr2proxy.find(v, r)) + return r; + + ast_manager &m = m_parent.m; + app* proxy = m_parent.fresh_proxy (); + app* def = m.mk_or (m.mk_not (proxy), v); + m_defs.push_back (def); + m_expr2proxy.insert (v, proxy); + m_proxy2def.insert (proxy, def); + + m_parent.assert_expr (def); + return proxy; } - // expand proxies - unsigned j = 0; - for (expr* rr : r) { - // skip background assumptions - if (bg.is_marked(rr)) - continue; + bool iuc_solver::def_manager::is_proxy (app *k, app_ref &def) { + app *r = nullptr; + bool found = m_proxy2def.find (k, r); + def = r; + return found; + } + + void iuc_solver::def_manager::reset () { + m_expr2proxy.reset (); + m_proxy2def.reset (); + m_defs.reset (); + } - // -- undo proxies, but only if they were introduced in check_sat - if (m_is_proxied && is_proxy(rr, e)) { - SASSERT (m.is_or (e)); - r[j++] = e->get_arg (1); + bool iuc_solver::def_manager::is_proxy_def (expr *v) { + // XXX This might not be the most robust way to check + return m_defs.contains (v); + } + + bool iuc_solver::is_proxy(expr *e, app_ref &def) { + if (!is_uninterp_const(e)) + return false; + + app* a = to_app (e); + + for (int i = m_defs.size (); i-- > 0; ) + if (m_defs[i].is_proxy (a, def)) + return true; + + return m_base_defs.is_proxy (a, def); + } + + void iuc_solver::collect_statistics (statistics &st) const { + m_solver.collect_statistics (st); + st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds()); + st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds()); + st.update ("time.iuc_solver.get_iuc.hyp_reduce2", m_hyp_reduce2_sw.get_seconds()); + st.update ("time.iuc_solver.get_iuc.learn_core", m_learn_core_sw.get_seconds()); + + st.update("iuc_solver.num_proxies", m_proxies.size()); + } + + void iuc_solver::reset_statistics () { + m_iuc_sw.reset(); + m_hyp_reduce1_sw.reset(); + m_hyp_reduce2_sw.reset(); + m_learn_core_sw.reset(); + } + + void iuc_solver::get_unsat_core (expr_ref_vector &core) { + m_solver.get_unsat_core (core); + undo_proxies_in_core (core); + } + + void iuc_solver::undo_proxies_in_core (expr_ref_vector &r) { + app_ref e(m); + expr_fast_mark1 bg; + for (unsigned i = 0; i < m_first_assumption; ++i) { + bg.mark(m_assumptions.get(i)); + } + + // expand proxies + unsigned j = 0; + for (expr* rr : r) { + // skip background assumptions + if (bg.is_marked(rr)) + continue; + + // -- undo proxies, but only if they were introduced in check_sat + if (m_is_proxied && is_proxy(rr, e)) { + SASSERT (m.is_or (e)); + r[j++] = e->get_arg (1); + } + else { + r[j++] = rr; + } + } + r.shrink (j); + } + + void iuc_solver::undo_proxies (expr_ref_vector &r) { + app_ref e(m); + // expand proxies + for (unsigned i = 0, sz = r.size (); i < sz; ++i) + if (is_proxy(r.get(i), e)) { + SASSERT (m.is_or (e)); + r[i] = e->get_arg (1); + } + } + + void iuc_solver::elim_proxies (expr_ref_vector &v) { + expr_ref f = mk_and (v); + scoped_ptr rep = mk_expr_simp_replacer (m); + rep->set_substitution (&m_elim_proxies_sub); + (*rep)(f); + v.reset(); + flatten_and(f, v); + } + + void iuc_solver::get_iuc(expr_ref_vector &core) { + scoped_watch _t_ (m_iuc_sw); + + typedef obj_hashtable expr_set; + expr_set core_lits; + for (unsigned i = m_first_assumption, sz = m_assumptions.size(); i < sz; ++i) { + expr *a = m_assumptions.get (i); + app_ref def(m); + if (is_proxy(a, def)) { core_lits.insert(def.get()); } + core_lits.insert (a); + } + + if (m_iuc == 0) { + // ORIGINAL PDR CODE + // AG: deprecated + proof_ref pr(m); + pr = get_proof (); + + farkas_learner learner_old; + learner_old.set_split_literals(m_split_literals); + + learner_old.get_lemmas (pr, core_lits, core); + elim_proxies (core); + simplify_bounds (core); // XXX potentially redundant } else { - r[j++] = rr; - } - } - r.shrink (j); -} - -void iuc_solver::undo_proxies (expr_ref_vector &r) -{ - app_ref e(m); - // expand proxies - for (unsigned i = 0, sz = r.size (); i < sz; ++i) - if (is_proxy(r.get(i), e)) { - SASSERT (m.is_or (e)); - r[i] = e->get_arg (1); - } -} - -void iuc_solver::elim_proxies (expr_ref_vector &v) -{ - expr_ref f = mk_and (v); - scoped_ptr rep = mk_expr_simp_replacer (m); - rep->set_substitution (&m_elim_proxies_sub); - (*rep)(f); - v.reset(); - flatten_and(f, v); -} - -void iuc_solver::get_iuc(expr_ref_vector &core) -{ - scoped_watch _t_ (m_iuc_sw); - - typedef obj_hashtable expr_set; - expr_set core_lits; - for (unsigned i = m_first_assumption, sz = m_assumptions.size(); i < sz; ++i) { - expr *a = m_assumptions.get (i); - app_ref def(m); - if (is_proxy(a, def)) { core_lits.insert(def.get()); } - core_lits.insert (a); - } - - if (m_iuc == 0) { - // ORIGINAL PDR CODE - // AG: deprecated - proof_ref pr(m); - pr = get_proof (); - - farkas_learner learner_old; - learner_old.set_split_literals(m_split_literals); - - learner_old.get_lemmas (pr, core_lits, core); - elim_proxies (core); - simplify_bounds (core); // XXX potentially redundant - } - else { - // NEW IUC - proof_ref res(get_proof(), m); - - // -- old hypothesis reducer while the new one is broken - if (m_old_hyp_reducer) { - scoped_watch _t_ (m_hyp_reduce1_sw); - // AG: deprecated - // pre-process proof in order to get a proof which is - // better suited for unsat-core-extraction - if (m_print_farkas_stats) { - iuc_proof iuc_before(m, res.get(), core_lits); - verbose_stream() << "\nOld reduce_hypotheses. Before:"; - iuc_before.dump_farkas_stats(); + // NEW IUC + proof_ref res(get_proof(), m); + + // -- old hypothesis reducer while the new one is broken + if (m_old_hyp_reducer) { + scoped_watch _t_ (m_hyp_reduce1_sw); + // AG: deprecated + // pre-process proof in order to get a proof which is + // better suited for unsat-core-extraction + if (m_print_farkas_stats) { + iuc_proof iuc_before(m, res.get(), core_lits); + verbose_stream() << "\nOld reduce_hypotheses. Before:"; + iuc_before.dump_farkas_stats(); + } + + proof_utils::reduce_hypotheses(res); + proof_utils::permute_unit_resolution(res); + + if (m_print_farkas_stats) { + iuc_proof iuc_after(m, res.get(), core_lits); + verbose_stream() << "Old reduce_hypothesis. After:"; + iuc_after.dump_farkas_stats(); + } } - - proof_utils::reduce_hypotheses(res); - proof_utils::permute_unit_resolution(res); - - if (m_print_farkas_stats) { - iuc_proof iuc_after(m, res.get(), core_lits); - verbose_stream() << "Old reduce_hypothesis. After:"; - iuc_after.dump_farkas_stats(); - } - } - // -- new hypothesis reducer - else - { + // -- new hypothesis reducer + else + { #if 0 - static unsigned bcnt = 0; + static unsigned bcnt = 0; + { + bcnt++; + TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";); + if (bcnt == 123) { + std::ofstream ofs; + ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot"); + iuc_proof iuc_pf_before(m, res.get(), core_lits); + iuc_pf_before.display_dot(ofs); + ofs.close(); + + proof_checker pc(m); + expr_ref_vector side(m); + ENSURE(pc.check(res, side)); + } + } +#endif + scoped_watch _t_ (m_hyp_reduce2_sw); + + // pre-process proof for better iuc extraction + if (m_print_farkas_stats) { + iuc_proof iuc_before(m, res.get(), core_lits); + verbose_stream() << "\n New hypothesis_reducer. Before:"; + iuc_before.dump_farkas_stats(); + } + + proof_ref pr1(m); + { + scoped_watch _t_ (m_hyp_reduce1_sw); + theory_axiom_reducer ta_reducer(m); + pr1 = ta_reducer.reduce (res.get()); + } + + proof_ref pr2(m); + { + scoped_watch _t_ (m_hyp_reduce2_sw); + hypothesis_reducer hyp_reducer(m); + pr2 = hyp_reducer.reduce(pr1); + } + + res = pr2; + + if (m_print_farkas_stats) { + iuc_proof iuc_after(m, res.get(), core_lits); + verbose_stream() << "New hypothesis_reducer. After:"; + iuc_after.dump_farkas_stats(); + } + } + + iuc_proof iuc_pf(m, res, core_lits); + +#if 0 + static unsigned cnt = 0; { - bcnt++; - TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";); - if (bcnt == 123) { + cnt++; + TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";); + if (cnt == 123) { std::ofstream ofs; - ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot"); - iuc_proof iuc_pf_before(m, res.get(), core_lits); - iuc_pf_before.display_dot(ofs); + ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot"); + iuc_pf.display_dot(ofs); ofs.close(); - proof_checker pc(m); expr_ref_vector side(m); ENSURE(pc.check(res, side)); } } #endif - scoped_watch _t_ (m_hyp_reduce2_sw); - - // pre-process proof for better iuc extraction - if (m_print_farkas_stats) { - iuc_proof iuc_before(m, res.get(), core_lits); - verbose_stream() << "\n New hypothesis_reducer. Before:"; - iuc_before.dump_farkas_stats(); + unsat_core_learner learner(m, iuc_pf); + + unsat_core_plugin* plugin; + // -- register iuc plugins + switch (m_iuc_arith) { + case 0: + case 1: + plugin = + alloc(unsat_core_plugin_farkas_lemma, + learner, m_split_literals, + (m_iuc_arith == 1) /* use constants from A */); + learner.register_plugin(plugin); + break; + case 2: + SASSERT(false && "Broken"); + plugin = alloc(unsat_core_plugin_farkas_lemma_optimized, learner, m); + learner.register_plugin(plugin); + break; + case 3: + plugin = alloc(unsat_core_plugin_farkas_lemma_bounded, learner, m); + learner.register_plugin(plugin); + break; + default: + UNREACHABLE(); + break; } - - proof_ref pr1(m); + + switch (m_iuc) { + case 1: + // -- iuc based on the lowest cut in the proof + plugin = alloc(unsat_core_plugin_lemma, learner); + learner.register_plugin(plugin); + break; + case 2: + // -- iuc based on the smallest cut in the proof + plugin = alloc(unsat_core_plugin_min_cut, learner, m); + learner.register_plugin(plugin); + break; + default: + UNREACHABLE(); + break; + } + { - scoped_watch _t_ (m_hyp_reduce1_sw); - theory_axiom_reducer ta_reducer(m); - pr1 = ta_reducer.reduce (res.get()); - } - - proof_ref pr2(m); - { - scoped_watch _t_ (m_hyp_reduce2_sw); - hypothesis_reducer hyp_reducer(m); - pr2 = hyp_reducer.reduce(pr1); - } - - res = pr2; - - if (m_print_farkas_stats) { - iuc_proof iuc_after(m, res.get(), core_lits); - verbose_stream() << "New hypothesis_reducer. After:"; - iuc_after.dump_farkas_stats(); + scoped_watch _t_ (m_learn_core_sw); + // compute interpolating unsat core + learner.compute_unsat_core(core); } + + elim_proxies (core); + // AG: this should be taken care of by minimizing the iuc cut + simplify_bounds (core); } - - iuc_proof iuc_pf(m, res, core_lits); - -#if 0 - static unsigned cnt = 0; - { - cnt++; - TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";); - if (cnt == 123) { - std::ofstream ofs; - ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot"); - iuc_pf.display_dot(ofs); - ofs.close(); - proof_checker pc(m); - expr_ref_vector side(m); - ENSURE(pc.check(res, side)); - } - } -#endif - unsat_core_learner learner(m, iuc_pf); - - unsat_core_plugin* plugin; - // -- register iuc plugins - switch (m_iuc_arith) { - case 0: - case 1: - plugin = - alloc(unsat_core_plugin_farkas_lemma, - learner, m_split_literals, - (m_iuc_arith == 1) /* use constants from A */); - learner.register_plugin(plugin); - break; - case 2: - SASSERT(false && "Broken"); - plugin = alloc(unsat_core_plugin_farkas_lemma_optimized, learner, m); - learner.register_plugin(plugin); - break; - case 3: - plugin = alloc(unsat_core_plugin_farkas_lemma_bounded, learner, m); - learner.register_plugin(plugin); - break; - default: - UNREACHABLE(); - break; - } - - switch (m_iuc) { - case 1: - // -- iuc based on the lowest cut in the proof - plugin = alloc(unsat_core_plugin_lemma, learner); - learner.register_plugin(plugin); - break; - case 2: - // -- iuc based on the smallest cut in the proof - plugin = alloc(unsat_core_plugin_min_cut, learner, m); - learner.register_plugin(plugin); - break; - default: - UNREACHABLE(); - break; - } - - { - scoped_watch _t_ (m_learn_core_sw); - // compute interpolating unsat core - learner.compute_unsat_core(core); - } - - elim_proxies (core); - // AG: this should be taken care of by minimizing the iuc cut - simplify_bounds (core); + + IF_VERBOSE(2, + verbose_stream () << "IUC Core:\n" << core << "\n";); } - - IF_VERBOSE(2, - verbose_stream () << "IUC Core:\n" << core << "\n";); -} - -void iuc_solver::refresh () -{ - // only refresh in non-pushed state - SASSERT (m_defs.empty()); - expr_ref_vector assertions (m); - for (unsigned i = 0, e = m_solver.get_num_assertions(); i < e; ++i) { - expr* a = m_solver.get_assertion (i); - if (!m_base_defs.is_proxy_def(a)) { assertions.push_back(a); } - + + void iuc_solver::refresh () { + // only refresh in non-pushed state + SASSERT (m_defs.empty()); + expr_ref_vector assertions (m); + for (unsigned i = 0, e = m_solver.get_num_assertions(); i < e; ++i) { + expr* a = m_solver.get_assertion (i); + if (!m_base_defs.is_proxy_def(a)) { assertions.push_back(a); } + + } + m_base_defs.reset (); + NOT_IMPLEMENTED_YET (); + // solver interface does not have a reset method. need to introduce it somewhere. + // m_solver.reset (); + for (unsigned i = 0, e = assertions.size (); i < e; ++i) + { m_solver.assert_expr(assertions.get(i)); } } - m_base_defs.reset (); - NOT_IMPLEMENTED_YET (); - // solver interface does not have a reset method. need to introduce it somewhere. - // m_solver.reset (); - for (unsigned i = 0, e = assertions.size (); i < e; ++i) - { m_solver.assert_expr(assertions.get(i)); } -} - + } diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index c0a0072ed..a51bfbef9 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -127,7 +127,7 @@ public: void pop(unsigned n) override; unsigned get_scope_level() const override { return m_solver.get_scope_level(); } - lbool check_sat(unsigned num_assumptions, expr * const *assumptions) override; + lbool check_sat_core(unsigned num_assumptions, expr * const *assumptions) override; lbool check_sat_cc(const expr_ref_vector &cube, vector const & clauses) override; void set_progress_callback(progress_callback *callback) override { m_solver.set_progress_callback(callback); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index e61a02d80..78851f5cb 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -158,7 +158,7 @@ namespace opt { return m_dump_benchmarks; } - lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + lbool opt_solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) { TRACE("opt_verbose", { tout << "context size: " << m_context.size() << "\n"; for (unsigned i = 0; i < m_context.size(); ++i) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 39562ec54..8d2abdb93 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -95,7 +95,7 @@ namespace opt { void assert_expr_core(expr * t) override; void push_core() override; void pop_core(unsigned n) override; - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override; + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override; void get_unsat_core(expr_ref_vector & r) override; void get_model_core(model_ref & _m) override; proof * get_proof() override; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 8823c40c5..34348f0fc 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -166,7 +166,7 @@ public: (m.is_not(e, e) && is_uninterp_const(e)); } - lbool check_sat(unsigned sz, expr * const * assumptions) override { + lbool check_sat_core(unsigned sz, expr * const * assumptions) override { m_solver.pop_to_base_level(); m_core.reset(); if (m_solver.inconsistent()) return l_false; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 48f6053fc..5d32d1bed 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -185,7 +185,7 @@ namespace smt { m_context.pop(n); } - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override { + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";); return m_context.check(num_assumptions, assumptions); } diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt index c8e206f7f..281a34018 100644 --- a/src/solver/CMakeLists.txt +++ b/src/solver/CMakeLists.txt @@ -16,5 +16,7 @@ z3_add_component(solver PYG_FILES combined_solver_params.pyg parallel_params.pyg + PYG_FILES + solver_params.pyg ) diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index e8fb34815..813b2be18 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -218,7 +218,7 @@ public: return l_undef; } - lbool check_sat(unsigned num_assumptions, expr * const * assumptions) override { + lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override { m_check_sat_executed = true; m_use_solver1_results = false; @@ -227,13 +227,13 @@ public: m_ignore_solver1) { // must use incremental solver switch_inc_mode(); - return m_solver2->check_sat(num_assumptions, assumptions); + return m_solver2->check_sat_core(num_assumptions, assumptions); } if (m_inc_mode) { if (m_inc_timeout == UINT_MAX) { IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";); - lbool r = m_solver2->check_sat(num_assumptions, assumptions); + lbool r = m_solver2->check_sat_core(num_assumptions, assumptions); if (r != l_undef || !use_solver1_when_undef() || get_manager().canceled()) { return r; } @@ -244,7 +244,7 @@ public: lbool r = l_undef; try { scoped_timer timer(m_inc_timeout, &eh); - r = m_solver2->check_sat(num_assumptions, assumptions); + r = m_solver2->check_sat_core(num_assumptions, assumptions); } catch (z3_exception&) { if (!eh.m_canceled) { @@ -260,7 +260,7 @@ public: IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";); m_use_solver1_results = true; - return m_solver1->check_sat(num_assumptions, assumptions); + return m_solver1->check_sat_core(num_assumptions, assumptions); } void set_progress_callback(progress_callback * callback) override { diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index f3c533704..6f4880d38 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -3,7 +3,7 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - solver.h + solver.cpp Abstract: @@ -21,25 +21,25 @@ Notes: #include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/ast_pp_util.h" +#include "ast/display_dimacs.h" #include "tactic/model_converter.h" #include "solver/solver.h" +#include "solver/solver_params.hpp" #include "model/model_evaluator.h" unsigned solver::get_num_assertions() const { - NOT_IMPLEMENTED_YET(); + UNREACHABLE(); return 0; } expr * solver::get_assertion(unsigned idx) const { - NOT_IMPLEMENTED_YET(); + UNREACHABLE(); return nullptr; } std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assumptions) const { expr_ref_vector fmls(get_manager()); - stopwatch sw; - sw.start(); get_assertions(fmls); ast_pp_util visitor(get_manager()); model_converter_ref mc = get_model_converter(); @@ -57,6 +57,12 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum return out; } +std::ostream& solver::display_dimacs(std::ostream& out) const { + expr_ref_vector fmls(get_manager()); + get_assertions(fmls); + return ::display_dimacs(out, fmls); +} + void solver::get_assertions(expr_ref_vector& fmls) const { unsigned sz = get_num_assertions(); for (unsigned i = 0; i < sz; ++i) { @@ -232,12 +238,16 @@ void solver::collect_param_descrs(param_descrs & r) { void solver::reset_params(params_ref const & p) { m_params = p; - m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false); + solver_params sp(m_params); + m_enforce_model_conversion = sp.enforce_model_conversion(); + m_cancel_backup_file = sp.cancel_backup_file(); } void solver::updt_params(params_ref const & p) { m_params.copy(p); - m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false); + solver_params sp(m_params); + m_enforce_model_conversion = sp.enforce_model_conversion(); + m_cancel_backup_file = sp.cancel_backup_file(); } @@ -309,3 +319,28 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { } return result; } + +lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) { + lbool r = l_undef; + try { + r = check_sat_core(num_assumptions, assumptions); + } + catch (...) { + if (get_manager().canceled()) { + dump_state(num_assumptions, assumptions); + } + throw; + } + if (r == l_undef && get_manager().canceled()) { + dump_state(num_assumptions, assumptions); + } + return r; +} + +void solver::dump_state(unsigned sz, expr* const* assumptions) { + std::string file = m_cancel_backup_file.str(); + if (file != "") { + std::ofstream ous(file); + display(ous, sz, assumptions); + } +} diff --git a/src/solver/solver.h b/src/solver/solver.h index 7437a5a08..161677cb5 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -44,8 +44,9 @@ public: - results based on check_sat_result API */ class solver : public check_sat_result { - params_ref m_params; - bool m_enforce_model_conversion; + params_ref m_params; + bool m_enforce_model_conversion; + symbol m_cancel_backup_file; public: solver(): m_enforce_model_conversion(false) {} ~solver() override {} @@ -140,7 +141,8 @@ public: If it is unsatisfiable, and unsat-core generation is enabled. Then, the unsat-core is a subset of these assumptions. */ - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0; + + lbool check_sat(unsigned num_assumptions, expr * const * assumptions); lbool check_sat(expr_ref_vector const& asms) { return check_sat(asms.size(), asms.c_ptr()); } @@ -227,6 +229,11 @@ public: */ virtual std::ostream& display(std::ostream & out, unsigned n = 0, expr* const* assumptions = nullptr) const; + /** + \brief Display the content of this solver in DIMACS format + */ + std::ostream& display_dimacs(std::ostream & out) const; + /** \brief expose model converter when solver produces partially reduced set of assertions. */ @@ -249,14 +256,17 @@ public: void disable_pop() { m_nopop = true; } }; + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0; protected: virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences); + void dump_state(unsigned sz, expr* const* assumptions); bool is_literal(ast_manager& m, expr* e); + }; typedef ref solver_ref; diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index a3fcd0e0b..6173dfddf 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -61,10 +61,10 @@ struct append_assumptions { } }; -lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) { +lbool solver_na2as::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { append_assumptions app(m_assumptions, num_assumptions, assumptions); TRACE("solver_na2as", display(tout);); - return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr()); + return check_sat_core2(m_assumptions.size(), m_assumptions.c_ptr()); } lbool solver_na2as::check_sat_cc(const expr_ref_vector &assumptions, vector const &clauses) { diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index d1515a206..67ec004cc 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -35,10 +35,9 @@ public: ~solver_na2as() override; void assert_expr_core2(expr * t, expr * a) override; - // virtual void assert_expr_core(expr * t) = 0; // Subclasses of solver_na2as should redefine the following *_core methods instead of these ones. - lbool check_sat(unsigned num_assumptions, expr * const * assumptions) override; + lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override; lbool check_sat_cc(const expr_ref_vector &assumptions, vector const &clauses) override; void push() override; void pop(unsigned n) override; @@ -49,7 +48,7 @@ public: lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override; lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override; protected: - virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0; + virtual lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) = 0; virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, vector const &clauses) { NOT_IMPLEMENTED_YET(); } virtual void push_core() = 0; virtual void pop_core(unsigned n) = 0; diff --git a/src/solver/solver_params.pyg b/src/solver/solver_params.pyg new file mode 100644 index 000000000..29690a164 --- /dev/null +++ b/src/solver/solver_params.pyg @@ -0,0 +1,8 @@ + +def_module_params('solver', + description='solver parameters', + export=True, + params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"), + ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"), + )) + diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 598bb6c02..0495e8a3d 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -119,7 +119,7 @@ public: } } - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override { + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { SASSERT(!m_pushed || get_scope_level() > 0); m_proof.reset(); scoped_watch _t_(m_pool.m_check_watch); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 492ddd443..298ed9bc5 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -62,7 +62,7 @@ public: void push_core() override; void pop_core(unsigned n) override; - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override; + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override; void collect_statistics(statistics & st) const override; void get_unsat_core(expr_ref_vector & r) override; @@ -136,7 +136,7 @@ void tactic2solver::pop_core(unsigned n) { m_result = nullptr; } -lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { +lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) { if (m_tactic.get() == nullptr) return l_false; ast_manager & m = m_assertions.m(); diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index 8791a6282..45d1344ba 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -137,9 +137,9 @@ public: } } - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override { + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { flush_assertions(); - return m_solver->check_sat(num_assumptions, assumptions); + return m_solver->check_sat_core(num_assumptions, assumptions); } void updt_params(params_ref const & p) override { solver::updt_params(p); m_solver->updt_params(p); } diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 185f23d13..b9a564542 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -78,9 +78,9 @@ public: m_rewriter.pop(n); } - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override { + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { m_solver->updt_params(get_params()); - return m_solver->check_sat(num_assumptions, assumptions); + return m_solver->check_sat_core(num_assumptions, assumptions); } void updt_params(params_ref const & p) override { solver::updt_params(p); m_solver->updt_params(p); } diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp index fd4fb8e73..b3620c8ec 100644 --- a/src/tactic/fd_solver/pb2bv_solver.cpp +++ b/src/tactic/fd_solver/pb2bv_solver.cpp @@ -75,9 +75,9 @@ public: m_rewriter.pop(n); } - lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override { + lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { flush_assertions(); - return m_solver->check_sat(num_assumptions, assumptions); + return m_solver->check_sat_core(num_assumptions, assumptions); } void updt_params(params_ref const & p) override { solver::updt_params(p); m_rewriter.updt_params(p); m_solver->updt_params(p); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 8f8b86a65..c2d93fa2a 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -20,6 +20,7 @@ Revision History: #include "ast/ast_smt2_pp.h" #include "ast/for_each_expr.h" #include "ast/well_sorted.h" +#include "ast/display_dimacs.h" #include "tactic/goal.h" goal::precision goal::mk_union(precision p1, precision p2) { @@ -262,14 +263,14 @@ void goal::assert_expr(expr * f, expr_dependency * d) { assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : nullptr, d); } -void goal::get_formulas(ptr_vector & result) { +void goal::get_formulas(ptr_vector & result) const { unsigned sz = size(); for (unsigned i = 0; i < sz; i++) { result.push_back(form(i)); } } -void goal::get_formulas(expr_ref_vector & result) { +void goal::get_formulas(expr_ref_vector & result) const { unsigned sz = size(); for (unsigned i = 0; i < sz; i++) { result.push_back(form(i)); @@ -434,63 +435,9 @@ void goal::display_ll(std::ostream & out) const { \brief Assumes that the formula is already in CNF. */ void goal::display_dimacs(std::ostream & out) const { - unsigned_vector expr2var; - ptr_vector exprs; - unsigned num_vars = 0; - unsigned num_cls = size(); - for (unsigned i = 0; i < num_cls; i++) { - expr * f = form(i); - unsigned num_lits; - expr * const * lits; - if (m().is_or(f)) { - num_lits = to_app(f)->get_num_args(); - lits = to_app(f)->get_args(); - } - else { - num_lits = 1; - lits = &f; - } - for (unsigned j = 0; j < num_lits; j++) { - expr * l = lits[j]; - if (m().is_not(l)) - l = to_app(l)->get_arg(0); - if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { - num_vars++; - expr2var.setx(l->get_id(), num_vars, UINT_MAX); - exprs.setx(l->get_id(), l, nullptr); - } - } - } - out << "p cnf " << num_vars << " " << num_cls << "\n"; - for (unsigned i = 0; i < num_cls; i++) { - expr * f = form(i); - unsigned num_lits; - expr * const * lits; - if (m().is_or(f)) { - num_lits = to_app(f)->get_num_args(); - lits = to_app(f)->get_args(); - } - else { - num_lits = 1; - lits = &f; - } - for (unsigned j = 0; j < num_lits; j++) { - expr * l = lits[j]; - if (m().is_not(l)) { - out << "-"; - l = to_app(l)->get_arg(0); - } - SASSERT(exprs[l->get_id()]); - out << expr2var[l->get_id()] << " "; - } - out << "0\n"; - } - for (expr* e : exprs) { - if (e && is_app(e)) { - symbol const& n = to_app(e)->get_decl()->get_name(); - out << "c " << expr2var[e->get_id()] << " " << n << "\n"; - } - } + expr_ref_vector fmls(m()); + get_formulas(fmls); + ::display_dimacs(out, fmls); } unsigned goal::num_exprs() const { diff --git a/src/tactic/goal.h b/src/tactic/goal.h index fa2f16eb6..33f9298ab 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -126,8 +126,8 @@ public: void update(unsigned i, expr * f, proof * pr = nullptr, expr_dependency * dep = nullptr); - void get_formulas(ptr_vector & result); - void get_formulas(expr_ref_vector & result); + void get_formulas(ptr_vector & result) const; + void get_formulas(expr_ref_vector & result) const; void elim_true(); void elim_redundancies(); diff --git a/src/util/chashtable.h b/src/util/chashtable.h index e49ac3bd4..19ff1ef51 100644 --- a/src/util/chashtable.h +++ b/src/util/chashtable.h @@ -32,6 +32,7 @@ Revision History: #include "util/debug.h" #include "util/trace.h" #include "util/tptr.h" +#include "util/util.h" #ifdef Z3DEBUG #include "util/hashtable.h" #endif From 8da1d6070b1d8287330b066ceb77a817a51b0d8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Jan 2019 14:00:56 -0800 Subject: [PATCH 09/12] throttle big-reductions #2101 #2098 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 16 ++++++++++++++++ src/sat/sat_big.cpp | 2 +- src/sat/sat_scc.cpp | 8 ++++---- 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9847e4264..a307df4bb 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -518,6 +518,12 @@ namespace z3 { sort(context & c, Z3_ast a):ast(c, a) {} sort(sort const & s):ast(s) {} operator Z3_sort() const { return reinterpret_cast(m_ast); } + + /** + \brief retrieve unique identifier for func_decl. + */ + unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; } + /** \brief Return true if this sort and \c s are equal. */ @@ -615,6 +621,11 @@ namespace z3 { operator Z3_func_decl() const { return reinterpret_cast(m_ast); } func_decl & operator=(func_decl const & s) { return static_cast(ast::operator=(s)); } + /** + \brief retrieve unique identifier for func_decl. + */ + unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; } + unsigned arity() const { return Z3_get_arity(ctx(), *this); } sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); } sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); } @@ -771,6 +782,11 @@ namespace z3 { return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision)); } + /** + \brief retrieve unique identifier for expression. + */ + unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; } + /** \brief Return int value of numeral, throw if result cannot fit in machine int diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 1aa923f1f..833c83820 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -172,6 +172,7 @@ namespace sat { void big::add_del(literal u, literal v) { if (u.index() > v.index()) std::swap(u, v); + m_del_bin[u.index()].push_back(v); } @@ -210,7 +211,6 @@ namespace sat { } wlist.set_end(itprev); } - s.propagate(false); return elim; } diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index e2d05385b..52641736a 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -244,10 +244,10 @@ namespace sat { } void scc::reduce_tr() { - unsigned quota = 0, num_reduced = 0; - while ((num_reduced = reduce_tr(false)) > quota) { quota = std::max(100u, num_reduced / 2); } - quota = 0; - while ((num_reduced = reduce_tr(true)) > quota) { quota = std::max(100u, num_reduced / 2); } + unsigned quota = 0, num_reduced = 0, count = 0; + while ((num_reduced = reduce_tr(false)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); } + quota = 0; count = 0; + while ((num_reduced = reduce_tr(true)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); } } void scc::collect_statistics(statistics & st) const { From ad81fee118628fbe0ace97865948ff9b8cbc8df7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Jan 2019 19:26:44 -0800 Subject: [PATCH 10/12] adding maxlex, throttle use of asymmetric literal addition Signed-off-by: Nikolaj Bjorner --- src/opt/CMakeLists.txt | 1 + src/opt/maxlex.cpp | 185 +++++++++++++++++++++++++++++++++++++ src/opt/maxlex.h | 32 +++++++ src/opt/maxres.cpp | 8 +- src/opt/maxsmt.cpp | 22 +++-- src/opt/maxsmt.h | 13 ++- src/opt/sortmax.cpp | 2 +- src/opt/wmax.cpp | 2 +- src/sat/sat_simplifier.cpp | 36 ++++++-- 9 files changed, 274 insertions(+), 27 deletions(-) create mode 100644 src/opt/maxlex.cpp create mode 100644 src/opt/maxlex.h diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt index dcb13c062..fb61c0c33 100644 --- a/src/opt/CMakeLists.txt +++ b/src/opt/CMakeLists.txt @@ -1,5 +1,6 @@ z3_add_component(opt SOURCES + maxlex.cpp maxres.cpp maxsmt.cpp opt_cmds.cpp diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp new file mode 100644 index 000000000..3cf9cea5a --- /dev/null +++ b/src/opt/maxlex.cpp @@ -0,0 +1,185 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + maxlex.cpp + +Abstract: + + MaxLex solves weighted max-sat problems where weights impose lexicographic order. + MaxSAT is particularly easy for this class: + In order of highest weight, check if soft constraint can be satisfied. + If so, assert it, otherwise assert the negation and record whether the soft + constraint is true or false in the solution. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-25-1 + +--*/ + +#include "opt/opt_context.h" +#include "opt/maxsmt.h" +#include "opt/maxlex.h" + +namespace opt { + + bool is_maxlex(weights_t & _ws) { + vector ws(_ws); + std::sort(ws.begin(), ws.end()); + ws.reverse(); + rational sum(0); + for (rational const& w : ws) { + sum += w; + } + for (rational const& w : ws) { + if (sum > w + w) return false; + sum -= w; + } + return true; + } + + class maxlex : public maxsmt_solver_base { + + struct cmp_soft { + bool operator()(soft const& s1, soft const& s2) const { + return s1.weight > s2.weight; + } + }; + + ast_manager& m; + maxsat_context& m_c; + + void update_assignment() { + model_ref mdl; + s().get_model(mdl); + if (mdl) { + m_c.model_updated(mdl.get()); + update_assignment(mdl); + } + } + + void assert_value(soft& soft) { + switch (soft.value) { + case l_true: + s().assert_expr(soft.s); + break; + case l_false: + s().assert_expr(expr_ref(m.mk_not(soft.s), m)); + break; + default: + break; + } + } + + void set_value(soft& soft, lbool v) { + soft.set_value(v); + assert_value(soft); + } + + void update_assignment(model_ref & mdl) { + for (auto & soft : m_soft) { + switch (soft.value) { + case l_undef: + if (mdl->is_true(soft.s)) { + set_value(soft, l_true); + } + else { + update_bounds(); + return; + } + break; + case l_true: + break; + case l_false: + break; + } + } + update_bounds(); + } + + void update_bounds() { + m_lower.reset(); + m_upper.reset(); + bool prefix_defined = true; + for (auto & soft : m_soft) { + if (!prefix_defined) { + m_upper += soft.weight; + continue; + } + switch (soft.value) { + case l_undef: + prefix_defined = false; + m_upper += soft.weight; + break; + case l_true: + break; + case l_false: + m_lower += soft.weight; + m_upper += soft.weight; + break; + } + } + trace_bounds("maxlex"); + } + + void init() { + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl); + } + + public: + + maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s): + maxsmt_solver_base(c, ws, s), + m(c.get_manager()), + m_c(c) { + cmp_soft cmp; + std::sort(m_soft.begin(), m_soft.end(), cmp); + } + + + lbool operator()() override { + init(); + + for (auto & soft : m_soft) { + if (soft.value == l_true) { + continue; + } + SASSERT(soft.value() == l_undef); + expr* a = soft.s; + lbool is_sat = s().check_sat(1, &a); + switch (is_sat) { + case l_false: + set_value(soft, l_false); + update_bounds(); + break; + case l_true: + update_assignment(); + SASSERT(soft.value == l_true); + break; + case l_undef: + return l_undef; + } + } + return l_true; + } + + void commit_assignment() override { + for (auto & soft : m_soft) { + if (soft.value == l_undef) { + return; + } + assert_value(soft); + } + } + + }; + + maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) { + return alloc(maxlex, c, id, ws, soft); + } + +} diff --git a/src/opt/maxlex.h b/src/opt/maxlex.h new file mode 100644 index 000000000..55aab76d3 --- /dev/null +++ b/src/opt/maxlex.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + maxlex.h + +Abstract: + + MaxLex solves weighted max-sat problems where weights impose lexicographic order. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-25-1 + +Notes: + +--*/ + +#ifndef MAXLEX_H_ +#define MAXLEX_H_ + +namespace opt { + + bool is_maxlex(weights_t & ws); + + maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft); + + +}; + +#endif diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index b507d6f54..789aaf8db 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -329,8 +329,8 @@ public: verify_assumptions(); m_lower.reset(); for (soft& s : m_soft) { - s.is_true = m_model->is_true(s.s); - if (!s.is_true) { + s.set_value(m_model->is_true(s.s)); + if (!s.is_true()) { m_lower += s.weight; } } @@ -764,7 +764,7 @@ public: TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;); for (soft& s : m_soft) { - s.is_true = m_model->is_true(s.s); + s.set_value(m_model->is_true(s.s)); } verify_assignment(); @@ -878,7 +878,7 @@ public: expr_ref n(m); for (soft& s : m_soft) { n = s.s; - if (!s.is_true) { + if (!s.is_true()) { n = mk_not(m, n); } _solver->assert_expr(n); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index dc4451b6c..329e7979c 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -18,17 +18,18 @@ Notes: --*/ #include +#include "util/uint_set.h" +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/pb_decl_plugin.h" #include "opt/maxsmt.h" #include "opt/maxres.h" +#include "opt/maxlex.h" #include "opt/wmax.h" #include "opt/opt_params.hpp" -#include "ast/ast_pp.h" -#include "util/uint_set.h" #include "opt/opt_context.h" #include "smt/theory_wmaxsat.h" #include "smt/theory_pb.h" -#include "ast/ast_util.h" -#include "ast/pb_decl_plugin.h" namespace opt { @@ -61,7 +62,7 @@ namespace opt { rational k(0), cost(0); vector weights; for (soft const& s : m_soft) { - if (s.is_true) { + if (s.is_true()) { k += s.weight; } else { @@ -80,13 +81,13 @@ namespace opt { m_lower.reset(); m_upper.reset(); for (soft& s : m_soft) { - s.is_true = m.is_true(s.s); - if (!s.is_true) m_upper += s.weight; + s.set_value(m.is_true(s.s)); + if (!s.is_true()) m_upper += s.weight; } TRACE("opt", tout << "upper: " << m_upper << " assignments: "; - for (soft& s : m_soft) tout << (s.is_true?"T":"F"); + for (soft& s : m_soft) tout << (s.is_true()?"T":"F"); tout << "\n";); return true; } @@ -234,7 +235,10 @@ namespace opt { symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";); - if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { + if (is_maxlex(m_weights)) { + m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints); + } + else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); } else if (maxsat_engine == symbol("pd-maxres")) { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index b61d876b3..796510ce2 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -59,10 +59,13 @@ namespace opt { struct soft { expr_ref s; rational weight; - bool is_true; - soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), is_true(t) {} - soft(soft const& other):s(other.s), weight(other.weight), is_true(other.is_true) {} - soft& operator=(soft const& other) { s = other.s; weight = other.weight; is_true = other.is_true; return *this; } + lbool value; + void set_value(bool t) { value = t?l_true:l_undef; } + void set_value(lbool t) { value = t; } + bool is_true() const { return value == l_true; } + soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {} + soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {} + soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; } }; ast_manager& m; maxsat_context& m_c; @@ -84,7 +87,7 @@ namespace opt { ~maxsmt_solver_base() override {} rational get_lower() const override { return m_lower; } rational get_upper() const override { return m_upper; } - bool get_assignment(unsigned index) const override { return m_soft[index].is_true; } + bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); } void collect_statistics(statistics& st) const override { } void get_model(model_ref& mdl, svector& labels) override { mdl = m_model.get(); labels = m_labels;} virtual void commit_assignment(); diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index df361f24a..1a19032e2 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -114,7 +114,7 @@ namespace opt { } void update_assignment() { - for (soft& s : m_soft) s.is_true = is_true(s.s); + for (soft& s : m_soft) s.set_value(is_true(s.s)); } bool is_true(expr* e) { diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index aa539bc44..9fb683179 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -122,7 +122,7 @@ namespace opt { } void update_assignment() { - for (soft& s : m_soft) s.is_true = is_true(s.s); + for (soft& s : m_soft) s.set_value(is_true(s.s)); } struct compare_asm { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 465618c5f..96b1588a2 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1014,6 +1014,9 @@ namespace sat { svector m_in_intersection; unsigned m_ala_qhead; clause_wrapper m_clause; + unsigned m_ala_cost; + unsigned m_ala_benefit; + unsigned m_ala_max_cost; blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l, vector & wlist): @@ -1021,8 +1024,11 @@ namespace sat { m_counter(limit), m_mc(_mc), m_queue(l, wlist), - m_clause(null_literal, null_literal) { + m_clause(null_literal, null_literal), + m_ala_cost(0), + m_ala_benefit(0) { m_in_intersection.resize(s.s.num_vars() * 2, false); + m_ala_max_cost = (s.s.m_clauses.size() * s.m_num_calls)/5; } void insert(literal l) { @@ -1034,6 +1040,10 @@ namespace sat { return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef; } + bool reached_max_cost() { + return m_ala_benefit <= m_ala_cost * 100 && m_ala_cost > m_ala_max_cost; + } + enum elim_type { bce_t, cce_t, @@ -1296,13 +1306,15 @@ namespace sat { */ bool add_ala() { unsigned init_size = m_covered_clause.size(); - for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) { + for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size && !reached_max_cost(); ++m_ala_qhead) { + ++m_ala_cost; literal l = m_covered_clause[m_ala_qhead]; for (watched & w : s.get_wlist(~l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); if (revisit_binary(l, lit)) continue; if (s.is_marked(lit)) { + ++m_ala_benefit; return true; } if (!s.is_marked(~lit)) { @@ -1333,6 +1345,7 @@ namespace sat { } if (!ok) continue; if (lit1 == null_literal) { + ++m_ala_benefit; return true; } m_covered_clause.push_back(~lit1); @@ -1504,7 +1517,9 @@ namespace sat { template void cce_binary() { - while (!m_queue.empty() && m_counter >= 0) { + m_ala_cost = 0; + m_ala_benefit = 0; + while (!m_queue.empty() && m_counter >= 0 && !reached_max_cost()) { s.checkpoint(); process_cce_binary(m_queue.next()); } @@ -1516,7 +1531,7 @@ namespace sat { watch_list & wlist = s.get_wlist(~l); m_counter -= wlist.size(); model_converter::kind k; - for (watched & w : wlist) { + for (watched& w : wlist) { if (!w.is_binary_non_learned_clause()) continue; if (!select_clause(2)) continue; literal l2 = w.get_literal(); @@ -1543,9 +1558,13 @@ namespace sat { template void cce_clauses() { literal blocked; + m_ala_cost = 0; + m_ala_benefit = 0; model_converter::kind k; - for (clause* cp : s.s.m_clauses) { - clause& c = *cp; + unsigned start = s.s.m_rand(); + unsigned sz = s.s.m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + clause& c = *s.s.m_clauses[(i + start) % sz]; if (c.was_removed() || c.is_learned()) continue; if (!select_clause(c.size())) continue; elim_type r = cce(c, blocked, k); @@ -1563,7 +1582,10 @@ namespace sat { break; } s.checkpoint(); - } + if (reached_max_cost()) { + break; + } + } } void inc_bc(elim_type et) { From b4f4a1f316772c1bb18ba414127c242d01b493d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Jan 2019 19:47:50 -0800 Subject: [PATCH 11/12] adding maxlex, throttle use of asymmetric literal addition Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 3cf9cea5a..89cebaa37 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -55,6 +55,7 @@ namespace opt { model_ref mdl; s().get_model(mdl); if (mdl) { + m_model = mdl; m_c.model_updated(mdl.get()); update_assignment(mdl); } @@ -79,16 +80,16 @@ namespace opt { } void update_assignment(model_ref & mdl) { + bool prefix_defined = true; for (auto & soft : m_soft) { + if (!prefix_defined) { + set_value(soft, l_undef); + continue; + } switch (soft.value) { case l_undef: - if (mdl->is_true(soft.s)) { - set_value(soft, l_true); - } - else { - update_bounds(); - return; - } + prefix_defined = mdl->is_true(soft.s); + set_value(soft, prefix_defined ? l_true : l_undef); break; case l_true: break; @@ -127,19 +128,20 @@ namespace opt { void init() { model_ref mdl; s().get_model(mdl); - update_assignment(mdl); + update_assignment(mdl); } + public: maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s): maxsmt_solver_base(c, ws, s), m(c.get_manager()), m_c(c) { + // ensure that soft constraints are sorted with largest soft constraints first. cmp_soft cmp; std::sort(m_soft.begin(), m_soft.end(), cmp); - } - + } lbool operator()() override { init(); @@ -167,6 +169,7 @@ namespace opt { return l_true; } + void commit_assignment() override { for (auto & soft : m_soft) { if (soft.value == l_undef) { @@ -175,7 +178,6 @@ namespace opt { assert_value(soft); } } - }; maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) { From d3d392da41c5e3e3bd51de3c5cb2b5265b4ef273 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Jan 2019 21:36:40 -0800 Subject: [PATCH 12/12] adding maxlex, delay mk_true() calls in goal2sat Signed-off-by: Nikolaj Bjorner --- src/opt/maxlex.cpp | 115 +++++++++++++++++++++++++++++++----- src/sat/tactic/goal2sat.cpp | 1 - 2 files changed, 100 insertions(+), 16 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 89cebaa37..1604db161 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -26,6 +26,10 @@ Author: namespace opt { bool is_maxlex(weights_t & _ws) { + // disable for now +#if true + return false; +#else vector ws(_ws); std::sort(ws.begin(), ws.end()); ws.reverse(); @@ -38,6 +42,7 @@ namespace opt { sum -= w; } return true; +#endif } class maxlex : public maxsmt_solver_base { @@ -131,21 +136,7 @@ namespace opt { update_assignment(mdl); } - - public: - - maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s): - maxsmt_solver_base(c, ws, s), - m(c.get_manager()), - m_c(c) { - // ensure that soft constraints are sorted with largest soft constraints first. - cmp_soft cmp; - std::sort(m_soft.begin(), m_soft.end(), cmp); - } - - lbool operator()() override { - init(); - + lbool maxlex1() { for (auto & soft : m_soft) { if (soft.value == l_true) { continue; @@ -169,6 +160,100 @@ namespace opt { return l_true; } + // try two literals per round. + // doesn't seem to make a difference based on sample test. + lbool maxlex2() { + unsigned sz = m_soft.size(); + for (unsigned i = 0; i < sz; ++i) { + auto& soft = m_soft[i]; + if (soft.value != l_undef) { + continue; + } + SASSERT(soft.value() == l_undef); + if (i + 1 == sz) { + expr* a = soft.s; + lbool is_sat = s().check_sat(1, &a); + switch (is_sat) { + case l_false: + set_value(soft, l_false); + update_bounds(); + break; + case l_true: + update_assignment(); + SASSERT(soft.value == l_true); + break; + case l_undef: + return l_undef; + } + } + else { + auto& soft2 = m_soft[i+1]; + expr_ref_vector core(m); + expr* a = soft.s; + expr* b = soft2.s; + expr* asms[2] = { a, b }; + lbool is_sat = s().check_sat(2, asms); + switch (is_sat) { + case l_true: + update_assignment(); + SASSERT(soft.value == l_true); + SASSERT(soft2.value == l_true); + break; + case l_false: + s().get_unsat_core(core); + if (core.contains(b)) { + expr_ref not_b(mk_not(m, b), m); + asms[1] = not_b; + switch (s().check_sat(2, asms)) { + case l_true: + // a, b is unsat, a, not b is sat. + set_value(soft2, l_false); + update_assignment(); + SASSERT(soft.value == l_true); + SASSERT(soft2.value == l_false); + break; + case l_false: + // a, b is unsat, a, not b is unsat -> a is unsat + // b is unsat, a, not b is unsat -> not a, not b + set_value(soft, l_false); + if (!core.contains(a)) { + set_value(soft2, l_false); + } + update_bounds(); + break; + case l_undef: + return l_undef; + } + } + else { + set_value(soft, l_false); + update_bounds(); + } + break; + case l_undef: + return l_undef; + } + } + } + return l_true; + } + + public: + + maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s): + maxsmt_solver_base(c, ws, s), + m(c.get_manager()), + m_c(c) { + // ensure that soft constraints are sorted with largest soft constraints first. + cmp_soft cmp; + std::sort(m_soft.begin(), m_soft.end(), cmp); + } + + lbool operator()() override { + init(); + return maxlex1(); + } + void commit_assignment() override { for (auto & soft : m_soft) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 68e18375f..419952f99 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -82,7 +82,6 @@ struct goal2sat::imp { m_is_lemma(false) { updt_params(p); m_true = sat::null_bool_var; - mk_true(); } void updt_params(params_ref const & p) {