mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +00:00
Code Activity

Fix typos in examples.

Browse source
This commit is contained in:
Bruce Mitchener 2019-08-15 11:39:44 +07:00 • committed by Nikolaj Bjorner
parent ec5b148ecc
commit 0edd587e5a
9 changed files with 12 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
examples/python/tutorial/jupyter/advanced.ipynb
View file

@ -527,7 +527,7 @@
"source": [
"Nevertheless, Z3 is often able to handle formulas involving quantifiers. It uses several approaches to handle quantifiers. The most prolific approach is using pattern-based quantifier instantiation. This approach allows instantiating quantified formulas with ground terms that appear in the current search context based on pattern annotations on quantifiers. Z3 also contains a model-based quantifier instantiation component that uses a model construction to find good terms to instantiate quantifiers with; and Z3 also handles many decidable fragments.\n",
"\n",
"Note that in the previous example the constants x and y were used to create quantified formulas. This is a \"trick\" for simplifying the construction of quantified formulas in Z3Py. Internally, these constants are replaced by bounded variables. The next example demonstrates that. The method body() retrives the quantified expression. In the resultant formula the bounded variables are free. The function Var(index, sort) creates a bounded/free variable with the given index and sort."
"Note that in the previous example the constants x and y were used to create quantified formulas. This is a \"trick\" for simplifying the construction of quantified formulas in Z3Py. Internally, these constants are replaced by bounded variables. The next example demonstrates that. The method body() retrieves the quantified expression. In the resultant formula the bounded variables are free. The function Var(index, sort) creates a bounded/free variable with the given index and sort."
]
},
{
@ -626,7 +626,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"When the more permissive pattern g(x) is used. Z3 proves the formula to be unsatisfiable. More restrive patterns minimize the number of instantiations (and potentially improve performance), but they may also make Z3 \"less complete\"."
"When the more permissive pattern g(x) is used. Z3 proves the formula to be unsatisfiable. More restrictive patterns minimize the number of instantiations (and potentially improve performance), but they may also make Z3 \"less complete\"."
]
},
{