1(** 2 The Z3 ML/OCaml Interface. 3 4 Copyright (C) 2012 Microsoft Corporation 5 @author CM Wintersteiger (cwinter) 2012-12-17 6*) 7 8(** General Z3 exceptions 9 10 Many functions in this API may throw an exception; if they do, it is this one.*) 11exception Error of string 12 13(** Context objects. 14 15 Most interactions with Z3 are interpreted in some context; many users will only 16 require one such object, but power users may require more than one. To start using 17 Z3, do 18 19 <code> 20 let ctx = (mk_context []) in 21 (...) 22 </code> 23 24 where a list of pairs of strings may be passed to set options on 25 the context, e.g., like so: 26 27 <code> 28 let cfg = [("model", "true"); ("...", "...")] in 29 let ctx = (mk_context cfg) in 30 (...) 31 </code> 32*) 33type context 34 35(** Create a context object 36 The following parameters can be set: 37 38 - proof (Boolean) Enable proof generation 39 - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting 40 - trace (Boolean) Tracing support for VCC 41 - trace_file_name (String) Trace out file for VCC traces 42 - timeout (unsigned) default timeout (in milliseconds) used for solvers 43 - well_sorted_check type checker 44 - auto_config use heuristics to automatically select solver and configure it 45 - model model generation for solvers, this parameter can be overwritten when creating a solver 46 - model_validate validate models produced by solvers 47 - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver 48*) 49val mk_context : (string * string) list -> context 50 51(** Interaction logging for Z3 52 Note that this is a global, static log and if multiple Context 53 objects are created, it logs the interaction with all of them. *) 54module Log : 55sig 56 (** Open an interaction log file. 57 @return True if opening the log file succeeds, false otherwise. *) 58 (* CMW: "open" is a reserved keyword. *) 59 val open_ : string -> bool 60 61 (** Closes the interaction log. *) 62 val close : unit -> unit 63 64 (** Appends a user-provided string to the interaction log. *) 65 val append : string -> unit 66end 67 68(** Version information *) 69module Version : 70sig 71 (** The major version. *) 72 val major : int 73 74 (** The minor version. *) 75 val minor : int 76 77 (** The build version. *) 78 val build : int 79 80 (** The revision. *) 81 val revision : int 82 83 (** A full version string. *) 84 val full_version : string 85 86 (** A string representation of the version information. *) 87 val to_string : string 88end 89 90(** Symbols are used to name several term and type constructors *) 91module Symbol : 92sig 93 type symbol 94 95 (** The kind of the symbol (int or string) *) 96 val kind : symbol -> Z3enums.symbol_kind 97 98 (** Indicates whether the symbol is of Int kind *) 99 val is_int_symbol : symbol -> bool 100 101 (** Indicates whether the symbol is of string kind. *) 102 val is_string_symbol : symbol -> bool 103 104 (** The int value of the symbol. *) 105 val get_int : symbol -> int 106 107 (** The string value of the symbol. *) 108 val get_string : symbol -> string 109 110 (** A string representation of the symbol. *) 111 val to_string : symbol -> string 112 113 (** Creates a new symbol using an integer. 114 Not all integers can be passed to this function. 115 The legal range of unsigned integers is 0 to 2^30-1. *) 116 val mk_int : context -> int -> symbol 117 118 (** Creates a new symbol using a string. *) 119 val mk_string : context -> string -> symbol 120 121 (** Create a list of symbols. *) 122 val mk_ints : context -> int list -> symbol list 123 124 (** Create a list of symbols. *) 125 val mk_strings : context -> string list -> symbol list 126end 127 128(** The abstract syntax tree (AST) module *) 129module rec AST : 130sig 131 type ast 132 133 (** Vectors of ASTs *) 134 module ASTVector : 135 sig 136 type ast_vector 137 138 (** Create an empty AST vector *) 139 val mk_ast_vector : context -> ast_vector 140 141 (** The size of the vector *) 142 val get_size : ast_vector -> int 143 144 (** Retrieves the i-th object in the vector. 145 @return An AST *) 146 val get : ast_vector -> int -> ast 147 148 (** Sets the i-th object in the vector. *) 149 val set : ast_vector -> int -> ast -> unit 150 151 (** Resize the vector to a new size. *) 152 val resize : ast_vector -> int -> unit 153 154 (** Add an ast to the back of the vector. The size 155 is increased by 1. *) 156 val push : ast_vector -> ast -> unit 157 158 (** Translates all ASTs in the vector to another context. 159 @return A new ASTVector *) 160 val translate : ast_vector -> context -> ast_vector 161 162 (** Translates the ASTVector into an (Ast.ast list) *) 163 val to_list : ast_vector -> ast list 164 165 (** Translates the ASTVector into an (Expr.expr list) *) 166 val to_expr_list : ast_vector -> Expr.expr list 167 168 (** Retrieves a string representation of the vector. *) 169 val to_string : ast_vector -> string 170 end 171 172 (** Map from AST to AST *) 173 module ASTMap : 174 sig 175 type ast_map 176 177 (** Create an empty mapping from AST to AST *) 178 val mk_ast_map : context -> ast_map 179 180 (** Checks whether the map contains a key. 181 @return True if the key in the map, false otherwise. *) 182 val contains : ast_map -> ast -> bool 183 184 (** Finds the value associated with the key. 185 This function signs an error when the key is not a key in the map. *) 186 val find : ast_map -> ast -> ast 187 188 (** Stores or replaces a new key/value pair in the map. *) 189 val insert : ast_map -> ast -> ast -> unit 190 191 (** Erases the key from the map.*) 192 val erase : ast_map -> ast -> unit 193 194 (** Removes all keys from the map. *) 195 val reset : ast_map -> unit 196 197 (** The size of the map *) 198 val get_size : ast_map -> int 199 200 (** The keys stored in the map. *) 201 val get_keys : ast_map -> ast list 202 203 (** Retrieves a string representation of the map.*) 204 val to_string : ast_map -> string 205 end 206 207 (** The AST's hash code. 208 @return A hash code *) 209 val hash : ast -> int 210 211 (** A unique identifier for the AST (unique among all ASTs). *) 212 val get_id : ast -> int 213 214 (** The kind of the AST. *) 215 val get_ast_kind : ast -> Z3enums.ast_kind 216 217 (** Indicates whether the AST is an Expr *) 218 val is_expr : ast -> bool 219 220 (** Indicates whether the AST is a bound variable*) 221 val is_var : ast -> bool 222 223 (** Indicates whether the AST is a Quantifier *) 224 val is_quantifier : ast -> bool 225 226 (** Indicates whether the AST is a Sort *) 227 val is_sort : ast -> bool 228 229 (** Indicates whether the AST is a func_decl *) 230 val is_func_decl : ast -> bool 231 232 (** A string representation of the AST. *) 233 val to_string : ast -> string 234 235 (** A string representation of the AST in s-expression notation. *) 236 val to_sexpr : ast -> string 237 238 (** Comparison operator. 239 @return True if the two ast's are from the same context 240 and represent the same sort; false otherwise. *) 241 val equal : ast -> ast -> bool 242 243 (** Object Comparison. 244 @return Negative if the first ast should be sorted before the second, positive if after else zero. *) 245 val compare : ast -> ast -> int 246 247 (** Translates (copies) the AST to another context. 248 @return A copy of the AST which is associated with the other context. *) 249 val translate : ast -> context -> ast 250end 251 252(** The Sort module implements type information for ASTs *) 253and Sort : 254sig 255 type sort 256 257 (** Comparison operator. 258 @return True if the two sorts are from the same context 259 and represent the same sort; false otherwise. *) 260 val equal : sort -> sort -> bool 261 262 (** Returns a unique identifier for the sort. *) 263 val get_id : sort -> int 264 265 (** The kind of the sort. *) 266 val get_sort_kind : sort -> Z3enums.sort_kind 267 268 (** The name of the sort *) 269 val get_name : sort -> Symbol.symbol 270 271 (** A string representation of the sort. *) 272 val to_string : sort -> string 273 274 (** Create a new uninterpreted sort. *) 275 val mk_uninterpreted : context -> Symbol.symbol -> sort 276 277 (** Create a new uninterpreted sort. *) 278 val mk_uninterpreted_s : context -> string -> sort 279end 280 281(** Function declarations *) 282and FuncDecl : 283sig 284 type func_decl 285 286 (** Parameters of Func_Decls *) 287 module Parameter : 288 sig 289 (** Parameters of func_decls *) 290 type parameter = 291 P_Int of int 292 | P_Dbl of float 293 | P_Sym of Symbol.symbol 294 | P_Srt of Sort.sort 295 | P_Ast of AST.ast 296 | P_Fdl of func_decl 297 | P_Rat of string 298 299 (** The kind of the parameter. *) 300 val get_kind : parameter -> Z3enums.parameter_kind 301 302 (** The int value of the parameter.*) 303 val get_int : parameter -> int 304 305 (** The float value of the parameter.*) 306 val get_float : parameter -> float 307 308 (** The Symbol.Symbol value of the parameter.*) 309 val get_symbol : parameter -> Symbol.symbol 310 311 (** The Sort value of the parameter.*) 312 val get_sort : parameter -> Sort.sort 313 314 (** The AST value of the parameter.*) 315 val get_ast : parameter -> AST.ast 316 317 (** The FunctionDeclaration value of the parameter.*) 318 val get_func_decl : parameter -> func_decl 319 320 (** The rational string value of the parameter.*) 321 val get_rational : parameter -> string 322 end 323 324 (** Creates a new function declaration. *) 325 val mk_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl 326 327 (** Creates a new function declaration. *) 328 val mk_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl 329 330 (** Creates a function declaration that can be used in a recursive function definition. 331 {!add_rec_def} *) 332 val mk_rec_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl 333 334 (** Creates a function declaration that can be used in a recursive function definition. 335 {!add_rec_def} *) 336 val mk_rec_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl 337 338 (** Registers a recursive function definition *) 339 val add_rec_def : context -> func_decl -> Expr.expr list -> Expr.expr -> unit 340 341 (** Creates a fresh function declaration with a name prefixed with a prefix string. *) 342 val mk_fresh_func_decl : context -> string -> Sort.sort list -> Sort.sort -> func_decl 343 344 345 (** Creates a new constant function declaration. *) 346 val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl 347 348 (** Creates a new constant function declaration. *) 349 val mk_const_decl_s : context -> string -> Sort.sort -> func_decl 350 351 (** Creates a fresh constant function declaration with a name prefixed with a prefix string. 352 {!mk_func_decl} 353 {!mk_func_decl} *) 354 val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl 355 356 (** Comparison operator. 357 @return True if a and b are from the same context and represent the same func_decl; false otherwise. *) 358 val equal : func_decl -> func_decl -> bool 359 360 (** A string representations of the function declaration. *) 361 val to_string : func_decl -> string 362 363 (** Returns a unique identifier for the function declaration. *) 364 val get_id : func_decl -> int 365 366 (** The arity of the function declaration *) 367 val get_arity : func_decl -> int 368 369 (** The size of the domain of the function declaration 370 {!get_arity} *) 371 val get_domain_size : func_decl -> int 372 373 (** The domain of the function declaration *) 374 val get_domain : func_decl -> Sort.sort list 375 376 (** The range of the function declaration *) 377 val get_range : func_decl -> Sort.sort 378 379 (** The kind of the function declaration. *) 380 val get_decl_kind : func_decl -> Z3enums.decl_kind 381 382 (** The name of the function declaration*) 383 val get_name : func_decl -> Symbol.symbol 384 385 (** The number of parameters of the function declaration *) 386 val get_num_parameters : func_decl -> int 387 388 (** The parameters of the function declaration *) 389 val get_parameters : func_decl -> Parameter.parameter list 390 391 (** Create expression that applies function to arguments. *) 392 val apply : func_decl -> Expr.expr list -> Expr.expr 393end 394 395(** Parameter sets (of Solvers, Tactics, ...) 396 397 A Params objects represents a configuration in the form of Symbol.symbol/value pairs. *) 398and Params : 399sig 400 type params 401 402 (** ParamDescrs describe sets of parameters (of Solvers, Tactics, ...) *) 403 module ParamDescrs : 404 sig 405 type param_descrs 406 407 (** Validate a set of parameters. *) 408 val validate : param_descrs -> params -> unit 409 410 (** Retrieve kind of parameter. *) 411 val get_kind : param_descrs -> Symbol.symbol -> Z3enums.param_kind 412 413 (** Retrieve all names of parameters. *) 414 val get_names : param_descrs -> Symbol.symbol list 415 416 (** The size of the ParamDescrs. *) 417 val get_size : param_descrs -> int 418 419 (** Retrieves a string representation of the ParamDescrs. *) 420 val to_string : param_descrs -> string 421 end 422 423 (** Adds a parameter setting. *) 424 val add_bool : params -> Symbol.symbol -> bool -> unit 425 426 (** Adds a parameter setting. *) 427 val add_int : params -> Symbol.symbol -> int -> unit 428 429 (** Adds a parameter setting. *) 430 val add_float : params -> Symbol.symbol -> float -> unit 431 432 (** Adds a parameter setting. *) 433 val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit 434 435 (** Creates a new parameter set *) 436 val mk_params : context -> params 437 438 (** A string representation of the parameter set. *) 439 val to_string : params -> string 440 441 (** Update a mutable configuration parameter. 442 443 The list of all configuration parameters can be obtained using the Z3 executable: 444 [z3.exe -p] 445 Only a few configuration parameters are mutable once the context is created. 446 An exception is thrown when trying to modify an immutable parameter. *) 447 val update_param_value : context -> string -> string -> unit 448 449 (** Selects the format used for pretty-printing expressions. 450 451 The default mode for pretty printing expressions is to produce 452 SMT-LIB style output where common subexpressions are printed 453 at each occurrence. The mode is called PRINT_SMTLIB_FULL. 454 To print shared common subexpressions only once, 455 use the PRINT_LOW_LEVEL mode. 456 To print in way that conforms to SMT-LIB standards and uses let 457 expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT. 458 {!AST.to_string} 459 {!Quantifier.Pattern.to_string} 460 {!FuncDecl.to_string} 461 {!Sort.to_string} *) 462 val set_print_mode : context -> Z3enums.ast_print_mode -> unit 463end 464 465(** General Expressions (terms) *) 466and Expr : 467sig 468 type expr 469 470 val ast_of_expr : Expr.expr -> AST.ast 471 val expr_of_ast : AST.ast -> Expr.expr 472 473 (** Returns a simplified version of the expression. 474 {!get_simplify_help} *) 475 val simplify : Expr.expr -> Params.params option -> expr 476 477 (** A string describing all available parameters to [Expr.Simplify]. *) 478 val get_simplify_help : context -> string 479 480 (** Retrieves parameter descriptions for simplifier. *) 481 val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs 482 483 (** The function declaration of the function that is applied in this expression. *) 484 val get_func_decl : Expr.expr -> FuncDecl.func_decl 485 486 (** The number of arguments of the expression. *) 487 val get_num_args : Expr.expr -> int 488 489 (** The arguments of the expression. *) 490 val get_args : Expr.expr -> Expr.expr list 491 492 (** Update the arguments of the expression using an array of expressions. 493 The number of new arguments should coincide with the current number of arguments. *) 494 val update : Expr.expr -> Expr.expr list -> expr 495 496 (** Substitute every occurrence of [from[i]] in the expression with [to[i]], for [i] smaller than [num_exprs]. 497 498 The result is the new expression. The arrays [from] and [to] must have size [num_exprs]. 499 For every [i] smaller than [num_exprs], we must have that 500 sort of [from[i]] must be equal to sort of [to[i]]. *) 501 val substitute : Expr.expr -> Expr.expr list -> Expr.expr list -> expr 502 503 (** Substitute every occurrence of [from] in the expression with [to]. 504 {!substitute} *) 505 val substitute_one : Expr.expr -> Expr.expr -> Expr.expr -> expr 506 507 (** Substitute the free variables in the expression with the expressions in the expr array 508 509 For every [i] smaller than [num_exprs], the variable with de-Bruijn index [i] is replaced with term [to[i]]. *) 510 val substitute_vars : Expr.expr -> Expr.expr list -> expr 511 512 (** Translates (copies) the term to another context. 513 @return A copy of the term which is associated with the other context *) 514 val translate : Expr.expr -> context -> expr 515 516 (** Returns a string representation of the expression. *) 517 val to_string : Expr.expr -> string 518 519 (** Indicates whether the term is a numeral *) 520 val is_numeral : Expr.expr -> bool 521 522 (** Indicates whether the term is well-sorted. 523 @return True if the term is well-sorted, false otherwise. *) 524 val is_well_sorted : Expr.expr -> bool 525 526 (** The Sort of the term. *) 527 val get_sort : Expr.expr -> Sort.sort 528 529 (** Indicates whether the term represents a constant. *) 530 val is_const : Expr.expr -> bool 531 532 (** Creates a new constant. *) 533 val mk_const : context -> Symbol.symbol -> Sort.sort -> expr 534 535 (** Creates a new constant. *) 536 val mk_const_s : context -> string -> Sort.sort -> expr 537 538 (** Creates a constant from the func_decl. *) 539 val mk_const_f : context -> FuncDecl.func_decl -> expr 540 541 (** Creates a fresh constant with a name prefixed with a string. *) 542 val mk_fresh_const : context -> string -> Sort.sort -> expr 543 544 (** Create a new function application. *) 545 val mk_app : context -> FuncDecl.func_decl -> Expr.expr list -> expr 546 547 (** Create a numeral of a given sort. 548 @return A Term with the given value and sort *) 549 val mk_numeral_string : context -> string -> Sort.sort -> expr 550 551 (** Create a numeral of a given sort. This function can be used to create numerals that fit in a machine integer. 552 It is slightly faster than [MakeNumeral] since it is not necessary to parse a string. 553 @return A Term with the given value and sort *) 554 val mk_numeral_int : context -> int -> Sort.sort -> expr 555 556 (** Comparison operator. 557 @return True if the two expr's are equal; false otherwise. *) 558 val equal : expr -> expr -> bool 559 560 (** Object Comparison. 561 @return Negative if the first expr should be sorted before the second, positive if after, else zero. *) 562 val compare : expr -> expr -> int 563end 564 565(** Boolean expressions; Propositional logic and equality *) 566module Boolean : 567sig 568 (** Create a Boolean sort *) 569 val mk_sort : context -> Sort.sort 570 571 (** Create a Boolean constant. *) 572 val mk_const : context -> Symbol.symbol -> Expr.expr 573 574 (** Create a Boolean constant. *) 575 val mk_const_s : context -> string -> Expr.expr 576 577 (** The true Term. *) 578 val mk_true : context -> Expr.expr 579 580 (** The false Term. *) 581 val mk_false : context -> Expr.expr 582 583 (** Creates a Boolean value. *) 584 val mk_val : context -> bool -> Expr.expr 585 586 (** Mk an expression representing [not(a)]. *) 587 val mk_not : context -> Expr.expr -> Expr.expr 588 589 (** Create an expression representing an if-then-else: [ite(t1, t2, t3)]. *) 590 val mk_ite : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 591 592 (** Create an expression representing [t1 iff t2]. *) 593 val mk_iff : context -> Expr.expr -> Expr.expr -> Expr.expr 594 595 (** Create an expression representing [t1 -> t2]. *) 596 val mk_implies : context -> Expr.expr -> Expr.expr -> Expr.expr 597 598 (** Create an expression representing [t1 xor t2]. *) 599 val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr 600 601 (** Create an expression representing the AND of args *) 602 val mk_and : context -> Expr.expr list -> Expr.expr 603 604 (** Create an expression representing the OR of args *) 605 val mk_or : context -> Expr.expr list -> Expr.expr 606 607 (** Creates the equality between two expr's. *) 608 val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr 609 610 (** Creates a [distinct] term. *) 611 val mk_distinct : context -> Expr.expr list -> Expr.expr 612 613 (** Indicates whether the expression is the true or false expression 614 or something else (L_UNDEF). *) 615 val get_bool_value : Expr.expr -> Z3enums.lbool 616 617 (** Indicates whether the term has Boolean sort. *) 618 val is_bool : Expr.expr -> bool 619 620 (** Indicates whether the term is the constant true. *) 621 val is_true : Expr.expr -> bool 622 623 (** Indicates whether the term is the constant false. *) 624 val is_false : Expr.expr -> bool 625 626 (** Indicates whether the term is an equality predicate. *) 627 val is_eq : Expr.expr -> bool 628 629 (** Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). *) 630 val is_distinct : Expr.expr -> bool 631 632 (** Indicates whether the term is a ternary if-then-else term *) 633 val is_ite : Expr.expr -> bool 634 635 (** Indicates whether the term is an n-ary conjunction *) 636 val is_and : Expr.expr -> bool 637 638 (** Indicates whether the term is an n-ary disjunction *) 639 val is_or : Expr.expr -> bool 640 641 (** Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) *) 642 val is_iff : Expr.expr -> bool 643 644 (** Indicates whether the term is an exclusive or *) 645 val is_xor : Expr.expr -> bool 646 647 (** Indicates whether the term is a negation *) 648 val is_not : Expr.expr -> bool 649 650 (** Indicates whether the term is an implication *) 651 val is_implies : Expr.expr -> bool 652end 653 654(** Quantifier expressions *) 655module Quantifier : 656sig 657 type quantifier 658 659 val expr_of_quantifier : quantifier -> Expr.expr 660 val quantifier_of_expr : Expr.expr -> quantifier 661 662 (** Quantifier patterns 663 664 Patterns comprise a list of terms. The list should be 665 non-empty. If the list comprises of more than one term, it is 666 also called a multi-pattern. *) 667 module Pattern : 668 sig 669 type pattern 670 671 (** The number of terms in the pattern. *) 672 val get_num_terms : pattern -> int 673 674 (** The terms in the pattern. *) 675 val get_terms : pattern -> Expr.expr list 676 677 (** A string representation of the pattern. *) 678 val to_string : pattern -> string 679 end 680 681 682 (** The de-Bruijn index of a bound variable. 683 684 Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain 685 the meaning of de-Bruijn indices by indicating the compilation process from 686 non-de-Bruijn formulas to de-Bruijn format. 687 <code> 688 abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) 689 abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) 690 abs1(x, x, n) = b_n 691 abs1(y, x, n) = y 692 abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) 693 abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1)) 694 </code> 695 The last line is significant: the index of a bound variable is different depending 696 on the scope in which it appears. The deeper ( x : expr ) appears, the higher is its 697 index. *) 698 val get_index : Expr.expr -> int 699 700 (** Indicates whether the quantifier is universal. *) 701 val is_universal : quantifier -> bool 702 703 (** Indicates whether the quantifier is existential. *) 704 val is_existential : quantifier -> bool 705 706 (** The weight of the quantifier. *) 707 val get_weight : quantifier -> int 708 709 (** The number of patterns. *) 710 val get_num_patterns : quantifier -> int 711 712 (** The patterns. *) 713 val get_patterns : quantifier -> Pattern.pattern list 714 715 (** The number of no-patterns. *) 716 val get_num_no_patterns : quantifier -> int 717 718 (** The no-patterns. *) 719 val get_no_patterns : quantifier -> Pattern.pattern list 720 721 (** The number of bound variables. *) 722 val get_num_bound : quantifier -> int 723 724 (** The symbols for the bound variables. *) 725 val get_bound_variable_names : quantifier -> Symbol.symbol list 726 727 (** The sorts of the bound variables. *) 728 val get_bound_variable_sorts : quantifier -> Sort.sort list 729 730 (** The body of the quantifier. *) 731 val get_body : quantifier -> Expr.expr 732 733 (** Creates a new bound variable. *) 734 val mk_bound : context -> int -> Sort.sort -> Expr.expr 735 736 (** Create a quantifier pattern. *) 737 val mk_pattern : context -> Expr.expr list -> Pattern.pattern 738 739 740 (** Create a universal Quantifier. *) 741 val mk_forall : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier 742 743 (** Create a universal Quantifier. *) 744 val mk_forall_const : context -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier 745 746 (** Create an existential Quantifier. *) 747 val mk_exists : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier 748 749 (** Create an existential Quantifier. *) 750 val mk_exists_const : context -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier 751 752 (** Create a lambda binding. *) 753 val mk_lambda_const : context -> Expr.expr list -> Expr.expr -> quantifier 754 755 (** Create a lambda binding where bound variables are given by symbols and sorts *) 756 val mk_lambda : context -> (Symbol.symbol * Sort.sort) list -> Expr.expr -> quantifier 757 758 (** Create a Quantifier. *) 759 val mk_quantifier : context -> bool -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier 760 761 (** Create a Quantifier. *) 762 val mk_quantifier_const : context -> bool -> Expr.expr list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier 763 764 (** A string representation of the quantifier. *) 765 val to_string : quantifier -> string 766end 767 768(** Functions to manipulate Array expressions *) 769module Z3Array : 770sig 771 (** Create a new array sort. *) 772 val mk_sort : context -> Sort.sort -> Sort.sort -> Sort.sort 773 774 (** Indicates whether the term is an array store. 775 It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). 776 Array store takes at least 3 arguments. *) 777 val is_store : Expr.expr -> bool 778 779 (** Indicates whether the term is an array select. *) 780 val is_select : Expr.expr -> bool 781 782 (** Indicates whether the term is a constant array. 783 For example, select(const(v),i) = v holds for every v and i. The function is unary. *) 784 val is_constant_array : Expr.expr -> bool 785 786 (** Indicates whether the term is a default array. 787 For example default(const(v)) = v. The function is unary. *) 788 val is_default_array : Expr.expr -> bool 789 790 (** Indicates whether the term is an array map. 791 It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i. *) 792 val is_array_map : Expr.expr -> bool 793 794 (** Indicates whether the term is an as-array term. 795 An as-array term is n array value that behaves as the function graph of the 796 function passed as parameter. *) 797 val is_as_array : Expr.expr -> bool 798 799 (** Indicates whether the term is of an array sort. *) 800 val is_array : Expr.expr -> bool 801 802 (** The domain of the array sort. *) 803 val get_domain : Sort.sort -> Sort.sort 804 805 (** The range of the array sort. *) 806 val get_range : Sort.sort -> Sort.sort 807 808 (** Create an array constant. *) 809 val mk_const : context -> Symbol.symbol -> Sort.sort -> Sort.sort -> Expr.expr 810 811 (** Create an array constant. *) 812 val mk_const_s : context -> string -> Sort.sort -> Sort.sort -> Expr.expr 813 814 (** Array read. 815 816 The argument [a] is the array and [i] is the index 817 of the array that gets read. 818 819 The node [a] must have an array sort [[domain -> range]], 820 and [i] must have the sort [domain]. 821 The sort of the result is [range]. 822 {!Z3Array.mk_sort} 823 {!mk_store} *) 824 val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr 825 826 (** Array update. 827 828 The node [a] must have an array sort [[domain -> range]], 829 [i] must have sort [domain], 830 [v] must have sort range. The sort of the result is [[domain -> range]]. 831 The semantics of this function is given by the theory of arrays described in the SMT-LIB 832 standard. See http://smtlib.org for more details. 833 The result of this function is an array that is equal to [a] 834 (with respect to [select]) 835 on all indices except for [i], where it maps to [v] 836 (and the [select] of [a] with 837 respect to [i] may be a different value). 838 {!Z3Array.mk_sort} 839 {!mk_select} *) 840 val mk_store : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 841 842 (** Create a constant array. 843 844 The resulting term is an array, such that a [select]on an arbitrary index 845 produces the value [v]. 846 {!Z3Array.mk_sort} 847 {!mk_select} *) 848 val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr 849 850 (** Maps f on the argument arrays. 851 852 Each element of [args] must be of an array sort [[domain_i -> range_i]]. 853 The function declaration [f] must have type [ range_1 .. range_n -> range]. 854 [v] must have sort range. The sort of the result is [[domain_i -> range]]. 855 {!Z3Array.mk_sort} 856 {!mk_select} 857 {!mk_store} *) 858 val mk_map : context -> FuncDecl.func_decl -> Expr.expr list -> Expr.expr 859 860 (** Access the array default value. 861 862 Produces the default range value, for arrays that can be represented as 863 finite maps with a default range value. *) 864 val mk_term_array : context -> Expr.expr -> Expr.expr 865 866 (** Create array extensionality index given two arrays with the same sort. 867 868 The meaning is given by the axiom: 869 (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) *) 870 val mk_array_ext : context -> Expr.expr -> Expr.expr -> Expr.expr 871 872end 873 874(** Functions to manipulate Set expressions *) 875module Set : 876sig 877 (** Create a set type. *) 878 val mk_sort : context -> Sort.sort -> Sort.sort 879 880 (** Indicates whether the term is set union *) 881 val is_union : Expr.expr -> bool 882 883 (** Indicates whether the term is set intersection *) 884 val is_intersect : Expr.expr -> bool 885 886 (** Indicates whether the term is set difference *) 887 val is_difference : Expr.expr -> bool 888 889 (** Indicates whether the term is set complement *) 890 val is_complement : Expr.expr -> bool 891 892 (** Indicates whether the term is set subset *) 893 val is_subset : Expr.expr -> bool 894 895 (** Create an empty set. *) 896 val mk_empty : context -> Sort.sort -> Expr.expr 897 898 (** Create the full set. *) 899 val mk_full : context -> Sort.sort -> Expr.expr 900 901 (** Add an element to the set. *) 902 val mk_set_add : context -> Expr.expr -> Expr.expr -> Expr.expr 903 904 (** Remove an element from a set. *) 905 val mk_del : context -> Expr.expr -> Expr.expr -> Expr.expr 906 907 (** Take the union of a list of sets. *) 908 val mk_union : context -> Expr.expr list -> Expr.expr 909 910 (** Take the intersection of a list of sets. *) 911 val mk_intersection : context -> Expr.expr list -> Expr.expr 912 913 (** Take the difference between two sets. *) 914 val mk_difference : context -> Expr.expr -> Expr.expr -> Expr.expr 915 916 (** Take the complement of a set. *) 917 val mk_complement : context -> Expr.expr -> Expr.expr 918 919 (** Check for set membership. *) 920 val mk_membership : context -> Expr.expr -> Expr.expr -> Expr.expr 921 922 (** Check for subsetness of sets. *) 923 val mk_subset : context -> Expr.expr -> Expr.expr -> Expr.expr 924end 925 926(** Functions to manipulate Finite Domain expressions *) 927module FiniteDomain : 928sig 929 (** Create a new finite domain sort. *) 930 val mk_sort : context -> Symbol.symbol -> int -> Sort.sort 931 932 (** Create a new finite domain sort. *) 933 val mk_sort_s : context -> string -> int -> Sort.sort 934 935 (** Indicates whether the term is of an array sort. *) 936 val is_finite_domain : Expr.expr -> bool 937 938 (** Indicates whether the term is a less than predicate over a finite domain. *) 939 val is_lt : Expr.expr -> bool 940 941 (** The size of the finite domain sort. *) 942 val get_size : Sort.sort -> int 943end 944 945 946(** Functions to manipulate Relation expressions *) 947module Relation : 948sig 949 (** Indicates whether the term is of a relation sort. *) 950 val is_relation : Expr.expr -> bool 951 952 (** Indicates whether the term is an relation store 953 954 Insert a record into a relation. 955 The function takes [n+1] arguments, where the first argument is the relation and the remaining [n] elements 956 correspond to the [n] columns of the relation. *) 957 val is_store : Expr.expr -> bool 958 959 (** Indicates whether the term is an empty relation *) 960 val is_empty : Expr.expr -> bool 961 962 (** Indicates whether the term is a test for the emptiness of a relation *) 963 val is_is_empty : Expr.expr -> bool 964 965 (** Indicates whether the term is a relational join *) 966 val is_join : Expr.expr -> bool 967 968 (** Indicates whether the term is the union or convex hull of two relations. 969 The function takes two arguments. *) 970 val is_union : Expr.expr -> bool 971 972 (** Indicates whether the term is the widening of two relations 973 The function takes two arguments. *) 974 val is_widen : Expr.expr -> bool 975 976 (** Indicates whether the term is a projection of columns (provided as numbers in the parameters). 977 The function takes one argument. *) 978 val is_project : Expr.expr -> bool 979 980 (** Indicates whether the term is a relation filter 981 982 Filter (restrict) a relation with respect to a predicate. 983 The first argument is a relation. 984 The second argument is a predicate with free de-Bruijn indices 985 corresponding to the columns of the relation. 986 So the first column in the relation has index 0. *) 987 val is_filter : Expr.expr -> bool 988 989 (** Indicates whether the term is an intersection of a relation with the negation of another. 990 991 Intersect the first relation with respect to negation 992 of the second relation (the function takes two arguments). 993 Logically, the specification can be described by a function 994 995 target = filter_by_negation(pos, neg, columns) 996 997 where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that 998 target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with 999 ( x : expr ) on the columns c1, d1, .., cN, dN. *) 1000 val is_negation_filter : Expr.expr -> bool 1001 1002 (** Indicates whether the term is the renaming of a column in a relation 1003 1004 The function takes one argument. 1005 The parameters contain the renaming as a cycle. *) 1006 val is_rename : Expr.expr -> bool 1007 1008 (** Indicates whether the term is the complement of a relation *) 1009 val is_complement : Expr.expr -> bool 1010 1011 (** Indicates whether the term is a relational select 1012 1013 Check if a record is an element of the relation. 1014 The function takes [n+1] arguments, where the first argument is a relation, 1015 and the remaining [n] arguments correspond to a record. *) 1016 val is_select : Expr.expr -> bool 1017 1018 (** Indicates whether the term is a relational clone (copy) 1019 1020 Create a fresh copy (clone) of a relation. 1021 The function is logically the identity, but 1022 in the context of a register machine allows 1023 for terms of kind {!is_union} 1024 to perform destructive updates to the first argument. *) 1025 val is_clone : Expr.expr -> bool 1026 1027 (** The arity of the relation sort. *) 1028 val get_arity : Sort.sort -> int 1029 1030 (** The sorts of the columns of the relation sort. *) 1031 val get_column_sorts : Sort.sort -> Sort.sort list 1032end 1033 1034(** Functions to manipulate Datatype expressions *) 1035module Datatype : 1036sig 1037 (** Datatype Constructors *) 1038 module Constructor : 1039 sig 1040 type constructor 1041 1042 (** The number of fields of the constructor. *) 1043 val get_num_fields : constructor -> int 1044 1045 (** The function declaration of the constructor. *) 1046 val get_constructor_decl : constructor -> FuncDecl.func_decl 1047 1048 (** The function declaration of the tester. *) 1049 val get_tester_decl : constructor -> FuncDecl.func_decl 1050 1051 (** The function declarations of the accessors *) 1052 val get_accessor_decls : constructor -> FuncDecl.func_decl list 1053 end 1054 1055 (** Create a datatype constructor. 1056 if the corresponding sort reference is 0, then the value in sort_refs should be an index 1057 referring to one of the recursive datatypes that is declared. *) 1058 val mk_constructor : context -> Symbol.symbol -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor 1059 1060 (** Create a datatype constructor. 1061 if the corresponding sort reference is 0, then the value in sort_refs should be an index 1062 referring to one of the recursive datatypes that is declared. *) 1063 val mk_constructor_s : context -> string -> Symbol.symbol -> Symbol.symbol list -> Sort.sort option list -> int list -> Constructor.constructor 1064 1065 (** Create a new datatype sort. *) 1066 val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort 1067 1068 (** Create a new datatype sort. *) 1069 val mk_sort_s : context -> string -> Constructor.constructor list -> Sort.sort 1070 1071 (** Create mutually recursive datatypes. *) 1072 val mk_sorts : context -> Symbol.symbol list -> Constructor.constructor list list -> Sort.sort list 1073 1074 (** Create mutually recursive data-types. *) 1075 val mk_sorts_s : context -> string list -> Constructor.constructor list list -> Sort.sort list 1076 1077 (** The number of constructors of the datatype sort. *) 1078 val get_num_constructors : Sort.sort -> int 1079 1080 (** The constructors. *) 1081 val get_constructors : Sort.sort -> FuncDecl.func_decl list 1082 1083 (** The recognizers. *) 1084 val get_recognizers : Sort.sort -> FuncDecl.func_decl list 1085 1086 (** The constructor accessors. *) 1087 val get_accessors : Sort.sort -> FuncDecl.func_decl list list 1088end 1089 1090(** Functions to manipulate Enumeration expressions *) 1091module Enumeration : 1092sig 1093 (** Create a new enumeration sort. *) 1094 val mk_sort : context -> Symbol.symbol -> Symbol.symbol list -> Sort.sort 1095 1096 (** Create a new enumeration sort. *) 1097 val mk_sort_s : context -> string -> string list -> Sort.sort 1098 1099 (** The function declarations of the constants in the enumeration. *) 1100 val get_const_decls : Sort.sort -> FuncDecl.func_decl list 1101 1102 (** Retrieves the inx'th constant declaration in the enumeration. *) 1103 val get_const_decl : Sort.sort -> int -> FuncDecl.func_decl 1104 1105 (** The constants in the enumeration. *) 1106 val get_consts : Sort.sort -> Expr.expr list 1107 1108 (** Retrieves the inx'th constant in the enumeration. *) 1109 val get_const : Sort.sort -> int -> Expr.expr 1110 1111 (** The test predicates for the constants in the enumeration. *) 1112 val get_tester_decls : Sort.sort -> FuncDecl.func_decl list 1113 1114 (** Retrieves the inx'th tester/recognizer declaration in the enumeration. *) 1115 val get_tester_decl : Sort.sort -> int -> FuncDecl.func_decl 1116end 1117 1118(** Functions to manipulate List expressions *) 1119module Z3List : 1120sig 1121 (** Create a new list sort. *) 1122 val mk_sort : context -> Symbol.symbol -> Sort.sort -> Sort.sort 1123 1124 (** Create a new list sort. *) 1125 val mk_list_s : context -> string -> Sort.sort -> Sort.sort 1126 1127 (** The declaration of the nil function of this list sort. *) 1128 val get_nil_decl : Sort.sort -> FuncDecl.func_decl 1129 1130 (** The declaration of the isNil function of this list sort. *) 1131 val get_is_nil_decl : Sort.sort -> FuncDecl.func_decl 1132 1133 (** The declaration of the cons function of this list sort. *) 1134 val get_cons_decl : Sort.sort -> FuncDecl.func_decl 1135 1136 (** The declaration of the isCons function of this list sort. *) 1137 val get_is_cons_decl : Sort.sort -> FuncDecl.func_decl 1138 1139 (** The declaration of the head function of this list sort. *) 1140 val get_head_decl : Sort.sort -> FuncDecl.func_decl 1141 1142 (** The declaration of the tail function of this list sort. *) 1143 val get_tail_decl : Sort.sort -> FuncDecl.func_decl 1144 1145 (** The empty list. *) 1146 val nil : Sort.sort -> Expr.expr 1147end 1148 1149(** Functions to manipulate Tuple expressions *) 1150module Tuple : 1151sig 1152 (** Create a new tuple sort. *) 1153 val mk_sort : context -> Symbol.symbol -> Symbol.symbol list -> Sort.sort list -> Sort.sort 1154 1155 (** The constructor function of the tuple. *) 1156 val get_mk_decl : Sort.sort -> FuncDecl.func_decl 1157 1158 (** The number of fields in the tuple. *) 1159 val get_num_fields : Sort.sort -> int 1160 1161 (** The field declarations. *) 1162 val get_field_decls : Sort.sort -> FuncDecl.func_decl list 1163end 1164 1165(** Functions to manipulate arithmetic expressions *) 1166module Arithmetic : 1167sig 1168 (** Integer Arithmetic *) 1169 module Integer : 1170 sig 1171 (** Create a new integer sort. *) 1172 val mk_sort : context -> Sort.sort 1173 1174 (** Get a big_int from an integer numeral *) 1175 val get_big_int : Expr.expr -> Z.t 1176 1177 (** Returns a string representation of a numeral. *) 1178 val numeral_to_string : Expr.expr -> string 1179 1180 (** Creates an integer constant. *) 1181 val mk_const : context -> Symbol.symbol -> Expr.expr 1182 1183 (** Creates an integer constant. *) 1184 val mk_const_s : context -> string -> Expr.expr 1185 1186 (** Create an expression representing [t1 mod t2]. 1187 The arguments must have int type. *) 1188 val mk_mod : context -> Expr.expr -> Expr.expr -> Expr.expr 1189 1190 (** Create an expression representing [t1 rem t2]. 1191 The arguments must have int type. *) 1192 val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr 1193 1194 (** Create an integer numeral. *) 1195 val mk_numeral_s : context -> string -> Expr.expr 1196 1197 (** Create an integer numeral. 1198 @return A Term with the given value and sort Integer *) 1199 val mk_numeral_i : context -> int -> Expr.expr 1200 1201 (** Coerce an integer to a real. 1202 1203 There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard. 1204 1205 You can take the floor of a real by creating an auxiliary integer Term [k] and 1206 and asserting [MakeInt2Real(k) <= t1 < MkInt2Real(k)+1]. 1207 The argument must be of integer sort. *) 1208 val mk_int2real : context -> Expr.expr -> Expr.expr 1209 1210 (** Create an n-bit bit-vector from an integer argument. 1211 1212 NB. This function is essentially treated as uninterpreted. 1213 So you cannot expect Z3 to precisely reflect the semantics of this function 1214 when solving constraints with this function. 1215 1216 The argument must be of integer sort. *) 1217 val mk_int2bv : context -> int -> Expr.expr -> Expr.expr 1218 end 1219 1220 (** Real Arithmetic *) 1221 module Real : 1222 sig 1223 (** Create a real sort. *) 1224 val mk_sort : context -> Sort.sort 1225 1226 (** The numerator of a rational numeral. *) 1227 val get_numerator : Expr.expr -> Expr.expr 1228 1229 (** The denominator of a rational numeral. *) 1230 val get_denominator : Expr.expr -> Expr.expr 1231 1232 (** Get a ratio from a real numeral *) 1233 val get_ratio : Expr.expr -> Q.t 1234 1235 (** Returns a string representation in decimal notation. 1236 The result has at most as many decimal places as indicated by the int argument.*) 1237 val to_decimal_string : Expr.expr-> int -> string 1238 1239 (** Returns a string representation of a numeral. *) 1240 val numeral_to_string : Expr.expr-> string 1241 1242 (** Creates a real constant. *) 1243 val mk_const : context -> Symbol.symbol -> Expr.expr 1244 1245 (** Creates a real constant. *) 1246 val mk_const_s : context -> string -> Expr.expr 1247 1248 (** Create a real numeral from a fraction. 1249 @return A Term with rational value and sort Real 1250 {!mk_numeral_s} *) 1251 val mk_numeral_nd : context -> int -> int -> Expr.expr 1252 1253 (** Create a real numeral. 1254 @return A Term with the given value and sort Real *) 1255 val mk_numeral_s : context -> string -> Expr.expr 1256 1257 (** Create a real numeral. 1258 @return A Term with the given value and sort Real *) 1259 val mk_numeral_i : context -> int -> Expr.expr 1260 1261 (** Creates an expression that checks whether a real number is an integer. *) 1262 val mk_is_integer : context -> Expr.expr -> Expr.expr 1263 1264 (** Coerce a real to an integer. 1265 1266 The semantics of this function follows the SMT-LIB standard for the function to_int. 1267 The argument must be of real sort. *) 1268 val mk_real2int : context -> Expr.expr -> Expr.expr 1269 1270 (** Algebraic Numbers *) 1271 module AlgebraicNumber : 1272 sig 1273 (** Return a upper bound for a given real algebraic number. 1274 The interval isolating the number is smaller than 1/10^precision. 1275 {!is_algebraic_number} 1276 @return A numeral Expr of sort Real *) 1277 val to_upper : Expr.expr -> int -> Expr.expr 1278 1279 (** Return a lower bound for the given real algebraic number. 1280 The interval isolating the number is smaller than 1/10^precision. 1281 {!is_algebraic_number} 1282 @return A numeral Expr of sort Real *) 1283 val to_lower : Expr.expr -> int -> Expr.expr 1284 1285 (** Returns a string representation in decimal notation. 1286 The result has at most as many decimal places as the int argument provided.*) 1287 val to_decimal_string : Expr.expr -> int -> string 1288 1289 (** Returns a string representation of a numeral. *) 1290 val numeral_to_string : Expr.expr -> string 1291 end 1292 end 1293 1294 (** Indicates whether the term is of integer sort. *) 1295 val is_int : Expr.expr -> bool 1296 1297 (** Indicates whether the term is an arithmetic numeral. *) 1298 val is_arithmetic_numeral : Expr.expr -> bool 1299 1300 (** Indicates whether the term is a less-than-or-equal *) 1301 val is_le : Expr.expr -> bool 1302 1303 (** Indicates whether the term is a greater-than-or-equal *) 1304 val is_ge : Expr.expr -> bool 1305 1306 (** Indicates whether the term is a less-than *) 1307 val is_lt : Expr.expr -> bool 1308 1309 (** Indicates whether the term is a greater-than *) 1310 val is_gt : Expr.expr -> bool 1311 1312 (** Indicates whether the term is addition (binary) *) 1313 val is_add : Expr.expr -> bool 1314 1315 (** Indicates whether the term is subtraction (binary) *) 1316 val is_sub : Expr.expr -> bool 1317 1318 (** Indicates whether the term is a unary minus *) 1319 val is_uminus : Expr.expr -> bool 1320 1321 (** Indicates whether the term is multiplication (binary) *) 1322 val is_mul : Expr.expr -> bool 1323 1324 (** Indicates whether the term is division (binary) *) 1325 val is_div : Expr.expr -> bool 1326 1327 (** Indicates whether the term is integer division (binary) *) 1328 val is_idiv : Expr.expr -> bool 1329 1330 (** Indicates whether the term is remainder (binary) *) 1331 val is_remainder : Expr.expr -> bool 1332 1333 (** Indicates whether the term is modulus (binary) *) 1334 val is_modulus : Expr.expr -> bool 1335 1336 (** Indicates whether the term is a coercion of integer to real (unary) *) 1337 val is_int2real : Expr.expr -> bool 1338 1339 (** Indicates whether the term is a coercion of real to integer (unary) *) 1340 val is_real2int : Expr.expr -> bool 1341 1342 (** Indicates whether the term is a check that tests whether a real is integral (unary) *) 1343 val is_real_is_int : Expr.expr -> bool 1344 1345 (** Indicates whether the term is of sort real. *) 1346 val is_real : Expr.expr -> bool 1347 1348 (** Indicates whether the term is an integer numeral. *) 1349 val is_int_numeral : Expr.expr -> bool 1350 1351 (** Indicates whether the term is a real numeral. *) 1352 val is_rat_numeral : Expr.expr -> bool 1353 1354 (** Indicates whether the term is an algebraic number *) 1355 val is_algebraic_number : Expr.expr -> bool 1356 1357 (** Create an expression representing [t[0] + t[1] + ...]. *) 1358 val mk_add : context -> Expr.expr list -> Expr.expr 1359 1360 (** Create an expression representing [t[0] * t[1] * ...]. *) 1361 val mk_mul : context -> Expr.expr list -> Expr.expr 1362 1363 (** Create an expression representing [t[0] - t[1] - ...]. *) 1364 val mk_sub : context -> Expr.expr list -> Expr.expr 1365 1366 (** Create an expression representing [-t]. *) 1367 val mk_unary_minus : context -> Expr.expr -> Expr.expr 1368 1369 (** Create an expression representing [t1 / t2]. *) 1370 val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr 1371 1372 (** Create an expression representing [t1 ^ t2]. *) 1373 val mk_power : context -> Expr.expr -> Expr.expr -> Expr.expr 1374 1375 (** Create an expression representing [t1 < t2] *) 1376 val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr 1377 1378 (** Create an expression representing [t1 <= t2] *) 1379 val mk_le : context -> Expr.expr -> Expr.expr -> Expr.expr 1380 1381 (** Create an expression representing [t1 > t2] *) 1382 val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr 1383 1384 (** Create an expression representing [t1 >= t2] *) 1385 val mk_ge : context -> Expr.expr -> Expr.expr -> Expr.expr 1386end 1387 1388(** Functions to manipulate bit-vector expressions *) 1389module BitVector : 1390sig 1391 (** Create a new bit-vector sort. *) 1392 val mk_sort : context -> int -> Sort.sort 1393 1394 (** Indicates whether the terms is of bit-vector sort. *) 1395 val is_bv : Expr.expr -> bool 1396 1397 (** Indicates whether the term is a bit-vector numeral *) 1398 val is_bv_numeral : Expr.expr -> bool 1399 1400 (** Indicates whether the term is a one-bit bit-vector with value one *) 1401 val is_bv_bit1 : Expr.expr -> bool 1402 1403 (** Indicates whether the term is a one-bit bit-vector with value zero *) 1404 val is_bv_bit0 : Expr.expr -> bool 1405 1406 (** Indicates whether the term is a bit-vector unary minus *) 1407 val is_bv_uminus : Expr.expr -> bool 1408 1409 (** Indicates whether the term is a bit-vector addition (binary) *) 1410 val is_bv_add : Expr.expr -> bool 1411 1412 (** Indicates whether the term is a bit-vector subtraction (binary) *) 1413 val is_bv_sub : Expr.expr -> bool 1414 1415 (** Indicates whether the term is a bit-vector multiplication (binary) *) 1416 val is_bv_mul : Expr.expr -> bool 1417 1418 (** Indicates whether the term is a bit-vector signed division (binary) *) 1419 val is_bv_sdiv : Expr.expr -> bool 1420 1421 (** Indicates whether the term is a bit-vector unsigned division (binary) *) 1422 val is_bv_udiv : Expr.expr -> bool 1423 1424 (** Indicates whether the term is a bit-vector signed remainder (binary) *) 1425 val is_bv_SRem : Expr.expr -> bool 1426 1427 (** Indicates whether the term is a bit-vector unsigned remainder (binary) *) 1428 val is_bv_urem : Expr.expr -> bool 1429 1430 (** Indicates whether the term is a bit-vector signed modulus *) 1431 val is_bv_smod : Expr.expr -> bool 1432 1433 (** Indicates whether the term is a bit-vector signed division by zero *) 1434 val is_bv_sdiv0 : Expr.expr -> bool 1435 1436 (** Indicates whether the term is a bit-vector unsigned division by zero *) 1437 val is_bv_udiv0 : Expr.expr -> bool 1438 1439 (** Indicates whether the term is a bit-vector signed remainder by zero *) 1440 val is_bv_srem0 : Expr.expr -> bool 1441 1442 (** Indicates whether the term is a bit-vector unsigned remainder by zero *) 1443 val is_bv_urem0 : Expr.expr -> bool 1444 1445 (** Indicates whether the term is a bit-vector signed modulus by zero *) 1446 val is_bv_smod0 : Expr.expr -> bool 1447 1448 (** Indicates whether the term is an unsigned bit-vector less-than-or-equal *) 1449 val is_bv_ule : Expr.expr -> bool 1450 1451 (** Indicates whether the term is a signed bit-vector less-than-or-equal *) 1452 val is_bv_sle : Expr.expr -> bool 1453 1454 (** Indicates whether the term is an unsigned bit-vector greater-than-or-equal *) 1455 val is_bv_uge : Expr.expr -> bool 1456 1457 (** Indicates whether the term is a signed bit-vector greater-than-or-equal *) 1458 val is_bv_sge : Expr.expr -> bool 1459 1460 (** Indicates whether the term is an unsigned bit-vector less-than *) 1461 val is_bv_ult : Expr.expr -> bool 1462 1463 (** Indicates whether the term is a signed bit-vector less-than *) 1464 val is_bv_slt : Expr.expr -> bool 1465 1466 (** Indicates whether the term is an unsigned bit-vector greater-than *) 1467 val is_bv_ugt : Expr.expr -> bool 1468 1469 (** Indicates whether the term is a signed bit-vector greater-than *) 1470 val is_bv_sgt : Expr.expr -> bool 1471 1472 (** Indicates whether the term is a bit-wise AND *) 1473 val is_bv_and : Expr.expr -> bool 1474 1475 (** Indicates whether the term is a bit-wise OR *) 1476 val is_bv_or : Expr.expr -> bool 1477 1478 (** Indicates whether the term is a bit-wise NOT *) 1479 val is_bv_not : Expr.expr -> bool 1480 1481 (** Indicates whether the term is a bit-wise XOR *) 1482 val is_bv_xor : Expr.expr -> bool 1483 1484 (** Indicates whether the term is a bit-wise NAND *) 1485 val is_bv_nand : Expr.expr -> bool 1486 1487 (** Indicates whether the term is a bit-wise NOR *) 1488 val is_bv_nor : Expr.expr -> bool 1489 1490 (** Indicates whether the term is a bit-wise XNOR *) 1491 val is_bv_xnor : Expr.expr -> bool 1492 1493 (** Indicates whether the term is a bit-vector concatenation (binary) *) 1494 val is_bv_concat : Expr.expr -> bool 1495 1496 (** Indicates whether the term is a bit-vector sign extension *) 1497 val is_bv_signextension : Expr.expr -> bool 1498 1499 (** Indicates whether the term is a bit-vector zero extension *) 1500 val is_bv_zeroextension : Expr.expr -> bool 1501 1502 (** Indicates whether the term is a bit-vector extraction *) 1503 val is_bv_extract : Expr.expr -> bool 1504 1505 (** Indicates whether the term is a bit-vector repetition *) 1506 val is_bv_repeat : Expr.expr -> bool 1507 1508 (** Indicates whether the term is a bit-vector reduce OR *) 1509 val is_bv_reduceor : Expr.expr -> bool 1510 1511 (** Indicates whether the term is a bit-vector reduce AND *) 1512 val is_bv_reduceand : Expr.expr -> bool 1513 1514 (** Indicates whether the term is a bit-vector comparison *) 1515 val is_bv_comp : Expr.expr -> bool 1516 1517 (** Indicates whether the term is a bit-vector shift left *) 1518 val is_bv_shiftleft : Expr.expr -> bool 1519 1520 (** Indicates whether the term is a bit-vector logical shift right *) 1521 val is_bv_shiftrightlogical : Expr.expr -> bool 1522 1523 (** Indicates whether the term is a bit-vector arithmetic shift left *) 1524 val is_bv_shiftrightarithmetic : Expr.expr -> bool 1525 1526 (** Indicates whether the term is a bit-vector rotate left *) 1527 val is_bv_rotateleft : Expr.expr -> bool 1528 1529 (** Indicates whether the term is a bit-vector rotate right *) 1530 val is_bv_rotateright : Expr.expr -> bool 1531 1532 (** Indicates whether the term is a bit-vector rotate left (extended) 1533 Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one. *) 1534 val is_bv_rotateleftextended : Expr.expr -> bool 1535 1536 (** Indicates whether the term is a bit-vector rotate right (extended) 1537 Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one. *) 1538 val is_bv_rotaterightextended : Expr.expr -> bool 1539 1540 (** Indicates whether the term is a coercion from bit-vector to integer 1541 This function is not supported by the decision procedures. Only the most 1542 rudimentary simplification rules are applied to this function. *) 1543 val is_int2bv : Expr.expr -> bool 1544 1545 (** Indicates whether the term is a coercion from integer to bit-vector 1546 This function is not supported by the decision procedures. Only the most 1547 rudimentary simplification rules are applied to this function. *) 1548 val is_bv2int : Expr.expr -> bool 1549 1550 (** Indicates whether the term is a bit-vector carry 1551 Compute the carry bit in a full-adder. The meaning is given by the 1552 equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3))) *) 1553 val is_bv_carry : Expr.expr -> bool 1554 1555 (** Indicates whether the term is a bit-vector ternary XOR 1556 The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) *) 1557 val is_bv_xor3 : Expr.expr -> bool 1558 1559 (** The size of a bit-vector sort. *) 1560 val get_size : Sort.sort -> int 1561 1562 (** Returns a string representation of a numeral. *) 1563 val numeral_to_string : Expr.expr -> string 1564 1565 (** Creates a bit-vector constant. *) 1566 val mk_const : context -> Symbol.symbol -> int -> Expr.expr 1567 1568 (** Creates a bit-vector constant. *) 1569 val mk_const_s : context -> string -> int -> Expr.expr 1570 1571 (** Bitwise negation. 1572 The argument must have a bit-vector sort. *) 1573 val mk_not : context -> Expr.expr -> Expr.expr 1574 1575 (** Take conjunction of bits in a vector,vector of length 1. 1576 The argument must have a bit-vector sort. *) 1577 val mk_redand : context -> Expr.expr -> Expr.expr 1578 1579 (** Take disjunction of bits in a vector,vector of length 1. 1580 The argument must have a bit-vector sort. *) 1581 val mk_redor : context -> Expr.expr -> Expr.expr 1582 1583 (** Bitwise conjunction. 1584 The arguments must have a bit-vector sort. *) 1585 val mk_and : context -> Expr.expr -> Expr.expr -> Expr.expr 1586 1587 (** Bitwise disjunction. 1588 The arguments must have a bit-vector sort. *) 1589 val mk_or : context -> Expr.expr -> Expr.expr -> Expr.expr 1590 1591 (** Bitwise XOR. 1592 The arguments must have a bit-vector sort. *) 1593 val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr 1594 1595 (** Bitwise NAND. 1596 The arguments must have a bit-vector sort. *) 1597 val mk_nand : context -> Expr.expr -> Expr.expr -> Expr.expr 1598 1599 (** Bitwise NOR. 1600 The arguments must have a bit-vector sort. *) 1601 val mk_nor : context -> Expr.expr -> Expr.expr -> Expr.expr 1602 1603 (** Bitwise XNOR. 1604 The arguments must have a bit-vector sort. *) 1605 val mk_xnor : context -> Expr.expr -> Expr.expr -> Expr.expr 1606 1607 (** Standard two's complement unary minus. 1608 The arguments must have a bit-vector sort. *) 1609 val mk_neg : context -> Expr.expr -> Expr.expr 1610 1611 (** Two's complement addition. 1612 The arguments must have the same bit-vector sort. *) 1613 val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr 1614 1615 (** Two's complement subtraction. 1616 The arguments must have the same bit-vector sort. *) 1617 val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr 1618 1619 (** Two's complement multiplication. 1620 The arguments must have the same bit-vector sort. *) 1621 val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr 1622 1623 (** Unsigned division. 1624 1625 It is defined as the floor of [t1/t2] if \c t2 is 1626 different from zero. If [t2] is zero, then the result 1627 is not uniquely specified. It can be set to any value 1628 that satisfies the constraints where unsigned division is used. 1629 The arguments must have the same bit-vector sort. *) 1630 val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.expr 1631 1632 (** Signed division. 1633 1634 It is defined in the following way: 1635 1636 - The \c floor of [t1/t2] if \c t2 is different from zero, and [t1*t2 >= 0]. 1637 1638 - The \c ceiling of [t1/t2] if \c t2 is different from zero, and [t1*t2 < 0]. 1639 1640 If [t2] is zero, then the result is is not uniquely specified. 1641 It can be set to any value that satisfies the constraints 1642 where signed division is used. 1643 The arguments must have the same bit-vector sort. *) 1644 val mk_sdiv : context -> Expr.expr -> Expr.expr -> Expr.expr 1645 1646 (** Unsigned remainder. 1647 1648 It is defined as [t1 - (t1 /u t2) * t2], where [/u] represents unsigned division. 1649 If [t2] is zero, then the result is not uniquely specified. 1650 It can be set to any value that satisfies the constraints 1651 where unsigned remainder is used. 1652 The arguments must have the same bit-vector sort. *) 1653 val mk_urem : context -> Expr.expr -> Expr.expr -> Expr.expr 1654 1655 (** Signed remainder. 1656 1657 It is defined as [t1 - (t1 /s t2) * t2], where [/s] represents signed division. 1658 The most significant bit (sign) of the result is equal to the most significant bit of \c t1. 1659 1660 If [t2] is zero, then the result is not uniquely specified. 1661 It can be set to any value that satisfies the constraints 1662 where signed remainder is used. 1663 The arguments must have the same bit-vector sort. *) 1664 val mk_srem : context -> Expr.expr -> Expr.expr -> Expr.expr 1665 1666 (** Two's complement signed remainder (sign follows divisor). 1667 1668 If [t2] is zero, then the result is not uniquely specified. 1669 It can be set to any value that satisfies the constraints 1670 where two's complement signed remainder is used. 1671 The arguments must have the same bit-vector sort. *) 1672 val mk_smod : context -> Expr.expr -> Expr.expr -> Expr.expr 1673 1674 (** Unsigned less-than 1675 1676 The arguments must have the same bit-vector sort. *) 1677 val mk_ult : context -> Expr.expr -> Expr.expr -> Expr.expr 1678 1679 (** Two's complement signed less-than 1680 1681 The arguments must have the same bit-vector sort. *) 1682 val mk_slt : context -> Expr.expr -> Expr.expr -> Expr.expr 1683 1684 (** Unsigned less-than or equal to. 1685 1686 The arguments must have the same bit-vector sort. *) 1687 val mk_ule : context -> Expr.expr -> Expr.expr -> Expr.expr 1688 1689 (** Two's complement signed less-than or equal to. 1690 1691 The arguments must have the same bit-vector sort. *) 1692 val mk_sle : context -> Expr.expr -> Expr.expr -> Expr.expr 1693 1694 (** Unsigned greater than or equal to. 1695 1696 The arguments must have the same bit-vector sort. *) 1697 val mk_uge : context -> Expr.expr -> Expr.expr -> Expr.expr 1698 1699 (** Two's complement signed greater than or equal to. 1700 1701 The arguments must have the same bit-vector sort. *) 1702 val mk_sge : context -> Expr.expr -> Expr.expr -> Expr.expr 1703 1704 (** Unsigned greater-than. 1705 1706 The arguments must have the same bit-vector sort. *) 1707 val mk_ugt : context -> Expr.expr -> Expr.expr -> Expr.expr 1708 1709 (** Two's complement signed greater-than. 1710 1711 The arguments must have the same bit-vector sort. *) 1712 val mk_sgt : context -> Expr.expr -> Expr.expr -> Expr.expr 1713 1714 (** Bit-vector concatenation. 1715 1716 The arguments must have a bit-vector sort. 1717 @return 1718 The result is a bit-vector of size [n1+n2], where [n1] ([n2]) 1719 is the size of [t1] ([t2]). *) 1720 val mk_concat : context -> Expr.expr -> Expr.expr -> Expr.expr 1721 1722 (** Bit-vector extraction. 1723 1724 Extract the bits between two limits from a bitvector of 1725 size [m] to yield a new bitvector of size [n], where 1726 [n = high - low + 1]. *) 1727 val mk_extract : context -> int -> int -> Expr.expr -> Expr.expr 1728 1729 (** Bit-vector sign extension. 1730 1731 Sign-extends the given bit-vector to the (signed) equivalent bitvector of 1732 size [m+i], where \c m is the size of the given bit-vector. *) 1733 val mk_sign_ext : context -> int -> Expr.expr -> Expr.expr 1734 1735 (** Bit-vector zero extension. 1736 1737 Extend the given bit-vector with zeros to the (unsigned) equivalent 1738 bitvector of size [m+i], where \c m is the size of the 1739 given bit-vector. *) 1740 val mk_zero_ext : context -> int -> Expr.expr -> Expr.expr 1741 1742 (** Bit-vector repetition. *) 1743 val mk_repeat : context -> int -> Expr.expr -> Expr.expr 1744 1745 (** Shift left. 1746 1747 It is equivalent to multiplication by [2^x] where \c x is the value of third argument. 1748 1749 NB. The semantics of shift operations varies between environments. This 1750 definition does not necessarily capture directly the semantics of the 1751 programming language or assembly architecture you are modeling.*) 1752 val mk_shl : context -> Expr.expr -> Expr.expr -> Expr.expr 1753 1754 (** Logical shift right 1755 1756 It is equivalent to unsigned division by [2^x] where \c x is the value of the third argument. 1757 1758 NB. The semantics of shift operations varies between environments. This 1759 definition does not necessarily capture directly the semantics of the 1760 programming language or assembly architecture you are modeling. 1761 1762 The arguments must have a bit-vector sort. *) 1763 val mk_lshr : context -> Expr.expr -> Expr.expr -> Expr.expr 1764 1765 (** Arithmetic shift right 1766 1767 It is like logical shift right except that the most significant 1768 bits of the result always copy the most significant bit of the 1769 second argument. 1770 1771 NB. The semantics of shift operations varies between environments. This 1772 definition does not necessarily capture directly the semantics of the 1773 programming language or assembly architecture you are modeling. 1774 1775 The arguments must have a bit-vector sort. *) 1776 val mk_ashr : context -> Expr.expr -> Expr.expr -> Expr.expr 1777 1778 (** Rotate Left. 1779 Rotate bits of \c t to the left \c i times. *) 1780 val mk_rotate_left : context -> int -> Expr.expr -> Expr.expr 1781 1782 (** Rotate Right. 1783 Rotate bits of \c t to the right \c i times.*) 1784 val mk_rotate_right : context -> int -> Expr.expr -> Expr.expr 1785 1786 (** Rotate Left. 1787 Rotate bits of the second argument to the left.*) 1788 val mk_ext_rotate_left : context -> Expr.expr -> Expr.expr -> Expr.expr 1789 1790 (** Rotate Right. 1791 Rotate bits of the second argument to the right. *) 1792 val mk_ext_rotate_right : context -> Expr.expr -> Expr.expr -> Expr.expr 1793 1794 (** Create an integer from the bit-vector argument 1795 1796 If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. 1797 So the result is non-negative and in the range [[0..2^N-1]], where 1798 N are the number of bits in the argument. 1799 If \c is_signed is true, \c t1 is treated as a signed bit-vector. 1800 1801 NB. This function is essentially treated as uninterpreted. 1802 So you cannot expect Z3 to precisely reflect the semantics of this function 1803 when solving constraints with this function.*) 1804 val mk_bv2int : context -> Expr.expr -> bool -> Expr.expr 1805 1806 (** Create a predicate that checks that the bit-wise addition does not overflow. 1807 1808 The arguments must be of bit-vector sort. *) 1809 val mk_add_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr 1810 1811 (** Create a predicate that checks that the bit-wise addition does not underflow. 1812 1813 The arguments must be of bit-vector sort. *) 1814 val mk_add_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr 1815 1816 (** Create a predicate that checks that the bit-wise subtraction does not overflow. 1817 1818 The arguments must be of bit-vector sort. *) 1819 val mk_sub_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr 1820 1821 (** Create a predicate that checks that the bit-wise subtraction does not underflow. 1822 1823 The arguments must be of bit-vector sort. *) 1824 val mk_sub_no_underflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr 1825 1826 (** Create a predicate that checks that the bit-wise signed division does not overflow. 1827 1828 The arguments must be of bit-vector sort. *) 1829 val mk_sdiv_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr 1830 1831 (** Create a predicate that checks that the bit-wise negation does not overflow. 1832 1833 The arguments must be of bit-vector sort. *) 1834 val mk_neg_no_overflow : context -> Expr.expr -> Expr.expr 1835 1836 (** Create a predicate that checks that the bit-wise multiplication does not overflow. 1837 1838 The arguments must be of bit-vector sort. *) 1839 val mk_mul_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr 1840 1841 (** Create a predicate that checks that the bit-wise multiplication does not underflow. 1842 1843 The arguments must be of bit-vector sort. *) 1844 val mk_mul_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr 1845 1846 (** Create a bit-vector numeral. *) 1847 val mk_numeral : context -> string -> int -> Expr.expr 1848end 1849 1850(** Sequences, Strings and Regular Expressions **) 1851module Seq : 1852sig 1853 (* create a sequence sort *) 1854 val mk_seq_sort : context -> Sort.sort -> Sort.sort 1855 1856 (* test if sort is a sequence sort *) 1857 val is_seq_sort : context -> Sort.sort -> bool 1858 1859 (* create regular expression sorts over sequences of the argument sort *) 1860 val mk_re_sort : context -> Sort.sort -> Sort.sort 1861 1862 (* test if sort is a regular expression sort *) 1863 val is_re_sort : context -> Sort.sort -> bool 1864 1865 (* create string sort *) 1866 val mk_string_sort : context -> Sort.sort 1867 1868 (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *) 1869 val is_string_sort : context -> Sort.sort -> bool 1870 1871 (* create a string literal *) 1872 val mk_string : context -> string -> Expr.expr 1873 1874 (* test if expression is a string *) 1875 val is_string : context -> Expr.expr -> bool 1876 1877 (* retrieve string from string Expr.expr *) 1878 val get_string : context -> Expr.expr -> string 1879 1880 (* the empty sequence over base sort *) 1881 val mk_seq_empty : context -> Sort.sort -> Expr.expr 1882 1883 (* a unit sequence *) 1884 val mk_seq_unit : context -> Expr.expr -> Expr.expr 1885 1886 (* sequence concatenation *) 1887 val mk_seq_concat : context -> Expr.expr list -> Expr.expr 1888 1889 (* predicate if the first argument is a prefix of the second *) 1890 val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr 1891 1892 (* predicate if the first argument is a suffix of the second *) 1893 val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr 1894 1895 (* predicate if the first argument contains the second *) 1896 val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr 1897 1898 (* extract sub-sequence starting at index given by second argument and of length provided by third argument *) 1899 val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 1900 1901 (* replace first occurrence of second argument by third *) 1902 val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 1903 1904 (* a unit sequence at index provided by second argument *) 1905 val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr 1906 1907 (* length of a sequence *) 1908 val mk_seq_length : context -> Expr.expr -> Expr.expr 1909 1910 (* index of the first occurrence of the second argument in the first *) 1911 val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 1912 1913 (* retrieve integer expression encoded in string *) 1914 val mk_str_to_int : context -> Expr.expr -> Expr.expr 1915 1916 (* convert an integer expression to a string *) 1917 val mk_int_to_str : context -> Expr.expr -> Expr.expr 1918 1919 (* create regular expression that accepts the argument sequence *) 1920 val mk_seq_to_re : context -> Expr.expr -> Expr.expr 1921 1922 (* regular expression membership predicate *) 1923 val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr 1924 1925 (* regular expression plus *) 1926 val mk_re_plus : context -> Expr.expr -> Expr.expr 1927 1928 (* regular expression star *) 1929 val mk_re_star : context -> Expr.expr -> Expr.expr 1930 1931 (* optional regular expression *) 1932 val mk_re_option : context -> Expr.expr -> Expr.expr 1933 1934 (* union of regular expressions *) 1935 val mk_re_union : context -> Expr.expr list -> Expr.expr 1936 1937 (* concatenation of regular expressions *) 1938 val mk_re_concat : context -> Expr.expr list -> Expr.expr 1939 1940 (* regular expression for the range between two characters *) 1941 val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr 1942 1943 (* bounded loop regular expression *) 1944 val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr 1945 1946 (* intersection of regular expressions *) 1947 val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr 1948 1949 (* the regular expression complement *) 1950 val mk_re_complement : context -> Expr.expr -> Expr.expr 1951 1952 (* the regular expression that accepts no sequences *) 1953 val mk_re_empty : context -> Sort.sort -> Expr.expr 1954 1955 (* the regular expression that accepts all sequences *) 1956 val mk_re_full : context -> Sort.sort -> Expr.expr 1957 1958end 1959 1960(** Floating-Point Arithmetic *) 1961module FloatingPoint : 1962sig 1963 1964 (** Rounding Modes *) 1965 module RoundingMode : 1966 sig 1967 (** Create the RoundingMode sort. *) 1968 val mk_sort : context -> Sort.sort 1969 1970 (** Indicates whether the terms is of floating-point rounding mode sort. *) 1971 val is_fprm : Expr.expr -> bool 1972 1973 (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) 1974 val mk_round_nearest_ties_to_even : context -> Expr.expr 1975 1976 (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) 1977 val mk_rne : context -> Expr.expr 1978 1979 (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) 1980 val mk_round_nearest_ties_to_away : context -> Expr.expr 1981 1982 (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) 1983 val mk_rna : context -> Expr.expr 1984 1985 (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) 1986 val mk_round_toward_positive : context -> Expr.expr 1987 1988 (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) 1989 val mk_rtp : context -> Expr.expr 1990 1991 (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) 1992 val mk_round_toward_negative : context -> Expr.expr 1993 1994 (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) 1995 val mk_rtn : context -> Expr.expr 1996 1997 (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) 1998 val mk_round_toward_zero : context -> Expr.expr 1999 2000 (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) 2001 val mk_rtz : context -> Expr.expr 2002 end 2003 2004 (** Create a FloatingPoint sort. *) 2005 val mk_sort : context -> int -> int -> Sort.sort 2006 2007 (** Create the half-precision (16-bit) FloatingPoint sort.*) 2008 val mk_sort_half : context -> Sort.sort 2009 2010 (** Create the half-precision (16-bit) FloatingPoint sort. *) 2011 val mk_sort_16 : context -> Sort.sort 2012 2013 (** Create the single-precision (32-bit) FloatingPoint sort.*) 2014 val mk_sort_single : context -> Sort.sort 2015 2016 (** Create the single-precision (32-bit) FloatingPoint sort. *) 2017 val mk_sort_32 : context -> Sort.sort 2018 2019 (** Create the double-precision (64-bit) FloatingPoint sort. *) 2020 val mk_sort_double : context -> Sort.sort 2021 2022 (** Create the double-precision (64-bit) FloatingPoint sort. *) 2023 val mk_sort_64 : context -> Sort.sort 2024 2025 (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) 2026 val mk_sort_quadruple : context -> Sort.sort 2027 2028 (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) 2029 val mk_sort_128 : context -> Sort.sort 2030 2031 (** Create a floating-point NaN of a given FloatingPoint sort. *) 2032 val mk_nan : context -> Sort.sort -> Expr.expr 2033 2034 (** Create a floating-point infinity of a given FloatingPoint sort. *) 2035 val mk_inf : context -> Sort.sort -> bool -> Expr.expr 2036 2037 (** Create a floating-point zero of a given FloatingPoint sort. *) 2038 val mk_zero : context -> Sort.sort -> bool -> Expr.expr 2039 2040 (** Create an expression of FloatingPoint sort from three bit-vector expressions. 2041 2042 This is the operator named `fp' in the SMT FP theory definition. 2043 Note that \c sign is required to be a bit-vector of size 1. Significand and exponent 2044 are required to be greater than 1 and 2 respectively. The FloatingPoint sort 2045 of the resulting expression is automatically determined from the bit-vector sizes 2046 of the arguments. *) 2047 val mk_fp : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2048 2049 (** Create a numeral of FloatingPoint sort from a float. 2050 2051 This function is used to create numerals that fit in a float value. 2052 It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. *) 2053 val mk_numeral_f : context -> float -> Sort.sort -> Expr.expr 2054 2055 (** Create a numeral of FloatingPoint sort from a signed integer. *) 2056 val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr 2057 2058 (** Create a numeral of FloatingPoint sort from a sign bit and two integers. *) 2059 val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr 2060 2061 (** Create a numeral of FloatingPoint sort from a string *) 2062 val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr 2063 2064 (** Indicates whether the terms is of floating-point sort. *) 2065 val is_fp : Expr.expr -> bool 2066 2067 2068 (** Indicates whether an expression is a floating-point abs expression *) 2069 val is_abs : Expr.expr -> bool 2070 2071 (** Indicates whether an expression is a floating-point neg expression *) 2072 val is_neg : Expr.expr -> bool 2073 2074 (** Indicates whether an expression is a floating-point add expression *) 2075 val is_add : Expr.expr -> bool 2076 2077 (** Indicates whether an expression is a floating-point sub expression *) 2078 val is_sub : Expr.expr -> bool 2079 2080 (** Indicates whether an expression is a floating-point mul expression *) 2081 val is_mul : Expr.expr -> bool 2082 2083 (** Indicates whether an expression is a floating-point div expression *) 2084 val is_div : Expr.expr -> bool 2085 2086 (** Indicates whether an expression is a floating-point fma expression *) 2087 val is_fma : Expr.expr -> bool 2088 2089 (** Indicates whether an expression is a floating-point sqrt expression *) 2090 val is_sqrt : Expr.expr -> bool 2091 2092 (** Indicates whether an expression is a floating-point rem expression *) 2093 val is_rem : Expr.expr -> bool 2094 2095 (** Indicates whether an expression is a floating-point round_to_integral expression *) 2096 val is_round_to_integral : Expr.expr -> bool 2097 2098 (** Indicates whether an expression is a floating-point min expression *) 2099 val is_min : Expr.expr -> bool 2100 2101 (** Indicates whether an expression is a floating-point max expression *) 2102 val is_max : Expr.expr -> bool 2103 2104 (** Indicates whether an expression is a floating-point leq expression *) 2105 val is_leq : Expr.expr -> bool 2106 2107 (** Indicates whether an expression is a floating-point lt expression *) 2108 val is_lt : Expr.expr -> bool 2109 2110 (** Indicates whether an expression is a floating-point geq expression *) 2111 val is_geq : Expr.expr -> bool 2112 2113 (** Indicates whether an expression is a floating-point gt expression *) 2114 val is_gt : Expr.expr -> bool 2115 2116 (** Indicates whether an expression is a floating-point eq expression *) 2117 val is_eq : Expr.expr -> bool 2118 2119 (** Indicates whether an expression is a floating-point is_normal expression *) 2120 val is_is_normal : Expr.expr -> bool 2121 2122 (** Indicates whether an expression is a floating-point is_subnormal expression *) 2123 val is_is_subnormal : Expr.expr -> bool 2124 2125 (** Indicates whether an expression is a floating-point is_zero expression *) 2126 val is_is_zero : Expr.expr -> bool 2127 2128 (** Indicates whether an expression is a floating-point is_infinite expression *) 2129 val is_is_infinite : Expr.expr -> bool 2130 2131 (** Indicates whether an expression is a floating-point is_nan expression *) 2132 val is_is_nan : Expr.expr -> bool 2133 2134 (** Indicates whether an expression is a floating-point is_negative expression *) 2135 val is_is_negative : Expr.expr -> bool 2136 2137 (** Indicates whether an expression is a floating-point is_positive expression *) 2138 val is_is_positive : Expr.expr -> bool 2139 2140 (** Indicates whether an expression is a floating-point to_fp expression *) 2141 val is_to_fp : Expr.expr -> bool 2142 2143 (** Indicates whether an expression is a floating-point to_fp_unsigned expression *) 2144 val is_to_fp_unsigned : Expr.expr -> bool 2145 2146 (** Indicates whether an expression is a floating-point to_ubv expression *) 2147 val is_to_ubv : Expr.expr -> bool 2148 2149 (** Indicates whether an expression is a floating-point to_sbv expression *) 2150 val is_to_sbv : Expr.expr -> bool 2151 2152 (** Indicates whether an expression is a floating-point to_real expression *) 2153 val is_to_real : Expr.expr -> bool 2154 2155 (** Indicates whether an expression is a floating-point to_ieee_bv expression *) 2156 val is_to_ieee_bv : Expr.expr -> bool 2157 2158 2159 (** Returns a string representation of a numeral. *) 2160 val numeral_to_string : Expr.expr -> string 2161 2162 (** Creates a floating-point constant. *) 2163 val mk_const : context -> Symbol.symbol -> Sort.sort -> Expr.expr 2164 2165 (** Creates a floating-point constant. *) 2166 val mk_const_s : context -> string -> Sort.sort -> Expr.expr 2167 2168 (** Floating-point absolute value *) 2169 val mk_abs : context -> Expr.expr -> Expr.expr 2170 2171 (** Floating-point negation *) 2172 val mk_neg : context -> Expr.expr -> Expr.expr 2173 2174 (** Floating-point addition *) 2175 val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2176 2177 (** Floating-point subtraction *) 2178 val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2179 2180 (** Floating-point multiplication *) 2181 val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2182 2183 (** Floating-point division *) 2184 val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2185 2186 (** Floating-point fused multiply-add. *) 2187 val mk_fma : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2188 2189 (** Floating-point square root *) 2190 val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr 2191 2192 (** Floating-point remainder *) 2193 val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr 2194 2195 (** Floating-point roundToIntegral. 2196 2197 Rounds a floating-point number to the closest integer, 2198 again represented as a floating-point number. *) 2199 val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr 2200 2201 (** Minimum of floating-point numbers. *) 2202 val mk_min : context -> Expr.expr -> Expr.expr -> Expr.expr 2203 2204 (** Maximum of floating-point numbers. *) 2205 val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr 2206 2207 (** Floating-point less than or equal. *) 2208 val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr 2209 2210 (** Floating-point less than. *) 2211 val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr 2212 2213 (** Floating-point greater than or equal. *) 2214 val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr 2215 2216 (** Floating-point greater than. *) 2217 val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr 2218 2219 (** Floating-point equality. *) 2220 val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr 2221 2222 (** Predicate indicating whether t is a normal floating-point number. *) 2223 val mk_is_normal : context -> Expr.expr -> Expr.expr 2224 2225 (** Predicate indicating whether t is a subnormal floating-point number. *) 2226 val mk_is_subnormal : context -> Expr.expr -> Expr.expr 2227 2228 (** Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero. *) 2229 val mk_is_zero : context -> Expr.expr -> Expr.expr 2230 2231 (** Predicate indicating whether t is a floating-point number representing +oo or -oo. *) 2232 val mk_is_infinite : context -> Expr.expr -> Expr.expr 2233 2234 (** Predicate indicating whether t is a NaN. *) 2235 val mk_is_nan : context -> Expr.expr -> Expr.expr 2236 2237 (** Predicate indicating whether t is a negative floating-point number. *) 2238 val mk_is_negative : context -> Expr.expr -> Expr.expr 2239 2240 (** Predicate indicating whether t is a positive floating-point number. *) 2241 val mk_is_positive : context -> Expr.expr -> Expr.expr 2242 2243 (** Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. *) 2244 val mk_to_fp_bv : context -> Expr.expr -> Sort.sort -> Expr.expr 2245 2246 (** Conversion of a FloatingPoint term into another term of different FloatingPoint sort. *) 2247 val mk_to_fp_float : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2248 2249 (** Conversion of a term of real sort into a term of FloatingPoint sort. *) 2250 val mk_to_fp_real : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2251 2252 (** Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. *) 2253 val mk_to_fp_signed : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2254 2255 (** Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. *) 2256 val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2257 2258 (** Conversion of a floating-point term into an unsigned bit-vector. *) 2259 val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr 2260 2261 (** Conversion of a floating-point term into a signed bit-vector. *) 2262 val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr 2263 2264 (** Conversion of a floating-point term into a real-numbered term. *) 2265 val mk_to_real : context -> Expr.expr -> Expr.expr 2266 2267 (** Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. *) 2268 val get_ebits : context -> Sort.sort -> int 2269 2270 (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *) 2271 val get_sbits : context -> Sort.sort -> int 2272 2273 (** Retrieves the sign of a floating-point literal. *) 2274 val get_numeral_sign : context -> Expr.expr -> bool * int 2275 2276 (** Return the sign of a floating-point numeral as a bit-vector expression. 2277 Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. *) 2278 val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr 2279 2280 (** Return the exponent value of a floating-point numeral as a string *) 2281 val get_numeral_exponent_string : context -> Expr.expr -> bool -> string 2282 2283 (** Return the exponent value of a floating-point numeral as a signed integer *) 2284 val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int 2285 2286 (** Return the exponent of a floating-point numeral as a bit-vector expression. 2287 Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *) 2288 val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr 2289 2290 (** Return the significand value of a floating-point numeral as a bit-vector expression. 2291 Remark: NaN's do not have a bit-vector significand, so they are invalid arguments. *) 2292 val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr 2293 2294 (** Return the significand value of a floating-point numeral as a string. *) 2295 val get_numeral_significand_string : context -> Expr.expr -> string 2296 2297 (** Return the significand value of a floating-point numeral as a uint64. 2298 Remark: This function extracts the significand bits, without the 2299 hidden bit or normalization. Throws an exception if the 2300 significand does not fit into an int. *) 2301 val get_numeral_significand_uint : context -> Expr.expr -> bool * int 2302 2303 (** Indicates whether a floating-point numeral is a NaN. *) 2304 val is_numeral_nan : context -> Expr.expr -> bool 2305 2306 (** Indicates whether a floating-point numeral is +oo or -oo. *) 2307 val is_numeral_inf : context -> Expr.expr -> bool 2308 2309 (** Indicates whether a floating-point numeral is +zero or -zero. *) 2310 val is_numeral_zero : context -> Expr.expr -> bool 2311 2312 (** Indicates whether a floating-point numeral is normal. *) 2313 val is_numeral_normal : context -> Expr.expr -> bool 2314 2315 (** Indicates whether a floating-point numeral is subnormal. *) 2316 val is_numeral_subnormal : context -> Expr.expr -> bool 2317 2318 (** Indicates whether a floating-point numeral is positive. *) 2319 val is_numeral_positive : context -> Expr.expr -> bool 2320 2321 (** Indicates whether a floating-point numeral is negative. *) 2322 val is_numeral_negative : context -> Expr.expr -> bool 2323 2324 (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) 2325 val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr 2326 2327 (** Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. *) 2328 val mk_to_fp_int_real : context -> Expr.expr -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2329 2330 (** The string representation of a numeral *) 2331 val numeral_to_string : Expr.expr -> string 2332end 2333 2334 2335(** Functions to manipulate proof expressions *) 2336module Proof : 2337sig 2338 (** Indicates whether the term is a Proof for the expression 'true'. *) 2339 val is_true : Expr.expr -> bool 2340 2341 (** Indicates whether the term is a proof for a fact asserted by the user. *) 2342 val is_asserted : Expr.expr -> bool 2343 2344 (** Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. *) 2345 val is_goal : Expr.expr -> bool 2346 2347 (** Indicates whether the term is a binary equivalence modulo namings. 2348 This binary predicate is used in proof terms. 2349 It captures equisatisfiability and equivalence modulo renamings. *) 2350 val is_oeq : Expr.expr -> bool 2351 2352 (** Indicates whether the term is proof via modus ponens 2353 2354 Given a proof for p and a proof for (implies p q), produces a proof for q. 2355 T1: p 2356 T2: (implies p q) 2357 [mp T1 T2]: q 2358 The second antecedents may also be a proof for (iff p q). *) 2359 val is_modus_ponens : Expr.expr -> bool 2360 2361 (** Indicates whether the term is a proof for (R t t), where R is a reflexive relation. 2362 This proof object has no antecedents. 2363 The only reflexive relations that are used are 2364 equivalence modulo namings, equality and equivalence. 2365 That is, R is either '~', '=' or 'iff'. *) 2366 val is_reflexivity : Expr.expr -> bool 2367 2368 (** Indicates whether the term is proof by symmetricity of a relation 2369 2370 Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). 2371 T1: (R t s) 2372 [symmetry T1]: (R s t) 2373 T1 is the antecedent of this proof object. *) 2374 val is_symmetry : Expr.expr -> bool 2375 2376 (** Indicates whether the term is a proof by transitivity of a relation 2377 2378 Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof 2379 for (R t u). 2380 T1: (R t s) 2381 T2: (R s u) 2382 [trans T1 T2]: (R t u) *) 2383 val is_transitivity : Expr.expr -> bool 2384 2385 (** Indicates whether the term is a proof by condensed transitivity of a relation 2386 2387 Condensed transitivity proof. 2388 It combines several symmetry and transitivity proofs. 2389 Example: 2390 T1: (R a b) 2391 T2: (R c b) 2392 T3: (R c d) 2393 [trans* T1 T2 T3]: (R a d) 2394 R must be a symmetric and transitive relation. 2395 2396 Assuming that this proof object is a proof for (R s t), then 2397 a proof checker must check if it is possible to prove (R s t) 2398 using the antecedents, symmetry and transitivity. That is, 2399 if there is a path from s to t, if we view every 2400 antecedent (R a b) as an edge between a and b. *) 2401 val is_Transitivity_star : Expr.expr -> bool 2402 2403 (** Indicates whether the term is a monotonicity proof object. 2404 2405 T1: (R t_1 s_1) 2406 ... 2407 Tn: (R t_n s_n) 2408 [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) 2409 Remark: if t_i == s_i, then the antecedent Ti is suppressed. 2410 That is, reflexivity proofs are suppressed to save space. *) 2411 val is_monotonicity : Expr.expr -> bool 2412 2413 (** Indicates whether the term is a quant-intro proof 2414 2415 Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). 2416 T1: (~ p q) 2417 [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) *) 2418 val is_quant_intro : Expr.expr -> bool 2419 2420 (** Indicates whether the term is a distributivity proof object. 2421 2422 Given that f (= or) distributes over g (= and), produces a proof for 2423 (= (f a (g c d)) 2424 (g (f a c) (f a d))) 2425 If f and g are associative, this proof also justifies the following equality: 2426 (= (f (g a b) (g c d)) 2427 (g (f a c) (f a d) (f b c) (f b d))) 2428 where each f and g can have arbitrary number of arguments. 2429 2430 This proof object has no antecedents. 2431 Remark. This rule is used by the CNF conversion pass and 2432 instantiated by f = or, and g = and. *) 2433 val is_distributivity : Expr.expr -> bool 2434 2435 (** Indicates whether the term is a proof by elimination of AND 2436 2437 Given a proof for (and l_1 ... l_n), produces a proof for l_i 2438 T1: (and l_1 ... l_n) 2439 [and-elim T1]: l_i *) 2440 val is_and_elimination : Expr.expr -> bool 2441 2442 (** Indicates whether the term is a proof by elimination of not-or 2443 2444 Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). 2445 T1: (not (or l_1 ... l_n)) 2446 [not-or-elim T1]: (not l_i) *) 2447 val is_or_elimination : Expr.expr -> bool 2448 2449 (** Indicates whether the term is a proof by rewriting 2450 2451 A proof for a local rewriting step (= t s). 2452 The head function symbol of t is interpreted. 2453 2454 This proof object has no antecedents. 2455 The conclusion of a rewrite rule is either an equality (= t s), 2456 an equivalence (iff t s), or equi-satisfiability (~ t s). 2457 Remark: if f is bool, then = is iff. 2458 2459 Examples: 2460 (= (+ ( x : expr ) 0) x) 2461 (= (+ ( x : expr ) 1 2) (+ 3 x)) 2462 (iff (or ( x : expr ) false) x) *) 2463 val is_rewrite : Expr.expr -> bool 2464 2465 (** Indicates whether the term is a proof by rewriting 2466 2467 A proof for rewriting an expression t into an expression s. 2468 This proof object can have n antecedents. 2469 The antecedents are proofs for equalities used as substitution rules. 2470 The object is also used in a few cases. The cases are: 2471 - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) 2472 - When converting bit-vectors to Booleans (BIT2BOOL=true) *) 2473 val is_rewrite_star : Expr.expr -> bool 2474 2475 (** Indicates whether the term is a proof for pulling quantifiers out. 2476 2477 A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *) 2478 val is_pull_quant : Expr.expr -> bool 2479 2480 (** Indicates whether the term is a proof for pushing quantifiers in. 2481 2482 A proof for: 2483 (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) 2484 (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) 2485 ... 2486 (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) 2487 This proof object has no antecedents *) 2488 val is_push_quant : Expr.expr -> bool 2489 2490 (** Indicates whether the term is a proof for elimination of unused variables. 2491 2492 A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) 2493 (forall (x_1 ... x_n) p[x_1 ... x_n])) 2494 2495 It is used to justify the elimination of unused variables. 2496 This proof object has no antecedents. *) 2497 val is_elim_unused_vars : Expr.expr -> bool 2498 2499 (** Indicates whether the term is a proof for destructive equality resolution 2500 2501 A proof for destructive equality resolution: 2502 (iff (forall (x) (or (not (= ( x : expr ) t)) P[x])) P[t]) 2503 if ( x : expr ) does not occur in t. 2504 2505 This proof object has no antecedents. 2506 2507 Several variables can be eliminated simultaneously. *) 2508 val is_der : Expr.expr -> bool 2509 2510 (** Indicates whether the term is a proof for quantifier instantiation 2511 2512 A proof of (or (not (forall (x) (P x))) (P a)) *) 2513 val is_quant_inst : Expr.expr -> bool 2514 2515 (** Indicates whether the term is a hypothesis marker. 2516 Mark a hypothesis in a natural deduction style proof. *) 2517 val is_hypothesis : Expr.expr -> bool 2518 2519 (** Indicates whether the term is a proof by lemma 2520 2521 T1: false 2522 [lemma T1]: (or (not l_1) ... (not l_n)) 2523 2524 This proof object has one antecedent: a hypothetical proof for false. 2525 It converts the proof in a proof for (or (not l_1) ... (not l_n)), 2526 when T1 contains the hypotheses: l_1, ..., l_n. *) 2527 val is_lemma : Expr.expr -> bool 2528 2529 (** Indicates whether the term is a proof by unit resolution 2530 2531 T1: (or l_1 ... l_n l_1' ... l_m') 2532 T2: (not l_1) 2533 ... 2534 T(n+1): (not l_n) 2535 [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') *) 2536 val is_unit_resolution : Expr.expr -> bool 2537 2538 (** Indicates whether the term is a proof by iff-true 2539 2540 T1: p 2541 [iff-true T1]: (iff p true) *) 2542 val is_iff_true : Expr.expr -> bool 2543 2544 (** Indicates whether the term is a proof by iff-false 2545 2546 T1: (not p) 2547 [iff-false T1]: (iff p false) *) 2548 val is_iff_false : Expr.expr -> bool 2549 2550 (** Indicates whether the term is a proof by commutativity 2551 2552 [comm]: (= (f a b) (f b a)) 2553 2554 f is a commutative operator. 2555 2556 This proof object has no antecedents. 2557 Remark: if f is bool, then = is iff. *) 2558 val is_commutativity : Expr.expr -> bool 2559 2560 (** Indicates whether the term is a proof for Tseitin-like axioms 2561 2562 Proof object used to justify Tseitin's like axioms: 2563 2564 (or (not (and p q)) p) 2565 (or (not (and p q)) q) 2566 (or (not (and p q r)) p) 2567 (or (not (and p q r)) q) 2568 (or (not (and p q r)) r) 2569 ... 2570 (or (and p q) (not p) (not q)) 2571 (or (not (or p q)) p q) 2572 (or (or p q) (not p)) 2573 (or (or p q) (not q)) 2574 (or (not (iff p q)) (not p) q) 2575 (or (not (iff p q)) p (not q)) 2576 (or (iff p q) (not p) (not q)) 2577 (or (iff p q) p q) 2578 (or (not (ite a b c)) (not a) b) 2579 (or (not (ite a b c)) a c) 2580 (or (ite a b c) (not a) (not b)) 2581 (or (ite a b c) a (not c)) 2582 (or (not (not a)) (not a)) 2583 (or (not a) a) 2584 2585 This proof object has no antecedents. 2586 Note: all axioms are propositional tautologies. 2587 Note also that 'and' and 'or' can take multiple arguments. 2588 You can recover the propositional tautologies by 2589 unfolding the Boolean connectives in the axioms a small 2590 bounded number of steps (=3). *) 2591 val is_def_axiom : Expr.expr -> bool 2592 2593 (** Indicates whether the term is a proof for introduction of a name 2594 2595 Introduces a name for a formula/term. 2596 Suppose e is an expression with free variables x, and def-intro 2597 introduces the name n(x). The possible cases are: 2598 2599 When e is of Boolean type: 2600 [def-intro]: (and (or n (not e)) (or (not n) e)) 2601 2602 or: 2603 [def-intro]: (or (not n) e) 2604 when e only occurs positively. 2605 2606 When e is of the form (ite cond th el): 2607 [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el))) 2608 2609 Otherwise: 2610 [def-intro]: (= n e) *) 2611 val is_def_intro : Expr.expr -> bool 2612 2613 (** Indicates whether the term is a proof for application of a definition 2614 2615 [apply-def T1]: F ~ n 2616 F is 'equivalent' to n, given that T1 is a proof that 2617 n is a name for F. *) 2618 val is_apply_def : Expr.expr -> bool 2619 2620 (** Indicates whether the term is a proof iff-oeq 2621 2622 T1: (iff p q) 2623 [iff~ T1]: (~ p q) *) 2624 val is_iff_oeq : Expr.expr -> bool 2625 2626 (** Indicates whether the term is a proof for a positive NNF step 2627 2628 Proof for a (positive) NNF step. Example: 2629 2630 T1: (not s_1) ~ r_1 2631 T2: (not s_2) ~ r_2 2632 T3: s_1 ~ r_1' 2633 T4: s_2 ~ r_2' 2634 [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) 2635 (and (or r_1 r_2') (or r_1' r_2))) 2636 2637 The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: 2638 (a) When creating the NNF of a positive force quantifier. 2639 The quantifier is retained (unless the bound variables are eliminated). 2640 Example 2641 T1: q ~ q_new 2642 [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new)) 2643 2644 (b) When recursively creating NNF over Boolean formulas, where the top-level 2645 connective is changed during NNF conversion. The relevant Boolean connectives 2646 for NNF_POS are 'implies', 'iff', 'xor', 'ite'. 2647 NNF_NEG furthermore handles the case where negation is pushed 2648 over Boolean connectives 'and' and 'or'. *) 2649 val is_nnf_pos : Expr.expr -> bool 2650 2651 (** Indicates whether the term is a proof for a negative NNF step 2652 2653 Proof for a (negative) NNF step. Examples: 2654 2655 T1: (not s_1) ~ r_1 2656 ... 2657 Tn: (not s_n) ~ r_n 2658 [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) 2659 and 2660 T1: (not s_1) ~ r_1 2661 ... 2662 Tn: (not s_n) ~ r_n 2663 [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) 2664 and 2665 T1: (not s_1) ~ r_1 2666 T2: (not s_2) ~ r_2 2667 T3: s_1 ~ r_1' 2668 T4: s_2 ~ r_2' 2669 [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) 2670 (and (or r_1 r_2) (or r_1' r_2'))) *) 2671 val is_nnf_neg : Expr.expr -> bool 2672 2673 (** Indicates whether the term is a proof for a Skolemization step 2674 2675 Proof for: 2676 2677 [sk]: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y))) 2678 [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y)) 2679 2680 This proof object has no antecedents. *) 2681 val is_skolemize : Expr.expr -> bool 2682 2683 (** Indicates whether the term is a proof by modus ponens for equi-satisfiability. 2684 2685 Modus ponens style rule for equi-satisfiability. 2686 T1: p 2687 T2: (~ p q) 2688 [mp~ T1 T2]: q *) 2689 val is_modus_ponens_oeq : Expr.expr -> bool 2690 2691 (** Indicates whether the term is a proof for theory lemma 2692 2693 Generic proof for theory lemmas. 2694 2695 The theory lemma function comes with one or more parameters. 2696 The first parameter indicates the name of the theory. 2697 For the theory of arithmetic, additional parameters provide hints for 2698 checking the theory lemma. 2699 The hints for arithmetic are: 2700 - farkas - followed by rational coefficients. Multiply the coefficients to the 2701 inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. 2702 - triangle-eq - Indicates a lemma related to the equivalence: 2703 (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) 2704 - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. *) 2705 val is_theory_lemma : Expr.expr -> bool 2706end 2707 2708(** Goals 2709 2710 A goal (aka problem). A goal is essentially a 2711 of formulas, that can be solved and/or transformed using 2712 tactics and solvers. *) 2713module Goal : 2714sig 2715 type goal 2716 2717 (** The precision of the goal. 2718 2719 Goals can be transformed using over and under approximations. 2720 An under approximation is applied when the objective is to find a model for a given goal. 2721 An over approximation is applied when the objective is to find a proof for a given goal. *) 2722 val get_precision : goal -> Z3enums.goal_prec 2723 2724 (** Indicates whether the goal is precise. *) 2725 val is_precise : goal -> bool 2726 2727 (** Indicates whether the goal is an under-approximation. *) 2728 val is_underapproximation : goal -> bool 2729 2730 (** Indicates whether the goal is an over-approximation. *) 2731 val is_overapproximation : goal -> bool 2732 2733 (** Indicates whether the goal is garbage (i.e., the product of over- and under-approximations). *) 2734 val is_garbage : goal -> bool 2735 2736 (** Adds the constraints to the given goal. *) 2737 val add : goal -> Expr.expr list -> unit 2738 2739 (** Indicates whether the goal contains `false'. *) 2740 val is_inconsistent : goal -> bool 2741 2742 (** The depth of the goal. 2743 This tracks how many transformations were applied to it. *) 2744 val get_depth : goal -> int 2745 2746 (** Erases all formulas from the given goal. *) 2747 val reset : goal -> unit 2748 2749 (** The number of formulas in the goal. *) 2750 val get_size : goal -> int 2751 2752 (** The formulas in the goal. *) 2753 val get_formulas : goal -> Expr.expr list 2754 2755 (** The number of formulas, subformulas and terms in the goal. *) 2756 val get_num_exprs : goal -> int 2757 2758 (** Indicates whether the goal is empty, and it is precise or the product of an under approximation. *) 2759 val is_decided_sat : goal -> bool 2760 2761 (** Indicates whether the goal contains `false', and it is precise or the product of an over approximation. *) 2762 val is_decided_unsat : goal -> bool 2763 2764 (** Translates (copies) the Goal to another context.. *) 2765 val translate : goal -> context -> goal 2766 2767 (** Simplifies the goal. Essentially invokes the `simplify' tactic on the goal. *) 2768 val simplify : goal -> Params.params option -> goal 2769 2770 (** Creates a new Goal. 2771 2772 Note that the Context must have been created with proof generation support if 2773 the fourth argument is set to true here. *) 2774 val mk_goal : context -> bool -> bool -> bool -> goal 2775 2776 (** A string representation of the Goal. *) 2777 val to_string : goal -> string 2778 2779 (** Goal to BoolExpr conversion. *) 2780 val as_expr : goal -> Expr.expr 2781end 2782 2783(** Models 2784 2785 A Model contains interpretations (assignments) of constants and functions. *) 2786module Model : 2787sig 2788 type model 2789 2790 (** Function interpretations 2791 2792 A function interpretation is represented as a finite map and an 'else'. 2793 Each entry in the finite map represents the value of a function given a set of arguments. *) 2794 module FuncInterp : 2795 sig 2796 type func_interp 2797 2798 (** Function interpretations entries 2799 2800 An Entry object represents an element in the finite map used to a function interpretation. *) 2801 module FuncEntry : 2802 sig 2803 type func_entry 2804 2805 (** Return the (symbolic) value of this entry. 2806 *) 2807 val get_value : func_entry -> Expr.expr 2808 2809 (** The number of arguments of the entry. 2810 *) 2811 val get_num_args : func_entry -> int 2812 2813 (** The arguments of the function entry. 2814 *) 2815 val get_args : func_entry -> Expr.expr list 2816 2817 (** A string representation of the function entry. 2818 *) 2819 val to_string : func_entry -> string 2820 end 2821 2822 (** The number of entries in the function interpretation. *) 2823 val get_num_entries : func_interp -> int 2824 2825 (** The entries in the function interpretation *) 2826 val get_entries : func_interp -> FuncEntry.func_entry list 2827 2828 (** The (symbolic) `else' value of the function interpretation. *) 2829 val get_else : func_interp -> Expr.expr 2830 2831 (** The arity of the function interpretation *) 2832 val get_arity : func_interp -> int 2833 2834 (** A string representation of the function interpretation. *) 2835 val to_string : func_interp -> string 2836 end 2837 2838 (** Retrieves the interpretation (the assignment) of a func_decl in the model. 2839 @return An expression if the function has an interpretation in the model, null otherwise. *) 2840 val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option 2841 2842 (** Retrieves the interpretation (the assignment) of an expression in the model. 2843 @return An expression if the constant has an interpretation in the model, null otherwise. *) 2844 val get_const_interp_e : model -> Expr.expr -> Expr.expr option 2845 2846 (** Retrieves the interpretation (the assignment) of a non-constant func_decl in the model. 2847 @return A FunctionInterpretation if the function has an interpretation in the model, null otherwise. *) 2848 val get_func_interp : model -> FuncDecl.func_decl -> FuncInterp.func_interp option 2849 2850 (** The number of constant interpretations in the model. *) 2851 val get_num_consts : model -> int 2852 2853 (** The function declarations of the constants in the model. *) 2854 val get_const_decls : model -> FuncDecl.func_decl list 2855 2856 (** The number of function interpretations in the model. *) 2857 val get_num_funcs : model -> int 2858 2859 (** The function declarations of the function interpretations in the model. *) 2860 val get_func_decls : model -> FuncDecl.func_decl list 2861 2862 (** All symbols that have an interpretation in the model. *) 2863 val get_decls : model -> FuncDecl.func_decl list 2864 2865 (** Evaluates an expression in the current model. 2866 The Boolean argument indicates whether to apply model completion. 2867 When model completion is true it will assign an interpretation for 2868 constants and functions that do not have an interpretation in the model. 2869 2870 This function may fail if the argument contains quantifiers, 2871 is partial (MODEL_PARTIAL enabled), or if it is not well-sorted. 2872 In this case a [ModelEvaluationFailedException] is thrown. 2873 *) 2874 val eval : model -> Expr.expr -> bool -> Expr.expr option 2875 2876 (** Alias for [eval]. *) 2877 val evaluate : model -> Expr.expr -> bool -> Expr.expr option 2878 2879 (** The number of uninterpreted sorts that the model has an interpretation for. *) 2880 val get_num_sorts : model -> int 2881 2882 (** The uninterpreted sorts that the model has an interpretation for. 2883 2884 Z3 also provides an interpretation for uninterpreted sorts used in a formula. 2885 The interpretation for a sort is a finite set of distinct values. We say this finite set is 2886 the "universe" of the sort. 2887 {!get_num_sorts} 2888 {!sort_universe} *) 2889 val get_sorts : model -> Sort.sort list 2890 2891 (** The finite set of distinct values that represent the interpretation of a sort. 2892 {!get_sorts} 2893 @return A list of expressions, where each is an element of the universe of the sort *) 2894 val sort_universe : model -> Sort.sort -> Expr.expr list 2895 2896 (** Conversion of models to strings. 2897 @return A string representation of the model. *) 2898 val to_string : model -> string 2899end 2900 2901(** Probes 2902 2903 Probes are used to inspect a goal (aka problem) and collect information that may be used to decide 2904 which solver and/or preprocessing step will be used. 2905 The complete list of probes may be obtained using the procedures [Context.NumProbes] 2906 and [Context.ProbeNames]. 2907 It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. 2908*) 2909module Probe : 2910sig 2911 type probe 2912 2913 (** Execute the probe over the goal. 2914 @return A probe always produce a float value. 2915 "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. *) 2916 val apply : probe -> Goal.goal -> float 2917 2918 (** The number of supported Probes. *) 2919 val get_num_probes : context -> int 2920 2921 (** The names of all supported Probes. *) 2922 val get_probe_names : context -> string list 2923 2924 (** Returns a string containing a description of the probe with the given name. *) 2925 val get_probe_description : context -> string -> string 2926 2927 (** Creates a new Probe. *) 2928 val mk_probe : context -> string -> probe 2929 2930 (** Create a probe that always evaluates to a float value. *) 2931 val const : context -> float -> probe 2932 2933 (** Create a probe that evaluates to "true" when the value returned by the first argument 2934 is less than the value returned by second argument *) 2935 val lt : context -> probe -> probe -> probe 2936 2937 (** Create a probe that evaluates to "true" when the value returned by the first argument 2938 is greater than the value returned by second argument *) 2939 val gt : context -> probe -> probe -> probe 2940 2941 (** Create a probe that evaluates to "true" when the value returned by the first argument 2942 is less than or equal the value returned by second argument *) 2943 val le : context -> probe -> probe -> probe 2944 2945 (** Create a probe that evaluates to "true" when the value returned by the first argument 2946 is greater than or equal the value returned by second argument *) 2947 val ge : context -> probe -> probe -> probe 2948 2949 2950 (** Create a probe that evaluates to "true" when the value returned by the first argument 2951 is equal the value returned by second argument *) 2952 val eq : context -> probe -> probe -> probe 2953 2954 (** Create a probe that evaluates to "true" when both of two probes evaluate to "true". *) 2955 val and_ : context -> probe -> probe -> probe 2956 2957 (** Create a probe that evaluates to "true" when either of two probes evaluates to "true". *) 2958 val or_ : context -> probe -> probe -> probe 2959 2960 (** Create a probe that evaluates to "true" when another probe does not evaluate to "true". *) 2961 val not_ : context -> probe -> probe 2962end 2963 2964(** Tactics 2965 2966 Tactics are the basic building block for creating custom solvers for specific problem domains. 2967 The complete list of tactics may be obtained using [Context.get_num_tactics] 2968 and [Context.get_tactic_names]. 2969 It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. 2970*) 2971module Tactic : 2972sig 2973 type tactic 2974 2975 (** Tactic application results 2976 2977 ApplyResult objects represent the result of an application of a 2978 tactic to a goal. It contains the subgoals that were produced. *) 2979 module ApplyResult : 2980 sig 2981 type apply_result 2982 2983 (** The number of Subgoals. *) 2984 val get_num_subgoals : apply_result -> int 2985 2986 (** Retrieves the subgoals from the apply_result. *) 2987 val get_subgoals : apply_result -> Goal.goal list 2988 2989 (** Retrieves a subgoal from the apply_result. *) 2990 val get_subgoal : apply_result -> int -> Goal.goal 2991 2992 (** A string representation of the ApplyResult. *) 2993 val to_string : apply_result -> string 2994 end 2995 2996 (** A string containing a description of parameters accepted by the tactic. *) 2997 val get_help : tactic -> string 2998 2999 (** Retrieves parameter descriptions for Tactics. *) 3000 val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs 3001 3002 (** Apply the tactic to the goal. *) 3003 val apply : tactic -> Goal.goal -> Params.params option -> ApplyResult.apply_result 3004 3005 (** The number of supported tactics. *) 3006 val get_num_tactics : context -> int 3007 3008 (** The names of all supported tactics. *) 3009 val get_tactic_names : context -> string list 3010 3011 (** Returns a string containing a description of the tactic with the given name. *) 3012 val get_tactic_description : context -> string -> string 3013 3014 (** Creates a new Tactic. *) 3015 val mk_tactic : context -> string -> tactic 3016 3017 (** Create a tactic that applies one tactic to a Goal and 3018 then another one to every subgoal produced by the first one. *) 3019 val and_then : context -> tactic -> tactic -> tactic list -> tactic 3020 3021 (** Create a tactic that first applies one tactic to a Goal and 3022 if it fails then returns the result of another tactic applied to the Goal. *) 3023 val or_else : context -> tactic -> tactic -> tactic 3024 3025 (** Create a tactic that applies one tactic to a goal for some time (in milliseconds). 3026 3027 If the tactic does not terminate within the timeout, then it fails. *) 3028 val try_for : context -> tactic -> int -> tactic 3029 3030 (** Create a tactic that applies one tactic to a given goal if the probe 3031 evaluates to true. 3032 3033 If the probe evaluates to false, then the new tactic behaves like the [skip] tactic. *) 3034 val when_ : context -> Probe.probe -> tactic -> tactic 3035 3036 (** Create a tactic that applies a tactic to a given goal if the probe 3037 evaluates to true and another tactic otherwise. *) 3038 val cond : context -> Probe.probe -> tactic -> tactic -> tactic 3039 3040 (** Create a tactic that keeps applying one tactic until the goal is not 3041 modified anymore or the maximum number of iterations is reached. *) 3042 val repeat : context -> tactic -> int -> tactic 3043 3044 (** Create a tactic that just returns the given goal. *) 3045 val skip : context -> tactic 3046 3047 (** Create a tactic always fails. *) 3048 val fail : context -> tactic 3049 3050 (** Create a tactic that fails if the probe evaluates to false. *) 3051 val fail_if : context -> Probe.probe -> tactic 3052 3053 (** Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) 3054 or trivially unsatisfiable (i.e., contains `false'). *) 3055 val fail_if_not_decided : context -> tactic 3056 3057 (** Create a tactic that applies a tactic using the given set of parameters. *) 3058 val using_params : context -> tactic -> Params.params -> tactic 3059 3060 (** Create a tactic that applies a tactic using the given set of parameters. 3061 Alias for [UsingParams]*) 3062 val with_ : context -> tactic -> Params.params -> tactic 3063 3064 (** Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). *) 3065 val par_or : context -> tactic list -> tactic 3066 3067 (** Create a tactic that applies a tactic to a given goal and then another tactic 3068 to every subgoal produced by the first one. The subgoals are processed in parallel. *) 3069 val par_and_then : context -> tactic -> tactic -> tactic 3070 3071 (** Interrupt the execution of a Z3 procedure. 3072 This procedure can be used to interrupt: solvers, simplifiers and tactics. *) 3073 val interrupt : context -> unit 3074end 3075 3076(** Objects that track statistical information. *) 3077module Statistics : 3078sig 3079 type statistics 3080 3081 (** Statistical data is organized into pairs of \[Key, Entry\], where every 3082 Entry is either a floating point or integer value. *) 3083 module Entry : 3084 sig 3085 type statistics_entry 3086 3087 (** The key of the entry. *) 3088 val get_key : statistics_entry -> string 3089 3090 (** The int-value of the entry. *) 3091 val get_int : statistics_entry -> int 3092 3093 (** The float-value of the entry. *) 3094 val get_float : statistics_entry -> float 3095 3096 (** True if the entry is uint-valued. *) 3097 val is_int : statistics_entry -> bool 3098 3099 (** True if the entry is float-valued. *) 3100 val is_float : statistics_entry -> bool 3101 3102 (** The string representation of the entry's value. *) 3103 val to_string_value : statistics_entry -> string 3104 3105 (** The string representation of the entry (key and value) *) 3106 val to_string : statistics_entry -> string 3107 end 3108 3109 (** A string representation of the statistical data. *) 3110 val to_string : statistics -> string 3111 3112 (** The number of statistical data. *) 3113 val get_size : statistics -> int 3114 3115 (** The data entries. *) 3116 val get_entries : statistics -> Entry.statistics_entry list 3117 3118 (** The statistical counters. *) 3119 val get_keys : statistics -> string list 3120 3121 (** The value of a particular statistical counter. *) 3122 val get : statistics -> string -> Entry.statistics_entry option 3123end 3124 3125(** Solvers *) 3126module Solver : 3127sig 3128 type solver 3129 type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE 3130 3131 val string_of_status : status -> string 3132 3133 (** A string that describes all available solver parameters. *) 3134 val get_help : solver -> string 3135 3136 (** Sets the solver parameters. *) 3137 val set_parameters : solver -> Params.params -> unit 3138 3139 (** Retrieves parameter descriptions for solver. *) 3140 val get_param_descrs : solver -> Params.ParamDescrs.param_descrs 3141 3142 (** The current number of backtracking points (scopes). 3143 {!pop} 3144 {!push} *) 3145 val get_num_scopes : solver -> int 3146 3147 (** Creates a backtracking point. 3148 {!pop} *) 3149 val push : solver -> unit 3150 3151 (** Backtracks a number of backtracking points. 3152 Note that an exception is thrown if the integer is not smaller than {!get_num_scopes} 3153 {!push} *) 3154 val pop : solver -> int -> unit 3155 3156 (** Resets the Solver. 3157 This removes all assertions from the solver. *) 3158 val reset : solver -> unit 3159 3160 (** Assert a constraint (or multiple) into the solver. *) 3161 val add : solver -> Expr.expr list -> unit 3162 3163 (** Assert multiple constraints (cs) into the solver, and track them (in the 3164 unsat) core using the Boolean constants in ps. 3165 3166 This API is an alternative to {!check} with assumptions for extracting unsat cores. 3167 Both APIs can be used in the same solver. The unsat core will contain a combination 3168 of the Boolean variables provided using {!assert_and_track} and the Boolean literals 3169 provided using {!check} with assumptions. *) 3170 val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit 3171 3172 (** Assert a constraint (c) into the solver, and track it (in the unsat) core 3173 using the Boolean constant p. 3174 3175 This API is an alternative to {!check} with assumptions for extracting unsat cores. 3176 Both APIs can be used in the same solver. The unsat core will contain a combination 3177 of the Boolean variables provided using {!assert_and_track} and the Boolean literals 3178 provided using {!check} with assumptions. *) 3179 val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit 3180 3181 (** The number of assertions in the solver. *) 3182 val get_num_assertions : solver -> int 3183 3184 (** The set of asserted formulas. *) 3185 val get_assertions : solver -> Expr.expr list 3186 3187 (** Checks whether the assertions in the solver are consistent or not. 3188 3189 {!Model} 3190 {!get_unsat_core} 3191 {!Proof} *) 3192 val check : solver -> Expr.expr list -> status 3193 3194 (** The model of the last [Check]. 3195 3196 The result is [None] if [Check] was not invoked before, 3197 if its results was not [SATISFIABLE], or if model production is not enabled. *) 3198 val get_model : solver -> Model.model option 3199 3200 (** The proof of the last [Check]. 3201 3202 The result is [null] if [Check] was not invoked before, 3203 if its results was not [UNSATISFIABLE], or if proof production is disabled. *) 3204 val get_proof : solver -> Expr.expr option 3205 3206 (** The unsat core of the last [Check]. 3207 3208 The unsat core is a subset of [Assertions] 3209 The result is empty if [Check] was not invoked before, 3210 if its results was not [UNSATISFIABLE], or if core production is disabled. *) 3211 val get_unsat_core : solver -> Expr.expr list 3212 3213 (** A brief justification of why the last call to [Check] returned [UNKNOWN]. *) 3214 val get_reason_unknown : solver -> string 3215 3216 (** Solver statistics. *) 3217 val get_statistics : solver -> Statistics.statistics 3218 3219 (** Creates a new (incremental) solver. 3220 3221 This solver also uses a set of builtin tactics for handling the first 3222 check-sat command, and check-sat commands that take more than a given 3223 number of milliseconds to be solved. *) 3224 val mk_solver : context -> Symbol.symbol option -> solver 3225 3226 (** Creates a new (incremental) solver. 3227 {!mk_solver} *) 3228 val mk_solver_s : context -> string -> solver 3229 3230 (** Creates a new (incremental) solver. *) 3231 val mk_simple_solver : context -> solver 3232 3233 (** Creates a solver that is implemented using the given tactic. 3234 3235 The solver supports the commands [Push] and [Pop], but it 3236 will always solve each check from scratch. *) 3237 val mk_solver_t : context -> Tactic.tactic -> solver 3238 3239 (** Create a clone of the current solver with respect to a context. *) 3240 val translate : solver -> context -> solver 3241 3242 (** A string representation of the solver. *) 3243 val to_string : solver -> string 3244end 3245 3246(** Fixedpoint solving *) 3247module Fixedpoint : 3248sig 3249 type fixedpoint 3250 3251 (** A string that describes all available fixedpoint solver parameters. *) 3252 val get_help : fixedpoint -> string 3253 3254 (** Sets the fixedpoint solver parameters. *) 3255 val set_parameters : fixedpoint -> Params.params -> unit 3256 3257 (** Retrieves parameter descriptions for Fixedpoint solver. *) 3258 val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs 3259 3260 (** Assert a constraints into the fixedpoint solver. *) 3261 val add : fixedpoint -> Expr.expr list -> unit 3262 3263 (** Register predicate as recursive relation. *) 3264 val register_relation : fixedpoint -> FuncDecl.func_decl -> unit 3265 3266 (** Add rule into the fixedpoint solver. *) 3267 val add_rule : fixedpoint -> Expr.expr -> Symbol.symbol option -> unit 3268 3269 (** Add table fact to the fixedpoint solver. *) 3270 val add_fact : fixedpoint -> FuncDecl.func_decl -> int list -> unit 3271 3272 (** Query the fixedpoint solver. 3273 A query is a conjunction of constraints. The constraints may include the recursively defined relations. 3274 The query is satisfiable if there is an instance of the query variables and a derivation for it. 3275 The query is unsatisfiable if there are no derivations satisfying the query variables. *) 3276 val query : fixedpoint -> Expr.expr -> Solver.status 3277 3278 (** Query the fixedpoint solver. 3279 A query is an array of relations. 3280 The query is satisfiable if there is an instance of some relation that is non-empty. 3281 The query is unsatisfiable if there are no derivations satisfying any of the relations. *) 3282 val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status 3283 3284 (** Update named rule into in the fixedpoint solver. *) 3285 val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit 3286 3287 (** Retrieve satisfying instance or instances of solver, 3288 or definitions for the recursive predicates that show unsatisfiability. *) 3289 val get_answer : fixedpoint -> Expr.expr option 3290 3291 (** Retrieve explanation why fixedpoint engine returned status Unknown. *) 3292 val get_reason_unknown : fixedpoint -> string 3293 3294 (** Retrieve the number of levels explored for a given predicate. *) 3295 val get_num_levels : fixedpoint -> FuncDecl.func_decl -> int 3296 3297 (** Retrieve the cover of a predicate. *) 3298 val get_cover_delta : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr option 3299 3300 (** Add <tt>property</tt> about the <tt>predicate</tt>. 3301 The property is added at <tt>level</tt>. *) 3302 val add_cover : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr -> unit 3303 3304 (** Retrieve internal string representation of fixedpoint object. *) 3305 val to_string : fixedpoint -> string 3306 3307 (** Instrument the Datalog engine on which table representation to use for recursive predicate. *) 3308 val set_predicate_representation : fixedpoint -> FuncDecl.func_decl -> Symbol.symbol list -> unit 3309 3310 (** Convert benchmark given as set of axioms, rules and queries to a string. *) 3311 val to_string_q : fixedpoint -> Expr.expr list -> string 3312 3313 (** Retrieve set of rules added to fixedpoint context. *) 3314 val get_rules : fixedpoint -> Expr.expr list 3315 3316 (** Retrieve set of assertions added to fixedpoint context. *) 3317 val get_assertions : fixedpoint -> Expr.expr list 3318 3319 (** Create a Fixedpoint context. *) 3320 val mk_fixedpoint : context -> fixedpoint 3321 3322 (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *) 3323 val get_statistics : fixedpoint -> Statistics.statistics 3324 3325 (** Parse an SMT-LIB2 string with fixedpoint rules. 3326 Add the rules to the current fixedpoint context. 3327 Return the set of queries in the string. *) 3328 val parse_string : fixedpoint -> string -> Expr.expr list 3329 3330 (** Parse an SMT-LIB2 file with fixedpoint rules. 3331 Add the rules to the current fixedpoint context. 3332 Return the set of queries in the file. *) 3333 val parse_file : fixedpoint -> string -> Expr.expr list 3334end 3335 3336(** Optimization *) 3337module Optimize : 3338sig 3339 type optimize 3340 type handle 3341 3342 (** Create a Optimize context. *) 3343 val mk_opt : context -> optimize 3344 3345 (** A string that describes all available optimize solver parameters. *) 3346 val get_help : optimize -> string 3347 3348 (** Sets the optimize solver parameters. *) 3349 val set_parameters : optimize -> Params.params -> unit 3350 3351 (** Retrieves parameter descriptions for Optimize solver. *) 3352 val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs 3353 3354 (** Assert a constraints into the optimize solver. *) 3355 val add : optimize -> Expr.expr list -> unit 3356 3357 (** Assert a soft constraint. 3358 Supply integer weight and string that identifies a group 3359 of soft constraints. *) 3360 val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle 3361 3362 (** Add maximization objective. *) 3363 val maximize : optimize -> Expr.expr -> handle 3364 3365 (** Add minimization objective. *) 3366 val minimize : optimize -> Expr.expr -> handle 3367 3368 (** Checks whether the assertions in the context are satisfiable and solves objectives. *) 3369 val check : optimize -> Solver.status 3370 3371 (** Retrieve model from satisfiable context *) 3372 val get_model : optimize -> Model.model option 3373 3374 (** Retrieve lower bound in current model for handle *) 3375 val get_lower : handle -> Expr.expr 3376 3377 (** Retrieve upper bound in current model for handle *) 3378 val get_upper : handle -> Expr.expr 3379 3380 (** Creates a backtracking point. {!pop} *) 3381 val push : optimize -> unit 3382 3383 (** Backtrack one backtracking point. 3384 Note that an exception is thrown if Pop is called without a corresponding [Push] 3385 {!push} *) 3386 val pop : optimize -> unit 3387 3388 (** Retrieve explanation why optimize engine returned status Unknown. *) 3389 val get_reason_unknown : optimize -> string 3390 3391 (** Retrieve SMT-LIB string representation of optimize object. *) 3392 val to_string : optimize -> string 3393 3394 (** Retrieve statistics information from the last call to check *) 3395 val get_statistics : optimize -> Statistics.statistics 3396 3397 (** Parse an SMT-LIB2 file with assertions, soft constraints and optimization 3398 objectives. Add the parsed constraints and objectives to the optimization 3399 context. *) 3400 val from_file : optimize -> string -> unit 3401 3402 (** Parse an SMT-LIB2 string with assertions, soft constraints and optimization 3403 objectives. Add the parsed constraints and objectives to the optimization 3404 context. *) 3405 val from_string : optimize -> string -> unit 3406 3407 (** Return the set of asserted formulas on the optimization context. *) 3408 val get_assertions : optimize -> Expr.expr list 3409 3410 (** Return objectives on the optimization context. If the objective function 3411 is a max-sat objective it is returned as a Pseudo-Boolean (minimization) 3412 sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...). If the objective 3413 function is entered as a maximization objective, then return the 3414 corresponding minimization objective. In this way the resulting 3415 objective function is always returned as a minimization objective. *) 3416 val get_objectives : optimize -> Expr.expr list 3417end 3418 3419 3420(** Functions for handling SMT and SMT2 expressions and files *) 3421module SMT : 3422sig 3423 (** Convert a benchmark into an SMT-LIB formatted string. 3424 3425 @return A string representation of the benchmark. *) 3426 val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string 3427 3428 (** Parse the given string using the SMT-LIB2 parser. 3429 3430 @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *) 3431 val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector 3432 3433 (** Parse the given file using the SMT-LIB2 parser. *) 3434 val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector 3435end 3436 3437 3438(** Set a global (or module) parameter, which is shared by all Z3 contexts. 3439 3440 When a Z3 module is initialized it will use the value of these parameters 3441 when Z3_params objects are not provided. 3442 The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. 3443 The character '.' is a delimiter (more later). 3444 The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. 3445 Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". 3446 This function can be used to set parameters for a specific Z3 module. 3447 This can be done by using <module-name>.<parameter-name>. 3448 For example: 3449 (set_global_param "pp.decimal" "true") 3450 will set the parameter "decimal" in the module "pp" to true. 3451*) 3452val set_global_param : string -> string -> unit 3453 3454(** Get a global (or module) parameter. 3455 3456 Returns None if the parameter does not exist. 3457 The caller must invoke #Z3_global_param_del_value to delete the value returned at param_value. 3458 This function cannot be invoked simultaneously from different threads without synchronization. 3459 The result string stored in param_value is stored in a shared location. 3460*) 3461val get_global_param : string -> string option 3462 3463(** Restore the value of all global (and module) parameters. 3464 3465 This command will not affect already created objects (such as tactics and solvers) 3466 {!set_global_param} 3467*) 3468 3469val global_param_reset_all : unit -> unit 3470 3471(** Enable/disable printing of warning messages to the console. 3472 3473 Note that this function is static and effects the behaviour of 3474 all contexts globally. *) 3475val toggle_warning_messages : bool -> unit 3476 3477(** 3478 Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode. 3479 3480 Remarks: It is a NOOP otherwise. 3481*) 3482val enable_trace : string -> unit 3483 3484(** 3485 Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode. 3486 3487 Remarks: It is a NOOP otherwise. 3488*) 3489val disable_trace : string -> unit 3490 3491 3492(** Memory management **) 3493module Memory : 3494sig 3495 (** Reset all allocated resources **) 3496 val reset : unit -> unit 3497end 3498