michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/simplifier/simplifier_actions): update target when simplifier produces a definitionally equal output that is not structurally equal

Browse source 
This update also uses the even target_updated to decide when the target
needs to be updated.
This commit is contained in:
Leonardo de Moura 2015-11-22 17:25:54 -08:00
parent 0c4fb6b3d5
commit 8681b34129
1 changed files with 19 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/blast/simplifier/simplifier_actions.cpp
View file

@ -16,12 +16,14 @@ namespace blast {
static unsigned g_ext_id = 0; static unsigned g_ext_id = 0;
struct simplifier_branch_extension : public branch_extension { struct simplifier_branch_extension : public branch_extension {
simp_rule_sets m_srss; simp_rule_sets m_srss;
bool m_simp_target{false}; // true if target needs to be simplified again
simplifier_branch_extension() {} simplifier_branch_extension() {}
simplifier_branch_extension(simplifier_branch_extension const & b): simplifier_branch_extension(simplifier_branch_extension const & b):
m_srss(b.m_srss) {} m_srss(b.m_srss) {}
virtual ~simplifier_branch_extension() {} virtual ~simplifier_branch_extension() {}
virtual branch_extension * clone() override { return new simplifier_branch_extension(*this); } virtual branch_extension * clone() override { return new simplifier_branch_extension(*this); }
virtual void initialized() override { m_srss = ::lean::get_simp_rule_sets(env()); } virtual void initialized() override { m_srss = ::lean::get_simp_rule_sets(env()); }
virtual void target_updated() override { m_simp_target = true; }
virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) override { } virtual void hypothesis_activated(hypothesis const &, hypothesis_idx) override { }
virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) override { } virtual void hypothesis_deleted(hypothesis const &, hypothesis_idx) override { }
simp_rule_sets const & get_simp_rule_sets() const { return m_srss; } simp_rule_sets const & get_simp_rule_sets() const { return m_srss; }
@ -67,14 +69,24 @@ public:
action_result simplify_target_action() { action_result simplify_target_action() {
if (!get_config().m_simp) if (!get_config().m_simp)
return action_result::failed(); return action_result::failed();
auto & ext = get_extension();
if (!ext.m_simp_target)
return action_result::failed(); // nothing to be done
ext.m_simp_target = false;
state & s = curr_state(); state & s = curr_state();
expr target = s.get_target(); expr target = s.get_target();
bool iff = use_iff(target); bool iff = use_iff(target);
name rname = iff ? get_iff_name() : get_eq_name(); name rname = iff ? get_iff_name() : get_eq_name();
auto r = simplify(rname, target, get_extension().get_simp_rule_sets()); auto r = simplify(rname, target, ext.get_simp_rule_sets());
if (!r.has_proof()) if (r.get_new() == target)
return action_result::failed(); // did nothing return action_result::failed(); // did nothing
if (r.has_proof()) {
// Remark: we only need to create the proof step if a proof was generated.
// If a proof was not generated and the resulting expression is not
// structurally equal, then they are definitionally equal and no proof is
// needed
s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof())); s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof()));
}
s.set_target(r.get_new()); s.set_target(r.get_new());
trace_action("simplify"); trace_action("simplify");
return action_result::new_branch(); return action_result::new_branch();