smt2_model_defs.mli 1.85 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
open Wstdlib
13 14 15

type variable = string

16 17 18 19 20 21 22 23 24 25
(* Simple counterexample that already represent a complete value *)
type simple_value =
  | Integer of string
  | Decimal of (string * string)
  | Fraction of (string * string)
  | Float of Model_parser.float_type
  | Other of string
  | Bitvector of string
  | Boolean of bool

26
type array =
27 28
  (* Array_var is used by let-bindings only *)
  | Array_var of variable
29 30 31 32
  | Const of term
  | Store of array * term * term

and term =
33
  | Sval of simple_value
34
  | Apply of (string * term list)
35 36 37 38 39
  | Array of array
  | Cvc4_Variable of variable
  | Function_Local_Variable of variable
  | Variable of variable
  | Ite of term * term * term * term
40
  | Record of string * ((string * term) list)
41
  | To_array of term
42 43
  (* TODO remove tree *)
  | Trees of (string * term) list
44 45

type definition =
46
  | Function of (variable * string option) list * term
47 48 49 50
  | Term of term (* corresponding value of a term *)
  | Noelement

val add_element: (string * definition) option ->
51
  definition Mstr.t -> definition Mstr.t
52

53
val make_local: (variable * string option) list -> term -> term
54 55 56

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