package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file smtbackend_smtlib_sig.ml

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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

type counter_example = unit

type sat =
  | Sat of counter_example
  | Unsat
  | Unknown


module type COMMON_S = sig

  (* An SMTLIB printer, with an higher-order abstract syntax
     interface, that does not require any buffering (for fast
     output). *)
  type logic
  type command

  
 (**************** Logics ****************)
  val qf_uf: logic            (* uninterpreted functions. *)
  val qf_lia: logic           (* linear arithmetic. *)
  val qf_nia: logic           (* general arithmetic. *)
  val qf_lra: logic           (* linear real arithmetic. *)
  val qf_auflia: logic        (* lia + uf + array. *)
  val auflia: logic
  val auflira: logic
  val aufnira: logic
  val lra: logic
  val qf_idl: logic
  val qf_rdl: logic
  val qf_ufidl: logic
  val qf_bv: logic            (* bitvectors *)
  val qf_ax: logic            (* arrays *)
  val qf_abv: logic           (* array + bitvectors *)
  val qf_aubv: logic          (* array + bitvectors + uninterpreted functions *)
  val horn: logic             (* Extension *)
      
  (**************** Commands ****************)

  type satisfiable = Sat | Unsat | Unknown;;
  val check_sat: unit -> satisfiable
  val set_logic: logic -> unit

  val set_option: string -> unit
  
end


