From 8be03f7c1f6d1bd1e9c27ded3c9942d109a63153 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 21 May 2018 14:18:11 -0700 Subject: [PATCH] spacer_context: skolemize quant vars before renaming Skolemization has to be done before renaming, otherwise, can't guarantee that variable names do not clash --- src/muz/spacer/spacer_context.cpp | 73 ++++++++++++++++++------------- src/muz/spacer/spacer_context.h | 4 +- 2 files changed, 46 insertions(+), 31 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 2baa70f46..044c0f091 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -72,34 +72,17 @@ pob::pob (pob* parent, pred_transformer& pt, void pob::set_post(expr* post) { - app_ref_vector b(get_ast_manager()); - set_post(post, b); + app_ref_vector empty_binding(get_ast_manager()); + set_post(post, empty_binding); } -void pob::set_post(expr* post, app_ref_vector const &b) { +void pob::set_post(expr* post, app_ref_vector const &binding) { normalize(post, m_post, m_pt.get_context().get_params().spacer_simplify_pob(), m_pt.get_context().get_params().spacer_use_eqclass()); m_binding.reset(); - if (b.empty()) return; - - m_binding.append(b); - - std::sort (m_binding.c_ptr(), m_binding.c_ptr() + m_binding.size(), sk_lt_proc()); - - // skolemize implicit existential quantifier - ast_manager &m = get_ast_manager(); - app_ref_vector pinned(m); - - expr_safe_replace sub(m); - for (unsigned i = 0, sz = m_binding.size(); i < sz; ++i) { - expr* e; - e = m_binding.get(i); - pinned.push_back (mk_zk_const (m, i, get_sort(e))); - sub.insert (e, pinned.back()); - } - sub(m_post); + if (!binding.empty()) {m_binding.append(binding);} } void pob::inherit(pob const &p) { @@ -216,6 +199,25 @@ pob *derivation::create_first_child (model_evaluator_util &mev) return create_next_child(mev); } +void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res) { + ast_manager &m = get_ast_manager(); + if (vars.empty()) {res = fml; return;} + if (m.is_true(fml) || m.is_false(fml)) {res = fml; return;} + + std::sort (vars.c_ptr(), vars.c_ptr() + vars.size(), sk_lt_proc()); + + app_ref_vector pinned(m); + + expr_safe_replace sub(m); + for (unsigned i = 0, sz = vars.size(); i < sz; ++i) { + expr* e; + e = vars.get(i); + pinned.push_back (mk_zk_const (m, i, get_sort(e))); + sub.insert (e, pinned.back()); + } + sub(fml, res); +} + pob *derivation::create_next_child (model_evaluator_util &mev) { timeit _timer (is_trace_enabled("spacer_timeit"), @@ -280,6 +282,11 @@ pob *derivation::create_next_child (model_evaluator_util &mev) m_evars.append (vars); } + if (!m_evars.empty()) { + // existentially quantify out m_evars from post and skolemize the result + exist_skolemize(post.get(), m_evars, post); + } + get_manager ().formula_o2n (post.get (), post, m_premises [m_active].get_oidx (), m_evars.empty()); @@ -290,7 +297,6 @@ pob *derivation::create_next_child (model_evaluator_util &mev) pob *n = m_premises[m_active].pt().mk_pob(&m_parent, prev_level (m_parent.level ()), m_parent.depth (), post, m_evars); - IF_VERBOSE (1, verbose_stream () << "\n\tcreate_child: " << n->pt ().head ()->get_name () << " (" << n->level () << ", " << n->depth () << ") " @@ -895,9 +901,8 @@ bool pred_transformer::propagate_to_next_level (unsigned src_level) {return m_frames.propagate_to_next_level (src_level);} -/// \brief adds a lema to the solver and to child solvers -void pred_transformer::add_lemma_core(lemma* lemma, - bool ground_only) +/// \brief adds a lemma to the solver and to child solvers +void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only) { unsigned lvl = lemma->level(); expr* l = lemma->get_expr(); @@ -1859,13 +1864,13 @@ void pred_transformer::frames::simplify_formulas () // ensure that the lemmas are sorted sort(); - ast_manager &m = m_pt.get_ast_manager (); + ast_manager &m = m_pt.get_ast_manager(); - tactic_ref simplifier = mk_unit_subsumption_tactic (m); + tactic_ref simplifier = mk_unit_subsumption_tactic(m); lemma_ref_vector new_lemmas; - unsigned lemmas_size = m_lemmas.size (); - goal_ref g (alloc (goal, m, false, false, false)); + unsigned lemmas_size = m_lemmas.size(); + goal_ref g(alloc (goal, m, false, false, false)); unsigned j = 0; // for every frame + infinity frame @@ -1933,6 +1938,11 @@ void pred_transformer::frames::simplify_formulas () << mk_pp(m_lemmas[n]->get_expr(), m) << "\n"; } + + verbose_stream() << "Simplified goal is:\n"; + for (unsigned k = 0; k < r->size(); ++k) + verbose_stream() << k << ": " + << mk_pp(r->form(k), m) << "\n"; } ENSURE(found); SASSERT(found); @@ -3013,7 +3023,8 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) TRACE ("spacer", tout << "expand-pob: " << n.pt().head()->get_name() << " level: " << n.level() - << " depth: " << (n.depth () - m_pob_queue.min_depth ()) << "\n" + << " depth: " << (n.depth () - m_pob_queue.min_depth ()) + << " fvsz: " << n.get_free_vars_size() << "\n" << mk_pp(n.post(), m) << "\n";); STRACE ("spacer.expand-add", @@ -3450,6 +3461,8 @@ bool context::create_children(pob& n, datalog::rule const& r, tout << "Implicant\n"; tout << mk_and (Phi) << "\n"; tout << "Projected Implicant\n" << mk_pp (phi1, m) << "\n"; + if (!vars.empty()) + tout << "could not eliminate: " << vars << "\n"; ); // expand literals. Ideally, we do not want to split aliasing diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 62d90e4c0..8de4a70f8 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -517,7 +517,7 @@ public: expr* post() const { return m_post.get (); } void set_post(expr *post); - void set_post(expr *post, app_ref_vector const &b); + void set_post(expr *post, app_ref_vector const &binding); /// indicate that a new post should be set for the node void new_post(expr *post) {if(post != m_post) {m_new_post = post;}} @@ -648,6 +648,8 @@ public: /// premise must be consistent with the transition relation pob *create_next_child (); + /// existentially quantify vars and skolemize the result + void exist_skolemize(expr *fml, app_ref_vector &vars, expr_ref &res); datalog::rule const& get_rule () const { return m_rule; } pob& get_parent () const { return m_parent; } ast_manager &get_ast_manager () const {return m_parent.get_ast_manager ();}