diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index afa4b5218..d9f89ce14 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -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'), )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 12a607191..da9898a16 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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 pool0_base = - mk_smt_solver(m, params_ref::get_empty(), symbol::null); + mk_smt_solver(m, p, params.spacer_logic()); ref pool1_base = - mk_smt_solver(m, params_ref::get_empty(), symbol::null); + mk_smt_solver(m, p, params.spacer_logic()); ref 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, diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 125017c24..5a38f723c 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -24,6 +24,8 @@ Notes: #define _SPACER_CONTEXT_H_ #include +#include + #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 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); diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 7f3882447..d1021da3e 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -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(); } diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index a55a4334b..4afcfb609 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -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);