[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
I have a rewrite rule:
NOT (ifu_instr_issued?(q,s,i) AND rbi = rb_head(q))
next_rb_ready(q,s,i)(rbi) = rb_ready_wb(q,s,i,rb_ready(q))(rbi)
This is installed as an (eager) auto-rewrite rule.
Then I have a sequent:
[-1] next_rb_ready(q!1, s!1, i!1)(rbi!1) = rb_ready!1
 ifu_instr_issued?(q!1, s!1, i!1) AND rbi!1 = rb_head(q!1)
(assert) simply doesn't rewrite with this. Tracking that
;;new_rewrite_next_rb_ready failed to rewrite
;;next_rb_ready(q!1, s!1, i!1)(rbi!1)
;;;;Hypothesis NOT (ifu_instr_issued?(q!1, s!1, i!1) AND
rbi!1 = rb_head(q!1)) did not simplify.
The rule "rewrite" however works.
Rule? (rewrite "new_rewrite_next_rb_ready")
Found matching substitution:
rbi: rbindex gets rbi!1,
i: inputs_type gets i!1,
s: schedule gets s!1,
q: state_I gets q!1,
Rewriting using new_rewrite_next_rb_ready, matching in *,
Why is assert not rewriting? Can I tell it something more so
that it simplifies as I want?