From 2bd29548dae911796863c02c5093c7f9d2f5da48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Dec 2016 17:27:56 -0800 Subject: [PATCH 1/3] improve parser error message over API, streamline names of statistics for arithmetic solver Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 4 ++++ src/opt/maxsmt.cpp | 6 ++++-- src/opt/opt_context.cpp | 6 +++++- src/opt/opt_solver.cpp | 1 + src/smt/arith_eq_adapter.cpp | 2 +- src/smt/theory_arith_core.h | 4 +++- src/smt/theory_arith_eq.h | 24 ++++++++++++++++++++---- src/smt/theory_arith_pp.h | 32 ++++++++++++++++---------------- 8 files changed, 54 insertions(+), 25 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 308db4081..3d8580178 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -289,6 +289,10 @@ extern "C" { //LOG_Z3_optimize_from_file(c, d, s); std::ifstream is(s); if (!is) { + std::ostringstream strm; + strm << "Could not open file " << s; + throw default_exception(strm.str()); + SET_ERROR_CODE(Z3_PARSER_ERROR); return; } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index f31009bbf..97b6a5293 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -350,8 +350,10 @@ namespace opt { for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { expr* e = m_soft_constraints[i]; bool is_not = m.is_not(e, e); - out << mk_pp(e, m) - << ((is_not != get_assignment(i))?" |-> true\n":" |-> false\n"); + out << m_weights[i] << ": " << mk_pp(e, m) + << ((is_not != get_assignment(i))?" |-> true ":" |-> false ") + << "\n"; + } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e63e29dc5..46122d619 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -792,10 +792,14 @@ namespace opt { arg = mk_not(m, arg); offset -= weight; } - if (m.is_true(arg) || weight.is_zero()) { + if (m.is_true(arg)) { + IF_VERBOSE(1, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> true\n";); + } + else if (weight.is_zero()) { // skip } else if (m.is_false(arg)) { + IF_VERBOSE(1, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> false\n";); offset += weight; } else { diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 42129be70..0d0c6d35a 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -47,6 +47,7 @@ namespace opt { m_first(true), m_was_unknown(false) { m_params.updt_params(p); + std::cout << "Case split strategy " << m_params.m_case_split_strategy << "\n"; if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { m_params.m_relevancy_lvl = 0; } diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index 411588d79..ce831f9ae 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -264,7 +264,7 @@ namespace smt { } void arith_eq_adapter::collect_statistics(::statistics & st) const { - st.update("eq adapter", m_stats.m_num_eq_axioms); + st.update("arith eq adapter", m_stats.m_num_eq_axioms); } void arith_eq_adapter::display_already_processed(std::ostream & out) const { diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a8d771d1a..9db5e8c72 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -465,7 +465,7 @@ namespace smt { tout << s_ante << "\n" << s_conseq << "\n";); literal lits[2] = {l_ante, l_conseq}; - ctx.mk_th_axiom(get_id(), 2, lits); + mk_clause(l_ante, l_conseq, 0, 0); if (ctx.relevancy()) { if (l_ante == false_literal) { ctx.mark_as_relevant(l_conseq); @@ -934,11 +934,13 @@ namespace smt { template void theory_arith::mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) { + TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; get_context().display_literals_verbose(tout, 2, lits); tout << "\n";); get_context().mk_th_axiom(get_id(), l1, l2, num_params, params); } template void theory_arith::mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) { + TRACE("arith", literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; get_context().display_literals_verbose(tout, 3, lits); tout << "\n";); get_context().mk_th_axiom(get_id(), l1, l2, l3, num_params, params); } diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 8577f3553..ae0f17757 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -44,6 +44,7 @@ namespace smt { SASSERT(lower_bound(v).is_rational()); numeral const & val = lower_bound(v).get_rational(); value_sort_pair key(val, is_int_src(v)); + TRACE("arith_eq", tout << mk_pp(get_enode(v)->get_owner(), get_manager()) << " = " << val << "\n";); theory_var v2; if (m_fixed_var_table.find(key, v2)) { if (v2 < static_cast(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) { @@ -247,6 +248,7 @@ namespace smt { // // x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2 // + TRACE("arith_eq_propagation", tout << "fixed\n";); lower(x2)->push_justification(ante, numeral::zero(), proofs_enabled()); upper(x2)->push_justification(ante, numeral::zero(), proofs_enabled()); m_stats.m_fixed_eqs++; @@ -324,28 +326,42 @@ namespace smt { template void theory_arith::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) { // Ignore equality if variables are already known to be equal. + ast_manager& m = get_manager(); if (is_equal(x, y)) return; // I doesn't make sense to propagate an equality (to the core) of variables of different sort. - if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) { - TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";); + if (m.get_sort(var2expr(x)) != m.get_sort(var2expr(y))) { + TRACE("arith", tout << mk_pp(var2expr(x), m) << " = " << mk_pp(var2expr(y), m) << "\n";); return; } context & ctx = get_context(); region & r = ctx.get_region(); enode * _x = get_enode(x); enode * _y = get_enode(y); + eq_vector const& eqs = antecedents.eqs(); + literal_vector const& lits = antecedents.lits(); justification * js = ctx.mk_justification( ext_theory_eq_propagation_justification( get_id(), r, - antecedents.lits().size(), antecedents.lits().c_ptr(), - antecedents.eqs().size(), antecedents.eqs().c_ptr(), + lits.size(), lits.c_ptr(), + eqs.size(), eqs.c_ptr(), _x, _y, antecedents.num_params(), antecedents.params("eq-propagate"))); TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n"; display_var(tout, x); display_var(tout, y);); + TRACE("arith_eq_propagation", + for (unsigned i = 0; i < lits.size(); ++i) { + ctx.display_detailed_literal(tout, lits[i]); + tout << "\n"; + } + for (unsigned i = 0; i < eqs.size(); ++i) { + tout << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n"; + } + tout << " ==> "; + tout << mk_pp(_x->get_owner(), m) << " = " << mk_pp(_y->get_owner(), m) << "\n"; + ); ctx.assign_eq(_x, _y, eq_justification(js)); } }; diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index ec14d8374..7b657d9c2 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -27,22 +27,22 @@ namespace smt { template void theory_arith::collect_statistics(::statistics & st) const { st.update("arith conflicts", m_stats.m_conflicts); - st.update("add rows", m_stats.m_add_rows); - st.update("pivots", m_stats.m_pivots); - st.update("assert lower", m_stats.m_assert_lower); - st.update("assert upper", m_stats.m_assert_upper); - st.update("assert diseq", m_stats.m_assert_diseq); - st.update("bound prop", m_stats.m_bound_props); - st.update("fixed eqs", m_stats.m_fixed_eqs); - st.update("offset eqs", m_stats.m_offset_eqs); - st.update("gcd tests", m_stats.m_gcd_tests); - st.update("ineq splits", m_stats.m_branches); - st.update("gomory cuts", m_stats.m_gomory_cuts); - st.update("max-min", m_stats.m_max_min); - st.update("grobner", m_stats.m_gb_compute_basis); - st.update("pseudo nonlinear", m_stats.m_nl_linear); - st.update("nonlinear bounds", m_stats.m_nl_bounds); - st.update("nonlinear horner", m_stats.m_nl_cross_nested); + st.update("arith add rows", m_stats.m_add_rows); + st.update("arith pivots", m_stats.m_pivots); + st.update("arith assert lower", m_stats.m_assert_lower); + st.update("arith assert upper", m_stats.m_assert_upper); + st.update("arith assert diseq", m_stats.m_assert_diseq); + st.update("arith bound prop", m_stats.m_bound_props); + st.update("arith fixed eqs", m_stats.m_fixed_eqs); + st.update("arith offset eqs", m_stats.m_offset_eqs); + st.update("arith gcd tests", m_stats.m_gcd_tests); + st.update("arith ineq splits", m_stats.m_branches); + st.update("arith gomory cuts", m_stats.m_gomory_cuts); + st.update("arith max-min", m_stats.m_max_min); + st.update("arith grobner", m_stats.m_gb_compute_basis); + st.update("arith pseudo nonlinear", m_stats.m_nl_linear); + st.update("arith nonlinear bounds", m_stats.m_nl_bounds); + st.update("arith nonlinear horner", m_stats.m_nl_cross_nested); m_arith_eq_adapter.collect_statistics(st); } From aaf6e67ec8aa10f07d700873a559b2cdf388cb0e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Dec 2016 17:43:47 -0800 Subject: [PATCH 2/3] add restart.max parameter to control cancellation based on restart count Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 1 - src/sat/sat_config.cpp | 4 +++- src/sat/sat_config.h | 1 + src/sat/sat_params.pyg | 1 + src/sat/sat_solver.cpp | 9 ++++++++- src/sat/sat_solver.h | 1 + 6 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 0d0c6d35a..42129be70 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -47,7 +47,6 @@ namespace opt { m_first(true), m_was_unknown(false) { m_params.updt_params(p); - std::cout << "Case split strategy " << m_params.m_case_split_strategy << "\n"; if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { m_params.m_relevancy_lvl = 0; } diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index f976e1d71..58505f8ac 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -26,6 +26,7 @@ namespace sat { m_always_true("always_true"), m_always_false("always_false"), m_caching("caching"), + m_restart_max(0), m_random("random"), m_geometric("geometric"), m_luby("luby"), @@ -66,7 +67,8 @@ namespace sat { m_restart_initial = p.restart_initial(); m_restart_factor = p.restart_factor(); - + m_restart_max = p.restart_max(); + m_random_freq = p.random_freq(); m_random_seed = p.random_seed(); if (m_random_seed == 0) diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 0234b5710..1cdabddef 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -52,6 +52,7 @@ namespace sat { restart_strategy m_restart; unsigned m_restart_initial; double m_restart_factor; // for geometric case + unsigned m_restart_max; double m_random_freq; unsigned m_random_seed; unsigned m_burst_search; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 90e715a9d..80e6f403f 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -7,6 +7,7 @@ def_module_params('sat', ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'), ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'), ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), + ('restart.max', UINT, 0, 'maximal number of restarts. Ignored if set to 0'), ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), ('random_seed', UINT, 0, 'random seed'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e6fa15a4c..a5c9005df 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -744,7 +744,6 @@ namespace sat { simplify_problem(); if (check_inconsistent()) return l_false; - if (m_config.m_max_conflicts == 0) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = 0\")\n";); return l_undef; @@ -766,6 +765,12 @@ namespace sat { simplify_problem(); if (check_inconsistent()) return l_false; gc(); + + if (m_config.m_restart_max != 0 && m_config.m_restart_max <= m_restarts) { + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); + return l_undef; + } + } } catch (abort_solver) { @@ -1126,6 +1131,7 @@ namespace sat { m_restart_threshold = m_config.m_restart_initial; m_luby_idx = 1; m_gc_threshold = m_config.m_gc_initial; + m_restarts = 0; m_min_d_tk = 1.0; m_stopwatch.reset(); m_stopwatch.start(); @@ -1308,6 +1314,7 @@ namespace sat { void solver::restart() { m_stats.m_restart++; + m_restarts++; IF_VERBOSE(1, verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision << " :restarts " << m_stats.m_restart << mk_stat(*this) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index bcd9a66d2..aa45a1043 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -293,6 +293,7 @@ namespace sat { protected: unsigned m_conflicts; + unsigned m_restarts; unsigned m_conflicts_since_restart; unsigned m_restart_threshold; unsigned m_luby_idx; From 8dde60f6345bd12f3222546dd41ca9a22a6beee7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Dec 2016 10:18:55 -0800 Subject: [PATCH 3/3] initialize watch in assign_eh Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 1 + src/smt/theory_pb.h | 3 --- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 1f11b9bf5..1885fc9c4 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -772,6 +772,7 @@ namespace smt { void theory_pb::assign_eh(bool_var v, bool is_true) { ptr_vector* ineqs = 0; literal nlit(v, is_true); + init_watch(v); TRACE("pb", tout << "assign: " << ~nlit << "\n";); ineqs = m_var_infos[v].m_lit_watch[nlit.sign()]; if (ineqs != 0) { diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 7f621f9c5..ee68bd26e 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -216,9 +216,6 @@ namespace smt { theory_pb_params m_params; svector m_var_infos; -// u_map m_lwatch; // per literal. -// u_map m_vwatch; // per variable. -// u_map m_ineqs; // per inequality. arg_map m_ineq_rep; // Simplex: representative inequality u_map m_ineq_row_info; // Simplex: row information per variable uint_set m_vars; // Simplex: 0-1 variables.