smt2_model_defs.mli 1.22 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31


open Stdlib

type variable = string

type array =
  | Const of term
  | Store of array * term * term

and term =
  | Integer of string
  | Decimal of (string * string)
  | Other of string
  | Array of array
  | Bitvector of string
  | Boolean of bool
  | Cvc4_Variable of variable
  | Function_Local_Variable of variable
  | Variable of variable
  | Ite of term * term * term * term
  | Record of int * (term list)
  | Discr of int * (term list)
  | To_array of term

type definition =
  | Function of variable list * term
  | Term of term (* corresponding value of a term *)
  | Noelement

(* Type returned by parsing of model.
Sylvain Dailler's avatar
Sylvain Dailler committed
32
   An hashtable that makes a correspondence between names (string) and
33 34
   associated definition (complex stuff) *)
(* The boolean is true when the term has no external variable *)
Sylvain Dailler's avatar
Sylvain Dailler committed
35
type correspondence_table = (bool * definition) Mstr.t
36 37

val add_element: (string * definition) option ->
Sylvain Dailler's avatar
Sylvain Dailler committed
38
  correspondence_table -> bool -> correspondence_table
39 40 41 42 43 44 45 46 47 48 49


val make_local: variable list -> term -> term

val print_term: Format.formatter -> term -> unit
val print_def: Format.formatter -> definition -> unit

val build_record_discr: term list -> term

(* Used for let bindings of z3 *)
val substitute: (string * term) list -> term -> term