Module Astral_internal.SMT

type t

Abstract type of SMT formulae.

type var
type range = t list Stdlib.Lazy.t list
type view =
  1. | Constant of Stdlib.String.t * Sort.t
  2. | Variable of var
  3. | True
  4. | False
  5. | And of t list
  6. | Or of t list
  7. | Not of t
  8. | Implies of t * t
  9. | Iff of t list
  10. | IfThenElse of t * t * t
  11. | Equal of t list
  12. | Distinct of t list
  13. | LesserEq of t * t
  14. | Exists of var list * range option * t
  15. | Forall of var list * range option * t
  16. | Exists2 of var list * range option * t
  17. | Forall2 of var list * range option * t
  18. | IntConst of int
  19. | Plus of t list
  20. | Minus of t * t
  21. | Mult of t list
  22. | BitConst of Bitvector.t
  23. | BitCheck of t * t
  24. | BitNot of t
  25. | BitAnd of t list * Sort.t
  26. | BitOr of t list * Sort.t
  27. | BitXor of t list * Sort.t
  28. | BitPlus of t list * Sort.t
  29. | BitImplies of t * t
  30. | BitNeg of t
  31. | BitShiftLeft of t * t
  32. | BitShiftRight of t * t
  33. | BitLesser of t * t
  34. | BitLesserEqual of t * t
  35. | ConstArr of t * Sort.t
  36. | Select of t * t
  37. | Store of t * t * t
  38. | Membership of t * t
  39. | Subset of t * t
  40. | Disjoint of t list
  41. | Union of t list * Sort.t
  42. | Inter of t list * Sort.t
  43. | Diff of t * t
  44. | Compl of t
  45. | Enumeration of t list * Sort.t
include Logic_sig.LOGIC with type t := t and module Sort = Sort and type Variable.t = var and type term := t
module Sort = Sort
module Variable : Logic_sig.VARIABLE with module Sort = Sort with type t = var
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 mk_var : string -> Sort.t -> t
val mk_fresh_var : string -> Sort.t -> t
val get_all_sorts : t -> Sort.t list
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_quantifier_free : t -> bool
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 free_vars : t -> Variable.t list
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:t -> t
val substitute_list : t -> vars:Variable.t list -> by: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
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 SMT_sig.EQUALITY with type t := t
val mk_eq : t list -> t
val mk_distinct : t list -> t
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 is_var : t -> bool
val is_constant : t -> bool
val to_constant : t -> Constant.t
module Boolean : sig ... end
module Range : sig ... end
module Quantifier : sig ... end
module Enumeration : sig ... end
module Arithmetic : sig ... end
module Bitvector : sig ... end
module Array : sig ... end
module Sets : sig ... end
module Model : sig ... end