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

doc: update guide (models changed, more printers needed)

Browse source
This commit is contained in:
Simon Cruanes 2021-08-07 21:09:20 -04:00
parent bef0c810d3
commit feff94bdbb
1 changed files with 22 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
doc/guide.md
View file

@ -100,7 +100,6 @@ for legibility:
# #install_printer Ty.pp;; # #install_printer Ty.pp;;
# #install_printer Fun.pp;; # #install_printer Fun.pp;;
# #install_printer Model.pp;; # #install_printer Model.pp;;
# #install_printer Solver.Atom.pp;;
# #install_printer Solver.Model.pp;; # #install_printer Solver.Model.pp;;
# #install_printer Proof.pp_debug;; # #install_printer Proof.pp_debug;;
Proof.pp_debug has a wrong type for a printing function. Proof.pp_debug has a wrong type for a printing function.
@ -203,6 +202,11 @@ val solver : Solver.t = <abstr>
# Solver.add_theory;; # Solver.add_theory;;
- : Solver.t -> Solver.theory -> unit = <fun> - : Solver.t -> Solver.theory -> unit = <fun>
# (* print solver's atoms *)
let pp_atom out a = Solver.Atom.pp solver out a;;
val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
# #install_printer pp_atom;;
``` ```
Alright, let's do some solving now ⚙️. We're going to assert Alright, let's do some solving now ⚙️. We're going to assert
@ -221,8 +225,8 @@ Sidekick_base_solver.Solver.Sat
(model (model
(true := true) (true := true)
(false := false) (false := false)
(p := false) (p := true)
(q := false) (q := true)
(_tseitin_equiv_0 := true)) (_tseitin_equiv_0 := true))
``` ```
@ -258,8 +262,8 @@ Sidekick_base_solver.Solver.Sat
(model (model
(true := true) (true := true)
(false := false) (false := false)
(p := false) (p := true)
(q := false) (q := true)
(_tseitin_equiv_0 := true)) (_tseitin_equiv_0 := true))
``` ```
@ -276,9 +280,9 @@ Sidekick_base_solver.Solver.Sat
(model (model
(true := true) (true := true)
(false := false) (false := false)
(p := false) (p := true)
(q := false) (q := true)
(r := false) (r := true)
(_tseitin_equiv_0 := true) (_tseitin_equiv_0 := true)
(_tseitin_implies_1 := true)) (_tseitin_implies_1 := true))
``` ```
@ -313,6 +317,11 @@ Let's create a new solver and add the theory of reals to it.
```ocaml ```ocaml
# let solver = Solver.create ~theories:[th_bool; th_lra] tstore () ();; # let solver = Solver.create ~theories:[th_bool; th_lra] tstore () ();;
val solver : Solver.t = <abstr> val solver : Solver.t = <abstr>
# (* print solver's atoms *)
let pp_atom out a = Solver.Atom.pp solver out a;;
val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
# #install_printer pp_atom;;
``` ```
Create a few arithmetic constants. Create a few arithmetic constants.
@ -406,6 +415,11 @@ Anyway, Sidekick knows how to reason about functions.
# let solver = Solver.create ~theories:[] tstore () ();; # let solver = Solver.create ~theories:[] tstore () ();;
val solver : Solver.t = <abstr> val solver : Solver.t = <abstr>
# (* print solver's atoms *)
let pp_atom out a = Solver.Atom.pp solver out a;;
val pp_atom : Format.formatter -> Solver.Atom.t -> unit = <fun>
# #install_printer pp_atom;;
# (* helper *) # (* helper *)
let appf1 x = Term.app_fun_l tstore f1 x;; let appf1 x = Term.app_fun_l tstore f1 x;;
val appf1 : Term.t list -> Term.t = <fun> val appf1 : Term.t list -> Term.t = <fun>