Module Gil_syntax.Formula

GIL Formulae

type t =
  1. | True
    (*

    Logical true

    *)
  2. | False
    (*

    Logical false

    *)
  3. | Not of t
    (*

    Logical negation

    *)
  4. | And of t * t
    (*

    Logical conjunction

    *)
  5. | Or of t * t
    (*

    Logical disjunction

    *)
  6. | Eq of Expr.t * Expr.t
    (*

    Expression equality

    *)
  7. | Impl of t * t
    (*

    Logical implication

    *)
  8. | FLess of Expr.t * Expr.t
    (*

    Expression less-than for numbers

    *)
  9. | FLessEq of Expr.t * Expr.t
    (*

    Expression less-than-or-equal for numbers

    *)
  10. | ILess of Expr.t * Expr.t
    (*

    Expression less-than for integers

    *)
  11. | ILessEq of Expr.t * Expr.t
    (*

    Expression less-than-or-equal for integeres

    *)
  12. | StrLess of Expr.t * Expr.t
    (*

    Expression less-than for strings

    *)
  13. | SetMem of Expr.t * Expr.t
    (*

    Set membership

    *)
  14. | SetSub of Expr.t * Expr.t
    (*

    Set subsetness

    *)
  15. | ForAll of (string * Type.t option) list * t
    (*

    Forall

    *)
  16. | IsInt of 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 -> (Expr.t -> Expr.t) option -> t -> t
val map_opt : (t -> t option * bool) option -> (t -> t) option -> (Expr.t -> 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

Get print info

val lists : t -> Expr.t list

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

val list_lexprs : t -> Gil_syntax.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 : 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 -> 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:Expr.t -> subst_with:Expr.t -> t -> t
val subst_clocs : (string -> 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