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

doc: update guide for now

Browse source
This commit is contained in:
Simon Cruanes 2022-09-10 15:02:17 -04:00
parent b8ee815d9d
commit 87e91660ad
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 12 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
doc/guide.md
View file

@ -209,10 +209,10 @@ We start with `p = q`.
- : Solver.res = - : Solver.res =
Sidekick_smt_solver.Solver.Sat Sidekick_smt_solver.Solver.Sat
(model (model
(false := false)
(q := true) (q := true)
(true := true)
((= Bool p q) := true) ((= Bool p q) := true)
(false := $@c[0]) (true := true)
(p := true)) (p := true))
``` ```
@ -246,10 +246,10 @@ Note that this doesn't affect satisfiability without assumptions:
- : Solver.res = - : Solver.res =
Sidekick_smt_solver.Solver.Sat Sidekick_smt_solver.Solver.Sat
(model (model
(false := false)
(q := false) (q := false)
(true := true)
((= Bool p q) := true) ((= Bool p q) := true)
(false := $@c[0]) (true := true)
(p := false)) (p := false))
``` ```
@ -264,12 +264,12 @@ We can therefore add more formulas and see where it leads us.
- : Solver.res = - : Solver.res =
Sidekick_smt_solver.Solver.Sat Sidekick_smt_solver.Solver.Sat
(model (model
(false := false)
(q := false) (q := false)
(r := true) (r := true)
(true := true)
((= Bool p q) := true) ((= Bool p q) := true)
((or r (not p) false) := true) ((box (or r (not p) false)) := true)
(false := $@c[0]) (true := true)
(p := false)) (p := false))
``` ```
@ -331,20 +331,12 @@ We can play with assertions now:
- : Solver.res = - : Solver.res =
Sidekick_smt_solver.Solver.Sat Sidekick_smt_solver.Solver.Sat
(model (model
(+ := $@c[4]) (false := false)
((box (<= (+ a ((* -1) b)) 0)) := true)
($_le_comb[0] := 0)
(a := 0) (a := 0)
((+ a) := $@c[2])
(0 := 0)
(b := 0) (b := 0)
((+ a ((* -1) b)) := $@c[0]) (true := true))
((<= (+ a ((* -1) b))) := $@c[6])
((* -1) := $@c[5])
(true := true)
((<= (+ a ((* -1) b)) 0) := true)
(((* -1) b) := $@c[1])
(<= := $@c[3])
(false := $@c[7])
($_le_comb[0] := 0))
# let a_geq_1 = LRA_term.geq tstore a (LRA_term.const tstore (Q.of_int 1));; # let a_geq_1 = LRA_term.geq tstore a (LRA_term.const tstore (Q.of_int 1));;
@ -361,7 +353,7 @@ val res : Solver.res =
{Sidekick_smt_solver.Solver.unsat_core = <fun>; unsat_step_id = <fun>} {Sidekick_smt_solver.Solver.unsat_core = <fun>; unsat_step_id = <fun>}
# match res with Solver.Unsat {unsat_core=us; _} -> us() |> Iter.to_list | _ -> assert false;; # match res with Solver.Unsat {unsat_core=us; _} -> us() |> Iter.to_list | _ -> assert false;;
- : Proof_trace.lit list = [(>= a 1); (<= b 1/2)] - : Proof_trace.lit list = [[[ (>= a 1) ]]; [[ (<= b 1/2) ]]]
``` ```
This just showed that `a=1, b=1/2, a>=b` is unsatisfiable. This just showed that `a=1, b=1/2, a>=b` is unsatisfiable.