Require Import Coqlib Floats Values Memory.
Require Import Integers.
Require Import Op Registers.
Require Import BTL_SEtheory.
Require Import BTL_SEsimuref.

Import SvalNotations.

Expansions and rewrites of macro-instructions using "fake" symbolic values

Definition rewrite_ops (RRULES: rrules_set) (op: operation) (lsv: list sval) (iinfo : option BTL.inst_info)
  : option (sval * list okclause) :=
  None.

Definition rewrite_cbranches (RRULES: rrules_set)
  (cond: condition) (args: list sval) (iinfo : BTL.inst_info) : option (condition * list_sval * list okclause) :=
  None.