diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 981698db7..80cd6373e 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -309,7 +309,6 @@ protected: symbol m_produce_unsat_assumptions; symbol m_produce_models; symbol m_produce_assignments; - symbol m_produce_interpolants; symbol m_produce_assertions; symbol m_regular_output_channel; symbol m_diagnostic_output_channel; @@ -326,7 +325,7 @@ protected: return s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions || - s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || + s == m_produce_models || s == m_produce_assignments || s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations || s == m_produce_assertions || s == m_reproducible_resource_limit; @@ -346,7 +345,6 @@ public: m_produce_unsat_assumptions(":produce-unsat-assumptions"), m_produce_models(":produce-models"), m_produce_assignments(":produce-assignments"), - m_produce_interpolants(":produce-interpolants"), m_produce_assertions(":produce-assertions"), m_regular_output_channel(":regular-output-channel"), m_diagnostic_output_channel(":diagnostic-output-channel"), @@ -418,10 +416,6 @@ class set_option_cmd : public set_get_option_cmd { check_not_initialized(ctx, m_produce_proofs); ctx.set_produce_proofs(to_bool(value)); } - else if (m_option == m_produce_interpolants) { - check_not_initialized(ctx, m_produce_interpolants); - ctx.set_produce_interpolants(to_bool(value)); - } else if (m_option == m_produce_unsat_cores) { check_not_initialized(ctx, m_produce_unsat_cores); ctx.set_produce_unsat_cores(to_bool(value)); @@ -577,9 +571,6 @@ public: else if (opt == m_produce_proofs) { print_bool(ctx, ctx.produce_proofs()); } - else if (opt == m_produce_interpolants) { - print_bool(ctx, ctx.produce_interpolants()); - } else if (opt == m_produce_unsat_cores) { print_bool(ctx, ctx.produce_unsat_cores()); } diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 738566ce2..9a4e65896 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -23,23 +23,35 @@ Revision History: #include "util/rlimit.h" #include "util/gparams.h" #include "sat/dimacs.h" +#include "sat/sat_params.hpp" #include "sat/sat_solver.h" +#include "sat/ba_solver.h" +#include "sat/tactic/goal2sat.h" +#include "ast/reg_decl_plugins.h" +#include "tactic/tactic.h" +#include "tactic/fd_solver/fd_solver.h" + extern bool g_display_statistics; static sat::solver * g_solver = nullptr; static clock_t g_start_time; +static tactic_ref g_tac; +static statistics g_st; static void display_statistics() { clock_t end_time = clock(); + if (g_tac && g_display_statistics) { + g_tac->collect_statistics(g_st); + } if (g_solver && g_display_statistics) { std::cout.flush(); std::cerr.flush(); - statistics st; - g_solver->collect_statistics(st); - st.update("total time", ((static_cast(end_time) - static_cast(g_start_time)) / CLOCKS_PER_SEC)); - st.display_smt2(std::cout); + g_solver->collect_statistics(g_st); + g_st.update("total time", ((static_cast(end_time) - static_cast(g_start_time)) / CLOCKS_PER_SEC)); + g_st.display_smt2(std::cout); } + g_display_statistics = false; } static void on_timeout() { @@ -162,14 +174,63 @@ void verify_solution(char const * file_name) { } } +lbool solve_parallel(sat::solver& s) { + params_ref p = gparams::get_module("sat"); + ast_manager m; + reg_decl_plugins(m); + sat2goal s2g; + ref mc; + atom2bool_var a2b(m); + for (unsigned v = 0; v < s.num_vars(); ++v) { + a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v); + } + goal_ref g = alloc(goal, m); + s2g(s, a2b, p, *g, mc); + + g_tac = mk_parallel_qffd_tactic(m, p); + std::string reason_unknown; + model_ref md; + labels_vec labels; + proof_ref pr(m); + expr_dependency_ref core(m); + lbool r = check_sat(*g_tac, g, md, labels, pr, core, reason_unknown); + switch (r) { + case l_true: + if (gparams::get_ref().get_bool("model_validate", false)) { + // populate the SAT solver with the model obtained from parallel execution. + for (auto const& kv : a2b) { + sat::literal lit; + bool is_true = m.is_true((*md)(kv.m_key)); + lit = sat::literal(kv.m_value, !is_true); + s.mk_clause(1, &lit); + } + // VERIFY(l_true == s.check()); + } + break; + case l_false: + break; + default: + break; + } + display_statistics(); + g_display_statistics = false; + g_tac = nullptr; + return r; +} + unsigned read_dimacs(char const * file_name) { g_start_time = clock(); register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); params_ref p = gparams::get_module("sat"); + params_ref par = gparams::get_module("parallel"); p.set_bool("produce_models", true); + sat_params sp(p); reslimit limit; sat::solver solver(p, limit); + if (sp.xor_solver()) { + solver.set_extension(alloc(sat::ba_solver)); + } g_solver = &solver; if (file_name) { @@ -194,13 +255,16 @@ unsigned read_dimacs(char const * file_name) { track_clauses(solver, solver2, assumptions, tracking_clauses); r = g_solver->check(assumptions.size(), assumptions.c_ptr()); } + else if (par.get_bool("enable", false)) { + r = solve_parallel(solver); + } else { r = g_solver->check(); } switch (r) { case l_true: std::cout << "sat\n"; - if (file_name) verify_solution(file_name); + if (file_name && gparams::get_ref().get_bool("model_validate", false)) verify_solution(file_name); display_model(*g_solver); break; case l_undef: @@ -213,7 +277,6 @@ unsigned read_dimacs(char const * file_name) { } break; } - if (g_display_statistics) - display_statistics(); + display_statistics(); return 0; }