Module Astral_internal.SL

module Variable : sig ... end
module Term : sig ... end
type t
include Logic_sig.LOGIC with type t := t and type term := Term.t and module Sort = Sort and module Variable := Variable
module Sort = Sort
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := t
val pp : Stdlib.Format.formatter -> t -> unit

Output to formatter

val print : ?prefix:string -> t -> unit

Output to stdout.

val show_option : t option -> string
val print_option : ?prefix:string -> t option -> unit
val dump : string -> t -> unit

Dump to file given by filename

Lists of printable values

val show_list : ?separator:string -> t list -> string
val pp_list : Stdlib.Format.formatter -> t list -> unit
val print_list : ?separator:string -> ?prefix:string -> t list -> unit
include Datatype_sig.COMPARABLE with type t := t
include Datatype_sig.COMPARISON with type t := t
include Datatype_sig.COLLECTIONS with type t := t
include Logic_sig.SORTED with type t := t and module Sort := Sort
val get_sort : t -> Sort.t
val has_sort : Sort.t -> t -> bool
val show_with_sort : t -> string
val hash : t -> int
val of_var : Variable.t -> t
val of_const : Constant.t -> t
val get_sort_in_term : string -> t -> Sort.t
val get_operands : t -> t list
val is_ground : ground:Variable.t list -> t -> bool
val is_ground' : forbidden:Variable.t list -> t -> bool

True if the term does not contatin any of provided variables.

val show : t -> string
val equal : t -> t -> bool
val compare : t -> t -> int
val map : (t -> t) -> t -> t
val get_vars : t -> Variable.t list

Return all variables, without duplicates.

val bound_vars : t -> Variable.t list
val rename_var : string -> string -> t -> t
val exists : (t -> bool) -> t -> bool
val for_all : (t -> bool) -> t -> bool
val select_subformulae : (t -> bool) -> t -> t list
val substitute : t -> var:Variable.t -> by:Term.t -> t
val substitute_list : t -> vars:Variable.t list -> by:Term.t list -> t
val replace_subformula : t -> subformula:t -> by:t -> t
val size : t -> int
type ast
val to_ast : ?dagify:bool -> t -> ast
val output_ast : string -> ast -> unit
val to_smt2 : t -> string

Human readable SMT-LIB string.

val to_sexp : t -> Sexplib.Sexp.t

S-expression representation used to generate SMT-LIB string. Usefull when printing a formula embeded in a larger s-expr.

type pred_sigs := (string * Sort.t list) list
val to_bench : ?pred_sigs:pred_sigs -> ?source:string -> ?status:[< `Sat | `Unsat | `Unknown ] -> ?options:string -> t -> string
val output_benchmark : ?pred_sigs:pred_sigs -> ?source:string -> ?status:[< `Sat | `Unsat | `Unknown ] -> ?options:string -> string -> t -> unit
val (===) : t -> t -> bool
type view =
  1. | Emp
  2. | True
  3. | False
  4. | Pure of SMT.t
  5. | Eq of Term.t list
  6. | Distinct of Term.t list
  7. | PointsTo of Term.t * MemoryModel.StructDef.t * Term.t list
  8. | Predicate of string * Term.t list * MemoryModel.StructDef.t list
  9. | And of t list
  10. | Or of t list
  11. | Not of t
  12. | GuardedNeg of t * t
  13. | Ite of t * t * t
  14. | Exists of Variable.t list * t
  15. | Forall of Variable.t list * t
  16. | Star of t list
  17. | Septraction of t * t
include Logic_sig.WITH_VIEW with type t := t and type view := view
val view : t -> view
val map_view : (view -> [< `Modify of t | `Skip ]) -> t -> t

Apply an action at each node of AST: TODO: add description of actions

include Datatype_sig.COLLECTIONS with type t := t
module Set : Datatype_sig.SET with type elt = t

Set over type t

module MonoList : Datatype_sig.MONO_LIST with type key = t and type t = t list

Monomorphic list over type t

module Map : Datatype_sig.MAP with type key = t

Polymorphic map from t to 'a

module MonoMap (Data : Datatype_sig.SHOW) : Datatype_sig.MONO_MAP with type key = t and type data = Data.t

Monomorphic map from t to Data.t

val of_smt : SMT.t -> t

Constructors

val nil : t
val mk_var : string -> Sort.t -> t

