Formula (gillian.Gil_syntax.Formula)

type t =

| True
(*
Logical true
*)
| False
(*
Logical false
*)
| Not of t
(*
Logical negation
*)
| And of t * t
(*
Logical conjunction
*)
| Or of t * t
(*
Logical disjunction
*)
| Eq of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Expression equality
*)
| Impl of t * t
(*
Logical implication
*)
| FLess of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Expression less-than for numbers
*)
| FLessEq of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Expression less-than-or-equal for numbers
*)
| ILess of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Expression less-than for integers
*)
| ILessEq of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Expression less-than-or-equal for integeres
*)
| StrLess of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Expression less-than for strings
*)
| SetMem of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Set membership
*)
| SetSub of Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t
(*
Set subsetness
*)
| ForAll of (string * Gillian.Gil_syntax.Type.t option) list * t
(*
Forall
*)
| IsInt of Gillian.Gil_syntax.Expr.t
(*
IsInt e <=> (e : float) /\ (e % 1. == 0)
*)

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val equal : t -> t -> Ppx_deriving_runtime.bool

val of_bool : bool -> t

module Set : Stdlib.Set.S with type elt := t

Sets of formulae

val map : 
  (t -> t * bool) option ->
  (t -> t) option ->
  (Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) option ->
  t ->
  t

deprecated
Use Visitors.endo instead

val map_opt : 
  (t -> t option * bool) option ->
  (t -> t) option ->
  (Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t option) option ->
  t ->
  t option

val lvars : t -> Utils.Prelude.SS.t

Get all the logical variables

val pvars : t -> Utils.Prelude.SS.t

Get all the program variables

val alocs : t -> Utils.Prelude.SS.t

Get all the abstract locations

val clocs : t -> Utils.Prelude.SS.t

Get all the concrete locations

val locs : t -> Utils.Prelude.SS.t

Get all locations

val get_print_info : 
  t ->
  Utils.Prelude.SS.t * Utils.Prelude.SS.t * Utils.Prelude.SS.t

Get print info

val lists : t -> Gillian.Gil_syntax.Expr.t list

Get all the logical expressions of the formula of the form (Lit (LList lst)) and (EList lst)

val list_lexprs : t -> Expr.Set.t

Get all the list expressions

val push_in_negations : t -> t

push_in_negations a takes negations off the toplevel of a and pushes them in the leaves. For example push_in_negations (Not (And (True, False))) returns Or (False, False)

val split_conjunct_formulae : t -> t list

Turns f1 /\ f2 /\ f3 into [f1; f2; f3]

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer

val full_pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer with constructors (will not parse)

val lift_logic_expr : Gillian.Gil_syntax.Expr.t -> (t * t) option

Lifts an expression to a formula, if possible. It returns the lifted expression and its negation

val to_expr : t -> Gillian.Gil_syntax.Expr.t option

Unlifts the formula to an expression, if possible

val conjunct : t list -> t

conjunct [a1; ...; an] returns a1 /\ ... /\ an

val disjunct : t list -> t

disjunct [a1; ...; an] returns a1 \/ ... \/ an

val subst_expr_for_expr : 
  to_subst:Gillian.Gil_syntax.Expr.t ->
  subst_with:Gillian.Gil_syntax.Expr.t ->
  t ->
  t

val subst_clocs : (string -> Gillian.Gil_syntax.Expr.t) -> t -> t

subst_clocs subst e Substitutes expressions of the form Lit (Loc l) with subst l in e

val get_disjuncts : t -> t list

get_disjuncts (a1 \/ ... \/ an) returns [a1; ...; an]

val strings_and_numbers : t -> string list * float list

Returns a list of strings and a list of numbers that are contained in the formula

module Infix : sig ... end