forked from cubicle-model-checker/cubicle
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathptree.mli
127 lines (94 loc) · 3.75 KB
/
ptree.mli
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
(**************************************************************************)
(* *)
(* Cubicle *)
(* *)
(* Copyright (C) 2011-2015 *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* *)
(* This file is distributed under the terms of the Apache Software *)
(* License version 2.0 *)
(* *)
(**************************************************************************)
open Types
open Util
type term =
| TVar of Variable.t
| TTerm of Term.t
type atom =
| AVar of Variable.t
| AAtom of Atom.t
| AEq of term * term
| ANeq of term * term
| ALe of term * term
| ALt of term * term
type formula =
| PAtom of atom
| PNot of formula
| PAnd of formula list
| POr of formula list
| PImp of formula * formula
| PEquiv of formula * formula
| PIte of formula * formula * formula
| PForall of Variable.t list * formula
| PExists of Variable.t list * formula
| PForall_other of Variable.t list * formula
| PExists_other of Variable.t list * formula
type term_or_formula = PF of formula | PT of term
type cformula = formula
(* type atom = [ PAtom of Atom.t ] *)
(* type clause = [atom | POr of atom list] *)
(* type conj = [atom | PAnd of atom list] *)
(* type cnf = [clause | PAnd of clause list] *)
(* type dnf = [conj | POr of conj list] *)
(* type uguard = [PForall_other of Variable.t list * dnf] *)
(* type guard = [dnf | uguard] *)
(* type prenex_forall_dnf = [dnf | PForall of Variable.t list * dnf] *)
(* type cube = [conj | PExists of Variable.t list * conj] *)
type pswts = (cformula * term) list
type pglob_update = PUTerm of term | PUCase of pswts
type pupdate = {
pup_loc : loc;
pup_arr : Hstring.t;
pup_arg : Variable.t list;
pup_swts : pswts;
}
type ptransition = {
ptr_lets : (Hstring.t * term) list;
ptr_name : Hstring.t;
ptr_args : Variable.t list;
ptr_reqs : cformula;
ptr_assigns : (Hstring.t * pglob_update) list;
ptr_upds : pupdate list;
ptr_nondets : Hstring.t list;
ptr_loc : loc;
}
type psystem = {
pglobals : (loc * Hstring.t * Smt.Type.t) list;
pconsts : (loc * Hstring.t * Smt.Type.t) list;
parrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list;
ptype_defs : (loc * Ast.type_constructors) list;
pinit : loc * Variable.t list * cformula;
pinvs : (loc * Variable.t list * cformula) list;
punsafe : (loc * Variable.t list * cformula) list;
ptrans : ptransition list;
}
type pdecl =
| PInit of (loc * Variable.t list * cformula)
| PInv of (loc * Variable.t list * cformula)
| PUnsafe of (loc * Variable.t list * cformula)
| PTrans of ptransition
| PFun
val add_fun_def : Hstring.t -> Variable.t list -> formula -> unit
val app_fun : Hstring.t -> term_or_formula list -> formula
val encode_psystem : psystem -> Ast.system
val psystem_of_decls:
pglobals : (loc * Hstring.t * Smt.Type.t) list ->
pconsts : (loc * Hstring.t * Smt.Type.t) list ->
parrays : (loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list ->
ptype_defs : (loc * Ast.type_constructors) list ->
pdecl list -> psystem
(** {2 Pretty printing ASTs} *)
val print_system : Format.formatter -> Ast.system -> unit