Module Astral_internal.BaseLogic

val do_simplification : bool Stdlib.ref

Enable/disable simplification for debugging

val use_simplification : bool -> unit
module Variable : sig ... end
module Sort = Sort
module Application : sig ... end
type t =
  1. | Variable of Variable.t
  2. | Application of Application.t * t Stdlib.List.t
  3. | Binder of binder * Variable.t Stdlib.List.t * t
and range = t Stdlib.List.t Stdlib.Lazy.t
and binder =
  1. | Exists of range Stdlib.List.t option
  2. | Forall of range Stdlib.List.t option
  3. | Exists2 of range Stdlib.List.t option
  4. | Forall2 of range Stdlib.List.t option
val equal_range : range -> range -> bool
val equal_binder : binder -> binder -> bool
val compare_range : range -> range -> int
val compare_binder : binder -> binder -> int
module Binder : sig ... end
val get_sort : t -> Variable.Sort.t
val has_sort : Sort.t -> t -> bool
val show_with_sort : t -> string
val is_quantifier_free : t -> bool
module Self : sig ... end
include sig ... end
val pp : Stdlib.Format.formatter -> Self.t -> unit
val print : ?prefix:string -> Self.t -> unit
val show_option : Self.t option -> string
val print_option : ?prefix:string -> Self.t option -> unit
val dump : string -> Self.t -> unit
val show_list : ?separator:string -> Self.t list -> string
val pp_list : Stdlib.Format.formatter -> Self.t list -> unit
val print_list : ?separator:string -> ?prefix:string -> Self.t list -> unit
include sig ... end
val show : Self.t -> string
val compare : Self.t -> Self.t -> int
val equal : Self.t -> Self.t -> bool
include sig ... end
module Set : sig ... end
module MonoList : sig ... end
module Map : sig ... end
module MonoMap (Data : sig ... end) : sig ... end
val hash : 'a -> int
val is_var : t -> bool
val is_atom : t -> bool
val is_constant : t -> bool
val mk_var : string -> Variable.Sort.t -> t
val mk_fresh_var : string -> Variable.Sort.t -> t
val mk_app : Application.t -> t Stdlib.List.t -> t
val mk_constant : Constant.t -> t
val mk_binder : binder -> Variable.t Stdlib.List.t -> t -> t
val of_var : Variable.t -> t
val of_const : Constant.t -> t
val to_constant : t -> Constant.t

Higher-order function

val map : (t -> t) -> t -> t
val map' : (t -> 'a) -> t -> 'a
val map_vars : (Variable.t -> t) -> t -> t
val map_app : (Application.t -> t list -> t) -> t -> t
val skolemisation : t -> t * Variable.t list

TODO: works only for SL (not implication etc.)

Predicates

val for_all : (t -> bool) -> t -> bool
val exists : (t -> bool) -> t -> bool
val for_all_apps : (Application.t -> bool) -> t -> bool

Variables & terms

val get_vars : t -> Variable.t list
val free_vars : t -> Variable.t list
val bound_vars : t -> Variable.t list
val free_vars_of_sort : Variable.Sort.t -> t -> Variable.t list
val is_ground : ground:Variable.t list -> t -> bool
val is_ground' : forbidden:Variable.t list -> t -> bool
val get_all_sorts : t -> Sort.t list
val rename_var : Stdlib.String.t -> string -> t -> t

Subformulae

val select_subformulae : (t -> bool) -> t -> t list
val positive_polarity : 'a -> Self.t -> bool

Substitutions

val substitute : t -> var:Variable.t -> by:t -> t
val replace_subformula : Self.t -> subformula:Self.t -> by:Self.t -> Self.t
val substitute_list : t -> vars:Variable.t list -> by:t list -> t
val (===) : Self.t -> Self.t -> bool
val get_sort_in_term : Stdlib.String.t -> t -> Variable.Sort.t
val get_sorts : t -> Sort.t list
val get_operands : t -> t Stdlib.List.t

Constructors

type type_error = string * string * Sort.t * t
val show_type_error : (string * string * Sort.t * Self.t) -> string
exception TypeError of type_error
val cnt : int Stdlib.ref
val check_type_prop : what:string -> expects:string -> (Variable.Sort.t -> bool) -> t -> unit
val check_type : what:string -> Sort.t -> t -> unit
val check_types : what:string -> Sort.t list -> t list -> unit
val check_same_type : what:string -> t list -> unit
val mk_smart_app_aux : Application.t -> Self.t option -> Self.t option -> Self.t list -> Self.t
val mk_smart_app : Application.t -> ?neutral:Self.t -> ?anihilator:Self.t -> Self.t Stdlib.List.t -> Self.t
module DefaultVars : sig ... end
module Boolean0 : sig ... end
module Equality : sig ... end
module Boolean : sig ... end
module Enumeration : sig ... end
module Arithmetic : sig ... end
module Sets : sig ... end
module Array : sig ... end
module Bitvector : sig ... end
module Quantifiers : sig ... end
module SeparationLogic : sig ... end

TODO

Higher-order functions

Scanning & Searching

val exists_app : (Application.t -> bool) -> t -> bool

Others

val size : t -> int

Printing and conversions

module F = Stdlib.Format
val declare_var : Variable.t -> string
val header : 'a -> t -> string option -> [< `Sat | `Unknown | `Unsat ] option -> string option -> string
val binder_var : Variable.t -> Sexplib.Sexp.t
type sexp_action =
  1. | App of string
  2. | Direct of Sexplib.Sexp.t list -> Sexplib.Sexp.t
  3. | Modify of string * t list
  4. | Skip
val app_to_sexp : Application.t -> t list -> sexp_action
val to_sexp : t -> Sexplib.Sexp.t
val to_smt2 : t -> string
val introduce_casts : ?expected:Sort.t -> (string * Sort.t list) list -> t -> t
val to_sexp_aux : t -> string
val to_bench : ?pred_sigs:(string * Sort.t list) list -> ?source:string -> ?status:[< `Sat | `Unknown | `Unsat ] -> ?options:string -> t -> string
val output_benchmark : ?pred_sigs:(string * Sort.t list) list -> ?source:string -> ?status:[< `Sat | `Unknown | `Unsat ] -> ?options:string -> string -> t -> unit
module U = UnicodeSymbols
module Vertex : sig ... end
module Edge : sig ... end

Integer as edge labels should ensure that children are sorted as intended.

module G : sig ... end
val edge_label : G.E.t -> string
module DotConfig : sig ... end
module Dot : sig ... end
type ast = G.t

Pretty application

type action =
  1. | Stop of string
  2. | Continue of string
  3. | ContinueWith of string * t list
val fold_heap_term : MemoryModel.Field.t -> ?n:int -> Self.t -> action
val fold_select : Self.t -> ?n:int -> Self.t -> action
val pretty_node_name : t -> action

TODO:

  • make the construction bottom-up for even prettier printing
  • constant sets
val to_ast : ?dagify:bool -> t -> G.t
val output_ast : string -> DotConfig.t -> unit