Class Model_parser.clean

class clean : object .. end

Helper class which can be inherited by API users to clean a model, for example by removing elements that do not match a given condition, or removing some "useless" fields in records, etc.


method model : model -> model
method element : model_element -> model_element option
method value : concrete_syntax_term -> concrete_syntax_term option
method var : string -> concrete_syntax_term option
method const : concrete_syntax_constant ->
concrete_syntax_term option
method integer : concrete_syntax_int -> concrete_syntax_term option
method string : string -> concrete_syntax_term option
method real : concrete_syntax_real -> concrete_syntax_term option
method fraction : concrete_syntax_frac -> concrete_syntax_term option
method float : concrete_syntax_float ->
concrete_syntax_term option
method boolean : bool -> concrete_syntax_term option
method bitvector : concrete_syntax_bv -> concrete_syntax_term option
method apply : string ->
concrete_syntax_term list ->
concrete_syntax_term option
method cond : concrete_syntax_term ->
concrete_syntax_term ->
concrete_syntax_term -> concrete_syntax_term option
method epsilon : string ->
concrete_syntax_term -> concrete_syntax_term option
method neg : concrete_syntax_term -> concrete_syntax_term option
method quant : concrete_syntax_quant ->
string list ->
concrete_syntax_term -> concrete_syntax_term option
method binop : concrete_syntax_binop ->
concrete_syntax_term ->
concrete_syntax_term -> concrete_syntax_term option
method func : string list ->
concrete_syntax_term -> concrete_syntax_term option
method funliteral : concrete_syntax_funlit_elts list ->
concrete_syntax_term -> concrete_syntax_term option
method record : (string * concrete_syntax_term) list ->
concrete_syntax_term option
method proj : string ->
concrete_syntax_term -> concrete_syntax_term option