mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

remove produce interpolants

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-14 15:00:25 -08:00
parent e954f59052
commit 54a125063b
2 changed files with 71 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/cmd_context/basic_cmds.cpp
View file

@ -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());
}

77
src/shell/dimacs_frontend.cpp
View file

@ -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<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
st.display_smt2(std::cout);
g_solver->collect_statistics(g_st);
g_st.update("total time", ((static_cast<double>(end_time) - static_cast<double>(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<sat2goal::mc> 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;
}