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 (** compare strings less-than-or-equal *) 1917 val mk_str_le : context -> Expr.expr -> Expr.expr -> Expr.expr 1918 1919 (** compare strings less-than *) 1920 val mk_str_lt : context -> Expr.expr -> Expr.expr -> Expr.expr 1921 1922 (** convert an integer expression to a string *) 1923 val mk_int_to_str : context -> Expr.expr -> Expr.expr 1924 1925 (** create regular expression that accepts the argument sequence *) 1926 val mk_seq_to_re : context -> Expr.expr -> Expr.expr 1927 1928 (** regular expression membership predicate *) 1929 val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr 1930 1931 (** regular expression plus *) 1932 val mk_re_plus : context -> Expr.expr -> Expr.expr 1933 1934 (** regular expression star *) 1935 val mk_re_star : context -> Expr.expr -> Expr.expr 1936 1937 (** optional regular expression *) 1938 val mk_re_option : context -> Expr.expr -> Expr.expr 1939 1940 (** union of regular expressions *) 1941 val mk_re_union : context -> Expr.expr list -> Expr.expr 1942 1943 (** concatenation of regular expressions *) 1944 val mk_re_concat : context -> Expr.expr list -> Expr.expr 1945 1946 (** regular expression for the range between two characters *) 1947 val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr 1948 1949 (** bounded loop regular expression *) 1950 val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr 1951 1952 (** intersection of regular expressions *) 1953 val mk_re_intersect : context -> Expr.expr list -> Expr.expr 1954 1955 (** the regular expression complement *) 1956 val mk_re_complement : context -> Expr.expr -> Expr.expr 1957 1958 (** the regular expression that accepts no sequences *) 1959 val mk_re_empty : context -> Sort.sort -> Expr.expr 1960 1961 (** the regular expression that accepts all sequences *) 1962 val mk_re_full : context -> Sort.sort -> Expr.expr 1963 1964end 1965 1966(** Floating-Point Arithmetic *) 1967module FloatingPoint : 1968sig 1969 1970 (** Rounding Modes *) 1971 module RoundingMode : 1972 sig 1973 (** Create the RoundingMode sort. *) 1974 val mk_sort : context -> Sort.sort 1975 1976 (** Indicates whether the terms is of floating-point rounding mode sort. *) 1977 val is_fprm : Expr.expr -> bool 1978 1979 (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) 1980 val mk_round_nearest_ties_to_even : context -> Expr.expr 1981 1982 (** Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. *) 1983 val mk_rne : context -> Expr.expr 1984 1985 (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) 1986 val mk_round_nearest_ties_to_away : context -> Expr.expr 1987 1988 (** Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. *) 1989 val mk_rna : context -> Expr.expr 1990 1991 (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) 1992 val mk_round_toward_positive : context -> Expr.expr 1993 1994 (** Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. *) 1995 val mk_rtp : context -> Expr.expr 1996 1997 (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) 1998 val mk_round_toward_negative : context -> Expr.expr 1999 2000 (** Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. *) 2001 val mk_rtn : context -> Expr.expr 2002 2003 (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) 2004 val mk_round_toward_zero : context -> Expr.expr 2005 2006 (** Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. *) 2007 val mk_rtz : context -> Expr.expr 2008 end 2009 2010 (** Create a FloatingPoint sort. *) 2011 val mk_sort : context -> int -> int -> Sort.sort 2012 2013 (** Create the half-precision (16-bit) FloatingPoint sort.*) 2014 val mk_sort_half : context -> Sort.sort 2015 2016 (** Create the half-precision (16-bit) FloatingPoint sort. *) 2017 val mk_sort_16 : context -> Sort.sort 2018 2019 (** Create the single-precision (32-bit) FloatingPoint sort.*) 2020 val mk_sort_single : context -> Sort.sort 2021 2022 (** Create the single-precision (32-bit) FloatingPoint sort. *) 2023 val mk_sort_32 : context -> Sort.sort 2024 2025 (** Create the double-precision (64-bit) FloatingPoint sort. *) 2026 val mk_sort_double : context -> Sort.sort 2027 2028 (** Create the double-precision (64-bit) FloatingPoint sort. *) 2029 val mk_sort_64 : context -> Sort.sort 2030 2031 (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) 2032 val mk_sort_quadruple : context -> Sort.sort 2033 2034 (** Create the quadruple-precision (128-bit) FloatingPoint sort. *) 2035 val mk_sort_128 : context -> Sort.sort 2036 2037 (** Create a floating-point NaN of a given FloatingPoint sort. *) 2038 val mk_nan : context -> Sort.sort -> Expr.expr 2039 2040 (** Create a floating-point infinity of a given FloatingPoint sort. *) 2041 val mk_inf : context -> Sort.sort -> bool -> Expr.expr 2042 2043 (** Create a floating-point zero of a given FloatingPoint sort. *) 2044 val mk_zero : context -> Sort.sort -> bool -> Expr.expr 2045 2046 (** Create an expression of FloatingPoint sort from three bit-vector expressions. 2047 2048 This is the operator named `fp' in the SMT FP theory definition. 2049 Note that \c sign is required to be a bit-vector of size 1. Significand and exponent 2050 are required to be greater than 1 and 2 respectively. The FloatingPoint sort 2051 of the resulting expression is automatically determined from the bit-vector sizes 2052 of the arguments. *) 2053 val mk_fp : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2054 2055 (** Create a numeral of FloatingPoint sort from a float. 2056 2057 This function is used to create numerals that fit in a float value. 2058 It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. *) 2059 val mk_numeral_f : context -> float -> Sort.sort -> Expr.expr 2060 2061 (** Create a numeral of FloatingPoint sort from a signed integer. *) 2062 val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr 2063 2064 (** Create a numeral of FloatingPoint sort from a sign bit and two integers. *) 2065 val mk_numeral_i_u : context -> bool -> int -> int -> Sort.sort -> Expr.expr 2066 2067 (** Create a numeral of FloatingPoint sort from a string *) 2068 val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr 2069 2070 (** Indicates whether the terms is of floating-point sort. *) 2071 val is_fp : Expr.expr -> bool 2072 2073 2074 (** Indicates whether an expression is a floating-point abs expression *) 2075 val is_abs : Expr.expr -> bool 2076 2077 (** Indicates whether an expression is a floating-point neg expression *) 2078 val is_neg : Expr.expr -> bool 2079 2080 (** Indicates whether an expression is a floating-point add expression *) 2081 val is_add : Expr.expr -> bool 2082 2083 (** Indicates whether an expression is a floating-point sub expression *) 2084 val is_sub : Expr.expr -> bool 2085 2086 (** Indicates whether an expression is a floating-point mul expression *) 2087 val is_mul : Expr.expr -> bool 2088 2089 (** Indicates whether an expression is a floating-point div expression *) 2090 val is_div : Expr.expr -> bool 2091 2092 (** Indicates whether an expression is a floating-point fma expression *) 2093 val is_fma : Expr.expr -> bool 2094 2095 (** Indicates whether an expression is a floating-point sqrt expression *) 2096 val is_sqrt : Expr.expr -> bool 2097 2098 (** Indicates whether an expression is a floating-point rem expression *) 2099 val is_rem : Expr.expr -> bool 2100 2101 (** Indicates whether an expression is a floating-point round_to_integral expression *) 2102 val is_round_to_integral : Expr.expr -> bool 2103 2104 (** Indicates whether an expression is a floating-point min expression *) 2105 val is_min : Expr.expr -> bool 2106 2107 (** Indicates whether an expression is a floating-point max expression *) 2108 val is_max : Expr.expr -> bool 2109 2110 (** Indicates whether an expression is a floating-point leq expression *) 2111 val is_leq : Expr.expr -> bool 2112 2113 (** Indicates whether an expression is a floating-point lt expression *) 2114 val is_lt : Expr.expr -> bool 2115 2116 (** Indicates whether an expression is a floating-point geq expression *) 2117 val is_geq : Expr.expr -> bool 2118 2119 (** Indicates whether an expression is a floating-point gt expression *) 2120 val is_gt : Expr.expr -> bool 2121 2122 (** Indicates whether an expression is a floating-point eq expression *) 2123 val is_eq : Expr.expr -> bool 2124 2125 (** Indicates whether an expression is a floating-point is_normal expression *) 2126 val is_is_normal : Expr.expr -> bool 2127 2128 (** Indicates whether an expression is a floating-point is_subnormal expression *) 2129 val is_is_subnormal : Expr.expr -> bool 2130 2131 (** Indicates whether an expression is a floating-point is_zero expression *) 2132 val is_is_zero : Expr.expr -> bool 2133 2134 (** Indicates whether an expression is a floating-point is_infinite expression *) 2135 val is_is_infinite : Expr.expr -> bool 2136 2137 (** Indicates whether an expression is a floating-point is_nan expression *) 2138 val is_is_nan : Expr.expr -> bool 2139 2140 (** Indicates whether an expression is a floating-point is_negative expression *) 2141 val is_is_negative : Expr.expr -> bool 2142 2143 (** Indicates whether an expression is a floating-point is_positive expression *) 2144 val is_is_positive : Expr.expr -> bool 2145 2146 (** Indicates whether an expression is a floating-point to_fp expression *) 2147 val is_to_fp : Expr.expr -> bool 2148 2149 (** Indicates whether an expression is a floating-point to_fp_unsigned expression *) 2150 val is_to_fp_unsigned : Expr.expr -> bool 2151 2152 (** Indicates whether an expression is a floating-point to_ubv expression *) 2153 val is_to_ubv : Expr.expr -> bool 2154 2155 (** Indicates whether an expression is a floating-point to_sbv expression *) 2156 val is_to_sbv : Expr.expr -> bool 2157 2158 (** Indicates whether an expression is a floating-point to_real expression *) 2159 val is_to_real : Expr.expr -> bool 2160 2161 (** Indicates whether an expression is a floating-point to_ieee_bv expression *) 2162 val is_to_ieee_bv : Expr.expr -> bool 2163 2164 2165 (** Returns a string representation of a numeral. *) 2166 val numeral_to_string : Expr.expr -> string 2167 2168 (** Creates a floating-point constant. *) 2169 val mk_const : context -> Symbol.symbol -> Sort.sort -> Expr.expr 2170 2171 (** Creates a floating-point constant. *) 2172 val mk_const_s : context -> string -> Sort.sort -> Expr.expr 2173 2174 (** Floating-point absolute value *) 2175 val mk_abs : context -> Expr.expr -> Expr.expr 2176 2177 (** Floating-point negation *) 2178 val mk_neg : context -> Expr.expr -> Expr.expr 2179 2180 (** Floating-point addition *) 2181 val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2182 2183 (** Floating-point subtraction *) 2184 val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2185 2186 (** Floating-point multiplication *) 2187 val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2188 2189 (** Floating-point division *) 2190 val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2191 2192 (** Floating-point fused multiply-add. *) 2193 val mk_fma : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 2194 2195 (** Floating-point square root *) 2196 val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr 2197 2198 (** Floating-point remainder *) 2199 val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr 2200 2201 (** Floating-point roundToIntegral. 2202 2203 Rounds a floating-point number to the closest integer, 2204 again represented as a floating-point number. *) 2205 val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr 2206 2207 (** Minimum of floating-point numbers. *) 2208 val mk_min : context -> Expr.expr -> Expr.expr -> Expr.expr 2209 2210 (** Maximum of floating-point numbers. *) 2211 val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr 2212 2213 (** Floating-point less than or equal. *) 2214 val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr 2215 2216 (** Floating-point less than. *) 2217 val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr 2218 2219 (** Floating-point greater than or equal. *) 2220 val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr 2221 2222 (** Floating-point greater than. *) 2223 val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr 2224 2225 (** Floating-point equality. *) 2226 val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr 2227 2228 (** Predicate indicating whether t is a normal floating-point number. *) 2229 val mk_is_normal : context -> Expr.expr -> Expr.expr 2230 2231 (** Predicate indicating whether t is a subnormal floating-point number. *) 2232 val mk_is_subnormal : context -> Expr.expr -> Expr.expr 2233 2234 (** Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero. *) 2235 val mk_is_zero : context -> Expr.expr -> Expr.expr 2236 2237 (** Predicate indicating whether t is a floating-point number representing +oo or -oo. *) 2238 val mk_is_infinite : context -> Expr.expr -> Expr.expr 2239 2240 (** Predicate indicating whether t is a NaN. *) 2241 val mk_is_nan : context -> Expr.expr -> Expr.expr 2242 2243 (** Predicate indicating whether t is a negative floating-point number. *) 2244 val mk_is_negative : context -> Expr.expr -> Expr.expr 2245 2246 (** Predicate indicating whether t is a positive floating-point number. *) 2247 val mk_is_positive : context -> Expr.expr -> Expr.expr 2248 2249 (** Conversion of a single IEEE 754-2008 bit-vector into a floating-point number. *) 2250 val mk_to_fp_bv : context -> Expr.expr -> Sort.sort -> Expr.expr 2251 2252 (** Conversion of a FloatingPoint term into another term of different FloatingPoint sort. *) 2253 val mk_to_fp_float : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2254 2255 (** Conversion of a term of real sort into a term of FloatingPoint sort. *) 2256 val mk_to_fp_real : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2257 2258 (** Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort. *) 2259 val mk_to_fp_signed : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2260 2261 (** Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort. *) 2262 val mk_to_fp_unsigned : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2263 2264 (** Conversion of a floating-point term into an unsigned bit-vector. *) 2265 val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr 2266 2267 (** Conversion of a floating-point term into a signed bit-vector. *) 2268 val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr 2269 2270 (** Conversion of a floating-point term into a real-numbered term. *) 2271 val mk_to_real : context -> Expr.expr -> Expr.expr 2272 2273 (** Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. *) 2274 val get_ebits : context -> Sort.sort -> int 2275 2276 (** Retrieves the number of bits reserved for the significand in a FloatingPoint sort. *) 2277 val get_sbits : context -> Sort.sort -> int 2278 2279 (** Retrieves the sign of a floating-point literal. *) 2280 val get_numeral_sign : context -> Expr.expr -> bool * int 2281 2282 (** Return the sign of a floating-point numeral as a bit-vector expression. 2283 Remark: NaN's do not have a bit-vector sign, so they are invalid arguments. *) 2284 val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr 2285 2286 (** Return the exponent value of a floating-point numeral as a string *) 2287 val get_numeral_exponent_string : context -> Expr.expr -> bool -> string 2288 2289 (** Return the exponent value of a floating-point numeral as a signed integer *) 2290 val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int 2291 2292 (** Return the exponent of a floating-point numeral as a bit-vector expression. 2293 Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *) 2294 val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr 2295 2296 (** Return the significand value of a floating-point numeral as a bit-vector expression. 2297 Remark: NaN's do not have a bit-vector significand, so they are invalid arguments. *) 2298 val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr 2299 2300 (** Return the significand value of a floating-point numeral as a string. *) 2301 val get_numeral_significand_string : context -> Expr.expr -> string 2302 2303 (** Return the significand value of a floating-point numeral as a uint64. 2304 Remark: This function extracts the significand bits, without the 2305 hidden bit or normalization. Throws an exception if the 2306 significand does not fit into an int. *) 2307 val get_numeral_significand_uint : context -> Expr.expr -> bool * int 2308 2309 (** Indicates whether a floating-point numeral is a NaN. *) 2310 val is_numeral_nan : context -> Expr.expr -> bool 2311 2312 (** Indicates whether a floating-point numeral is +oo or -oo. *) 2313 val is_numeral_inf : context -> Expr.expr -> bool 2314 2315 (** Indicates whether a floating-point numeral is +zero or -zero. *) 2316 val is_numeral_zero : context -> Expr.expr -> bool 2317 2318 (** Indicates whether a floating-point numeral is normal. *) 2319 val is_numeral_normal : context -> Expr.expr -> bool 2320 2321 (** Indicates whether a floating-point numeral is subnormal. *) 2322 val is_numeral_subnormal : context -> Expr.expr -> bool 2323 2324 (** Indicates whether a floating-point numeral is positive. *) 2325 val is_numeral_positive : context -> Expr.expr -> bool 2326 2327 (** Indicates whether a floating-point numeral is negative. *) 2328 val is_numeral_negative : context -> Expr.expr -> bool 2329 2330 (** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *) 2331 val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr 2332 2333 (** Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. *) 2334 val mk_to_fp_int_real : context -> Expr.expr -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr 2335 2336 (** The string representation of a numeral *) 2337 val numeral_to_string : Expr.expr -> string 2338end 2339 2340 2341(** Functions to manipulate proof expressions *) 2342module Proof : 2343sig 2344 (** Indicates whether the term is a Proof for the expression 'true'. *) 2345 val is_true : Expr.expr -> bool 2346 2347 (** Indicates whether the term is a proof for a fact asserted by the user. *) 2348 val is_asserted : Expr.expr -> bool 2349 2350 (** Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. *) 2351 val is_goal : Expr.expr -> bool 2352 2353 (** Indicates whether the term is a binary equivalence modulo namings. 2354 This binary predicate is used in proof terms. 2355 It captures equisatisfiability and equivalence modulo renamings. *) 2356 val is_oeq : Expr.expr -> bool 2357 2358 (** Indicates whether the term is proof via modus ponens 2359 2360 Given a proof for p and a proof for (implies p q), produces a proof for q. 2361 T1: p 2362 T2: (implies p q) 2363 [mp T1 T2]: q 2364 The second antecedents may also be a proof for (iff p q). *) 2365 val is_modus_ponens : Expr.expr -> bool 2366 2367 (** Indicates whether the term is a proof for (R t t), where R is a reflexive relation. 2368 This proof object has no antecedents. 2369 The only reflexive relations that are used are 2370 equivalence modulo namings, equality and equivalence. 2371 That is, R is either '~', '=' or 'iff'. *) 2372 val is_reflexivity : Expr.expr -> bool 2373 2374 (** Indicates whether the term is proof by symmetricity of a relation 2375 2376 Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). 2377 T1: (R t s) 2378 [symmetry T1]: (R s t) 2379 T1 is the antecedent of this proof object. *) 2380 val is_symmetry : Expr.expr -> bool 2381 2382 (** Indicates whether the term is a proof by transitivity of a relation 2383 2384 Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof 2385 for (R t u). 2386 T1: (R t s) 2387 T2: (R s u) 2388 [trans T1 T2]: (R t u) *) 2389 val is_transitivity : Expr.expr -> bool 2390 2391 (** Indicates whether the term is a proof by condensed transitivity of a relation 2392 2393 Condensed transitivity proof. 2394 It combines several symmetry and transitivity proofs. 2395 Example: 2396 T1: (R a b) 2397 T2: (R c b) 2398 T3: (R c d) 2399 [trans* T1 T2 T3]: (R a d) 2400 R must be a symmetric and transitive relation. 2401 2402 Assuming that this proof object is a proof for (R s t), then 2403 a proof checker must check if it is possible to prove (R s t) 2404 using the antecedents, symmetry and transitivity. That is, 2405 if there is a path from s to t, if we view every 2406 antecedent (R a b) as an edge between a and b. *) 2407 val is_Transitivity_star : Expr.expr -> bool 2408 2409 (** Indicates whether the term is a monotonicity proof object. 2410 2411 T1: (R t_1 s_1) 2412 ... 2413 Tn: (R t_n s_n) 2414 [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) 2415 Remark: if t_i == s_i, then the antecedent Ti is suppressed. 2416 That is, reflexivity proofs are suppressed to save space. *) 2417 val is_monotonicity : Expr.expr -> bool 2418 2419 (** Indicates whether the term is a quant-intro proof 2420 2421 Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). 2422 T1: (~ p q) 2423 [quant-intro T1]: (~ (forall (x) p) (forall (x) q)) *) 2424 val is_quant_intro : Expr.expr -> bool 2425 2426 (** Indicates whether the term is a distributivity proof object. 2427 2428 Given that f (= or) distributes over g (= and), produces a proof for 2429 (= (f a (g c d)) 2430 (g (f a c) (f a d))) 2431 If f and g are associative, this proof also justifies the following equality: 2432 (= (f (g a b) (g c d)) 2433 (g (f a c) (f a d) (f b c) (f b d))) 2434 where each f and g can have arbitrary number of arguments. 2435 2436 This proof object has no antecedents. 2437 Remark. This rule is used by the CNF conversion pass and 2438 instantiated by f = or, and g = and. *) 2439 val is_distributivity : Expr.expr -> bool 2440 2441 (** Indicates whether the term is a proof by elimination of AND 2442 2443 Given a proof for (and l_1 ... l_n), produces a proof for l_i 2444 T1: (and l_1 ... l_n) 2445 [and-elim T1]: l_i *) 2446 val is_and_elimination : Expr.expr -> bool 2447 2448 (** Indicates whether the term is a proof by elimination of not-or 2449 2450 Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). 2451 T1: (not (or l_1 ... l_n)) 2452 [not-or-elim T1]: (not l_i) *) 2453 val is_or_elimination : Expr.expr -> bool 2454 2455 (** Indicates whether the term is a proof by rewriting 2456 2457 A proof for a local rewriting step (= t s). 2458 The head function symbol of t is interpreted. 2459 2460 This proof object has no antecedents. 2461 The conclusion of a rewrite rule is either an equality (= t s), 2462 an equivalence (iff t s), or equi-satisfiability (~ t s). 2463 Remark: if f is bool, then = is iff. 2464 2465 Examples: 2466 (= (+ ( x : expr ) 0) x) 2467 (= (+ ( x : expr ) 1 2) (+ 3 x)) 2468 (iff (or ( x : expr ) false) x) *) 2469 val is_rewrite : Expr.expr -> bool 2470 2471 (** Indicates whether the term is a proof by rewriting 2472 2473 A proof for rewriting an expression t into an expression s. 2474 This proof object can have n antecedents. 2475 The antecedents are proofs for equalities used as substitution rules. 2476 The object is also used in a few cases. The cases are: 2477 - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) 2478 - When converting bit-vectors to Booleans (BIT2BOOL=true) *) 2479 val is_rewrite_star : Expr.expr -> bool 2480 2481 (** Indicates whether the term is a proof for pulling quantifiers out. 2482 2483 A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *) 2484 val is_pull_quant : Expr.expr -> bool 2485 2486 (** Indicates whether the term is a proof for pushing quantifiers in. 2487 2488 A proof for: 2489 (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) 2490 (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) 2491 ... 2492 (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) 2493 This proof object has no antecedents *) 2494 val is_push_quant : Expr.expr -> bool 2495 2496 (** Indicates whether the term is a proof for elimination of unused variables. 2497 2498 A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) 2499 (forall (x_1 ... x_n) p[x_1 ... x_n])) 2500 2501 It is used to justify the elimination of unused variables. 2502 This proof object has no antecedents. *) 2503 val is_elim_unused_vars : Expr.expr -> bool 2504 2505 (** Indicates whether the term is a proof for destructive equality resolution 2506 2507 A proof for destructive equality resolution: 2508 (iff (forall (x) (or (not (= ( x : expr ) t)) P[x])) P[t]) 2509 if ( x : expr ) does not occur in t. 2510 2511 This proof object has no antecedents. 2512 2513 Several variables can be eliminated simultaneously. *) 2514 val is_der : Expr.expr -> bool 2515 2516 (** Indicates whether the term is a proof for quantifier instantiation 2517 2518 A proof of (or (not (forall (x) (P x))) (P a)) *) 2519 val is_quant_inst : Expr.expr -> bool 2520 2521 (** Indicates whether the term is a hypothesis marker. 2522 Mark a hypothesis in a natural deduction style proof. *) 2523 val is_hypothesis : Expr.expr -> bool 2524 2525 (** Indicates whether the term is a proof by lemma 2526 2527 T1: false 2528 [lemma T1]: (or (not l_1) ... (not l_n)) 2529 2530 This proof object has one antecedent: a hypothetical proof for false. 2531 It converts the proof in a proof for (or (not l_1) ... (not l_n)), 2532 when T1 contains the hypotheses: l_1, ..., l_n. *) 2533 val is_lemma : Expr.expr -> bool 2534 2535 (** Indicates whether the term is a proof by unit resolution 2536 2537 T1: (or l_1 ... l_n l_1' ... l_m') 2538 T2: (not l_1) 2539 ... 2540 T(n+1): (not l_n) 2541 [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') *) 2542 val is_unit_resolution : Expr.expr -> bool 2543 2544 (** Indicates whether the term is a proof by iff-true 2545 2546 T1: p 2547 [iff-true T1]: (iff p true) *) 2548 val is_iff_true : Expr.expr -> bool 2549 2550 (** Indicates whether the term is a proof by iff-false 2551 2552 T1: (not p) 2553 [iff-false T1]: (iff p false) *) 2554 val is_iff_false : Expr.expr -> bool 2555 2556 (** Indicates whether the term is a proof by commutativity 2557 2558 [comm]: (= (f a b) (f b a)) 2559 2560 f is a commutative operator. 2561 2562 This proof object has no antecedents. 2563 Remark: if f is bool, then = is iff. *) 2564 val is_commutativity : Expr.expr -> bool 2565 2566 (** Indicates whether the term is a proof for Tseitin-like axioms 2567 2568 Proof object used to justify Tseitin's like axioms: 2569 2570 (or (not (and p q)) p) 2571 (or (not (and p q)) q) 2572 (or (not (and p q r)) p) 2573 (or (not (and p q r)) q) 2574 (or (not (and p q r)) r) 2575 ... 2576 (or (and p q) (not p) (not q)) 2577 (or (not (or p q)) p q) 2578 (or (or p q) (not p)) 2579 (or (or p q) (not q)) 2580 (or (not (iff p q)) (not p) q) 2581 (or (not (iff p q)) p (not q)) 2582 (or (iff p q) (not p) (not q)) 2583 (or (iff p q) p q) 2584 (or (not (ite a b c)) (not a) b) 2585 (or (not (ite a b c)) a c) 2586 (or (ite a b c) (not a) (not b)) 2587 (or (ite a b c) a (not c)) 2588 (or (not (not a)) (not a)) 2589 (or (not a) a) 2590 2591 This proof object has no antecedents. 2592 Note: all axioms are propositional tautologies. 2593 Note also that 'and' and 'or' can take multiple arguments. 2594 You can recover the propositional tautologies by 2595 unfolding the Boolean connectives in the axioms a small 2596 bounded number of steps (=3). *) 2597 val is_def_axiom : Expr.expr -> bool 2598 2599 (** Indicates whether the term is a proof for introduction of a name 2600 2601 Introduces a name for a formula/term. 2602 Suppose e is an expression with free variables x, and def-intro 2603 introduces the name n(x). The possible cases are: 2604 2605 When e is of Boolean type: 2606 [def-intro]: (and (or n (not e)) (or (not n) e)) 2607 2608 or: 2609 [def-intro]: (or (not n) e) 2610 when e only occurs positively. 2611 2612 When e is of the form (ite cond th el): 2613 [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el))) 2614 2615 Otherwise: 2616 [def-intro]: (= n e) *) 2617 val is_def_intro : Expr.expr -> bool 2618 2619 (** Indicates whether the term is a proof for application of a definition 2620 2621 [apply-def T1]: F ~ n 2622 F is 'equivalent' to n, given that T1 is a proof that 2623 n is a name for F. *) 2624 val is_apply_def : Expr.expr -> bool 2625 2626 (** Indicates whether the term is a proof iff-oeq 2627 2628 T1: (iff p q) 2629 [iff~ T1]: (~ p q) *) 2630 val is_iff_oeq : Expr.expr -> bool 2631 2632 (** Indicates whether the term is a proof for a positive NNF step 2633 2634 Proof for a (positive) NNF step. Example: 2635 2636 T1: (not s_1) ~ r_1 2637 T2: (not s_2) ~ r_2 2638 T3: s_1 ~ r_1' 2639 T4: s_2 ~ r_2' 2640 [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) 2641 (and (or r_1 r_2') (or r_1' r_2))) 2642 2643 The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: 2644 (a) When creating the NNF of a positive force quantifier. 2645 The quantifier is retained (unless the bound variables are eliminated). 2646 Example 2647 T1: q ~ q_new 2648 [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new)) 2649 2650 (b) When recursively creating NNF over Boolean formulas, where the top-level 2651 connective is changed during NNF conversion. The relevant Boolean connectives 2652 for NNF_POS are 'implies', 'iff', 'xor', 'ite'. 2653 NNF_NEG furthermore handles the case where negation is pushed 2654 over Boolean connectives 'and' and 'or'. *) 2655 val is_nnf_pos : Expr.expr -> bool 2656 2657 (** Indicates whether the term is a proof for a negative NNF step 2658 2659 Proof for a (negative) NNF step. Examples: 2660 2661 T1: (not s_1) ~ r_1 2662 ... 2663 Tn: (not s_n) ~ r_n 2664 [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) 2665 and 2666 T1: (not s_1) ~ r_1 2667 ... 2668 Tn: (not s_n) ~ r_n 2669 [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) 2670 and 2671 T1: (not s_1) ~ r_1 2672 T2: (not s_2) ~ r_2 2673 T3: s_1 ~ r_1' 2674 T4: s_2 ~ r_2' 2675 [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) 2676 (and (or r_1 r_2) (or r_1' r_2'))) *) 2677 val is_nnf_neg : Expr.expr -> bool 2678 2679 (** Indicates whether the term is a proof for a Skolemization step 2680 2681 Proof for: 2682 2683 [sk]: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y))) 2684 [sk]: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y)) 2685 2686 This proof object has no antecedents. *) 2687 val is_skolemize : Expr.expr -> bool 2688 2689 (** Indicates whether the term is a proof by modus ponens for equi-satisfiability. 2690 2691 Modus ponens style rule for equi-satisfiability. 2692 T1: p 2693 T2: (~ p q) 2694 [mp~ T1 T2]: q *) 2695 val is_modus_ponens_oeq : Expr.expr -> bool 2696 2697 (** Indicates whether the term is a proof for theory lemma 2698 2699 Generic proof for theory lemmas. 2700 2701 The theory lemma function comes with one or more parameters. 2702 The first parameter indicates the name of the theory. 2703 For the theory of arithmetic, additional parameters provide hints for 2704 checking the theory lemma. 2705 The hints for arithmetic are: 2706 - farkas - followed by rational coefficients. Multiply the coefficients to the 2707 inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. 2708 - triangle-eq - Indicates a lemma related to the equivalence: 2709 (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) 2710 - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. *) 2711 val is_theory_lemma : Expr.expr -> bool 2712end 2713 2714(** Goals 2715 2716 A goal (aka problem). A goal is essentially a 2717 of formulas, that can be solved and/or transformed using 2718 tactics and solvers. *) 2719module Goal : 2720sig 2721 type goal 2722 2723 (** The precision of the goal. 2724 2725 Goals can be transformed using over and under approximations. 2726 An under approximation is applied when the objective is to find a model for a given goal. 2727 An over approximation is applied when the objective is to find a proof for a given goal. *) 2728 val get_precision : goal -> Z3enums.goal_prec 2729 2730 (** Indicates whether the goal is precise. *) 2731 val is_precise : goal -> bool 2732 2733 (** Indicates whether the goal is an under-approximation. *) 2734 val is_underapproximation : goal -> bool 2735 2736 (** Indicates whether the goal is an over-approximation. *) 2737 val is_overapproximation : goal -> bool 2738 2739 (** Indicates whether the goal is garbage (i.e., the product of over- and under-approximations). *) 2740 val is_garbage : goal -> bool 2741 2742 (** Adds the constraints to the given goal. *) 2743 val add : goal -> Expr.expr list -> unit 2744 2745 (** Indicates whether the goal contains `false'. *) 2746 val is_inconsistent : goal -> bool 2747 2748 (** The depth of the goal. 2749 This tracks how many transformations were applied to it. *) 2750 val get_depth : goal -> int 2751 2752 (** Erases all formulas from the given goal. *) 2753 val reset : goal -> unit 2754 2755 (** The number of formulas in the goal. *) 2756 val get_size : goal -> int 2757 2758 (** The formulas in the goal. *) 2759 val get_formulas : goal -> Expr.expr list 2760 2761 (** The number of formulas, subformulas and terms in the goal. *) 2762 val get_num_exprs : goal -> int 2763 2764 (** Indicates whether the goal is empty, and it is precise or the product of an under approximation. *) 2765 val is_decided_sat : goal -> bool 2766 2767 (** Indicates whether the goal contains `false', and it is precise or the product of an over approximation. *) 2768 val is_decided_unsat : goal -> bool 2769 2770 (** Translates (copies) the Goal to another context.. *) 2771 val translate : goal -> context -> goal 2772 2773 (** Simplifies the goal. Essentially invokes the `simplify' tactic on the goal. *) 2774 val simplify : goal -> Params.params option -> goal 2775 2776 (** Creates a new Goal. 2777 2778 Note that the Context must have been created with proof generation support if 2779 the fourth argument is set to true here. *) 2780 val mk_goal : context -> bool -> bool -> bool -> goal 2781 2782 (** A string representation of the Goal. *) 2783 val to_string : goal -> string 2784 2785 (** Goal to BoolExpr conversion. *) 2786 val as_expr : goal -> Expr.expr 2787end 2788 2789(** Models 2790 2791 A Model contains interpretations (assignments) of constants and functions. *) 2792module Model : 2793sig 2794 type model 2795 2796 (** Function interpretations 2797 2798 A function interpretation is represented as a finite map and an 'else'. 2799 Each entry in the finite map represents the value of a function given a set of arguments. *) 2800 module FuncInterp : 2801 sig 2802 type func_interp 2803 2804 (** Function interpretations entries 2805 2806 An Entry object represents an element in the finite map used to a function interpretation. *) 2807 module FuncEntry : 2808 sig 2809 type func_entry 2810 2811 (** Return the (symbolic) value of this entry. 2812 *) 2813 val get_value : func_entry -> Expr.expr 2814 2815 (** The number of arguments of the entry. 2816 *) 2817 val get_num_args : func_entry -> int 2818 2819 (** The arguments of the function entry. 2820 *) 2821 val get_args : func_entry -> Expr.expr list 2822 2823 (** A string representation of the function entry. 2824 *) 2825 val to_string : func_entry -> string 2826 end 2827 2828 (** The number of entries in the function interpretation. *) 2829 val get_num_entries : func_interp -> int 2830 2831 (** The entries in the function interpretation *) 2832 val get_entries : func_interp -> FuncEntry.func_entry list 2833 2834 (** The (symbolic) `else' value of the function interpretation. *) 2835 val get_else : func_interp -> Expr.expr 2836 2837 (** The arity of the function interpretation *) 2838 val get_arity : func_interp -> int 2839 2840 (** A string representation of the function interpretation. *) 2841 val to_string : func_interp -> string 2842 end 2843 2844 (** Retrieves the interpretation (the assignment) of a func_decl in the model. 2845 @return An expression if the function has an interpretation in the model, null otherwise. *) 2846 val get_const_interp : model -> FuncDecl.func_decl -> Expr.expr option 2847 2848 (** Retrieves the interpretation (the assignment) of an expression in the model. 2849 @return An expression if the constant has an interpretation in the model, null otherwise. *) 2850 val get_const_interp_e : model -> Expr.expr -> Expr.expr option 2851 2852 (** Retrieves the interpretation (the assignment) of a non-constant func_decl in the model. 2853 @return A FunctionInterpretation if the function has an interpretation in the model, null otherwise. *) 2854 val get_func_interp : model -> FuncDecl.func_decl -> FuncInterp.func_interp option 2855 2856 (** The number of constant interpretations in the model. *) 2857 val get_num_consts : model -> int 2858 2859 (** The function declarations of the constants in the model. *) 2860 val get_const_decls : model -> FuncDecl.func_decl list 2861 2862 (** The number of function interpretations in the model. *) 2863 val get_num_funcs : model -> int 2864 2865 (** The function declarations of the function interpretations in the model. *) 2866 val get_func_decls : model -> FuncDecl.func_decl list 2867 2868 (** All symbols that have an interpretation in the model. *) 2869 val get_decls : model -> FuncDecl.func_decl list 2870 2871 (** Evaluates an expression in the current model. 2872 The Boolean argument indicates whether to apply model completion. 2873 When model completion is true it will assign an interpretation for 2874 constants and functions that do not have an interpretation in the model. 2875 2876 This function may fail if the argument contains quantifiers, 2877 is partial (MODEL_PARTIAL enabled), or if it is not well-sorted. 2878 In this case a [ModelEvaluationFailedException] is thrown. 2879 *) 2880 val eval : model -> Expr.expr -> bool -> Expr.expr option 2881 2882 (** Alias for [eval]. *) 2883 val evaluate : model -> Expr.expr -> bool -> Expr.expr option 2884 2885 (** The number of uninterpreted sorts that the model has an interpretation for. *) 2886 val get_num_sorts : model -> int 2887 2888 (** The uninterpreted sorts that the model has an interpretation for. 2889 2890 Z3 also provides an interpretation for uninterpreted sorts used in a formula. 2891 The interpretation for a sort is a finite set of distinct values. We say this finite set is 2892 the "universe" of the sort. 2893 {!get_num_sorts} 2894 {!sort_universe} *) 2895 val get_sorts : model -> Sort.sort list 2896 2897 (** The finite set of distinct values that represent the interpretation of a sort. 2898 {!get_sorts} 2899 @return A list of expressions, where each is an element of the universe of the sort *) 2900 val sort_universe : model -> Sort.sort -> Expr.expr list 2901 2902 (** Conversion of models to strings. 2903 @return A string representation of the model. *) 2904 val to_string : model -> string 2905end 2906 2907(** Probes 2908 2909 Probes are used to inspect a goal (aka problem) and collect information that may be used to decide 2910 which solver and/or preprocessing step will be used. 2911 The complete list of probes may be obtained using the procedures [Context.NumProbes] 2912 and [Context.ProbeNames]. 2913 It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. 2914*) 2915module Probe : 2916sig 2917 type probe 2918 2919 (** Execute the probe over the goal. 2920 @return A probe always produce a float value. 2921 "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. *) 2922 val apply : probe -> Goal.goal -> float 2923 2924 (** The number of supported Probes. *) 2925 val get_num_probes : context -> int 2926 2927 (** The names of all supported Probes. *) 2928 val get_probe_names : context -> string list 2929 2930 (** Returns a string containing a description of the probe with the given name. *) 2931 val get_probe_description : context -> string -> string 2932 2933 (** Creates a new Probe. *) 2934 val mk_probe : context -> string -> probe 2935 2936 (** Create a probe that always evaluates to a float value. *) 2937 val const : context -> float -> probe 2938 2939 (** Create a probe that evaluates to "true" when the value returned by the first argument 2940 is less than the value returned by second argument *) 2941 val lt : context -> probe -> probe -> probe 2942 2943 (** Create a probe that evaluates to "true" when the value returned by the first argument 2944 is greater than the value returned by second argument *) 2945 val gt : context -> probe -> probe -> probe 2946 2947 (** Create a probe that evaluates to "true" when the value returned by the first argument 2948 is less than or equal the value returned by second argument *) 2949 val le : context -> probe -> probe -> probe 2950 2951 (** Create a probe that evaluates to "true" when the value returned by the first argument 2952 is greater than or equal the value returned by second argument *) 2953 val ge : context -> probe -> probe -> probe 2954 2955 2956 (** Create a probe that evaluates to "true" when the value returned by the first argument 2957 is equal the value returned by second argument *) 2958 val eq : context -> probe -> probe -> probe 2959 2960 (** Create a probe that evaluates to "true" when both of two probes evaluate to "true". *) 2961 val and_ : context -> probe -> probe -> probe 2962 2963 (** Create a probe that evaluates to "true" when either of two probes evaluates to "true". *) 2964 val or_ : context -> probe -> probe -> probe 2965 2966 (** Create a probe that evaluates to "true" when another probe does not evaluate to "true". *) 2967 val not_ : context -> probe -> probe 2968end 2969 2970(** Tactics 2971 2972 Tactics are the basic building block for creating custom solvers for specific problem domains. 2973 The complete list of tactics may be obtained using [Context.get_num_tactics] 2974 and [Context.get_tactic_names]. 2975 It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end. 2976*) 2977module Tactic : 2978sig 2979 type tactic 2980 2981 (** Tactic application results 2982 2983 ApplyResult objects represent the result of an application of a 2984 tactic to a goal. It contains the subgoals that were produced. *) 2985 module ApplyResult : 2986 sig 2987 type apply_result 2988 2989 (** The number of Subgoals. *) 2990 val get_num_subgoals : apply_result -> int 2991 2992 (** Retrieves the subgoals from the apply_result. *) 2993 val get_subgoals : apply_result -> Goal.goal list 2994 2995 (** Retrieves a subgoal from the apply_result. *) 2996 val get_subgoal : apply_result -> int -> Goal.goal 2997 2998 (** A string representation of the ApplyResult. *) 2999 val to_string : apply_result -> string 3000 end 3001 3002 (** A string containing a description of parameters accepted by the tactic. *) 3003 val get_help : tactic -> string 3004 3005 (** Retrieves parameter descriptions for Tactics. *) 3006 val get_param_descrs : tactic -> Params.ParamDescrs.param_descrs 3007 3008 (** Apply the tactic to the goal. *) 3009 val apply : tactic -> Goal.goal -> Params.params option -> ApplyResult.apply_result 3010 3011 (** The number of supported tactics. *) 3012 val get_num_tactics : context -> int 3013 3014 (** The names of all supported tactics. *) 3015 val get_tactic_names : context -> string list 3016 3017 (** Returns a string containing a description of the tactic with the given name. *) 3018 val get_tactic_description : context -> string -> string 3019 3020 (** Creates a new Tactic. *) 3021 val mk_tactic : context -> string -> tactic 3022 3023 (** Create a tactic that applies one tactic to a Goal and 3024 then another one to every subgoal produced by the first one. *) 3025 val and_then : context -> tactic -> tactic -> tactic list -> tactic 3026 3027 (** Create a tactic that first applies one tactic to a Goal and 3028 if it fails then returns the result of another tactic applied to the Goal. *) 3029 val or_else : context -> tactic -> tactic -> tactic 3030 3031 (** Create a tactic that applies one tactic to a goal for some time (in milliseconds). 3032 3033 If the tactic does not terminate within the timeout, then it fails. *) 3034 val try_for : context -> tactic -> int -> tactic 3035 3036 (** Create a tactic that applies one tactic to a given goal if the probe 3037 evaluates to true. 3038 3039 If the probe evaluates to false, then the new tactic behaves like the [skip] tactic. *) 3040 val when_ : context -> Probe.probe -> tactic -> tactic 3041 3042 (** Create a tactic that applies a tactic to a given goal if the probe 3043 evaluates to true and another tactic otherwise. *) 3044 val cond : context -> Probe.probe -> tactic -> tactic -> tactic 3045 3046 (** Create a tactic that keeps applying one tactic until the goal is not 3047 modified anymore or the maximum number of iterations is reached. *) 3048 val repeat : context -> tactic -> int -> tactic 3049 3050 (** Create a tactic that just returns the given goal. *) 3051 val skip : context -> tactic 3052 3053 (** Create a tactic always fails. *) 3054 val fail : context -> tactic 3055 3056 (** Create a tactic that fails if the probe evaluates to false. *) 3057 val fail_if : context -> Probe.probe -> tactic 3058 3059 (** Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) 3060 or trivially unsatisfiable (i.e., contains `false'). *) 3061 val fail_if_not_decided : context -> tactic 3062 3063 (** Create a tactic that applies a tactic using the given set of parameters. *) 3064 val using_params : context -> tactic -> Params.params -> tactic 3065 3066 (** Create a tactic that applies a tactic using the given set of parameters. 3067 Alias for [UsingParams]*) 3068 val with_ : context -> tactic -> Params.params -> tactic 3069 3070 (** Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). *) 3071 val par_or : context -> tactic list -> tactic 3072 3073 (** Create a tactic that applies a tactic to a given goal and then another tactic 3074 to every subgoal produced by the first one. The subgoals are processed in parallel. *) 3075 val par_and_then : context -> tactic -> tactic -> tactic 3076 3077 (** Interrupt the execution of a Z3 procedure. 3078 This procedure can be used to interrupt: solvers, simplifiers and tactics. *) 3079 val interrupt : context -> unit 3080end 3081 3082(** Objects that track statistical information. *) 3083module Statistics : 3084sig 3085 type statistics 3086 3087 (** Statistical data is organized into pairs of \[Key, Entry\], where every 3088 Entry is either a floating point or integer value. *) 3089 module Entry : 3090 sig 3091 type statistics_entry 3092 3093 (** The key of the entry. *) 3094 val get_key : statistics_entry -> string 3095 3096 (** The int-value of the entry. *) 3097 val get_int : statistics_entry -> int 3098 3099 (** The float-value of the entry. *) 3100 val get_float : statistics_entry -> float 3101 3102 (** True if the entry is uint-valued. *) 3103 val is_int : statistics_entry -> bool 3104 3105 (** True if the entry is float-valued. *) 3106 val is_float : statistics_entry -> bool 3107 3108 (** The string representation of the entry's value. *) 3109 val to_string_value : statistics_entry -> string 3110 3111 (** The string representation of the entry (key and value) *) 3112 val to_string : statistics_entry -> string 3113 end 3114 3115 (** A string representation of the statistical data. *) 3116 val to_string : statistics -> string 3117 3118 (** The number of statistical data. *) 3119 val get_size : statistics -> int 3120 3121 (** The data entries. *) 3122 val get_entries : statistics -> Entry.statistics_entry list 3123 3124 (** The statistical counters. *) 3125 val get_keys : statistics -> string list 3126 3127 (** The value of a particular statistical counter. *) 3128 val get : statistics -> string -> Entry.statistics_entry option 3129end 3130 3131(** Solvers *) 3132module Solver : 3133sig 3134 type solver 3135 type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE 3136 3137 val string_of_status : status -> string 3138 3139 (** A string that describes all available solver parameters. *) 3140 val get_help : solver -> string 3141 3142 (** Sets the solver parameters. *) 3143 val set_parameters : solver -> Params.params -> unit 3144 3145 (** Retrieves parameter descriptions for solver. *) 3146 val get_param_descrs : solver -> Params.ParamDescrs.param_descrs 3147 3148 (** The current number of backtracking points (scopes). 3149 {!pop} 3150 {!push} *) 3151 val get_num_scopes : solver -> int 3152 3153 (** Creates a backtracking point. 3154 {!pop} *) 3155 val push : solver -> unit 3156 3157 (** Backtracks a number of backtracking points. 3158 Note that an exception is thrown if the integer is not smaller than {!get_num_scopes} 3159 {!push} *) 3160 val pop : solver -> int -> unit 3161 3162 (** Resets the Solver. 3163 This removes all assertions from the solver. *) 3164 val reset : solver -> unit 3165 3166 (** Assert a constraint (or multiple) into the solver. *) 3167 val add : solver -> Expr.expr list -> unit 3168 3169 (** Assert multiple constraints (cs) into the solver, and track them (in the 3170 unsat) core using the Boolean constants in ps. 3171 3172 This API is an alternative to {!check} with assumptions for extracting unsat cores. 3173 Both APIs can be used in the same solver. The unsat core will contain a combination 3174 of the Boolean variables provided using {!assert_and_track} and the Boolean literals 3175 provided using {!check} with assumptions. *) 3176 val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit 3177 3178 (** Assert a constraint (c) into the solver, and track it (in the unsat) core 3179 using the Boolean constant p. 3180 3181 This API is an alternative to {!check} with assumptions for extracting unsat cores. 3182 Both APIs can be used in the same solver. The unsat core will contain a combination 3183 of the Boolean variables provided using {!assert_and_track} and the Boolean literals 3184 provided using {!check} with assumptions. *) 3185 val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit 3186 3187 (** The number of assertions in the solver. *) 3188 val get_num_assertions : solver -> int 3189 3190 (** The set of asserted formulas. *) 3191 val get_assertions : solver -> Expr.expr list 3192 3193 (** Checks whether the assertions in the solver are consistent or not. 3194 3195 {!Model} 3196 {!get_unsat_core} 3197 {!Proof} *) 3198 val check : solver -> Expr.expr list -> status 3199 3200 (** The model of the last [Check]. 3201 3202 The result is [None] if [Check] was not invoked before, 3203 if its results was not [SATISFIABLE], or if model production is not enabled. *) 3204 val get_model : solver -> Model.model option 3205 3206 (** The proof of the last [Check]. 3207 3208 The result is [null] if [Check] was not invoked before, 3209 if its results was not [UNSATISFIABLE], or if proof production is disabled. *) 3210 val get_proof : solver -> Expr.expr option 3211 3212 (** The unsat core of the last [Check]. 3213 3214 The unsat core is a subset of [Assertions] 3215 The result is empty if [Check] was not invoked before, 3216 if its results was not [UNSATISFIABLE], or if core production is disabled. *) 3217 val get_unsat_core : solver -> Expr.expr list 3218 3219 (** A brief justification of why the last call to [Check] returned [UNKNOWN]. *) 3220 val get_reason_unknown : solver -> string 3221 3222 (** Solver statistics. *) 3223 val get_statistics : solver -> Statistics.statistics 3224 3225 (** Creates a new (incremental) solver. 3226 3227 This solver also uses a set of builtin tactics for handling the first 3228 check-sat command, and check-sat commands that take more than a given 3229 number of milliseconds to be solved. *) 3230 val mk_solver : context -> Symbol.symbol option -> solver 3231 3232 (** Creates a new (incremental) solver. 3233 {!mk_solver} *) 3234 val mk_solver_s : context -> string -> solver 3235 3236 (** Creates a new (incremental) solver. *) 3237 val mk_simple_solver : context -> solver 3238 3239 (** Creates a solver that is implemented using the given tactic. 3240 3241 The solver supports the commands [Push] and [Pop], but it 3242 will always solve each check from scratch. *) 3243 val mk_solver_t : context -> Tactic.tactic -> solver 3244 3245 (** Create a clone of the current solver with respect to a context. *) 3246 val translate : solver -> context -> solver 3247 3248 (** A string representation of the solver. *) 3249 val to_string : solver -> string 3250end 3251 3252(** Fixedpoint solving *) 3253module Fixedpoint : 3254sig 3255 type fixedpoint 3256 3257 (** A string that describes all available fixedpoint solver parameters. *) 3258 val get_help : fixedpoint -> string 3259 3260 (** Sets the fixedpoint solver parameters. *) 3261 val set_parameters : fixedpoint -> Params.params -> unit 3262 3263 (** Retrieves parameter descriptions for Fixedpoint solver. *) 3264 val get_param_descrs : fixedpoint -> Params.ParamDescrs.param_descrs 3265 3266 (** Assert a constraints into the fixedpoint solver. *) 3267 val add : fixedpoint -> Expr.expr list -> unit 3268 3269 (** Register predicate as recursive relation. *) 3270 val register_relation : fixedpoint -> FuncDecl.func_decl -> unit 3271 3272 (** Add rule into the fixedpoint solver. *) 3273 val add_rule : fixedpoint -> Expr.expr -> Symbol.symbol option -> unit 3274 3275 (** Add table fact to the fixedpoint solver. *) 3276 val add_fact : fixedpoint -> FuncDecl.func_decl -> int list -> unit 3277 3278 (** Query the fixedpoint solver. 3279 A query is a conjunction of constraints. The constraints may include the recursively defined relations. 3280 The query is satisfiable if there is an instance of the query variables and a derivation for it. 3281 The query is unsatisfiable if there are no derivations satisfying the query variables. *) 3282 val query : fixedpoint -> Expr.expr -> Solver.status 3283 3284 (** Query the fixedpoint solver. 3285 A query is an array of relations. 3286 The query is satisfiable if there is an instance of some relation that is non-empty. 3287 The query is unsatisfiable if there are no derivations satisfying any of the relations. *) 3288 val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status 3289 3290 (** Update named rule into in the fixedpoint solver. *) 3291 val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit 3292 3293 (** Retrieve satisfying instance or instances of solver, 3294 or definitions for the recursive predicates that show unsatisfiability. *) 3295 val get_answer : fixedpoint -> Expr.expr option 3296 3297 (** Retrieve explanation why fixedpoint engine returned status Unknown. *) 3298 val get_reason_unknown : fixedpoint -> string 3299 3300 (** Retrieve the number of levels explored for a given predicate. *) 3301 val get_num_levels : fixedpoint -> FuncDecl.func_decl -> int 3302 3303 (** Retrieve the cover of a predicate. *) 3304 val get_cover_delta : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr option 3305 3306 (** Add <tt>property</tt> about the <tt>predicate</tt>. 3307 The property is added at <tt>level</tt>. *) 3308 val add_cover : fixedpoint -> int -> FuncDecl.func_decl -> Expr.expr -> unit 3309 3310 (** Retrieve internal string representation of fixedpoint object. *) 3311 val to_string : fixedpoint -> string 3312 3313 (** Instrument the Datalog engine on which table representation to use for recursive predicate. *) 3314 val set_predicate_representation : fixedpoint -> FuncDecl.func_decl -> Symbol.symbol list -> unit 3315 3316 (** Convert benchmark given as set of axioms, rules and queries to a string. *) 3317 val to_string_q : fixedpoint -> Expr.expr list -> string 3318 3319 (** Retrieve set of rules added to fixedpoint context. *) 3320 val get_rules : fixedpoint -> Expr.expr list 3321 3322 (** Retrieve set of assertions added to fixedpoint context. *) 3323 val get_assertions : fixedpoint -> Expr.expr list 3324 3325 (** Create a Fixedpoint context. *) 3326 val mk_fixedpoint : context -> fixedpoint 3327 3328 (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *) 3329 val get_statistics : fixedpoint -> Statistics.statistics 3330 3331 (** Parse an SMT-LIB2 string with fixedpoint rules. 3332 Add the rules to the current fixedpoint context. 3333 Return the set of queries in the string. *) 3334 val parse_string : fixedpoint -> string -> Expr.expr list 3335 3336 (** Parse an SMT-LIB2 file with fixedpoint rules. 3337 Add the rules to the current fixedpoint context. 3338 Return the set of queries in the file. *) 3339 val parse_file : fixedpoint -> string -> Expr.expr list 3340end 3341 3342(** Optimization *) 3343module Optimize : 3344sig 3345 type optimize 3346 type handle 3347 3348 (** Create a Optimize context. *) 3349 val mk_opt : context -> optimize 3350 3351 (** A string that describes all available optimize solver parameters. *) 3352 val get_help : optimize -> string 3353 3354 (** Sets the optimize solver parameters. *) 3355 val set_parameters : optimize -> Params.params -> unit 3356 3357 (** Retrieves parameter descriptions for Optimize solver. *) 3358 val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs 3359 3360 (** Assert a constraints into the optimize solver. *) 3361 val add : optimize -> Expr.expr list -> unit 3362 3363 (** Assert a soft constraint. 3364 Supply integer weight and string that identifies a group 3365 of soft constraints. *) 3366 val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle 3367 3368 (** Add maximization objective. *) 3369 val maximize : optimize -> Expr.expr -> handle 3370 3371 (** Add minimization objective. *) 3372 val minimize : optimize -> Expr.expr -> handle 3373 3374 (** Checks whether the assertions in the context are satisfiable and solves objectives. *) 3375 val check : optimize -> Solver.status 3376 3377 (** Retrieve model from satisfiable context *) 3378 val get_model : optimize -> Model.model option 3379 3380 (** Retrieve lower bound in current model for handle *) 3381 val get_lower : handle -> Expr.expr 3382 3383 (** Retrieve upper bound in current model for handle *) 3384 val get_upper : handle -> Expr.expr 3385 3386 (** Creates a backtracking point. {!pop} *) 3387 val push : optimize -> unit 3388 3389 (** Backtrack one backtracking point. 3390 Note that an exception is thrown if Pop is called without a corresponding [Push] 3391 {!push} *) 3392 val pop : optimize -> unit 3393 3394 (** Retrieve explanation why optimize engine returned status Unknown. *) 3395 val get_reason_unknown : optimize -> string 3396 3397 (** Retrieve SMT-LIB string representation of optimize object. *) 3398 val to_string : optimize -> string 3399 3400 (** Retrieve statistics information from the last call to check *) 3401 val get_statistics : optimize -> Statistics.statistics 3402 3403 (** Parse an SMT-LIB2 file with assertions, soft constraints and optimization 3404 objectives. Add the parsed constraints and objectives to the optimization 3405 context. *) 3406 val from_file : optimize -> string -> unit 3407 3408 (** Parse an SMT-LIB2 string with assertions, soft constraints and optimization 3409 objectives. Add the parsed constraints and objectives to the optimization 3410 context. *) 3411 val from_string : optimize -> string -> unit 3412 3413 (** Return the set of asserted formulas on the optimization context. *) 3414 val get_assertions : optimize -> Expr.expr list 3415 3416 (** Return objectives on the optimization context. If the objective function 3417 is a max-sat objective it is returned as a Pseudo-Boolean (minimization) 3418 sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...). If the objective 3419 function is entered as a maximization objective, then return the 3420 corresponding minimization objective. In this way the resulting 3421 objective function is always returned as a minimization objective. *) 3422 val get_objectives : optimize -> Expr.expr list 3423end 3424 3425 3426(** Functions for handling SMT and SMT2 expressions and files *) 3427module SMT : 3428sig 3429 (** Convert a benchmark into an SMT-LIB formatted string. 3430 3431 @return A string representation of the benchmark. *) 3432 val benchmark_to_smtstring : context -> string -> string -> string -> string -> Expr.expr list -> Expr.expr -> string 3433 3434 (** Parse the given string using the SMT-LIB2 parser. 3435 3436 @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *) 3437 val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector 3438 3439 (** Parse the given file using the SMT-LIB2 parser. *) 3440 val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector 3441end 3442 3443 3444(** Set a global (or module) parameter, which is shared by all Z3 contexts. 3445 3446 When a Z3 module is initialized it will use the value of these parameters 3447 when Z3_params objects are not provided. 3448 The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. 3449 The character '.' is a delimiter (more later). 3450 The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. 3451 Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". 3452 This function can be used to set parameters for a specific Z3 module. 3453 This can be done by using <module-name>.<parameter-name>. 3454 For example: 3455 (set_global_param "pp.decimal" "true") 3456 will set the parameter "decimal" in the module "pp" to true. 3457*) 3458val set_global_param : string -> string -> unit 3459 3460(** Get a global (or module) parameter. 3461 3462 Returns None if the parameter does not exist. 3463 The caller must invoke #Z3_global_param_del_value to delete the value returned at param_value. 3464 This function cannot be invoked simultaneously from different threads without synchronization. 3465 The result string stored in param_value is stored in a shared location. 3466*) 3467val get_global_param : string -> string option 3468 3469(** Restore the value of all global (and module) parameters. 3470 3471 This command will not affect already created objects (such as tactics and solvers) 3472 {!set_global_param} 3473*) 3474 3475val global_param_reset_all : unit -> unit 3476 3477(** Enable/disable printing of warning messages to the console. 3478 3479 Note that this function is static and effects the behaviour of 3480 all contexts globally. *) 3481val toggle_warning_messages : bool -> unit 3482 3483(** 3484 Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode. 3485 3486 Remarks: It is a NOOP otherwise. 3487*) 3488val enable_trace : string -> unit 3489 3490(** 3491 Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode. 3492 3493 Remarks: It is a NOOP otherwise. 3494*) 3495val disable_trace : string -> unit 3496 3497 3498(** Memory management **) 3499module Memory : 3500sig 3501 (** Reset all allocated resources **) 3502 val reset : unit -> unit 3503end 3504