[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Rewriting




Hi,

I have a rewrite rule:

new_rewrite_next_rb_ready: LEMMA
	FORALL(q:state_I,s:schedule,i:inputs_type,rbi:rbindex):
	NOT (ifu_instr_issued?(q,s,i) AND rbi = rb_head(q)) 
		IMPLIES
	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
[-2]  ...
[-3]  ...
  |-------
[1]   ifu_instr_issued?(q!1, s!1, i!1) AND rbi!1 = rb_head(q!1)
[2]   ...


(assert) simply doesn't rewrite with this. Tracking that 
produces:

;;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?

Thanks
Ravi