From 5c67c9d907ca196c7efb1e757ced48707a1e9b35 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 17:08:31 -0700 Subject: [PATCH] print certificate for #2202, enable CTL-C for API fix #2203 Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 3 +++ src/api/api_opt.cpp | 3 +++ src/api/api_solver.cpp | 9 +++------ src/muz/base/dl_context.cpp | 10 ++++++++-- src/muz/base/dl_context.h | 2 +- src/opt/opt_context.cpp | 2 ++ src/sat/sat_model_converter.cpp | 18 ++++++++++++++---- src/solver/solver.cpp | 3 --- src/util/params.cpp | 3 +++ src/util/params.h | 1 + 10 files changed, 38 insertions(+), 16 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 790470275..57037f1a8 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -24,6 +24,7 @@ Revision History: #include "api/api_stats.h" #include "muz/fp/datalog_parser.h" #include "util/cancel_eh.h" +#include "util/scoped_ctrl_c.h" #include "util/scoped_timer.h" #include "muz/fp/dl_cmds.h" #include "cmd_context/cmd_context.h" @@ -280,11 +281,13 @@ extern "C" { lbool r = l_undef; unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + bool use_ctrl_c = to_fixedpoint(d)->m_params.get_bool("ctrl_c", true); { scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); scoped_timer timer(timeout, &eh); + scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); try { r = to_fixedpoint_ref(d)->ctx().query(to_expr(q)); } diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 5d35b23b0..ad2c75764 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -18,6 +18,7 @@ Revision History: #include #include "util/cancel_eh.h" #include "util/scoped_timer.h" +#include "util/scoped_ctrl_c.h" #include "util/file_path.h" #include "parsers/smt2/smt2parser.h" #include "opt/opt_context.h" @@ -148,8 +149,10 @@ extern "C" { cancel_eh eh(mk_c(c)->m().limit()); unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = to_optimize_ptr(o)->get_params().get_uint("rlimit", mk_c(c)->get_rlimit()); + bool use_ctrl_c = to_optimize_ptr(o)->get_params().get_bool("ctrl_c", true); api::context::set_interruptable si(*(mk_c(c)), eh); { + scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index cafbfb9ff..fb7a937cc 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -31,9 +31,6 @@ Revision History: #include "api/api_stats.h" #include "api/api_ast_vector.h" #include "solver/tactic2solver.h" -#include "util/scoped_ctrl_c.h" -#include "util/cancel_eh.h" -#include "util/scoped_timer.h" #include "util/file_path.h" #include "tactic/portfolio/smt_strategic_solver.h" #include "smt/smt_solver.h" @@ -465,7 +462,7 @@ extern "C" { expr * const * _assumptions = to_exprs(assumptions); unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); - bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); + bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); lbool result; @@ -656,7 +653,7 @@ extern "C" { lbool result = l_undef; unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); - bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); + bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); { @@ -698,7 +695,7 @@ extern "C" { } unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); - bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); + bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", true); cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); { diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index e8578f327..d4af4693a 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -730,6 +730,7 @@ namespace datalog { void context::collect_params(param_descrs& p) { fp_params::collect_param_descrs(p); insert_timeout(p); + insert_ctrl_c(p); } void context::updt_params(params_ref const& p) { @@ -854,7 +855,11 @@ namespace datalog { UNREACHABLE(); } ensure_engine(); - return m_engine->query(query); + lbool r = m_engine->query(query); + if (r != l_undef && get_params().print_certificate()) { + display_certificate(std::cout) << "\n"; + } + return r; } lbool context::query_from_lvl (expr* query, unsigned lvl) { @@ -951,9 +956,10 @@ namespace datalog { } } - void context::display_certificate(std::ostream& out) { + std::ostream& context::display_certificate(std::ostream& out) { ensure_engine(); m_engine->display_certificate(out); + return out; } void context::display(std::ostream & out) const { diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index a14ef163f..b20e2813e 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -581,7 +581,7 @@ namespace datalog { /** \brief Display a certificate for reachability and/or unreachability. */ - void display_certificate(std::ostream& out); + std::ostream& display_certificate(std::ostream& out); /** \brief query result if it contains fact. diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e7c9e72ea..b43147c33 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1487,6 +1487,8 @@ namespace opt { void context::collect_param_descrs(param_descrs & r) { opt_params::collect_param_descrs(r); + insert_timeout(r); + insert_ctrl_c(r); } void context::updt_params(params_ref const& p) { diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index fab3be418..ddb7df74b 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -144,20 +144,30 @@ namespace sat { DEBUG_CODE({ // all clauses must be satisfied bool sat = false; - for (literal l : it->m_clauses) { + bool undef = false; + for (literal const& l : it->m_clauses) { if (l == null_literal) { CTRACE("sat", !sat, + if (m_solver) m_solver->display(tout); display(tout); for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n"; + for (literal const& l2 : it->m_clauses) { + if (l2 == null_literal) tout << "\n"; else tout << l2 << " "; + if (&l == &l2) break; + } ); - SASSERT(sat); + SASSERT(sat || undef); sat = false; + undef = false; continue; } if (sat) continue; - if (value_at(l, m) == l_true) - sat = true; + switch (value_at(l, m)) { + case l_undef: undef = true; break; + case l_true: sat = true; break; + default: break; + } } }); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 89421f079..20c2166a2 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -223,9 +223,6 @@ void solver::assert_expr(expr* f, expr* t) { assert_expr_core2(fml, a); } -static void insert_ctrl_c(param_descrs & r) { - r.insert("ctrl_c", CPK_BOOL, "enable interrupts from ctrl-c", "false"); -} void solver::collect_param_descrs(param_descrs & r) { diff --git a/src/util/params.cpp b/src/util/params.cpp index bfb6095d6..dd98dd958 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -305,6 +305,9 @@ void insert_rlimit(param_descrs & r) { r.insert("rlimit", CPK_UINT, "default resource limit used for solvers. Unrestricted when set to 0.", "0"); } +void insert_ctrl_c(param_descrs & r) { + r.insert("ctrl_c", CPK_BOOL, "enable interrupts from ctrl-c", "true"); +} class params { friend class params_ref; diff --git a/src/util/params.h b/src/util/params.h index 5330993c1..8d036456d 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -140,5 +140,6 @@ void insert_produce_models(param_descrs & r); void insert_produce_proofs(param_descrs & r); void insert_timeout(param_descrs & r); void insert_rlimit(param_descrs & r); +void insert_ctrl_c(param_descrs & r); #endif