Previous  Up  Next

Module Formula

module Formula: sig .. end
Represent formulas with first-order, mso, and real variables.

Basic Type Definitions.


type var = [ `Const of string | `FO of string | `Real of string | `SO of string ]
What we call variables can be a constant, a first-order variable, a second-order variable, or a real-valued variable.
type const_var = [ `Const of string ] 
type fo_var = [ `FO of string ] 
type const_or_fo_var = [ `Const of string | `FO of string ] 
type so_var = [ `SO of string ] 
type real_var = [ `Real of string ] 
val var_of_string : string -> var
We recognize if the variable is FO (x), MSO (X), SO (|x) or Real (:x).
val const_var_of_string : string -> const_var
val fo_var_of_string : string -> fo_var
val const_or_fo_var_of_string : string -> const_or_fo_var
val so_var_of_string : string -> so_var
val real_var_of_string : string -> real_var
val is_const : var -> bool
Check variable type.
val is_fo : var -> bool
val is_so : var -> bool
val is_real : var -> bool
val to_const : var -> const_var
Casts to particular variable types.
val to_fo : var -> fo_var
val to_const_or_fo : var -> const_or_fo_var
val to_so : var -> so_var
val to_real : var -> real_var
val var_tup : [< var ] array -> var array
val compare_vars : ([< var ] as 'a) -> 'a -> int
Compare two variables. We assume FO < MSO < SO < Real.
val compare_var_lists : ([< var ] as 'a) list -> 'a list -> int
val compare_var_tups : ([< var ] as 'a) array -> 'a array -> int
type sign_op =
| EQZero
| GZero
| LZero
| GEQZero
| LEQZero
| NEQZero
Sign operands.
val sign_op_str : ?unicode:bool -> sign_op -> string
Print a sign_op as string.
type formula =
| Rel of string * const_or_fo_var array
| Eq of const_or_fo_var * const_or_fo_var
| SO of so_var * const_or_fo_var array
| RealExpr of real_expr * sign_op
| Not of formula
| And of formula list
| Or of formula list
| Ex of var list * formula
| All of var list * formula
| Lfp of so_var * fo_var array * formula
| Gfp of so_var * fo_var array * formula
| Let of string * string list * formula * formula
This type describes formulas of relational logic with equality. We allow only simple boolean junctors, other are resolved during parsing.
type real_expr =
| RVar of string
| Const of float
| Plus of real_expr * real_expr
| Times of real_expr * real_expr
| Pow of real_expr * real_expr
| Fun of string * const_or_fo_var
| Char of formula
| Sum of fo_var list * formula * real_expr
| RLet of string * real_expr * real_expr
Real-valued terms allow counting, characteristic functions, arithmetic.
val size : ?acc:int -> formula -> int
val size_real : ?acc:int -> real_expr -> int
val so_compare_weight : int Pervasives.ref
Weight of SO atoms when comparing, defaults to 1.
val compare : formula -> formula -> int
Compare two formulas.
val compare_re : real_expr -> real_expr -> int
Compare two real expressions.
val is_atom : formula -> bool
val is_literal : formula -> bool
type eq_sys = ((string * string) * real_expr) list
Equation system: a left-hand-side f,a actually represents Fun (f, `FO a)

Printing Functions


val var_str : [< var ] -> string
Print a variable as a string.
val var_list_str : [< var ] list -> string
Print a variable list as a string.
val str : ?unicode:bool -> formula -> string
Print a formula as a string.
val mona_str : formula -> string
val print : ?unicode:bool -> formula -> unit
val sprint : ?unicode:bool -> formula -> string
val fprint : ?unicode:bool -> Format.formatter -> formula -> unit
val real_str : ?unicode:bool -> real_expr -> string
Print a real_expr as a string.
val print_real : ?unicode:bool -> real_expr -> unit
val sprint_real : ?unicode:bool -> real_expr -> string
val fprint_real : ?unicode:bool -> Format.formatter -> real_expr -> unit
val fprint_prec : bool -> int -> Format.formatter -> formula -> unit
val fprint_real_prec : bool -> int -> Format.formatter -> real_expr -> unit
val fprint_eqs : ?unicode:bool -> ?diff:bool -> Format.formatter -> eq_sys -> unit
Print an equation system.
val eq_str : ?unicode:bool -> ?diff:bool -> eq_sys -> string

Formula syntax check


val syntax_ok : ?sg:(string * int) list Pervasives.ref ->
       ?fp:(string * bool) list -> ?pos:bool -> formula -> bool
We check that relations and SO variables appear with unique arities and that fixed-point variables appear only positively.
val syntax_ok_re : ?sg:(string * int) list Pervasives.ref ->
       ?fp:(string * bool) list -> ?pos:bool -> real_expr -> bool

Basic flattening functions.


val flatten : formula -> formula
Only flatten the formula.
val flatten_re : real_expr -> real_expr
val flatten_sort : formula -> formula
Flatten and sort multiple or's and and's.
val flatten_sort_re : real_expr -> real_expr

Runge - Kutta method for real-expr defined equation systems.

*
val compile : string -> eq_sys -> float -> float array -> float array
Compile eq_sys to function.
val rk4_step : float ->
       float -> (float -> float array -> float array) -> float array -> float array
Perform a Runge-Kutta (RK4) step for vars with vals_init and right-hand side eq_terms. Time variable tvar starts at tinit and moves tstep.
val rkCK_default_start : unit ->
       float Pervasives.ref * float Pervasives.ref * float Pervasives.ref *
       float Pervasives.ref
Implements the Cash-Karp algorithm with varying order and adaptive step, precisely as described in the paper "A Variable Order Runge-Kutta Method for Initial Value Problems with Varying Right-Hand Sides" by J. R. Cash and Alan H. Karp, ACM Trans. Math. Software, 1990. The interface is as in rk4_step above, except now the tolerance is used (given by epsilon) and some initial references must be set (use the ones from rkCK_default_start). We also return time passed and next step size.
val rkCK_step : ?epsilon:float ->
       float Pervasives.ref * float Pervasives.ref * float Pervasives.ref *
       float Pervasives.ref ->
       float ->
       float ->
       (float -> float array -> float array) ->
       float array -> float array * float * float

Hash-consed Formulas and Real Expressions.


type raw_formula =
| HRel of string * const_or_fo_var array
| HEq of const_or_fo_var * const_or_fo_var
| HSO of so_var * const_or_fo_var array
| HRealExpr of hc_real_expr * sign_op
| HNot of hc_formula
| HAnd of hc_formula list
| HOr of hc_formula list
| HEx of var list * hc_formula
| HAll of var list * hc_formula
| HLfp of so_var * fo_var array * hc_formula
| HGfp of so_var * fo_var array * hc_formula
| HLet of string * string list * hc_formula * hc_formula
The raw and hash-consed types.
type raw_real_expr =
| HRVar of string
| HConst of float
| HPlus of hc_real_expr * hc_real_expr
| HTimes of hc_real_expr * hc_real_expr
| HPow of hc_real_expr * hc_real_expr
| HFun of string * const_or_fo_var
| HChar of hc_formula
| HSum of fo_var list * hc_formula * hc_real_expr
| HRLet of string * hc_real_expr * hc_real_expr 
type hc_formula = raw_formula HashCons.hc 
type hc_real_expr = raw_real_expr HashCons.hc 
module FormulaCons: HashCons.S  with type data = raw_formula 
                                 and type other_value = int list
Hash-consed formula module. 
module RealExprCons: HashCons.S  with type data = raw_real_expr 
                                  and type other_value = int list
Hash-consed formula module. 
val hc : formula -> hc_formula
Hash-cons a formula.
val hc_real : real_expr -> hc_real_expr
Hash-cons a real expression.
val cAnd : hc_formula list -> hc_formula
Hash-cons a conjunction.
val unhc : hc_formula -> formula
Un-hash-cons a formula.
val unhc_real : hc_real_expr -> real_expr
Un-hash-cons a real expression.