sig
  type rule = {
    discrete : DiscreteRule.rule;
    dynamics : Formula.eq_sys;
    update : Formula.eq_sys;
    inv : Formula.formula;
    post : Formula.formula;
  }
  val make_rule :
    (string * (string list * Formula.formula)) list ->
    DiscreteRule.rule ->
    Formula.eq_sys ->
    Formula.eq_sys ->
    ?inv:Formula.formula ->
    ?post:Formula.formula -> unit -> ContinuousRule.rule
  val str : ContinuousRule.rule -> string
  val fprint_full : bool -> Format.formatter -> ContinuousRule.rule -> unit
  val fprint : Format.formatter -> ContinuousRule.rule -> unit
  val print : ContinuousRule.rule -> unit
  val sprint : ContinuousRule.rule -> string
  val matching_str : Structure.structure -> (string * int) list -> string
  val apply_to_side :
    bool ->
    (Structure.structure -> Structure.structure * 'a) ->
    (string * int) list ->
    (string * (string list * Formula.formula)) list ->
    ContinuousRule.rule -> ContinuousRule.rule
  val lhs : ContinuousRule.rule -> Structure.structure option
  val rhs : ContinuousRule.rule -> Structure.structure option
  val map_to_formulas :
    (Formula.formula -> Formula.formula) ->
    ContinuousRule.rule -> ContinuousRule.rule
  val fold_over_formulas :
    (Formula.formula -> 'a -> 'a) -> ContinuousRule.rule -> 'a -> 'a
  val matches :
    Structure.structure -> ContinuousRule.rule -> DiscreteRule.matching list
  val matches_post :
    Structure.structure ->
    ContinuousRule.rule list ->
    ContinuousRule.rule -> float -> DiscreteRule.matching list
  val rewrite_single_nocheck :
    Structure.structure ->
    ContinuousRule.rule list ->
    float ->
    DiscreteRule.matching ->
    ContinuousRule.rule ->
    float ->
    (string * float) list ->
    Structure.structure * float * ((string * string) * float list) list
  val rewrite_single :
    Structure.structure ->
    ContinuousRule.rule list ->
    float ->
    DiscreteRule.matching ->
    ContinuousRule.rule ->
    float ->
    (string * float) list ->
    (Structure.structure * float * ((string * string) * float list) list)
    option
  val compare_diff :
    ?cmp_funs:(float -> float -> bool) ->
    ContinuousRule.rule -> ContinuousRule.rule -> bool * string
end