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

fix test

Browse source
This commit is contained in:
Simon Cruanes 2022-02-14 11:36:50 -05:00
parent fb552ba8b2
commit 7f45cc6967
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 16 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
doc/guide.md
View file

@ -224,7 +224,7 @@ Sidekick_base_solver.Solver.Sat
(false := false) (false := false)
(p := true) (p := true)
(q := true) (q := true)
(_tseitin_equiv_0 := true)) ((= p q) := true))
``` ```
It is satisfiable, and we got a model where "p" and "q" are both false. It is satisfiable, and we got a model where "p" and "q" are both false.
@ -261,7 +261,7 @@ Sidekick_base_solver.Solver.Sat
(false := false) (false := false)
(p := true) (p := true)
(q := true) (q := true)
(_tseitin_equiv_0 := true)) ((= p q) := true))
``` ```
We can therefore add more formulas and see where it leads us. We can therefore add more formulas and see where it leads us.
@ -280,8 +280,8 @@ Sidekick_base_solver.Solver.Sat
(p := true) (p := true)
(q := true) (q := true)
(r := true) (r := true)
(_tseitin_equiv_0 := true) ((= p q) := true)
(_tseitin_implies_1 := true)) ((=> p r) := true))
``` ```
Still satisfiable, but now we see `r` in the model, too. And now: Still satisfiable, but now we see `r` in the model, too. And now:
@ -344,8 +344,12 @@ Sidekick_base_solver.Solver.Sat
(model (model
(true := true) (true := true)
(false := false) (false := false)
(_sk_lra__le0 := 0) (a := 0)
((_sk_lra__le0 <= 0) := true)) (b := 0)
((<= (+ a (* -1 b)) 0) := true)
(_sk_lra__le_comb0 := 0)
((= a b) := true)
((>= (+ a (* -1 b)) 0) := true))
# let a_geq_1 = Term.LRA.(geq tstore a (const tstore (Q.of_int 1)));; # let a_geq_1 = Term.LRA.(geq tstore a (const tstore (Q.of_int 1)));;
@ -362,7 +366,7 @@ val res : Solver.res =
{Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>} {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <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.lit list = [(a >= 1); (b <= 1/2)] - : Proof.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.
@ -379,7 +383,7 @@ an uninterpreted type.
```ocaml ```ocaml
# let u = Ty.atomic_uninterpreted (ID.make "u");; # let u = Ty.atomic_uninterpreted (ID.make "u");;
val u : Ty.t = u/12 val u : Ty.t = u/9
# let u1 = Term.const_undefined tstore (ID.make "u1") u;; # let u1 = Term.const_undefined tstore (ID.make "u1") u;;
val u1 : Term.t = u1 val u1 : Term.t = u1
@ -389,19 +393,19 @@ val u2 : Term.t = u2
val u3 : Term.t = u3 val u3 : Term.t = u3
# let f1 = Fun.mk_undef' (ID.make "f1") [u] u;; # let f1 = Fun.mk_undef' (ID.make "f1") [u] u;;
val f1 : Fun.t = f1/16 val f1 : Fun.t = f1/13
# Fun.view f1;; # Fun.view f1;;
- : Fun.view = - : Fun.view =
Sidekick_base.Fun.Fun_undef Sidekick_base.Fun.Fun_undef
{Sidekick_base.Base_types.fun_ty_args = [u/12]; fun_ty_ret = u/12} {Sidekick_base.Base_types.fun_ty_args = [u/9]; fun_ty_ret = u/9}
# let f1_u1 = Term.app_fun_l tstore f1 [u1];; # let f1_u1 = Term.app_fun_l tstore f1 [u1];;
val f1_u1 : Term.t = (f1 u1) val f1_u1 : Term.t = (f1 u1)
# Term.ty f1_u1;; # Term.ty f1_u1;;
- : Ty.t = u/12 - : Ty.t = u/9
# Term.view f1_u1;; # Term.view f1_u1;;
- : Term.t Term.view = Sidekick_base.Term.App_fun (f1/16, [|u1|]) - : Term.t Term.view = Sidekick_base.Term.App_fun (f1/13, [|u1|])
``` ```
Anyway, Sidekick knows how to reason about functions. Anyway, Sidekick knows how to reason about functions.