simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

test: update doc guide

Browse source
This commit is contained in:
Simon Cruanes 2022-09-26 20:57:55 -04:00
parent dbe64f5975
commit 1c11a82a7d
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
doc/guide.md
View file

@ -209,11 +209,11 @@ We start with `p = q`.
- : Solver.res =
Sidekick_smt_solver.Solver.Sat
(model
(false := false)
(p := true)
(q := true)
((box (= Bool p q)) := true)
(true := true)
(p := true))
(false := false)
([[ (= p q) ]] := true))
```
It is satisfiable, and we got a model where "p" and "q" are both false.
@ -246,11 +246,11 @@ Note that this doesn't affect satisfiability without assumptions:
- : Solver.res =
Sidekick_smt_solver.Solver.Sat
(model
(false := false)
(p := true)
(q := true)
((box (= Bool p q)) := true)
(true := true)
(p := true))
(false := false)
([[ (= p q) ]] := true))
```
We can therefore add more formulas and see where it leads us.
@ -264,13 +264,13 @@ We can therefore add more formulas and see where it leads us.
- : Solver.res =
Sidekick_smt_solver.Solver.Sat
(model
(false := false)
(p := true)
(q := true)
((box (= Bool p q)) := true)
(r := true)
((box (or r (not p) false)) := true)
(true := true)
(p := true))
(false := false)
([[ (= p q) ]] := true)
([[ (or r (not p) false) ]] := true))
```
Still satisfiable, but now we see `r` in the model, too. And now:
@ -331,12 +331,12 @@ We can play with assertions now:
- : Solver.res =
Sidekick_smt_solver.Solver.Sat
(model
(b := 0)
(true := true)
(false := false)
((box (<= (+ a ((* -1) b)) 0)) := true)
($_le_comb[0] := 0)
(a := 0)
(true := true))
(b := 0)
([[ (<= (+ a ((* -1) b)) 0) ]] := true)
($_le_comb[0] := 0))
# let a_geq_1 = LRA_term.geq tstore a (LRA_term.const tstore (Q.of_int 1));;