From b33f5fa5b1aaf1831ce891aee5b22da10bad6862 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 26 Aug 2021 09:19:21 -0400 Subject: [PATCH] fix tests --- doc/guide.md | 52 ++++++++++++----------------------- src/tests/basic.drup.expected | 17 +++++++++--- src/tests/dune | 2 +- 3 files changed, 32 insertions(+), 39 deletions(-) diff --git a/doc/guide.md b/doc/guide.md index f523fc31..c6102a80 100644 --- a/doc/guide.md +++ b/doc/guide.md @@ -97,12 +97,11 @@ for legibility: # open Sidekick_base;; # open Sidekick_base_solver;; # #install_printer Term.pp;; +# #install_printer Lit.pp;; # #install_printer Ty.pp;; # #install_printer Fun.pp;; # #install_printer Model.pp;; # #install_printer Solver.Model.pp;; -# #install_printer Proof.pp_debug;; -Proof.pp_debug has a wrong type for a printing function. ``` ## First steps in solving @@ -197,16 +196,11 @@ A list of theories can be added initially, or later using `Solver.add_theory`. ```ocaml -# let solver = Solver.create ~theories:[th_bool] tstore () ();; +# let solver = Solver.create ~theories:[th_bool] ~proof:(Proof_stub.create()) tstore () ();; val solver : Solver.t = # Solver.add_theory;; - : Solver.t -> Solver.theory -> unit = - -# (* print solver's atoms *) - let pp_atom out a = Solver.Atom.pp solver out a;; -val pp_atom : Format.formatter -> Solver.Atom.t -> unit = -# #install_printer pp_atom;; ``` Alright, let's do some solving now ⚙️. We're going to assert @@ -240,11 +234,11 @@ whether the assertions and hypotheses are satisfiable together. ```ocaml # Solver.solve solver - ~assumptions:[Solver.mk_atom_t' solver p; - Solver.mk_atom_t' solver q ~sign:false];; + ~assumptions:[Solver.mk_lit_t solver p; + Solver.mk_lit_t solver q ~sign:false];; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.proof = ; unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = } ``` Here it's unsat, because we asserted "p = q", and then assumed "p" @@ -301,7 +295,7 @@ val q_imp_not_r : Term.t = (=> q (not r)) # Solver.solve ~assumptions:[] solver;; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.proof = ; unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = } ``` This time we got _unsat_ and there is no way of undoing it. @@ -315,13 +309,8 @@ We can solve linear real arithmetic problems as well. Let's create a new solver and add the theory of reals to it. ```ocaml -# let solver = Solver.create ~theories:[th_bool; th_lra] tstore () ();; +# let solver = Solver.create ~theories:[th_bool; th_lra] ~proof:(Proof_stub.create()) tstore () ();; val solver : Solver.t = - -# (* print solver's atoms *) - let pp_atom out a = Solver.Atom.pp solver out a;; -val pp_atom : Format.formatter -> Solver.Atom.t -> unit = -# #install_printer pp_atom;; ``` Create a few arithmetic constants. @@ -362,15 +351,15 @@ val a_geq_1 : Term.t = (>= a 1) val b_leq_half : Term.t = (<= b 1/2) # let res = Solver.solve solver - ~assumptions:[Solver.mk_atom_t' solver p; - Solver.mk_atom_t' solver a_geq_1; - Solver.mk_atom_t' solver b_leq_half];; + ~assumptions:[Solver.mk_lit_t solver p; + Solver.mk_lit_t solver a_geq_1; + Solver.mk_lit_t solver b_leq_half];; val res : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.proof = ; unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = } -# match res with Solver.Unsat {unsat_core=lazy us; _} -> us | _ -> assert false;; -- : Solver.Atom.t list = [(a >= 1); (b <= 1/2)] +# match res with Solver.Unsat {unsat_core=us; _} -> us() |> Iter.to_list | _ -> assert false;; +- : Proof_stub.lit list = [(a >= 1); (b <= 1/2)] ``` This just showed that `a=1, b=1/2, a>=b` is unsatisfiable. @@ -412,14 +401,9 @@ val f1_u1 : Term.t = (f1 u1) Anyway, Sidekick knows how to reason about functions. ```ocaml -# let solver = Solver.create ~theories:[] tstore () ();; +# let solver = Solver.create ~theories:[] ~proof:(Proof_stub.create()) tstore () ();; val solver : Solver.t = -# (* print solver's atoms *) - let pp_atom out a = Solver.Atom.pp solver out a;; -val pp_atom : Format.formatter -> Solver.Atom.t -> unit = -# #install_printer pp_atom;; - # (* helper *) let appf1 x = Term.app_fun_l tstore f1 x;; val appf1 : Term.t list -> Term.t = @@ -435,16 +419,16 @@ val appf1 : Term.t list -> Term.t = - : unit = () # Solver.solve solver - ~assumptions:[Solver.mk_atom_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 = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.proof = ; unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = } # Solver.solve solver - ~assumptions:[Solver.mk_atom_t' solver ~sign:false (Term.eq tstore u2 u3)];; + ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u2 u3)];; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.proof = ; unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = } ``` Assuming: `f1(u1)=u2, f1(u2)=u3, f1^2(u1)=u1, f1^3(u1)=u1`, diff --git a/src/tests/basic.drup.expected b/src/tests/basic.drup.expected index 192e100d..6225382f 100644 --- a/src/tests/basic.drup.expected +++ b/src/tests/basic.drup.expected @@ -1,4 +1,13 @@ --4 -1 0 --1 0 --3 0 - 0 +i 1 2 -3 0 +i -1 -2 3 0 +i 2 3 -4 0 +i -2 -3 4 0 +i 1 3 4 0 +i -1 -3 -4 0 +i -1 2 4 0 +i 1 -2 -4 0 +r -4 -1 0 +r -1 0 +r -3 0 +r -2 -4 1 0 +r 0 diff --git a/src/tests/dune b/src/tests/dune index a02366ec..7e52dbd5 100644 --- a/src/tests/dune +++ b/src/tests/dune @@ -26,4 +26,4 @@ (locks /test) (package sidekick-bin) (action - (diff basic.drup basic.drup.expected))) + (diff basic.drup.expected basic.drup)))