Create SL term consisting of a location variable with given name.

val mk_fresh_var : string -> Sort.t -> t

Create SL term consisting of a fresh location variable with given name.

val mk_eq : Term.t list -> t
val mk_eq2 : Term.t -> Term.t -> t
val mk_distinct : Term.t list -> t
val mk_distinct2 : Term.t -> Term.t -> t
val mk_pto_struct : Term.t -> MemoryModel.StructDef.t -> Term.t list -> t

Low-level pointer constructor

val mk_pto_tuple : Term.t -> Term.t list -> t

Create a term representing points-to: x -> (y_0, ..., y_(n-1)).

This will create a points-to assertion using a structure definition named *tuple_n* with fields *f_0*, ..., *f_(n-1)*.

val mk_pto : Term.t -> Term.t -> t

Create a term representing a pointer with a single target location.

val mk_predicate : string -> ?structs:MemoryModel.StructDef.t list -> Term.t list -> t

Create an instance of an inductive predicate with given name. This instance can be parametrised by a list of structures. For example, Astral's built-in list-segment predicate can be parametrised by any structure with a single field with sort same as the sort of instantance's arguments.

val emp : t
val tt : t
val ff : t
val mk_pure : SMT.t -> t

Create a pure assertion as a separation logic formula. The input has to be of boolean sort.

Note that pure formula are satisfiable only on empty footprints. Thus, (pure true) is equivalent to emp.

val negate_pure : t -> t
val mk_not : t -> t
val mk_star : t list -> t
val mk_and : t list -> t
val mk_or : t list -> t
val mk_implies : t -> t -> t
val mk_iff : t list -> t
val mk_ite : t -> t -> t -> t
val mk_multiple_ite : (t * t) list -> t -> t
val mk_gneg : t -> t -> t
val mk_septraction : t -> t -> t
val mk_wand : t -> t -> t
val mk_exists : Variable.t list -> t -> t
val mk_forall : Variable.t list -> t -> t
val mk_exists' : Sort.t list -> (Term.t list -> t) -> t
val mk_forall' : Sort.t list -> (Term.t list -> t) -> t

Properties

val is_false : t -> bool
val is_emp : t -> bool
val is_pointer : t -> bool
val is_spatial_atom : t -> bool

Fragment classification

val is_pure : t -> bool

Boolean combination of (dis-)equalities over location variables.

val is_pure_smt : t -> bool

No location variables.

val is_atom : t -> bool
val is_nil : t -> bool
val is_predicate : t -> bool
val is_atomic : t -> bool
val is_symbolic_heap : t -> bool
val is_symbolic_heap_entl : t -> bool
val is_negation_free : t -> bool
val is_positive : t -> bool
val is_quantifier_free : t -> bool
val is_low_level : t -> bool
type fragment =
  1. | SymbolicHeap_SAT
  2. | SymbolicHeap_ENTL
  3. | Positive
  4. | Arbitrary
  5. | Atomic
val show_fragment : fragment -> string
val classify_fragment : t -> fragment
type query =
  1. | SymbolicHeap_SAT of t
  2. | SymbolicHeap_ENTL of t * t
  3. | Arbitrary of t
val as_equality : t -> Term.t list option
val as_pointer : t -> Term.t * MemoryModel.StructDef.t * Term.t list
val as_predicate : t -> string * Term.t list
val as_query : t -> query
val as_entailment : t -> t * t
val get_fields : t -> MemoryModel.Field.t list
val get_all_sorts : ?with_nil:bool -> t -> Sort.t list

Syntactic manipulation

val skolemisation : t -> t * Variable.t list
val free_vars : ?with_nil:bool -> ?with_pure:bool -> t -> Variable.t list
val free_vars_of_sort : Sort.t -> t -> Variable.t list
val get_terms : t -> Term.t list
val get_terms_of_sort : Sort.t -> t -> Term.t list
val get_root : t -> Term.t

Operations requiring the sort of heap

val get_loc_terms : ?with_free_vars:bool -> t -> HeapSort.t -> Term.t list
module Infix : sig ... end

Misc

val as_symbolic_heap : t -> t list * t list
val as_quantified_symbolic_heap : t -> Variable.t list * t list
val translate_pure_with_heap_term : (Term.t -> SMT.t) -> t -> SMT.t
val pointer_size : t -> int option