Dev

website/docs-programming/02 - Z3 Python - Readonly/01 - Introduction.md

@@ -857,21 +857,22 @@ package. This variable is true if the package must be in the system. If package
 packages `b`, `c` and `z`, we write:
 
 
-```z3-python
+```
 DependsOn(a, [b, c, z])
 ```
 
 `DependsOn` is a simple Python function that creates Z3 constraints that capture the 
 depends clause semantics.
 
 
+
 ```z3-py
 def DependsOn(pack, deps):
    return And([ Implies(pack, dep) for dep in deps ])
 ```
 
 
-Thus, `DependsOn(a, [b, c, z])` generates the constraint
+Thus, `DependsOn(a, [b, c, z])` generates the constraint.
 
 
 ```

website/docs-programming/02 - Z3 Python - Readonly/02 - advanced.md

@@ -45,7 +45,7 @@ is equal to <tt>n2.hash()</tt>.
 x = Int('x')
 print (x + 1).hash()
 print (1 + x).hash()
-print x.sort().hash()
+print (x.sort().hash())
 ```
 
 Z3 expressions can be divided in three basic groups: **applications**,

website/docs-programming/02 - Z3 Python - Readonly/03 - Strategies.md

@@ -53,12 +53,12 @@ and `solve-eqs` to each subgoal produced by `simplify`. In this example, only on
 x, y = Reals('x y')
 g  = Goal()
 g.add(x > 0, y > 0, x == y + 2)
-print g
+print (g)
 
 t1 = Tactic('simplify')
 t2 = Tactic('solve-eqs')
 t  = Then(t1, t2)
-print t(g)
+print (t(g))
 ```
 
 In the example above, variable `x` is eliminated, and is not present the resultant goal.
@@ -76,7 +76,7 @@ g.add(Or(x < 0, x > 0), x == y + 1, y < 0)
 t = Tactic('split-clause')
 r = t(g)
 for g in r: 
-    print g
+    print (g)
 ```
 
 ## Tactics 
@@ -115,7 +115,7 @@ g.add(Or(x == 0, x == 1),
 # Split all clauses"
 split_all = Repeat(OrElse(Tactic('split-clause'),
                           Tactic('skip')))
-print split_all(g)
+print (split_all(g))
 
 split_at_most_2 = Repeat(OrElse(Tactic('split-clause'),
                           Tactic('skip')),
@@ -127,7 +127,7 @@ split_solve = Then(Repeat(OrElse(Tactic('split-clause'),
                                  Tactic('skip'))),
                    Tactic('solve-eqs'))
 
-print split_solve(g)
+print (split_solve(g))
 ```
 
 In the tactic `split_solver`, the tactic `solve-eqs` discharges all but one goal.
