smtlib-utils 0.5 (latest) · OCaml Package

Trivial AST for parsing

val pp_to_string : (Format.formatter -> 'a -> unit) -> 'a -> string

type var = string

type ty_var = string

type ty =

| Ty_bool
| Ty_real
| Ty_bv of int
| Ty_app of ty_var * ty list
| Ty_arrow of ty list * ty

Polymorphic types

type typed_var = var * ty

type arith_op =

| Leq
| Lt
| Geq
| Gt
| Add
| Minus
| Mult
| Div

type bitvec_op =

| BVUlt
| BVSlt
| BVNot
| BVAnd
| BVXor
| BVShl
| BVLsht
| BVAshr
| BVAdd
| BVMul
| BVURem
| BVUDiv
| Concat
| Sign_extend of int
| Extract of int * int

type term =

| True
| False
| Const of string
| Arith of arith_op * term list
| Bitvec of bitvec_op * term list
| App of string * term list
| HO_app of term * term
| Match of term * match_branch list
| If of term * term * term
| Let of (var * term) list * term
| Is_a of string * term
| Fun of typed_var * term
| Eq of term * term
| Imply of term * term
| And of term list
| Or of term list
| Not of term
| Distinct of term list
| Cast of term * ty
| Forall of (var * ty) list * term
| Exists of (var * ty) list * term
| Attr of term * (string * string) list

AST: S-expressions with locations

and match_branch =

| Match_default of term
| Match_case of string * var list * term

type cstor = {

cstor_ty_vars : ty_var list;
cstor_name : string;
cstor_args : (string * ty) list;

}

type 'arg fun_decl = {

fun_ty_vars : ty_var list;
fun_name : string;
fun_args : 'arg list;
fun_ret : ty;

}

type fun_def = {

fr_decl : typed_var fun_decl;
fr_body : term;

}

type funs_rec_def = {

fsr_decls : typed_var fun_decl list;
fsr_bodies : term list;

}

type prop_literal = string * bool

type statement = {

stmt : stmt;
loc : Smtlib_utils__.Loc.t option;

}

and stmt =

| Stmt_set_logic of string
| Stmt_set_info of string * string
| Stmt_set_option of string list
| Stmt_decl_sort of string * int
| Stmt_decl of ty fun_decl
| Stmt_fun_def of fun_def
| Stmt_fun_rec of fun_def
| Stmt_funs_rec of funs_rec_def
| Stmt_data of ((string * int) * cstor list) list
| Stmt_assert of term
| Stmt_get_assertions
| Stmt_get_assignment
| Stmt_get_info of string
| Stmt_get_model
| Stmt_get_option of string
| Stmt_get_proof
| Stmt_get_unsat_assumptions
| Stmt_get_unsat_core
| Stmt_get_value of term list
| Stmt_check_sat
| Stmt_check_sat_assuming of prop_literal list
| Stmt_pop of int
| Stmt_push of int
| Stmt_reset
| Stmt_reset_assertions
| Stmt_exit

Errors

exception Parse_error of Smtlib_utils__.Loc.t option * string

val parse_error : ?loc:Smtlib_utils__.Loc.t -> string -> 'a

val parse_errorf : 
  ?loc:Smtlib_utils__.Loc.t ->
  ('a, unit, string, 'b) format4 ->
  'a

Constructors

val ty_bool : ty

val ty_bv : int -> ty

val ty_app : ty_var -> ty list -> ty

val ty_const : ty_var -> ty

val ty_real : ty

val ty_arrow_l : ty list -> ty -> ty

val ty_arrow : ty -> ty -> ty

val true_ : term

val false_ : term

val const : string -> term

val app : string -> term list -> term

val ho_app : term -> term -> term

val ho_app_l : term -> term list -> term

val match_ : term -> match_branch list -> term

val if_ : term -> term -> term -> term

val fun_ : typed_var -> term -> term

val fun_l : typed_var list -> term -> term

val let_ : (var * term) list -> term -> term

val eq : term -> term -> term

val imply : term -> term -> term

val is_a : string -> term -> term