module type TYPED_S = sig
  include COMMON_S
  type 'a sort
  type 'a value

  (**************** Commands ****************)

  val assert_: bool value -> unit (* command t   *)

  (**************** Bool and generic functions ****************)
  val bool: bool sort

  val let_: ?name:string -> 'a value -> ('a value -> 'b value) -> 'b value
  val forall: ?name:string -> 'a sort -> ('a value -> bool value) -> bool value
  val exists: ?name:string -> 'a sort -> ('a value -> bool value) -> bool value      

  val (=): 'a value -> 'a value -> bool value
  val (||): bool value -> bool value -> bool value            
  
  (* Int theory *)
  val int: int sort      
  val numeral: int -> int value
  val (<): int value -> int value -> bool value

  (* Array theory, with extensibility: arrays are equal iff all elements are equal. *)
  type ('a,'b) array            (* Array from 'a sort to 'b sort. *)
      
  val array: 'a sort -> 'b sort -> ('a,'b) array sort
  val select: ('a,'b) array value -> 'a value -> 'b value
  val store: ('a,'b) array value -> 'a value -> 'b value -> ('a,'b) array value    

  (* Fixed_Size_Bitvectors theory *)
  type bitvector                (* Bitvector of a given size. TODO: compute sizes statically with GADTs? Works with extract?*)

  val bitvec: int -> bitvector sort

  (* Smallest bits in the integer *)
  val bvlit: size:int -> Z.t -> bitvector value
  
  val concat: bitvector value -> bitvector value -> bitvector value
  val bvnot: bitvector value -> bitvector value
  val bvneg: bitvector value -> bitvector value

  val bvand: bitvector value -> bitvector value -> bitvector value
  val bvor: bitvector value -> bitvector value -> bitvector value
  val bvadd: bitvector value -> bitvector value -> bitvector value
  val bvmul: bitvector value -> bitvector value -> bitvector value
  val bvudiv: bitvector value -> bitvector value -> bitvector value
  val bvurem: bitvector value -> bitvector value -> bitvector value
  val bvshl: bitvector value -> bitvector value -> bitvector value
  val bvlshr: bitvector value -> bitvector value -> bitvector value
  val bvult: bitvector value -> bitvector value -> bool value

  (* Extensionso Fixed_Size_Bitvectors, but described in 
     http://smtlib.cs.uiowa.edu/logics-all.shtml.  *)
  val bvxor: bitvector value -> bitvector value -> bitvector value      
  val bvsdiv: bitvector value -> bitvector value -> bitvector value
  val bvsrem: bitvector value -> bitvector value -> bitvector value
  val bvule: bitvector value -> bitvector value -> bool value
  val bvslt: bitvector value -> bitvector value -> bool value
  val bvsle: bitvector value -> bitvector value -> bool value            

end


module type UNTYPED_S = sig

  include COMMON_S
  
  type sort
  type value


  (**************** Commands ****************)
  
  (* Execute the command.  *)

  val assert_: value -> unit
  val get_assignment: unit -> unit

  (* TODO: Difficult to make declare fun generic in terms of arity. *)
  (* MAYBE: A monadic interface would make explicit the fact that
     declare_var has a side-effect. *)
  val declare_var: ?name:string -> sort -> value
  val define_var: ?name:string -> sort -> value -> value

  (**************** Bool and generic functions ****************)
  val bool: sort

  val let_: ?name:string -> value -> (value -> value) -> value
  val forall: ?name:string -> sort -> (value -> value) -> value
  val exists: ?name:string -> sort -> (value -> value) -> value      

  val (=): value -> value -> value
  val (||): value -> value -> value
  val (&&): value -> value -> value
  val (=>): value -> value -> value

  val and_list: value list -> value
  val or_list: value list -> value      
  
  val not: value -> value
  val true_: value
  val false_: value            
  
  (* Int theory *)
  val int: sort      
  val numeral: int -> value
  val numeralz: Z.t -> value      
  val (<): value -> value -> value
  val (<=): value -> value -> value      
  val (-): value -> value -> value
  val neg: value -> value
  val (+): value -> value -> value
  val ( * ): value -> value -> value
  val div: value -> value -> value
  val modu: value -> value -> value                  


  (* Array theory, with extensibility: arrays are equal iff all elements are equal. *)

  val array: sort -> sort -> sort
  val select: value -> value -> value
  val store: value -> value -> value -> value    

  (* Fixed_Size_Bitvectors theory *)
  val bitvec: int -> sort

  (* Smallest bits in the integer *)
  val bvlit: size:int -> Z.t -> value
  
  val concat: value -> value -> value
  val bvnot: value -> value
  val bvneg: value -> value

  val bvand: value -> value -> value
  val bvor: value -> value -> value
  val bvadd: value -> value -> value
  val bvmul: value -> value -> value
  val bvudiv: value -> value -> value
  val bvurem: value -> value -> value
  val bvshl: value -> value -> value
  val bvlshr: value -> value -> value
  val bvult: value -> value -> value

  val extract: first:int -> last:int -> value -> value
  
  (* Extensions to Fixed_Size_Bitvectors, but described in 
     http://smtlib.cs.uiowa.edu/logics-all.shtml.  *)
  val bvxor: value -> value -> value      
  val bvsdiv: value -> value -> value
  val bvsrem: value -> value -> value
  val bvsmod: value -> value -> value      
  val bvule: value -> value -> value
  val bvslt: value -> value -> value
  val bvsle: value -> value -> value
  val bvashr: value -> value -> value

  (* The int indicates how much bit to extend. *)
  val sign_extend: int -> value -> value
  val zero_extend: int -> value -> value      
  
end

(**************** Mu-z extensions, described in http://rise4fun.com/Z3/tutorialcontent/fixedpoints ****************)
module type UNTYPED_MUZ = sig
  include UNTYPED_S

  type relation = value list -> value

  val declare_rel: ?name:string -> sort list -> relation * string
  
  (* A horn rule, with premices and a conclusion. *)
  val rule: value list -> value -> unit
  val fact: value -> unit

  (* val query: relation t -> value list -> unit *)
  val query: value -> satisfiable
  (* Note: query is used differently on different versions of z3. *)
  val query2: string -> satisfiable
  val declare_muz_var: ?name:string -> sort -> value

end

module type PARAM_S = sig
  val print : string -> unit
  val inc: Stdlib.in_channel
  val flush: unit -> unit
end