From cab4e4b461efc4328a24df3fc3a446662a2fc75a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Sep 2017 18:32:46 -0500 Subject: [PATCH] add feature to display benchmark in format seen by SAT solver Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 14 ++++++++++++++ src/cmd_context/cmd_context.h | 1 + src/cmd_context/extra_cmds/dbg_cmds.cpp | 15 +++++++++++---- src/sat/sat_config.cpp | 3 ++- src/sat/sat_config.h | 1 + src/sat/sat_params.pyg | 3 ++- src/sat/sat_solver.cpp | 7 +++++++ src/sat/sat_solver/inc_sat_solver.cpp | 1 - src/tactic/portfolio/enum2bv_solver.cpp | 1 - 9 files changed, 38 insertions(+), 8 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3889d6205..fa3b06649 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1545,6 +1545,20 @@ void cmd_context::reset_assertions() { } +void cmd_context::display_dimacs() { + if (m_solver) { + try { + gparams::set("sat.dimacs.display", "true"); + m_solver->check_sat(0, nullptr); + } + catch (...) { + gparams::set("sat.dimacs.display", "false"); + throw; + } + gparams::set("sat.dimacs.display", "false"); + } +} + void cmd_context::display_model(model_ref& mdl) { if (mdl) { model_params p; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 5883a8d8e..b60f590a9 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -419,6 +419,7 @@ public: void display_assertions(); void display_statistics(bool show_total_time = false, double total_time = 0.0); + void display_dimacs(); void reset(bool finalize = false); void assert_expr(expr * t); void assert_expr(symbol const & name, expr * t); diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 7d20685ac..dfdfa6175 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -31,7 +31,6 @@ Notes: #include "ast/rewriter/var_subst.h" #include "util/gparams.h" -#ifndef _EXTERNAL_RELEASE BINARY_SYM_CMD(get_quantifier_body_cmd, "dbg-get-qbody", @@ -343,10 +342,19 @@ public: } }; -#endif +class print_dimacs_cmd : public cmd { +public: + print_dimacs_cmd():cmd("display-dimacs") {} + virtual char const * get_usage() const { return ""; } + virtual char const * get_descr(cmd_context & ctx) const { return "print benchmark in DIMACS format"; } + virtual unsigned get_arity() const { return 0; } + virtual void prepare(cmd_context & ctx) {} + virtual void execute(cmd_context & ctx) { ctx.display_dimacs(); } +}; + void install_dbg_cmds(cmd_context & ctx) { -#ifndef _EXTERNAL_RELEASE + ctx.insert(alloc(print_dimacs_cmd)); ctx.insert(alloc(get_quantifier_body_cmd)); ctx.insert(alloc(set_cmd)); ctx.insert(alloc(pp_var_cmd)); @@ -369,5 +377,4 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(instantiate_cmd)); ctx.insert(alloc(instantiate_nested_cmd)); ctx.insert(alloc(set_next_id)); -#endif } diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 9cd343bd3..c67511275 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -35,7 +35,7 @@ namespace sat { m_glue("glue"), m_glue_psm("glue_psm"), m_psm_glue("psm_glue") { - m_num_parallel = 1; + m_num_parallel = 1; updt_params(p); } @@ -114,6 +114,7 @@ namespace sat { m_core_minimize = p.core_minimize(); m_core_minimize_partial = p.core_minimize_partial(); m_dyn_sub_res = p.dyn_sub_res(); + m_dimacs_display = p.dimacs_display(); } void config::collect_param_descrs(param_descrs & r) { diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index edd9f0bfc..36f22e83f 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -74,6 +74,7 @@ namespace sat { bool m_core_minimize; bool m_core_minimize_partial; + bool m_dimacs_display; symbol m_always_true; symbol m_always_false; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 60708fd5c..2b1dc6646 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -23,4 +23,5 @@ def_module_params('sat', ('core.minimize', BOOL, False, 'minimize computed core'), ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('parallel_threads', UINT, 1, 'number of parallel threads to use'), - ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) + ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), + ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 77bd2283d..2fa0c46f0 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -724,6 +724,13 @@ namespace sat { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); + if (m_config.m_dimacs_display) { + display_dimacs(std::cout); + for (unsigned i = 0; i < num_lits; ++lits) { + std::cout << dimacs_lit(lits[i]) << " 0\n"; + } + return l_undef; + } if (m_config.m_num_parallel > 1 && !m_par) { return check_par(num_lits, lits); } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 21f9f1e8a..69645d705 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -105,7 +105,6 @@ public: virtual void set_progress_callback(progress_callback * callback) {} - void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) { if (weights != 0) { for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 36a178c41..5880302d9 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -97,7 +97,6 @@ public: virtual void get_labels(svector & r) { m_solver->get_labels(r); } virtual ast_manager& get_manager() const { return m; } virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } - virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { datatype_util dt(m); bv_util bv(m);