diff --git a/website/README.md b/website/README.md index aaba2fa1e..08199f6bb 100644 --- a/website/README.md +++ b/website/README.md @@ -4,13 +4,14 @@ This website is built using [Docusaurus 2](https://docusaurus.io/), a modern sta ### Installation -``` +```sh +$ npm install $ yarn ``` ### Local Development -``` +```sh $ yarn start ``` @@ -18,7 +19,7 @@ This command starts a local development server and opens up a browser window. Mo ### Build -``` +```sh $ yarn build ``` @@ -28,13 +29,13 @@ This command generates static content into the `build` directory and can be serv Using SSH: -``` +```sh $ USE_SSH=true yarn deploy ``` Not using SSH: -``` +```sh $ GIT_USER= yarn deploy ``` diff --git a/website/docs-programming/01 - Z3 JavaScript Examples.md b/website/docs-programming/01 - Z3 JavaScript Examples.md index 2a1befd5b..b5079c0db 100644 --- a/website/docs-programming/01 - Z3 JavaScript Examples.md +++ b/website/docs-programming/01 - Z3 JavaScript Examples.md @@ -9,7 +9,7 @@ You can run and modify the examples locally in your browser. :::info The bindings do not support all features of z3. For example, you cannot (yet) create array expressions in the same way -that you can create arithmetic expressions. The JavaScript bindings have the distinct advantage that they allow to use +that you can create arithmetic expressions. The JavaScript bindings have the distinct advantage that they let you use z3 directly in your browser with minimal extra dependencies. ::: @@ -105,7 +105,7 @@ Z3.solve(Z3.Not(conjecture)); We illustrate how to use the solver in finding assignments of array values that satisfy a given predicate. In this example, we want to find two arrays of length 4 -that have the same sum, but are not equal. +that have the same sum, but are not equal: ```z3-js const { Array, BitVec } = Z3; @@ -164,7 +164,7 @@ Z3.solve(Z3.Not(conjecture)); we illustrate the use of the `Solver` object in the following example. Instead of calling `Z3.solve` we here create a solver object and add assertions to it. The `solver.check()` method is used to check -satisfiability (we expect the result to be `sat` for this example). The method `solver.model()` is used to retrieve a model. +satisfiability (we expect the result to be `sat` for this example). The method `solver.model()` is used to retrieve a model: ```z3-js const solver = new Z3.Solver(); @@ -203,7 +203,7 @@ Z3.solve(Z3.Not(conjecture)); ## Solve sudoku -The popular Sudoko can be solved. +The popular Sudoku can be solved. ```z3-js function toSudoku(data: string): (number | null)[][] { @@ -364,7 +364,7 @@ signed and unsigned bit-vectors. Instead the API supports operations that have different meaning depending on whether a bit-vector is treated as a signed or unsigned numeral. These are signed comparison and signed division, remainder operations. -In the following we illustrate the use of signed and unsigned less-than-or-equal. +In the following we illustrate the use of signed and unsigned less-than-or-equal: ```z3-js const x = Z3.BitVec.const('x', 32); @@ -417,7 +417,7 @@ const is_eq = (xv ^ yv) - 103n === (xv * yv) % 2n ** 32n; // true ## Using Z3 objects wrapped in JavaScript -The following example illustrates the use of AstVector +The following example illustrates the use of AstVector: ```z3-js const solver = new Z3.Solver(); diff --git a/website/docs-programming/04 - Parameters.md b/website/docs-programming/04 - Parameters.md index dbf171ccb..7fdb7c6e6 100644 --- a/website/docs-programming/04 - Parameters.md +++ b/website/docs-programming/04 - Parameters.md @@ -55,7 +55,7 @@ default_tactic | symbol | overwrite default tactic in strategic solver | propagate_values.max_rounds | unsigned int | maximal number of rounds to propagate values. | 4 solve_eqs.context_solve | bool | solve equalities within disjunctions. | true solve_eqs.ite_solver | bool | use if-then-else solvers. | true -solve_eqs.max_occs | unsigned int | maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295 +solve_eqs.max_occs | unsigned int | maximum number of occurrences for considering a variable for Gaussian eliminations. | 4294967295 solve_eqs.theory_solver | bool | use theory solvers. | true ## pp @@ -117,7 +117,7 @@ cce | bool | eliminate covered clauses | false core.minimize | bool | minimize computed core | false core.minimize_partial | bool | apply partial (cheap) core minimization | false cut | bool | enable AIG based simplification in-processing | false -cut.aig | bool | extract aigs (and ites) from cluases for cut simplification | false +cut.aig | bool | extract aigs (and ites) from clauses for cut simplification | false cut.delay | unsigned int | delay cut simplification by in-processing round | 2 cut.dont_cares | bool | integrate dont cares with cuts | true cut.force | bool | force redoing cut-enumeration until a fixed-point | false @@ -127,7 +127,7 @@ cut.redundancies | bool | integrate redundancy checking of cuts | true cut.xor | bool | extract xors from clauses for cut simplification | false ddfw.init_clause_weight | unsigned int | initial clause weight for DDFW local search | 8 ddfw.reinit_base | unsigned int | increment basis for geometric backoff scheme of re-initialization of weights | 10000 -ddfw.restart_base | unsigned int | number of flips used a starting point for hessitant restart backoff | 100000 +ddfw.restart_base | unsigned int | number of flips used a starting point for hesitant restart backoff | 100000 ddfw.threads | unsigned int | number of ddfw threads to run in parallel with sat solver | 0 ddfw.use_reward_pct | unsigned int | percentage to pick highest reward variable when it has reward 0 | 15 ddfw_search | bool | use ddfw local search instead of CDCL | false @@ -166,7 +166,7 @@ lookahead.cube.psat.clause_base | double | clause base for PSAT cutoff | 2 lookahead.cube.psat.trigger | double | trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat | 5 lookahead.cube.psat.var_exp | double | free variable exponent for PSAT cutoff | 1 lookahead.delta_fraction | double | number between 0 and 1, the smaller the more literals are selected for double lookahead | 1.0 -lookahead.double | bool | enable doubld lookahead | true +lookahead.double | bool | enable double lookahead | true lookahead.global_autarky | bool | prefer to branch on variables that occur in clauses that are reduced | false lookahead.preselect | bool | use pre-selection of subset of variables for branching | false lookahead.reward | symbol | select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu | march_cu @@ -262,7 +262,7 @@ enable_sls | bool | enable SLS tuning during weighted maxsat | false incremental | bool | set incremental mode. It disables pre-processing and enables adding constraints in model event handler | false lns_conflicts | unsigned int | initial conflict count for LNS search | 1000 maxlex.enable | bool | enable maxlex heuristic for lexicographic MaxSAT problems | true -maxres.add_upper_bound_block | bool | restict upper bound with constraint | false +maxres.add_upper_bound_block | bool | restrict upper bound with constraint | false maxres.hill_climb | bool | give preference for large weight cores | true maxres.max_core_size | unsigned int | break batch of generated cores if size reaches this number | 3 maxres.max_correction_set_size | unsigned int | allow generating correction set constraints up to maximal size | 3 @@ -272,10 +272,10 @@ maxres.pivot_on_correction_set | bool | reduce soft constraints if the current maxres.wmax | bool | use weighted theory solver to constrain upper bounds | false maxsat_engine | symbol | select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'rc2' | maxres optsmt_engine | symbol | select optimization engine: 'basic', 'symba' | basic -pb.compile_equality | bool | compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites) | false +pb.compile_equality | bool | compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalities) | false pp.neat | bool | use neat (as opposed to less readable, but faster) pretty printer when displaying context | true pp.wcnf | bool | print maxsat benchmark into wcnf format | false -priority | symbol | select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box' | lex +priority | symbol | select how to prioritize objectives: 'lex' (lexicographic), 'pareto', 'box' | lex rc2.totalizer | bool | use totalizer for rc2 encoding | true rlimit | unsigned int | resource limit (0 means no limit) | 0 solution_prefix | symbol | path prefix to dump intermediary, but non-optimal, solutions | @@ -294,7 +294,7 @@ conquer.restart.max | unsigned int | maximal number of restarts during conquer enable | bool | enable parallel solver by default on selected tactics (for QF_BV) | false simplify.exp | double | restart and inprocess max is multiplied by simplify.exp ^ depth | 1 simplify.inprocess.max | unsigned int | maximal number of inprocessing steps during simplification | 2 -simplify.max_conflicts | unsigned int | maximal number of conflicts during simplifcation phase | 4294967295 +simplify.max_conflicts | unsigned int | maximal number of conflicts during simplification phase | 4294967295 simplify.restart.max | unsigned int | maximal number of restarts during simplification phase | 5000 threads.max | unsigned int | caps maximal number of threads below the number of processors | 10000 @@ -317,7 +317,7 @@ real algebraic number package. Non-default parameter settings are not supported ----------|------|-------------|-------- factor | bool | use polynomial factorization to simplify polynomials representing algebraic numbers | true factor_max_prime | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31 -factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1 +factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifting and searching | 1 factor_search_size | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space | 5000 min_mag | unsigned int | Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16 zero_accuracy | unsigned int | one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0 @@ -563,7 +563,7 @@ core.minimize | bool | minimize unsat core produced by SMT context | false core.validate | bool | [internal] validate unsat core produced by SMT context. This option is intended for debugging | false cube_depth | unsigned int | cube depth. | 1 dack | unsigned int | 0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution | 1 -dack.eq | bool | enable dynamic ackermannization for transtivity of equalities | false +dack.eq | bool | enable dynamic ackermannization for transitivity of equalities | false dack.factor | double | number of instance per conflict | 0.1 dack.gc | unsigned int | Dynamic ackermannization garbage collection frequency (per conflict) | 2000 dack.gc_inv_decay | double | Dynamic ackermannization garbage collection decay | 0.8 diff --git a/website/docs-programming/06 - Proof Logs.md b/website/docs-programming/06 - Proof Logs.md index 0e89b7603..e2ede2b36 100644 --- a/website/docs-programming/06 - Proof Logs.md +++ b/website/docs-programming/06 - Proof Logs.md @@ -21,17 +21,20 @@ including for replaying tactics in Isabelle, for generation of interpolants, and separating hyper-planes from linear programming proofs (Farkas lemma). A separate format is used to trace inference steps for proof mining. Proof logs allow to simplify some of the infrastructure around proof reconstruction during search and for proof mining. The same logs -can be targetted for the different use cases. The survey [ProofsForSMT](https://z3prover.github.io/slides/proofs.html) discusses proof formats in use by SMT solvers and includes some additional technical details on proof logs. +can be targeted for the different use cases. The survey [ProofsForSMT](https://z3prover.github.io/slides/proofs.html) discusses proof formats in use by SMT solvers and includes some additional technical details on proof logs. ## Callbacks for clause inferences The API exposes a function `Z3_solver_register_on_clause` -that is first exposed for C, C++, .Net and Python. We here illustrate using -it from Python. The function lets a client register a callback function that is -invoked whenever the main SMT search engine makes an inference. The main inference -steps are (1) introducing an _assumption_, that is, a clause that is entained from the +that is first exposed for C, C++, .Net and Python. +Here we illustrate using it from Python. +This function lets a client register a callback that is +invoked whenever the main SMT search engine makes an inference. +The main inference +steps are (1) introducing an _assumption_, +that is, a clause that is entailed by the input formula (formally, the clause is satisfiability preserving when added to the input formula), (2) _deleting_ a clause from the set of active clauses, (3) _rup_, inferring a clause through propositional reasoning, the clause can be justified using @@ -77,7 +80,7 @@ def monitor_instances(): ### Monitor clauses annotated with detailed justifications If you set proof mode to _true_, then the inferred clauses are annotated by more detailed proof terms. The detailed proof terms -use a repetorire or low level inference rules. +use a repertoire or low level inference rules. ```z3-python def monitor_with_proofs(): @@ -150,7 +153,7 @@ encodings. The pair `-inst 2` indicates that two quantifier instantiations were not self-validated They were instead validated using a call to SMT solving. A log for an smt invocation is exemplified in the next line. -Note that the pair `+inst 6` indicates that 6 quantifier instantations were validated +Note that the pair `+inst 6` indicates that 6 quantifier instantiations were validated using a syntactic (cheap) check. Some quantifier instantiations based on quantifier elimination are not simple substitutions and therefore a simple syntactic check does not suffice. diff --git a/website/docs-smtlib/01 - logic/01 - intro.md b/website/docs-smtlib/01 - logic/01 - intro.md index 487f80e8c..f03084f29 100644 --- a/website/docs-smtlib/01 - logic/01 - intro.md +++ b/website/docs-smtlib/01 - logic/01 - intro.md @@ -6,7 +6,7 @@ sidebar_position: 1 Z3 is a state-of-the art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. Z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories. -The main objective of the tutorial is to introduce the reader on how to use Z3 effectively for logical modeling and solving. The tutorial provides some general background on logical modeling, but we have to defer a full introduction to first-order logic and decision procedures to text-books in order to develop an in depth understanding of the underlying concepts. To clarify: a deep understanding of logical modeling is not necessarily required to understand this tutorial and modeling with Z3, but it is necessary to understand for writing complex models. +The main objective of the tutorial is to introduce the reader on how to use Z3 effectively for logical modeling and solving. The tutorial provides some general background on logical modeling, but we defer a full introduction to first-order logic and decision procedures to text-books, if you want to develop an in-depth understanding of the underlying concepts. To clarify: a deep understanding of logical modeling is not required to understand this tutorial and modeling with Z3, but it is necessary for writing complex models. :::info @@ -18,16 +18,16 @@ The main objective of the tutorial is to introduce the reader on how to use Z3 e ::: -Z3 is a low level tool. It is best used as a component in the context of other tools that require solving logical formulas. Consequently, Z3 exposes a number of API facilities to make it convenient for tools to map into Z3, but there are no stand-alone editors or user-centric facilities for interacting with Z3. The language syntax used in the front ends favor simplicity in contrast to linguistic convenience. +Z3 is a low-level tool. It is best used as a component in the context of other tools that require solving logical formulas. Consequently, Z3 exposes a number of API facilities to make it convenient for tools to map into Z3, but there are no stand-alone editors or user-centric facilities for interacting with Z3. The language syntax used in the front ends favor simplicity in contrast to linguistic convenience. ## SMTLIB Format > This tutorial uses Z3's frontend for the [SMTLIB format](http://smtlib.cs.uiowa.edu/). -The format is a community standard used by several SMT solvers. -It uses LISP like syntax to make it easy for tools to serialize and de-serialize models. -On the flip-side it is not optimized for human readability. -The SMTLIB initiative defines several theories and z3 supports all main theories in the SMTLIB2 format. +The SMTLIB format is a community standard used by several SMT solvers. +It uses LISP-like syntax to make it easy for tools to serialize and de-serialize models. +On the flip-side, it is not optimized for human readability. +The SMTLIB initiative defines several theories, and Z3 supports all main theories in the SMTLIB2 format. This tutorial cross-references the definitions of theories in relevant sections. :::tip diff --git a/website/docs-smtlib/01 - logic/02 - basiccommands.md b/website/docs-smtlib/01 - logic/02 - basiccommands.md index 298c58374..2133c11a3 100644 --- a/website/docs-smtlib/01 - logic/02 - basiccommands.md +++ b/website/docs-smtlib/01 - logic/02 - basiccommands.md @@ -7,7 +7,9 @@ sidebar_position: 2 The Z3 input format is an extension of the one defined by the [SMT-LIB format](http://www.smtlib.org). ::: -A Z3 script is a sequence of commands. As an extension of the SMT-LIB format, this means that Z3 is not technically a programming language in the same way that Java, Python, or Javascript are - meaning there are no loops or variables as they are commonly understood on the whole. The help command displays a list of all available commands. The command `echo` displays a message. Internally, Z3 maintains a stack of user provided formulas and declarations. We say these are the assertions provided by the user. The command `declare-const` declares a constant of a given type (aka sort). The command `declare-fun` declares a function. In the following example, we declared a function that receives an integer and a Boolean and returns an integer. +A Z3 script is a sequence of commands. As an extension of the SMT-LIB format, this means that Z3 is not technically a programming language in the same way that Java, Python, or Javascript are; there are no loops or variables as they are commonly understood, for example. The `help` command displays a list of all available commands. The command `echo` displays a message. + +Internally, Z3 maintains a stack of user provided formulas and declarations. We say these are the assertions provided by the user. The command `declare-const` declares a constant of a given type (aka sort). The command `declare-fun` declares a function. In the following example, we declare a function `f` that receives an integer and a Boolean and returns an integer. ```z3 (echo "starting Z3...") @@ -15,7 +17,7 @@ A Z3 script is a sequence of commands. As an extension of the SMT-LIB format, th (declare-fun f (Int Bool) Int) ``` -The command assert adds a formula into the Z3 internal stack. We say the set of formulas in the Z3 stack is satisfiable if there is an interpretation (for the user declared constants and functions) that makes all asserted formulas true. +The `assert` command adds a formula to the Z3 internal stack. We say that the set of formulas in the Z3 stack is *satisfiable* if there is an interpretation (for the user declared constants and functions) that makes all asserted formulas true. ```z3 (declare-const a Int) @@ -25,9 +27,11 @@ The command assert adds a formula into the Z3 internal stack. We say the set of (check-sat) ``` -The first asserted formula states that the constant a must be less than 10. The second one states that the function f applied to a and true must return a value less than 100. The command check-sat determines whether the current formulas on the Z3 stack are satisfiable or not. If the formulas are satisfiable, Z3 returns sat. If they are not satisfiable (i.e., they are unsatisfiable), Z3 returns unsat. Z3 may also return unknown when it can't determine whether a formula is satisfiable or not. +The first asserted formula states that the constant `a` must be less than 10. The second one states that the function `f` applied to `a` and `true` must return a value less than 100. +The `check-sat` command determines whether the current formulas on the Z3 stack are satisfiable or not. If the formulas are satisfiable, Z3 returns `sat`. If they are not satisfiable, Z3 returns `unsat`. +Z3 may also return `unknown` if it can't determine whether a formula is satisfiable or not. -When the command check-sat returns sat, the command get-model can be used to retrieve an interpretation that makes all formulas on the Z3 internal stack true. +When the `check-sat` command returns `sat`, the `get-model` command can be used to retrieve an interpretation that makes all formulas on the Z3 internal stack true. ```z3 (declare-const a Int) @@ -53,12 +57,17 @@ is very similar to a function definition used in programming languages. In this > (ite (and (= x!1 11) (= x!2 false)) 21 0) -evaluates (returns) 21 when x!1 is equal to 11, and x!2 is equal to false. Otherwise, it returns 0. +evaluates to (returns) 21 when x!1 is equal to 11, and x!2 is equal to false. Otherwise, it returns 0. ## Using Scopes -In some applications, we want to explore several similar problems that share several definitions and assertions. We can use the commands push and pop for doing that. Z3 maintains a global stack of declarations and assertions. The command push creates a new scope by saving the current stack size. The command pop removes any assertion or declaration performed between it and the matching push. The check-sat and get-assertions commands always operate on the content of the global stack. +In some applications, we want to explore several similar problems that share several definitions and assertions. +We can use the commands `push` and `pop` for doing that. Z3 maintains a global stack of declarations and assertions. +The `push` command creates a new scope by saving the current stack size. +The `pop` command removes any assertion or declaration performed between it and the matching `push`. +The `check-sat` and `get-assertions` commands always operate on the content of the global stack. -In the following example, the command (assert p) signs an error because the pop command removed the declaration for p. If the last pop command is removed, then the error is corrected. +In the following example, the command `(assert p)` gives an error because `pop` removed the declaration for p. +If the last `pop` command is removed, then the error is corrected. ```z3 ignore-errors (declare-const x Int) @@ -77,10 +86,14 @@ In the following example, the command (assert p) signs an error because the pop (pop) (assert p) ; error, since declaration of p was removed from the stack ``` -The push and pop commands can optionally receive a numeral argument as specified by the SMT 2 language. +The `push` and `pop` commands can optionally receive a numeral argument +indicating how many stack levels to push or pop, +as specified by the SMT 2 language. ## Configuration -The command set-option is used to configure Z3. Z3 has several options to control its behavior. Some of these options (e.g., produce-proofs) can only be set before any declaration or assertion. We use the reset command to erase all assertions and declarations. After the reset command, all configuration options can be set. +The `set-option` command is used to configure Z3. +Z3 has several options to control its behavior. +Some of these options (e.g., produce-proofs) can only be set before any declaration or assertion. We use the `reset` command to erase all assertions and declarations. After `reset`, all configuration options can be set. ```z3 ignore-errors (set-option :print-success true) @@ -95,13 +108,15 @@ The command set-option is used to configure Z3. Z3 has several options to contro (set-option :produce-proofs false) ; ok ``` -The option print-success true is particularly useful when Z3 is being controlled by another application using pipes. In this mode, commands, that otherwise would not print any output, will print success. +The `print-success true` option is particularly useful when Z3 is being controlled by another application using pipes. In this mode, commands that otherwise would not print any output, will print `success`. -> There is a [summary of all parameters](../../programming/Parameters) +:::info +Here is a [summary of all parameters](../../programming/Parameters) +::: ### Additional commands -The command `(display t)` just applies the Z3 pretty printer to the given expression. The command `(simplify t)` displays a possibly simpler expression equivalent to t. This command accepts many different options, `(help simplify)` will display all available options. +The command `(display t)` just applies the Z3 pretty printer to the given expression. The command `(simplify t)` displays a possibly simpler expression equivalent to t. This command accepts many different options, and `(help simplify)` will display all available options. ```z3 (declare-const a (Array Int Int)) @@ -124,7 +139,7 @@ The define-sort command defines a new sort symbol that is an abbreviation for a > (define-sort [symbol] ([symbol]+) [sort]) -The following example defines several abbreviations for sort expressions. +The following example defines several abbreviations for sort expressions: ```z3 (define-sort IList () (List Int)) diff --git a/website/docs-smtlib/01 - logic/05 - Quantifiers.md b/website/docs-smtlib/01 - logic/05 - Quantifiers.md index 394c94e28..f55104353 100644 --- a/website/docs-smtlib/01 - logic/05 - Quantifiers.md +++ b/website/docs-smtlib/01 - logic/05 - Quantifiers.md @@ -466,7 +466,7 @@ The list fragment can encode properties about data-structures such as lists. For (= (state p) RUN)) (= (prio p) (prio (next p)))))) -;; Verifying Verification Conditions (VCs) for remove procdure +;; Verifying Verification Conditions (VCs) for remove procedure (declare-const x Ptr) ;; new-state, new-next, new-prev and new-prio represent the state ;; of the system after executing the remove procedure. @@ -569,7 +569,7 @@ The essentially almost uninterpreted fragment subsumes the previous fragments, a (= (state p) RUN)) (>= (prio p) (prio (next p)))))) -;; Verifying Verification Conditions (VCs) for remove procdure +;; Verifying Verification Conditions (VCs) for remove procedure (declare-const x Ptr) ;; new-state, new-next, new-prev and new-prio represent the state ;; of the system after executing the remove procedure. diff --git a/website/docs-smtlib/01 - logic/06 - Lambdas.md b/website/docs-smtlib/01 - logic/06 - Lambdas.md index 7c26e315e..2df7de02b 100644 --- a/website/docs-smtlib/01 - logic/06 - Lambdas.md +++ b/website/docs-smtlib/01 - logic/06 - Lambdas.md @@ -55,7 +55,7 @@ Thus, in z3 arrays are synonymous with function spaces. You can transition betwe functions using `as-array` to convert a function to an array and using function macros to treat an array as a function. The example also illustrates a subtle use of recursive function declarations. Functions declared using `define-fun-rec` are expanded on demand and therefore the function symbols are available as arguments to `as-array`. -This contrasts functinos declared using `define-fun` that are treated as macros that are expanded at parse time. Their function symbols cannot be passed to `as-array`. +This contrasts with functions declared using `define-fun` that are treated as macros that are expanded at parse time. Their function symbols cannot be passed to `as-array`. ```z3 (declare-fun f (Int) Int) diff --git a/website/docs-smtlib/01 - logic/07 - Recursive Functions.md b/website/docs-smtlib/01 - logic/07 - Recursive Functions.md index 0e4176ab1..6fd21392c 100644 --- a/website/docs-smtlib/01 - logic/07 - Recursive Functions.md +++ b/website/docs-smtlib/01 - logic/07 - Recursive Functions.md @@ -28,7 +28,7 @@ You can define recursive functions ``` Z3 unfolds the definition of recursive functions incrementally by iterative deepening: -it attempts first to establish satisfiabiltiy modulo a fixed bound on number of unfoldings; +it attempts first to establish satisfiability modulo a fixed bound on number of unfoldings; if the resulting formula is unsatisfiable _and_ the reason for unsatisfiability is due to the bound restriction, it increases the fixed bound incrementally. Note that this approach does not involve reasoning by induction that is often required to prove deeper properties of recursive functions. diff --git a/website/docs-smtlib/02 - theories/01 - Arithmetic.md b/website/docs-smtlib/02 - theories/01 - Arithmetic.md index 568145140..ab19fb60c 100644 --- a/website/docs-smtlib/02 - theories/01 - Arithmetic.md +++ b/website/docs-smtlib/02 - theories/01 - Arithmetic.md @@ -17,7 +17,7 @@ Z3 supports the theory of arithmetic described in the following places. ## Basics -Z3 has builtin support for integer and real constants. This two types should not be confused with machine integers (32-bit or 64-bit) and floating point numbers. These two types (sorts) represent the mathematical integers and reals. The command declare-const is used to declare integer and real constants. +Z3 has built-in support for integer and real constants. These two types should not be confused with machine integers (32-bit or 64-bit) and floating point numbers. These two types (sorts) represent the mathematical integers and reals. The command `declare-const` is used to declare integer and real constants. ```z3 (declare-const a Int) @@ -28,7 +28,7 @@ Z3 has builtin support for integer and real constants. This two types should not ``` -After constants are declared, the user can assert.smt formulas containing these constants. The formulas contain arithmetic operators such as +, -, *, and so on. The command check-sat will instruct Z3 to try to find an interpretation for the declared constants that makes all formulas true. The interpretation is basically assigning a number to each constant. If such interpretation exists, we say it is a model for the asserted formulas. The command get-model displays the model built by Z3. +After constants are declared, the user can assert formulas containing that use these constants and arithmetic operators such as +, -, *, etc. The `check-sat` command instructs Z3 to try to find an interpretation for the declared constants that makes all formulas true. The interpretation is basically assigning a number to each constant. If such interpretation exists, we say it is a model for the asserted formulas. The command `get-model` displays the model built by Z3. ```z3 (declare-const a Int) @@ -124,7 +124,7 @@ of _difference arithmetic_ constraints. In the example we model three jobs, each job has two tasks to be completed by two workers. Thus, there are six variables for every task/worker combination. The start time of job 1 on worker 2 is given by `t12`. It has duration 1, so has to start at least one unit before -the completion deadline 8. It follows task `t11` which has duration 2 adn cannot overlap with other tasks on work station 2. +the completion deadline 8. It follows task `t11` which has duration 2 and cannot overlap with other tasks on work station 2. ## Non-linear arithmetic @@ -143,7 +143,7 @@ We say a formula is nonlinear if it contains expressions of the form (* t s) whe (assert (= (+ (* b b b) (sin (* b c))) 7)) (check-sat) -(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...") +(echo "yet it can show unsatisfiability for some nontrivial nonlinear problems...") (declare-const x Real) (declare-const y Real) (declare-const z Real) @@ -195,7 +195,7 @@ Actually, in Z3 all functions are total, although the result may be under-specif :::info We say that an interpreted function (such as `/`) is _under-specified_ when the meaning of the function is not fixed on all values of arguments. The division, modulus and remainder functions are _under-specified_ when the second argument is 0. Constraints that -allow the second arguments to these functions to be 0 can still be satisfiable when there are interepretations of the functions +allow the second arguments to these functions to be 0 can still be satisfiable when there are interpretations of the functions at 0 that satisfy the constraints. ::: @@ -207,12 +207,12 @@ at 0 that satisfy the constraints. (get-model) ; Although division by zero is not specified, division is still a function. -; So, (/ a 0.0) cannot evaluated to 10.0 and 2.0. +; Therefore, (/ a 0.0) cannot evaluate to both 10.0 and 2.0. (assert (= (/ a 0.0) 2.0)) (check-sat) ``` -If you are not happy with this behavior, you may use ite (if-then-else) operator to guard every division, and assign whatever interpretation you like to the division by zero. This example uses define-fun constructor to create a new operator mydiv. This is essentially a macro, and Z3 will expand its definition for every application of mydiv. +If you are not happy with this behavior, you may use the `ite` (if-then-else) operator to guard every division, and assign whatever interpretation you like to the division by zero. This example uses define-fun constructor to create a new operator mydiv. This is essentially a macro, and Z3 will expand its definition for every application of mydiv. ```z3 ; defining my own division operator where x0.0 == 0.0 for every x. @@ -232,9 +232,9 @@ If you are not happy with this behavior, you may use ite (if-then-else) operator Z3 contains a combination of several engines for solving arithmetic formulas. The engines are invoked based on the shape of arithmetic formulas. For linear real arithmetic formulas it uses dual simplex to determine feasibility. -For linear integer arithmetic formulas it uses thechniques from integer programming: cuts and branch and bound. +For linear integer arithmetic formulas it uses techniques from integer programming: cuts and branch and bound. There are specialized solvers for different arithmetic fragments and, finally, for non-linear arithmetic -constraints z3 contains several small hammers that integrate Grobner basis simplificaitons, bounds propagation, +constraints z3 contains several small hammers that integrate Grobner basis simplifications, bounds propagation, non-linear cylindric algebraic decomposition and reducing non-linear constraints to linear form by sampling at tangent points. Logic| Fragment | Solver | Example diff --git a/website/docs-smtlib/03 - strategies/01 - intro.md b/website/docs-smtlib/03 - strategies/01 - intro.md index 5ca4af123..b8c63aa0b 100644 --- a/website/docs-smtlib/03 - strategies/01 - intro.md +++ b/website/docs-smtlib/03 - strategies/01 - intro.md @@ -3,7 +3,7 @@ title: Introduction sidebar_position: 1 --- -High-performance solvers, such as Z3, contain many tightly integrated, handcrafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform very badly on new classes of problems. This issue is becoming increasingly pressing as solvers begin to gain the attention of practitioners in diverse areas of science and engineering. In many cases, changes to the solver heuristics can make a tremendous difference. +High-performance solvers, such as Z3, contain many tightly integrated, handcrafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform very badly on new classes of problems. This issue is becoming increasingly pressing as solvers gain the attention of practitioners in diverse areas of science and engineering. In many cases, changes to the solver heuristics can make a tremendous difference. In this tutorial we show how to create custom strategies using the basic building blocks available in Z3. Z3 implements the ideas proposed in this [article](https://web.archive.org/web/20190206110824/http://research.microsoft.com/en-us/um/people/leonardo/strategy.pdf). diff --git a/website/docs-smtlib/03 - strategies/02 - goals.md b/website/docs-smtlib/03 - strategies/02 - goals.md index be386ce42..daf8cc325 100644 --- a/website/docs-smtlib/03 - strategies/02 - goals.md +++ b/website/docs-smtlib/03 - strategies/02 - goals.md @@ -3,11 +3,13 @@ title: Goals sidebar_position: 2 --- -Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic reasoning steps are represented as functions known as tactics, and tactics are composed using combinators known as tacticals. Tactics process sets of formulas called Goals. +Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic reasoning steps are represented as functions known as *tactics*, and tactics are composed using combinators known as *tacticals*. Tactics process sets of formulas called Goals. -When a tactic is applied to some goal G, four different outcomes are possible. In SMT 2.0, the goal is the conjunction of all assertions. The tactic succeeds in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi. +When a tactic is applied to some goal G, four different outcomes are possible. In SMT 2.0, the goal is the conjunction of all assertions. The tactic succeeds in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, we face the problem of model conversion. A model converter constructs a model for G using a model for some subgoal Gi. -In the following example, we use the command apply to execute a tactic composed of two built-in tactics: simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted only to linear arithmetic. It can also eliminate arbitrary variables. Then, combinator then applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. In this example, only one subgoal is produced. +In the following example, we use the command `apply` to execute a tactic composed of two built-in tactics: `simplify` and `solve-eqs`. The tactic `simplify` applies transformations equivalent to the ones found in the `simplify` command. +The tactic `solve-eqs` eliminates variables using Gaussian elimination. +Actually, `solve-eqs` is not restricted linear arithmetic, but can also eliminate arbitrary variables. The combinator `then` applies `simplify` to the input goal and `solve-eqs` to each subgoal produced by `simplify`. In this example, only one subgoal is produced. ```z3 (declare-const x Real) @@ -20,9 +22,10 @@ In the following example, we use the command apply to execute a tactic composed (apply (then simplify solve-eqs)) ``` -In the example above, variable x is eliminated, and is not present the resultant goal. +In the example above, variable x is eliminated, and is not present in the resultant goal. -In Z3, we say a clause is any constraint of the form (or f_1 ... f_n). The tactic split-clause will select a clause (or f_1 ... f_n) in the input goal, and split it n subgoals. One for each subformula f_i. +In Z3, a *clause* is any constraint of the form `(or f_1 ... f_n)`. +The tactic `split-clause` will select a clause `(or f_1 ... f_n)` in the input goal, and split it into n subgoals, one for each subformula `f_i`. ```z3 (declare-const x Real) diff --git a/website/docs-smtlib/03 - strategies/03 - tactics.md b/website/docs-smtlib/03 - strategies/03 - tactics.md index efb1c5c25..7f102be92 100644 --- a/website/docs-smtlib/03 - strategies/03 - tactics.md +++ b/website/docs-smtlib/03 - strategies/03 - tactics.md @@ -59,7 +59,7 @@ A tactic can be used to decide whether a set of assertions has a solution (i.e., In the example above, the tactic used implements a basic bit-vector solver using equation solving, bit-blasting, and a propositional SAT solver. -In the following example, we use the combinator using-params to configure our little solver. We also include the tactic aig which tries to compress Boolean formulas using And-Inverted Graphs. +In the following example, we use the combinator using-params to configure our little solver. We also include the tactic `aig` which tries to compress Boolean formulas using And-Inverted Graphs. ```z3 (declare-const x (_ BitVec 16)) @@ -78,7 +78,7 @@ In the following example, we use the combinator using-params to configure our li (get-value ((bvand x y))) ``` -The tactic `smt` wraps the main solver in Z3 as a tactic. +The tactic `smt` wraps the main solver in Z3 as a tactic: ```z3 (declare-const x Int) @@ -90,7 +90,7 @@ The tactic `smt` wraps the main solver in Z3 as a tactic. (get-model) ``` -Now, we show how to implement a solver for integer arithmetic using SAT. The solver is complete only for problems where every variable has a lower and upper bound. +We now show how to implement a solver for integer arithmetic using SAT. The solver is complete only for problems where every variable has a lower and upper bound: ```z3 (declare-const x Int) diff --git a/website/docs-smtlib/04 - optimization/01 - intro.md b/website/docs-smtlib/04 - optimization/01 - intro.md index 87ded4571..826a93c20 100644 --- a/website/docs-smtlib/04 - optimization/01 - intro.md +++ b/website/docs-smtlib/04 - optimization/01 - intro.md @@ -3,5 +3,9 @@ title: Introduction sidebar_position: 1 --- -Z3's main functionality to checking the satisfiability of logical formulas over one or more theories. Z3 can produce models for satisfiable formulas. Yet in many cases arbitrary models are insufficient and applications are really solving optimization problems: one or more values should be minimal or maximal. When there are multiple objectives, they should be combined using Pareto fronts, lexicographic priorities, or optimized independently. This section describes a feature exposed by Z3 that lets users formulate objective functions directly with Z3. Under the hood is a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. +Z3's main functionality is checking the satisfiability of logical formulas over one or more theories. Z3 can also produce models for satisfiable formulas. +However, arbitrary models are insufficient in many cases where applications are really solving optimization problems: +one or more values should be minimal or maximal. When there are multiple objectives, they should be combined using Pareto fronts, lexicographic priorities, or optimized independently. + +This section describes a feature exposed by Z3 that lets users formulate objective functions directly with Z3. Under the hood is a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. diff --git a/website/docs-smtlib/04 - optimization/02 - apioptimization.md b/website/docs-smtlib/04 - optimization/02 - apioptimization.md index 6eff61335..d790d1479 100644 --- a/website/docs-smtlib/04 - optimization/02 - apioptimization.md +++ b/website/docs-smtlib/04 - optimization/02 - apioptimization.md @@ -4,7 +4,7 @@ sidebar_position: 2 --- Z3's programmatic [API](https://z3prover.github.io/api/html/) exposes all available optimization features. -- [Follow this link for a tutorial on using optimization features from F#.](http://lonelypad.blogspot.dk/2014/08/f-and-linear-programming-introduction.html). +- [Follow this link for a tutorial on using optimization features from F#.](http://lonelypad.blogspot.dk/2014/08/f-and-linear-programming-introduction.html) - The Python API is also convenient for prototyping. The Optimize Python object is used when solving constraints with optimization objectives. diff --git a/website/docs-smtlib/04 - optimization/03 - arithmeticaloptimization.md b/website/docs-smtlib/04 - optimization/03 - arithmeticaloptimization.md index 72264bdbb..af13d31af 100644 --- a/website/docs-smtlib/04 - optimization/03 - arithmeticaloptimization.md +++ b/website/docs-smtlib/04 - optimization/03 - arithmeticaloptimization.md @@ -9,7 +9,7 @@ Command | Meaning ---------------------------------------|------------------------------------------------------------------- `(maximize t)` | The result of `(check-sat)` should seek to produce a model that _maximizes_ the value of `t`. The expression can be integer, real or Bit-vector sort. `(minimize t)` | The result of `(check-sat)` should seek to produce a model that _minimizes_ the value of `t` The expression can be integer, real or Bit-vector sort. -`(add-soft b [:weight w] [:id id])` | The result of `(check-sat)` should seek to satisfy soft constraints. The default weigth is 1. Weights are used to give priorities. Soft constraints can be grouped in disjoint groups by tagging them with optional identifiers. +`(add-soft b [:weight w] [:id id])` | The result of `(check-sat)` should seek to satisfy soft constraints. The default weight is 1. Weights are used to give priorities. Soft constraints can be grouped in disjoint groups by tagging them with optional identifiers. `(get-objectives)` | After `(check-sat)` retrieve the values of the maximize, minimize and soft constraint objectives. diff --git a/website/docs-smtlib/04 - optimization/04 - softconstraints.md b/website/docs-smtlib/04 - optimization/04 - softconstraints.md index 079e8b04e..8c28a3170 100644 --- a/website/docs-smtlib/04 - optimization/04 - softconstraints.md +++ b/website/docs-smtlib/04 - optimization/04 - softconstraints.md @@ -40,7 +40,7 @@ Floating point and integer weights can be mixed; internally weights are converte (get-model) ``` -You can use identifiers to group soft constraints. You can also repeat the same soft constraint. Every repetition counts independently. In the example we add the soft constrsaint `a` twice and force it to be false. The penalty for group `x` is therefore 2. The penalty for group `y` is because there is only one soft constraint that is impossible to satisfy. +You can use identifiers to group soft constraints. You can also repeat the same soft constraint. Every repetition counts independently. In the example we add the soft constraint `a` twice and force it to be false. The penalty for group `x` is therefore 2. The penalty for group `y` is because there is only one soft constraint that is impossible to satisfy. ```z3 (declare-const a Bool) diff --git a/website/docs-smtlib/04 - optimization/07 - advancedtopics.md b/website/docs-smtlib/04 - optimization/07 - advancedtopics.md index 75b14161f..60b285559 100644 --- a/website/docs-smtlib/04 - optimization/07 - advancedtopics.md +++ b/website/docs-smtlib/04 - optimization/07 - advancedtopics.md @@ -5,7 +5,8 @@ sidebar_position: 7 ## Difference Logic -Z3 uses by default an implementation of dual Simplex to solve feasibility and primal Simplex for optimality. For arithmetical constraints that only have differences between variables, known as difference logic, Z3 furthermore contains alternative decision procedures tuned for this domain. These have to be configured explicitly. There is a choice between a solver tuned for sparse constraints (where the ratio of variables is high compared to number of inequalities) and a solver tuned for dense constraints. +By default, Z3 uses dual Simplex to solve feasibility, and primal Simplex for optimality. +For arithmetical constraints that only have differences between variables, known as *difference logic*, Z3 contains alternative decision procedures tuned for this domain. These have to be configured explicitly. There is a choice between a solver tuned for sparse constraints (where the ratio of variables is high compared to number of inequalities) and a solver tuned for dense constraints. ```z3 (set-option :smt.arith.solver 1) ; enables difference logic solver for sparse constraints @@ -21,9 +22,10 @@ Z3 uses by default an implementation of dual Simplex to solve feasibility and pr ## Weighted Max-SAT solvers, a portfolio -The default solver for MaxSAT problems is the MaxRes algorithm. Several other alternative solvers are available. The default solver -is chosen based on benchmarking against MaxSAT competition benchmarks, but other solver combinations, such as wmax, may work well for some domains. -When the objectives are weighted by weights such as 1, 2, 4, 8, 16, such that the sum of weights in every prefix is lower than the next weight, the solver +The default solver for MaxSAT problems is the MaxRes algorithm. +Several alternative solvers are available. The default solver +is chosen based on benchmarking against MaxSAT competition benchmarks, but other solver combinations, such as `wmax`, may work well for some domains. +When the objectives have weights such as 1, 2, 4, 8, 16, such that the sum of weights in every prefix is lower than the next weight, the solver uses a lexicographic optimization algorithm that attempts to first solve for the highest weight before continuing with lower weights. The other main MaxSAT algorithms available are @@ -44,7 +46,7 @@ For example, the constraints (check-sat) ``` -get rewritten internally to a problem of the form +are rewritten internally to a problem of the form ```z3 (declare-const x Bool) @@ -57,7 +59,7 @@ You can disable this transformation by setting (set-option :opt.elim_01 false) ``` -For problems that are either already bit-vector or Boolean or can be rewritten to this form, the engine uses a core solver based on a tuned SAT solver. +For problems that are already bit-vector or Boolean, or can be rewritten to this form, the engine uses a core solver based on a tuned SAT solver. You can turn off the use of the SAT solver by setting: ```z3