@@ -147,7 +147,7 @@ g.add(Or(x == 0, x == 1),
 split_all = Repeat(OrElse(Tactic('split-clause'),
                           Tactic('skip')))
 for s in split_all(g):
-    print s
+    print (s)
 ```
 
 A tactic can be converted into a solver object using the method `solver()`.
@@ -186,9 +186,9 @@ x, y = BitVecs('x y', 16)
 bv_solver.add(x*32 + y == 13, x & y < 10, y > -100)
 print bv_solver.check()
 m = bv_solver.model()
-print m
-print x*32 + y, "==", m.evaluate(x*32 + y)
-print x & y, "==", m.evaluate(x & y)
+print (m)
+print (x*32 + y, "==", m.evaluate(x*32 + y))
+print (x & y, "==", m.evaluate(x & y))
 ```
 
 
@@ -198,8 +198,8 @@ The tactic `smt` wraps the main solver in Z3 as a tactic.
 x, y = Ints('x y')
 s = Tactic('smt').solver()
 s.add(x > y + 1)
-print s.check()
-print s.model()
+print s(.check())
+print (s.model())
 ```
 
 Now, we show how to implement a solver for integer arithmetic using SAT. The solver is complete
@@ -238,15 +238,15 @@ g.add(x > 10, y == x + 3, z > y)
 
 r = t(g)
 # r contains only one subgoal
-print r
+print (r)
 
 s = Solver()
 s.add(r[0])
-print s.check()
+print (s.check())
 # Model for the subgoal
-print s.model()
+print (s.model())
 # Model for the original goal
-print r.convert_model(s.model())
+print (r.convert_model(s.model()))
 ```
 
 ### Using tactics to simplify benchmarks
@@ -331,7 +331,7 @@ g.add(x**2 - y**2 >= 0)
 p = Probe('num-consts')
 t = If(p > 2, 'simplify', 'factor')
 
-print t(g)
+print (t(g))
 
 g = Goal()
 g.add(x + x + y + z >= 0, x**2 - y**2 >= 0)

website/docs-programming/06 - Proof Logs.md

@@ -325,3 +325,74 @@ rup []
 ```
 
 SMT proofs are of course generally much larger.
+
+
+## Proof trimming
+
+You can trim proofs. Consider the following example:
+
+```
+(set-option :sat.euf true)
+(set-option :tactic.default_tactic smt)
+(set-option :solver.proof.log log.smt2)
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const d Bool)
+
+(assert (or a (not b)))
+(assert (or b (not c)))
+(assert (or c (not d)))
+(assert (or d (not a)))
+(assert a)
+(assert (not c))
+(check-sat)
+```
+
+The contents of log.smt2:
+
+```
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(assume a (not b))
+(declare-fun c () Bool)
+(assume b (not c))
+(declare-fun d () Bool)
+(assume c (not d))
+(assume (not a) d)
+(assume a)
+(assume (not c))
+(declare-fun rup () Proof)
+(infer d rup)
+(infer rup)
+```
+
+Let us trim the proof.
+
+```
+z3 log.smt2 solver.proof.trim=true
+```
+
+The trimmed proof is printed to standard output.
+A side-effect of trimming is a collection of dependencies that are included as arguments to a term that justifies
+assumptions or inferences. Assumptions have a single number in the dependency. The number is used to identify the assumption.
+Inferences list a fresh number followed by premises used by unit propagation to infer the clause.
+
+```
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(declare-fun deps (Int) Proof)
+(define-const $32 Proof (deps 2))
+(assume c (not d) $32)
+(declare-fun a () Bool)
+(define-const $34 Proof (deps 3))
+(assume (not a) d $34)
+(define-const $36 Proof (deps 4))
+(assume a $36)
+(define-const $38 Proof (deps 5))
+(assume (not c) $38)
+(declare-fun rup () Proof)
+(declare-fun deps (Int Int Int Int Int) Proof)
+(define-const $40 Proof (deps 7 2 3 4 5))
+(infer rup $40)
+```

website/docs-programming/08 - Rust.md

@@ -0,0 +1,12 @@
+---
+
+title: Rust
+
+sidebar_position: 8
+
+---
+
+
+
+* [Rust documentation](https://docs.rs/z3-sys/latest/z3_sys/)
+* [Extended set of Rust use cases](https://microsoft.github.io/z3guide/static/doc/z3_rust_guide.pdf)

website/solutions/z3/4.12.1/c2bff7c817eaf3ecbf17da41d3737f4d09698d6e/input.json

@@ -0,0 +1 @@
+{"input":"(simplify (bvadd #x07 #x03)) ; addition\n(simplify (bvsub #x07 #x03)) ; subtraction\n(simplify (bvneg #x07)) ; unary minus\n(simplify (bvmul #x07 #x03)) ; multiplication\n(simplify (bvudiv #x07 #x03)) ; unsigned division\n(simplify (bvsdiv #x07 #x03)) ; signed division\n(simplify (bvurem #x07 #x03)) ; unsigned remainder\n(simplify (bvsrem #x07 #x03)) ; signed remainder\n(simplify (bvsmod #x07 #x03)) ; signed modulo\n(simplify (bvshl #x07 #x03)) ; shift left\n(simplify (bvlshr #xf0 #x03)) ; unsigned (logical) shift right\n(simplify (bvashr #xf0 #x03)) ; signed (arithmetical) shift right"}

website/solutions/z3/4.12.1/c2bff7c817eaf3ecbf17da41d3737f4d09698d6e/output.json

@@ -0,0 +1 @@
+{"output":"#x0a\n#x04\n#xf9\n#x15\n#x02\n#x02\n#x01\n#x01\n#x01\n#x38\n#x1e\n#xfe\n","error":"","status":"z3-ran","hash":"c2bff7c817eaf3ecbf17da41d3737f4d09698d6e"}