From bed3e6c2fd21249e7eb2eea89c8d32dfd8ffad62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Feb 2017 17:52:45 -0800 Subject: [PATCH] feat(library/tactic/smt): add get_config and use it to implement slift smt_tactic.slift was losing the configuration. --- library/init/meta/smt/smt_tactic.lean | 26 +++++----- src/library/tactic/smt/congruence_closure.cpp | 24 +++++++++ src/library/tactic/smt/congruence_closure.h | 2 + src/library/tactic/smt/ematch.cpp | 9 ++++ src/library/tactic/smt/ematch.h | 2 + src/library/tactic/smt/smt_state.cpp | 49 ++++++++++++++++--- src/library/tactic/smt/smt_state.h | 11 ++++- src/library/tactic/smt/util.cpp | 1 + 8 files changed, 103 insertions(+), 21 deletions(-) diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean index 8d3b3ed7d6..4e693bf44d 100644 --- a/library/init/meta/smt/smt_tactic.lean +++ b/library/init/meta/smt/smt_tactic.lean @@ -119,7 +119,7 @@ meta constant ematch_using : hinst_lemmas → smt_tactic unit meta constant mk_ematch_eqn_lemmas_for_core : transparency → name → smt_tactic hinst_lemmas meta constant to_cc_state : smt_tactic cc_state meta constant to_em_state : smt_tactic ematch_state -meta constant get_config : smt_tactic cc_config +meta constant get_config : smt_tactic smt_config /-- Preprocess the given term using the same simplifications rules used when we introduce a new hypothesis. The result is pair containing the resulting @@ -191,20 +191,22 @@ private meta def mk_smt_goals_for (cfg : smt_config) : list expr → list smt_go [new_tg] ← get_goals | tactic.failed, mk_smt_goals_for tgs (new_sg::sr) (new_tg::tr) +/- See slift -/ +meta def slift_aux {α : Type} (t : tactic α) (cfg : smt_config) : smt_tactic α := +λ ss, do + _::sgs ← return ss | fail "slift tactic failed, there no smt goals to be solved", + tg::tgs ← tactic.get_goals | tactic.failed, + tactic.set_goals [tg], a ← t, + new_tgs ← tactic.get_goals, + (new_sgs, new_tgs) ← mk_smt_goals_for cfg new_tgs [] [], + tactic.set_goals (new_tgs ++ tgs), + return (a, new_sgs ++ sgs) + /-- This lift operation will restart the SMT state. - It is useful for using tactics that change the set of hypotheses. --/ + It is useful for using tactics that change the set of hypotheses. -/ meta def slift {α : Type} (t : tactic α) : smt_tactic α := -λ ss, do - _::sgs ← return ss | fail "slift tactic failed, there no smt goals to be solved", - cfg ← return {smt_config .}, -- TODO(Leo): use get_config - tg::tgs ← tactic.get_goals | tactic.failed, - tactic.set_goals [tg], a ← t, - new_tgs ← tactic.get_goals, - (new_sgs, new_tgs) ← mk_smt_goals_for cfg new_tgs [] [], - tactic.set_goals (new_tgs ++ tgs), - return (a, new_sgs ++ sgs) +get_config >>= slift_aux t meta def trace_state : smt_tactic unit := do (s₁, s₂) ← smt_tactic.read, diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp index 520f702711..654b6ae301 100644 --- a/src/library/tactic/smt/congruence_closure.cpp +++ b/src/library/tactic/smt/congruence_closure.cpp @@ -18,6 +18,8 @@ Author: Leonardo de Moura #include "library/app_builder.h" #include "library/projection.h" #include "library/constructions/constructor.h" +#include "library/vm/vm_option.h" +#include "library/vm/vm_list.h" #include "library/tactic/smt/util.h" #include "library/tactic/smt/congruence_closure.h" @@ -225,6 +227,28 @@ bool congruence_closure::state::in_heterogeneous_eqc(expr const & e) const { return false; } +/* +structure cc_config := +(ignore_instances : bool) +(ac : bool) +(ho_fns : option (list name)) +(em : bool) + */ +vm_obj congruence_closure::state::mk_vm_cc_config() const { + vm_obj ho_fns; + if (get_config().m_all_ho) { + ho_fns = mk_vm_none(); + } else { + buffer fns; + m_ho_fns.to_buffer(fns); + ho_fns = mk_vm_some(to_obj(fns)); + } + vm_obj ignore_instances = mk_vm_bool(get_config().m_ignore_instances); + vm_obj ac = mk_vm_bool(get_config().m_ac); + vm_obj em = mk_vm_bool(get_config().m_em); + return mk_vm_constructor(0, ignore_instances, ac, ho_fns, em); +} + /** \brief Return true iff the given function application are congruent See paper: Congruence Closure for Intensional Type Theory. */ diff --git a/src/library/tactic/smt/congruence_closure.h b/src/library/tactic/smt/congruence_closure.h index a9ffd6c3fa..f7e2f031e8 100644 --- a/src/library/tactic/smt/congruence_closure.h +++ b/src/library/tactic/smt/congruence_closure.h @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/congr_lemma.h" #include "library/relation_manager.h" #include "library/defeq_canonizer.h" +#include "library/vm/vm.h" #include "library/tactic/simp_result.h" #include "library/tactic/smt/theory_ac.h" @@ -175,6 +176,7 @@ public: unsigned get_gmt() const { return m_gmt; } void inc_gmt() { m_gmt++; } config const & get_config() const { return m_config; } + vm_obj mk_vm_cc_config() const; }; private: diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp index 27747c72ab..c2fce6b0a1 100644 --- a/src/library/tactic/smt/ematch.cpp +++ b/src/library/tactic/smt/ematch.cpp @@ -82,6 +82,15 @@ bool ematch_state::save_instance(expr const & lemma, buffer const & args) return save_instance(key); } +/* +structure ematch_config := +(max_instances : nat) +(max_generation : nat) +*/ +vm_obj ematch_state::mk_vm_ematch_config() const { + return mk_vm_constructor(0, mk_vm_nat(get_config().m_max_instances), mk_vm_nat(get_config().m_max_generation)); +} + /* Allocator for ematching constraints. */ MK_THREAD_LOCAL_GET(small_object_allocator, get_emc_allocator, "ematch constraint"); diff --git a/src/library/tactic/smt/ematch.h b/src/library/tactic/smt/ematch.h index ae3e279304..b0bdcfd27a 100644 --- a/src/library/tactic/smt/ematch.h +++ b/src/library/tactic/smt/ematch.h @@ -44,6 +44,8 @@ public: hinst_lemmas const & get_new_lemmas() const { return m_new_lemmas; } void add_lemma(hinst_lemma const & lemma) { m_new_lemmas.insert(lemma); } void set_lemmas(hinst_lemmas const & lemmas) { m_lemmas.clear(); m_new_lemmas = lemmas; } + ematch_config const & get_config() const { return m_config; } + vm_obj mk_vm_ematch_config() const; }; struct new_instance { diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 56cfa04ee4..e9b0b8d37c 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -31,10 +31,14 @@ Author: Leonardo de Moura #include "library/tactic/smt/smt_state.h" namespace lean { +smt_goal::smt_goal(smt_config_ref const & cfg): + m_cc_state(cfg->m_ho_fns, cfg->m_cc_config), + m_em_state(cfg->m_em_config, cfg->m_em_lemmas), + m_cfg(cfg) { +} + smt_goal::smt_goal(smt_config const & cfg): - m_cc_state(cfg.m_ho_fns, cfg.m_cc_config), - m_em_state(cfg.m_em_config, cfg.m_em_lemmas), - m_pre_config(cfg.m_pre_config) { + smt_goal(std::make_shared(cfg)) { } smt::smt(type_context & ctx, defeq_can_state & dcs, smt_goal & g): @@ -108,8 +112,8 @@ void smt::ematch_using(hinst_lemma const & lemma, buffer & result) static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg); expr smt::normalize(expr const & e) { - type_context::zeta_scope _1(m_ctx, m_goal.m_pre_config.m_zeta); - dsimplify_fn dsimp = mk_dsimp(m_ctx, m_dcs, m_goal.m_pre_config); + type_context::zeta_scope _1(m_ctx, m_goal.get_pre_config().m_zeta); + dsimplify_fn dsimp = mk_dsimp(m_ctx, m_dcs, m_goal.get_pre_config()); return dsimp(e); } @@ -432,7 +436,8 @@ structure smt_pre_config := */ static smt_pre_config to_smt_pre_config(vm_obj const & cfg, tactic_state const & s) { smt_pre_config r; - r.m_simp_lemmas = get_simp_lemmas(to_name(cfield(cfg, 0)), s); + r.m_simp_attr = to_name(cfield(cfg, 0)); + r.m_simp_lemmas = get_simp_lemmas(r.m_simp_attr, s); r.m_max_steps = force_to_unsigned(cfield(cfg, 1)); r.m_zeta = to_bool(cfield(cfg, 2)); return r; @@ -450,7 +455,8 @@ static smt_config to_smt_config(vm_obj const & cfg, tactic_state const & s) { std::tie(r.m_ho_fns, r.m_cc_config) = to_ho_fns_cc_config(cfield(cfg, 0)); r.m_em_config = to_ematch_config(cfield(cfg, 1)); r.m_pre_config = to_smt_pre_config(cfield(cfg, 2), s); - r.m_em_lemmas = get_hinst_lemmas(to_name(cfield(cfg, 3)), s); + r.m_em_attr = to_name(cfield(cfg, 3)); + r.m_em_lemmas = get_hinst_lemmas(r.m_em_attr, s); return r; } @@ -951,6 +957,34 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons LEAN_TACTIC_CATCH(ts); } +/* +structure smt_pre_config := +(simp_attr : name := `pre_smt) +(max_steps : nat := 1000000) +(zeta : bool := ff) + +structure smt_config := +(cc_cfg : cc_config := {}) +(em_cfg : ematch_config := {}) +(pre_cfg : smt_pre_config := {}) +(em_attr : name := `ematch) +*/ +vm_obj smt_tactic_get_config(vm_obj const & ss, vm_obj const & ts) { + if (is_nil(ss)) return mk_smt_state_empty_exception(ts); + smt_goal g = to_smt_goal(head(ss)); + smt_config const & cfg = g.get_config(); + smt_pre_config const & pre = g.get_pre_config(); + + vm_obj cc_cfg = g.get_cc_state().mk_vm_cc_config(); + vm_obj em_cfg = g.get_em_state().mk_vm_ematch_config(); + vm_obj pre_cfg = mk_vm_constructor(0, to_obj(pre.m_simp_attr), mk_vm_nat(pre.m_max_steps), mk_vm_bool(pre.m_zeta)); + vm_obj em_attr = to_obj(cfg.m_em_attr); + + vm_obj r = mk_vm_constructor(0, cc_cfg, em_cfg, pre_cfg, em_attr); + + return mk_smt_tactic_success(r, ss, ts); +} + void initialize_smt_state() { register_trace_class("smt"); register_trace_class(name({"smt", "fact"})); @@ -969,6 +1003,7 @@ void initialize_smt_state() { DECLARE_VM_BUILTIN(name({"smt_tactic", "ematch_using"}), smt_tactic_ematch_using); DECLARE_VM_BUILTIN(name({"smt_tactic", "to_cc_state"}), smt_tactic_to_cc_state); DECLARE_VM_BUILTIN(name({"smt_tactic", "to_em_state"}), smt_tactic_to_em_state); + DECLARE_VM_BUILTIN(name({"smt_tactic", "get_config"}), smt_tactic_get_config); DECLARE_VM_BUILTIN(name({"smt_tactic", "preprocess"}), smt_tactic_preprocess); DECLARE_VM_BUILTIN(name({"smt_tactic", "get_lemmas"}), smt_tactic_get_lemmas); DECLARE_VM_BUILTIN(name({"smt_tactic", "set_lemmas"}), smt_tactic_set_lemmas); diff --git a/src/library/tactic/smt/smt_state.h b/src/library/tactic/smt/smt_state.h index aad7dc358e..54bb667652 100644 --- a/src/library/tactic/smt/smt_state.h +++ b/src/library/tactic/smt/smt_state.h @@ -15,6 +15,7 @@ namespace lean { class smt; struct smt_pre_config { + name m_simp_attr; simp_lemmas m_simp_lemmas; unsigned m_max_steps; bool m_zeta; @@ -25,19 +26,25 @@ struct smt_config { cc_config m_cc_config; ematch_config m_em_config; smt_pre_config m_pre_config; + name m_em_attr; hinst_lemmas m_em_lemmas; }; +typedef std::shared_ptr smt_config_ref; + class smt_goal { friend class smt; cc_state m_cc_state; ematch_state m_em_state; - smt_pre_config m_pre_config; + smt_config_ref m_cfg; public: + smt_goal(smt_config_ref const & cfg); smt_goal(smt_config const & cfg); cc_state const & get_cc_state() const { return m_cc_state; } ematch_state const & get_em_state() const { return m_em_state; } - smt_pre_config const & get_pre_config() const { return m_pre_config; } + smt_pre_config const & get_pre_config() const { return m_cfg->m_pre_config; } + smt_config const & get_config() const { return *m_cfg; } + void add_lemma(hinst_lemma const & lemma) { m_em_state.add_lemma(lemma); } void set_lemmas(hinst_lemmas const & lemmas) { m_em_state.set_lemmas(lemmas); } }; diff --git a/src/library/tactic/smt/util.cpp b/src/library/tactic/smt/util.cpp index c8d4173f12..08c8250b10 100644 --- a/src/library/tactic/smt/util.cpp +++ b/src/library/tactic/smt/util.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "library/annotation.h" #include "library/util.h" #include "library/replace_visitor.h" +#include "library/vm/vm.h" #include "library/tactic/smt/congruence_closure.h" namespace lean {