From 40aa2f7cb294d6ab8afb8aede0e28d06962df190 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 05:49:24 -0700 Subject: [PATCH] fix 3838 fix #3837 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 17 +++++++++++------ src/ast/rewriter/rewriter_def.h | 6 ++++++ src/muz/base/hnf.cpp | 13 +++++-------- src/muz/fp/horn_tactic.cpp | 14 +++++++++----- 4 files changed, 31 insertions(+), 19 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c410e897e..49ff2426b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) { if (n->get_id() != id) return; ++s_count; std::cout << s_count << "\n"; - //SASSERT(s_count != 2); + SASSERT(s_count != 1); } #endif @@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - // track_id(n, 48); + // track_id(n, 323); TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); @@ -2902,8 +2902,8 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))); CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0), tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n"; - tout << mk_bounded_pp(p1, *this, 5) << "\n\n"; - tout << mk_bounded_pp(p2, *this, 5) << "\n\n"; + tout << p1->get_id() << ": " << mk_bounded_pp(p1, *this, 5) << "\n\n"; + tout << p2->get_id() << ": " << mk_bounded_pp(p2, *this, 5) << "\n\n"; ); SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0)); if (is_reflexivity(p1)) @@ -2913,7 +2913,10 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { // OEQ is compatible with EQ for transitivity. func_decl* f = to_app(get_fact(p1))->get_decl(); if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl(); - return mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); + proof* p = mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1))); + +// SASSERT(p->get_id() != 202); + return p; } proof * ast_manager::mk_transitivity(proof * p1, proof * p2, proof * p3) { @@ -2955,7 +2958,9 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_app(R, f1, f2)); - return mk_app(m_basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr()); + proof* p = mk_app(m_basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr()); + SASSERT(p->get_id() != 202); + return p; } proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) { diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 6a7433063..1cb07a0ee 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -184,6 +184,7 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { if (to_app(t)->get_num_args() == 0) { if (process_const(to_app(t))) return true; + TRACE("rewriter", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r,m()) << "\n";); t = m_r; } if (max_depth != RW_UNBOUNDED_DEPTH) @@ -302,6 +303,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (m_pr2) tout << mk_bounded_pp(m_pr2, m()) << "\n"; ); SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2)); + SASSERT(st == BR_FAILED || rewrites_from(new_t, m_pr2)); SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); if (st != BR_FAILED) { result_stack().shrink(fr.m_spos); @@ -314,6 +316,8 @@ void rewriter_tpl::process_app(app * t, frame & fr) { m_pr = m().mk_transitivity(m_pr, m_pr2); m_pr2 = nullptr; result_pr_stack().push_back(m_pr); + SASSERT(rewrites_to(m_r, m_pr)); + SASSERT(rewrites_from(t, m_pr)); } if (st == BR_DONE) { cache_result(t, m_r, m_pr, fr.m_cache_result); @@ -346,6 +350,8 @@ void rewriter_tpl::process_app(app * t, frame & fr) { result_pr_stack().push_back(m_pr); } m_r = result_stack().back(); + SASSERT(rewrites_to(m_r, m_pr)); + SASSERT(rewrites_from(t, m_pr)); result_stack().pop_back(); result_stack().pop_back(); result_stack().push_back(m_r); diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index 5d09f88b0..a9a0b4692 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -165,10 +165,7 @@ public: } } TRACE("hnf", - tout << mk_pp(n, m) << "\n==>\n"; - for (unsigned i = 0; i < result.size(); ++i) { - tout << mk_pp(result[i].get(), m) << "\n"; - }); + tout << mk_pp(n, m) << "\n==>\n" << result << "\n";); } bool checkpoint() { @@ -458,13 +455,13 @@ private: } - proof_ref mk_congruence(proof* p1, expr_ref_vector const& body, expr* head, proof_ref_vector& defs) { + proof_ref mk_congruence(proof* p, expr_ref_vector const& body, expr* head, proof_ref_vector& defs) { if (defs.empty()) { - return proof_ref(p1, m); + return proof_ref(p, m); } else { - SASSERT(p1); - proof_ref p2(m), p3(m); + SASSERT(p); + proof_ref p1(p, m), p2(m), p3(m); app_ref fml = mk_implies(body, head); expr* fact = m.get_fact(p1); if (m.is_iff(fact)) { diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 6cc2636a6..b8485a1f7 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -349,15 +349,19 @@ class horn_tactic : public tactic { void check_parameters() { fp_params const& p = m_ctx.get_params(); if (p.engine() == symbol("datalog")) - not_supported(); + not_supported("engine=datalog"); if (p.datalog_generate_explanations()) - not_supported(); + not_supported("datalog.generate_explanations"); if (p.datalog_magic_sets_for_queries()) - not_supported(); + not_supported("datalog.magic_sets_for_queries"); + if (p.xform_instantiate_arrays()) + not_supported("xform.instantiate_arrays"); + if (p.xform_magic()) + not_supported("xform.magic"); } - void not_supported() { - throw default_exception("unsupported parameter combination passed to HORN tactic"); + void not_supported(char const* s) { + throw default_exception(std::string("unsupported parameter ") + s); } };