mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
Logging facility for spacer plus minor improvements (#3368)
* [spacer] logging solver events New option fp.spacer.trace_file='file.log' enables logging solving events into a file. These events are useful for debugging the solver, but also for visualizing the solving process in a variety of ways * [spacer] allow setting logic for solvers used by spacer * [spacer] option to set arithmetic solver explicitly * [spacer] improve of dumping solver_pool state for debugging * fix propagate_ineqs to handle strict inequality Co-authored-by: Nham Van Le <nv3le@precious3.eng.uwaterloo.ca>
This commit is contained in:
Arie Gurfinkel
GitHub
parent
f06deca7e0
commit
6180a5276d
5 changed files with 143 additions and 58 deletions
|
|
@ -172,6 +172,7 @@ def_module_params('fp',
|
|||
('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
|
||||
('spacer.min_level', UINT, 0, 'Minimal level to explore'),
|
||||
('spacer.print_json', SYMBOL, '', 'Print pobs tree in JSON format to a given file'),
|
||||
('spacer.trace_file', SYMBOL, '', 'Log file for progress events'),
|
||||
('spacer.ctp', BOOL, True, 'Enable counterexample-to-pushing'),
|
||||
('spacer.use_inc_clause', BOOL, True, 'Use incremental clause to represent trans'),
|
||||
('spacer.dump_benchmarks', BOOL, False, 'Dump SMT queries as benchmarks'),
|
||||
|
|
@ -180,5 +181,6 @@ def_module_params('fp',
|
|||
('spacer.gpdr.bfs', BOOL, True, 'Use BFS exploration strategy for expanding model search'),
|
||||
('spacer.use_bg_invs', BOOL, False, 'Enable external background invariants'),
|
||||
('spacer.use_lim_num_gen', BOOL, False, 'Enable limit numbers generalizer to get smaller numbers'),
|
||||
|
||||
('spacer.logic', SYMBOL, '', 'SMT-LIB logic to configure internal SMT solvers'),
|
||||
('spacer.arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
|
||||
))
|
||||
|
|
|
|||
|
|
@ -943,25 +943,7 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only)
|
|||
SASSERT(!lemma->is_ground() || is_clause(m, l));
|
||||
SASSERT(!is_quantifier(l) || is_clause(m, to_quantifier(l)->get_expr()));
|
||||
|
||||
TRACE("spacer", tout << "add-lemma-core: " << pp_level (lvl)
|
||||
<< " " << head ()->get_name ()
|
||||
<< " " << mk_pp (l, m) << "\n";);
|
||||
|
||||
TRACE("core_array_eq", tout << "add-lemma-core: " << pp_level (lvl)
|
||||
<< " " << head ()->get_name ()
|
||||
<< " " << mk_pp (l, m) << "\n";);
|
||||
|
||||
STRACE ("spacer_progress",
|
||||
tout << "** add-lemma: " << pp_level (lvl) << " "
|
||||
<< head ()->get_name () << " "
|
||||
<< mk_epp (l, m) << "\n";
|
||||
|
||||
if (!lemma->is_ground()) {
|
||||
tout << "Bindings: " << lemma->get_bindings() << "\n";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
get_context().log_add_lemma(*this, *lemma);
|
||||
|
||||
if (is_infty_level(lvl)) { m_stats.m_num_invariants++; }
|
||||
|
||||
|
|
@ -2296,13 +2278,18 @@ context::context(fp_params const& params, ast_manager& m) :
|
|||
m_last_result(l_undef),
|
||||
m_inductive_lvl(0),
|
||||
m_expanded_lvl(0),
|
||||
m_json_marshaller(this) {
|
||||
m_json_marshaller(this),
|
||||
m_trace_stream(nullptr) {
|
||||
|
||||
params_ref p;
|
||||
p.set_uint("arith.solver", params.spacer_arith_solver());
|
||||
|
||||
ref<solver> pool0_base =
|
||||
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
|
||||
mk_smt_solver(m, p, params.spacer_logic());
|
||||
ref<solver> pool1_base =
|
||||
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
|
||||
mk_smt_solver(m, p, params.spacer_logic());
|
||||
ref<solver> pool2_base =
|
||||
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
|
||||
mk_smt_solver(m, p, params.spacer_logic());
|
||||
|
||||
unsigned max_num_contexts = params.spacer_max_num_contexts();
|
||||
m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts);
|
||||
|
|
@ -2310,12 +2297,24 @@ context::context(fp_params const& params, ast_manager& m) :
|
|||
m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts);
|
||||
|
||||
updt_params();
|
||||
|
||||
if (m_params.spacer_trace_file().is_non_empty_string()) {
|
||||
m_trace_stream = alloc(std::fstream,
|
||||
m_params.spacer_trace_file().bare_str(),
|
||||
std::ios_base::out);
|
||||
}
|
||||
}
|
||||
|
||||
context::~context()
|
||||
{
|
||||
reset_lemma_generalizers();
|
||||
reset();
|
||||
|
||||
if (m_trace_stream) {
|
||||
m_trace_stream->close();
|
||||
dealloc(m_trace_stream);
|
||||
m_trace_stream = nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
void context::updt_params() {
|
||||
|
|
@ -3048,23 +3047,92 @@ lbool context::solve_core (unsigned from_lvl)
|
|||
m_pob_queue.inc_level ();
|
||||
lvl = m_pob_queue.max_level ();
|
||||
m_stats.m_max_depth = std::max(m_stats.m_max_depth, lvl);
|
||||
IF_VERBOSE(1,verbose_stream() << "Entering level "<< lvl << "\n";);
|
||||
|
||||
STRACE("spacer_progress", tout << "\n* LEVEL " << lvl << "\n";);
|
||||
IF_VERBOSE(1,
|
||||
if (m_params.print_statistics()) {
|
||||
statistics st;
|
||||
collect_statistics(st);
|
||||
st.display_smt2(verbose_stream());
|
||||
};
|
||||
);
|
||||
|
||||
log_enter_level(lvl);
|
||||
}
|
||||
// communicate failure to datalog::context
|
||||
if (m_context) { m_context->set_status(datalog::BOUNDED); }
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
void context::log_enter_level(unsigned lvl) {
|
||||
|
||||
if (m_trace_stream) { *m_trace_stream << "\n* LEVEL " << lvl << "\n\n"; }
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "Entering level " << lvl << "\n";);
|
||||
STRACE("spacer_progress", tout << "\n* LEVEL " << lvl << "\n";);
|
||||
|
||||
IF_VERBOSE(
|
||||
1, if (m_params.print_statistics()) {
|
||||
statistics st;
|
||||
collect_statistics(st);
|
||||
st.display_smt2(verbose_stream());
|
||||
};);
|
||||
}
|
||||
|
||||
void context::log_propagate() {
|
||||
if (m_trace_stream) *m_trace_stream << "Propagating\n\n";
|
||||
STRACE("spacer_progress", tout << "Propagating\n";);
|
||||
IF_VERBOSE(1, verbose_stream() << "Propagating: " << std::flush;);
|
||||
}
|
||||
|
||||
void context::log_expand_pob(pob &n) {
|
||||
if (m_trace_stream) {
|
||||
std::string pob_id = "none";
|
||||
if (n.parent()) pob_id = std::to_string(n.parent()->post()->get_id());
|
||||
|
||||
*m_trace_stream << "** expand-pob: " << n.pt().head()->get_name()
|
||||
<< " level: " << n.level()
|
||||
<< " depth: " << (n.depth() - m_pob_queue.min_depth())
|
||||
<< " exprID: " << n.post()->get_id() << " pobID: " << pob_id << "\n"
|
||||
<< mk_epp(n.post(), m) << "\n\n";
|
||||
}
|
||||
|
||||
TRACE("spacer", tout << "expand-pob: " << n.pt().head()->get_name()
|
||||
<< " level: " << n.level()
|
||||
<< " depth: " << (n.depth() - m_pob_queue.min_depth())
|
||||
<< " fvsz: " << n.get_free_vars_size() << "\n"
|
||||
<< mk_pp(n.post(), m) << "\n";);
|
||||
|
||||
STRACE("spacer_progress",
|
||||
tout << "** expand-pob: " << n.pt().head()->get_name()
|
||||
<< " level: " << n.level()
|
||||
<< " depth: " << (n.depth() - m_pob_queue.min_depth()) << "\n"
|
||||
<< mk_epp(n.post(), m) << "\n\n";);
|
||||
}
|
||||
|
||||
void context::log_add_lemma(pred_transformer &pt, lemma &new_lemma) {
|
||||
unsigned lvl = new_lemma.level();
|
||||
expr *fml = new_lemma.get_expr();
|
||||
std::string pob_id = "none";
|
||||
if (new_lemma.get_pob())
|
||||
pob_id = std::to_string(new_lemma.get_pob()->post()->get_id());
|
||||
if (m_trace_stream) {
|
||||
*m_trace_stream << "** add-lemma: "
|
||||
<< pp_level(lvl) << " "
|
||||
<< "exprID: " << fml->get_id() << " "
|
||||
<< "pobID: " << pob_id << "\n"
|
||||
<< pt.head()->get_name() << "\n"
|
||||
<< mk_epp(fml, m) << "\n";
|
||||
if (!new_lemma.is_ground()) {
|
||||
*m_trace_stream << "Bindings: " << new_lemma.get_bindings()
|
||||
<< "\n";
|
||||
}
|
||||
*m_trace_stream << "\n";
|
||||
}
|
||||
|
||||
TRACE("spacer", tout << "add-lemma-core: " << pp_level(lvl) << " "
|
||||
<< pt.head()->get_name() << " " << mk_pp(fml, m) << "\n";);
|
||||
|
||||
STRACE("spacer_progress",
|
||||
tout << "** add-lemma: " << pp_level(lvl) << " "
|
||||
<< pt.head()->get_name() << " " << mk_epp(fml, m)
|
||||
<< "\n";
|
||||
if (!new_lemma.is_ground()) {
|
||||
tout << "Bindings: " << new_lemma.get_bindings() << "\n";
|
||||
}
|
||||
tout << "\n";);
|
||||
}
|
||||
|
||||
|
||||
//
|
||||
bool context::check_reachability ()
|
||||
|
|
@ -3295,24 +3363,8 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
|
|||
{
|
||||
SASSERT(out.empty());
|
||||
pob::on_expand_event _evt(n);
|
||||
TRACE ("spacer",
|
||||
tout << "expand-pob: " << n.pt().head()->get_name()
|
||||
<< " level: " << n.level()
|
||||
<< " depth: " << (n.depth () - m_pob_queue.min_depth ())
|
||||
<< " fvsz: " << n.get_free_vars_size() << "\n"
|
||||
<< mk_pp(n.post(), m) << "\n";);
|
||||
|
||||
STRACE ("spacer_progress",
|
||||
tout << "** expand-pob: " << n.pt().head()->get_name()
|
||||
<< " level: " << n.level()
|
||||
<< " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n"
|
||||
<< mk_epp(n.post(), m) << "\n\n";);
|
||||
|
||||
TRACE ("core_array_eq",
|
||||
tout << "expand-pob: " << n.pt().head()->get_name()
|
||||
<< " level: " << n.level()
|
||||
<< " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n"
|
||||
<< mk_pp(n.post(), m) << "\n";);
|
||||
log_expand_pob(n);
|
||||
|
||||
stopwatch watch;
|
||||
IF_VERBOSE (1, verbose_stream () << "expand: " << n.pt ().head ()->get_name ()
|
||||
|
|
@ -3520,6 +3572,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
|
|||
throw unknown_exception();
|
||||
}
|
||||
|
||||
|
||||
//
|
||||
// check if predicate transformer has a satisfiable predecessor state.
|
||||
// returns either a satisfiable predecessor state or
|
||||
|
|
@ -3543,9 +3596,9 @@ bool context::propagate(unsigned min_prop_lvl,
|
|||
if (m_simplify_formulas_pre) {
|
||||
simplify_formulas();
|
||||
}
|
||||
STRACE ("spacer_progress", tout << "Propagating\n";);
|
||||
|
||||
IF_VERBOSE (1, verbose_stream () << "Propagating: " << std::flush;);
|
||||
log_propagate();
|
||||
|
||||
|
||||
for (unsigned lvl = min_prop_lvl; lvl <= full_prop_lvl; lvl++) {
|
||||
IF_VERBOSE (1,
|
||||
|
|
|
|||
|
|
@ -24,6 +24,8 @@ Notes:
|
|||
#define _SPACER_CONTEXT_H_
|
||||
|
||||
#include <queue>
|
||||
#include <fstream>
|
||||
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include "muz/spacer/spacer_manager.h"
|
||||
#include "muz/spacer/spacer_prop_solver.h"
|
||||
|
|
@ -899,7 +901,7 @@ enum spacer_children_order {
|
|||
};
|
||||
|
||||
class context {
|
||||
|
||||
friend class pred_transformer;
|
||||
struct stats {
|
||||
unsigned m_num_queries;
|
||||
unsigned m_num_reuse_reach;
|
||||
|
|
@ -982,6 +984,7 @@ class context {
|
|||
unsigned m_blast_term_ite_inflation;
|
||||
scoped_ptr_vector<spacer_callback> m_callbacks;
|
||||
json_marshaller m_json_marshaller;
|
||||
std::fstream* m_trace_stream;
|
||||
|
||||
// Solve using gpdr strategy
|
||||
lbool gpdr_solve_core();
|
||||
|
|
@ -991,6 +994,12 @@ class context {
|
|||
model &mdl,
|
||||
pob_ref_buffer &out);
|
||||
|
||||
// progress logging
|
||||
void log_enter_level(unsigned lvl);
|
||||
void log_propagate();
|
||||
void log_expand_pob(pob &);
|
||||
void log_add_lemma(pred_transformer &, lemma&);
|
||||
|
||||
// Functions used by search.
|
||||
lbool solve_core(unsigned from_lvl = 0);
|
||||
bool is_requeue(pob &n);
|
||||
|
|
|
|||
|
|
@ -279,6 +279,7 @@ private:
|
|||
lbool last_status, double last_time) {
|
||||
std::string file_name = mk_file_name();
|
||||
std::ofstream out(file_name);
|
||||
STRACE("spacer.ind_gen", tout << "Dumping benchmark to " << file_name << "\n";);
|
||||
if (!out) {
|
||||
IF_VERBOSE(0, verbose_stream() << "could not open file " << file_name << " for output\n");
|
||||
return;
|
||||
|
|
@ -294,7 +295,7 @@ private:
|
|||
}
|
||||
|
||||
out << "(check-sat";
|
||||
for (auto * lit : cube) out << " " << mk_pp(lit, m);
|
||||
for (auto * lit : cube) out << " " << mk_pp(lit, m) << "\n";
|
||||
out << ")\n";
|
||||
|
||||
out << "(exit)\n";
|
||||
|
|
@ -302,6 +303,7 @@ private:
|
|||
m_base->collect_statistics(st);
|
||||
st.update("time", last_time);
|
||||
st.display_smt2(out);
|
||||
m_base->get_params().display(out);
|
||||
out.close();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -202,8 +202,27 @@ struct propagate_ineqs_tactic::imp {
|
|||
k = GE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
else if (m_util.is_lt(t)) {
|
||||
if (sign) {
|
||||
k = GE;
|
||||
strict = false;
|
||||
} else {
|
||||
k = LE;
|
||||
strict = true;
|
||||
}
|
||||
}
|
||||
else if (m_util.is_gt(t)) {
|
||||
//x > y == x <=y, strict = false
|
||||
if (sign) {
|
||||
k = LE;
|
||||
strict = false;
|
||||
} else {
|
||||
k = GE;
|
||||
strict = true;
|
||||
}
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
expr * lhs = to_app(t)->get_arg(0);
|
||||
expr * rhs = to_app(t)->get_arg(1);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue