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

promote test results

Browse source
This commit is contained in:
Simon Cruanes 2022-07-22 21:45:56 -04:00
parent 851dda696a
commit c8800fe3e2
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
doc/guide.md
View file

@ -239,7 +239,7 @@ whether the assertions and hypotheses are satisfiable together.
Solver.mk_lit_t solver q ~sign:false];; Solver.mk_lit_t solver q ~sign:false];;
- : Solver.res = - : Solver.res =
Sidekick_base_solver.Solver.Unsat Sidekick_base_solver.Solver.Unsat
{Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>} {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_step_id = <fun>}
``` ```
Here it's unsat, because we asserted "p = q", and then assumed "p" Here it's unsat, because we asserted "p = q", and then assumed "p"
@ -296,7 +296,7 @@ val q_imp_not_r : Term.t = (=> q (not r))
# Solver.solve ~assumptions:[] solver;; # Solver.solve ~assumptions:[] solver;;
- : Solver.res = - : Solver.res =
Sidekick_base_solver.Solver.Unsat Sidekick_base_solver.Solver.Unsat
{Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>} {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_step_id = <fun>}
``` ```
This time we got _unsat_ and there is no way of undoing it. This time we got _unsat_ and there is no way of undoing it.
@ -359,10 +359,10 @@ val b_leq_half : Term.t = (<= b 1/2)
Solver.mk_lit_t solver b_leq_half];; Solver.mk_lit_t solver b_leq_half];;
val res : Solver.res = val res : Solver.res =
Sidekick_base_solver.Solver.Unsat Sidekick_base_solver.Solver.Unsat
{Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>} {Sidekick_base_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.lit list = [(>= a 1); (<= b 1/2)] - : Lit.t 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.
@ -428,13 +428,13 @@ val appf1 : Term.t list -> Term.t = <fun>
~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u1 (appf1[u1]))];; ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u1 (appf1[u1]))];;
- : Solver.res = - : Solver.res =
Sidekick_base_solver.Solver.Unsat Sidekick_base_solver.Solver.Unsat
{Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>} {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_step_id = <fun>}
# Solver.solve solver # Solver.solve solver
~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u2 u3)];; ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u2 u3)];;
- : Solver.res = - : Solver.res =
Sidekick_base_solver.Solver.Unsat Sidekick_base_solver.Solver.Unsat
{Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>} {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_step_id = <fun>}
``` ```
Assuming: `f1(u1)=u2, f1(u2)=u3, f1^2(u1)=u1, f1^3(u1)=u1`, Assuming: `f1(u1)=u2, f1(u2)=u3, f1^2(u1)=u1, f1^3(u1)=u1`,

4
src/tests/regression/reg_model_lra1.out.expected
View file

@ -2,8 +2,8 @@
(true := true) (true := true)
(false := false) (false := false)
(a := 5/3) (a := 5/3)
((* 3 a) := 0) ((* 3 a) := 5)
(5 := 0) (5 := 5)
((= (* 3 a) 5) := true) ((= (* 3 a) 5) := true)
((<= (* 3 a) 5) := true) ((<= (* 3 a) 5) := true)
((>= (* 3 a) 5) := true)) ((>= (* 3 a) 5) := true))