val and_ : term list -> term

val or_ : term list -> term

val distinct : term list -> term

val cast : term -> ty:ty -> term

val forall : (var * ty) list -> term -> term

val exists : (var * ty) list -> term -> term

val attr : term -> (string * string) list -> term

val not_ : term -> term

val arith : arith_op -> term list -> term

val bitvec : bitvec_op -> term list -> term

val _mk : ?loc:Smtlib_utils__.Loc.t -> stmt -> statement

val mk_cstor : vars:ty_var list -> string -> (string * ty) list -> cstor

val mk_fun_decl : ty_vars:ty_var list -> string -> 'a list -> ty -> 'a fun_decl

val mk_fun_rec : 
  ty_vars:ty_var list ->
  string ->
  typed_var list ->
  ty ->
  term ->
  fun_def

val decl_sort : ?loc:Smtlib_utils__.Loc.t -> string -> arity:int -> statement

val decl_fun : 
  ?loc:Smtlib_utils__.Loc.t ->
  tyvars:ty_var list ->
  string ->
  ty list ->
  ty ->
  statement

val fun_def : ?loc:Smtlib_utils__.Loc.t -> fun_def -> statement

val fun_rec : ?loc:Smtlib_utils__.Loc.t -> fun_def -> statement

val funs_rec : 
  ?loc:Smtlib_utils__.Loc.t ->
  typed_var fun_decl list ->
  term list ->
  statement

val data : 
  ?loc:Smtlib_utils__.Loc.t ->
  ((string * int) * cstor list) list ->
  statement

val data_zip : 
  ?loc:Smtlib_utils__.Loc.t ->
  (string * int) list ->
  cstor list list ->
  statement

val assert_ : ?loc:Smtlib_utils__.Loc.t -> term -> statement

val check_sat : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val check_sat_assuming : 
  ?loc:Smtlib_utils__.Loc.t ->
  prop_literal list ->
  statement

val exit : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val set_logic : ?loc:Smtlib_utils__.Loc.t -> string -> statement

val set_info : ?loc:Smtlib_utils__.Loc.t -> string -> string -> statement

val get_info : ?loc:Smtlib_utils__.Loc.t -> string -> statement

val set_option : ?loc:Smtlib_utils__.Loc.t -> string list -> statement

val get_option : ?loc:Smtlib_utils__.Loc.t -> string -> statement

val push : ?loc:Smtlib_utils__.Loc.t -> int -> statement

val pop : ?loc:Smtlib_utils__.Loc.t -> int -> statement

val get_proof : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val get_model : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val get_assertions : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val get_assignment : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val get_value : ?loc:Smtlib_utils__.Loc.t -> term list -> statement

val get_unsat_core : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val get_unsat_assumptions : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val reset : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val reset_assertions : ?loc:Smtlib_utils__.Loc.t -> unit -> statement

val loc : statement -> Smtlib_utils__.Loc.t option

val view : statement -> stmt

val fpf : Format.formatter -> ('a, Format.formatter, unit) format -> 'a

val pp_list : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a list ->
  unit

val pp_str : Format.formatter -> string -> unit

val pp_tyvar : Format.formatter -> string -> unit

val pp_ty : Format.formatter -> ty -> unit

val str_of_arith : arith_op -> string

val str_of_bitvec : bitvec_op -> string

val pp_arith : Format.formatter -> arith_op -> unit

val pp_bitvec : Format.formatter -> bitvec_op -> unit

val _lvl_top : int

val pp_typed_var : Format.formatter -> typed_var -> unit

val pp_term : Format.formatter -> term -> unit

val pp_par : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  (string list * 'a) ->
  unit

val pp_fun_decl : 
  (Format.formatter -> 'a -> unit) ->
  Format.formatter ->
  'a fun_decl ->
  unit

val pp_fr : Format.formatter -> fun_def -> unit

val pp_prop_lit : Format.formatter -> (string * bool) -> unit

val pp_stmt : Format.formatter -> statement -> unit

package smtlib-utils

Trivial AST for parsing

Errors

Constructors