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

feat(th-bool): add proof_rules, use std gensym

Browse source
This commit is contained in:
Simon Cruanes 2022-08-10 22:08:09 -04:00
parent 647d66a196
commit 81f159d25d
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
5 changed files with 74 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -2,6 +2,7 @@ open Sidekick_core
module Intf = Intf module Intf = Intf
open Intf open Intf
module SI = SMT.Solver_internal module SI = SMT.Solver_internal
module Proof_rules = Proof_rules
module T = Term module T = Term
module type ARG = Intf.ARG module type ARG = Intf.ARG
@ -9,9 +10,9 @@ module type ARG = Intf.ARG
module Make (A : ARG) : sig module Make (A : ARG) : sig
val theory : SMT.theory val theory : SMT.theory
end = struct end = struct
type state = { tst: T.store; gensym: A.Gensym.t } type state = { tst: T.store; gensym: Gensym.t }
let create tst : state = { tst; gensym = A.Gensym.create tst } let create tst : state = { tst; gensym = Gensym.create tst }
let[@inline] not_ tst t = A.mk_bool tst (B_not t) let[@inline] not_ tst t = A.mk_bool tst (B_not t)
let[@inline] eq tst a b = A.mk_bool tst (B_eq (a, b)) let[@inline] eq tst a b = A.mk_bool tst (B_eq (a, b))
@ -44,7 +45,7 @@ end = struct
let[@inline] ret u = Some (u, Iter.of_list !steps) in let[@inline] ret u = Some (u, Iter.of_list !steps) in
(* proof is [t <=> u] *) (* proof is [t <=> u] *)
let ret_bequiv t1 u = let ret_bequiv t1 u =
(add_step_ @@ mk_step_ @@ fun () -> A.P.lemma_bool_equiv t1 u); (add_step_ @@ mk_step_ @@ fun () -> Proof_rules.lemma_bool_equiv t1 u);
ret u ret u
in in
@ -55,21 +56,21 @@ end = struct
| B_not _ -> None | B_not _ -> None
| B_atom _ -> None | B_atom _ -> None
| B_and a -> | B_and a ->
if Iter.exists is_false a then if List.exists is_false a then
ret (T.false_ tst) ret (T.false_ tst)
else if Iter.for_all is_true a then else if List.for_all is_true a then
ret (T.true_ tst) ret (T.true_ tst)
else else
None None
| B_or a -> | B_or a ->
if Iter.exists is_true a then if List.exists is_true a then
ret (T.true_ tst) ret (T.true_ tst)
else if Iter.for_all is_false a then else if List.for_all is_false a then
ret (T.false_ tst) ret (T.false_ tst)
else else
None None
| B_imply (args, u) -> | B_imply (args, u) ->
if Iter.exists is_false args then if List.exists is_false args then
ret (T.true_ tst) ret (T.true_ tst)
else if is_true u then else if is_true u then
ret (T.true_ tst) ret (T.true_ tst)
@ -83,11 +84,11 @@ end = struct
(match A.view_as_bool a with (match A.view_as_bool a with
| B_bool true -> | B_bool true ->
add_step_eq t b ~using:(Option.to_list prf_a) add_step_eq t b ~using:(Option.to_list prf_a)
~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t); ~c0:(mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
ret b ret b
| B_bool false -> | B_bool false ->
add_step_eq t c ~using:(Option.to_list prf_a) add_step_eq t c ~using:(Option.to_list prf_a)
~c0:(mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t); ~c0:(mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t);
ret c ret c
| _ -> None) | _ -> None)
| B_equiv (a, b) when is_true a -> ret_bequiv t b | B_equiv (a, b) when is_true a -> ret_bequiv t b
@ -104,7 +105,7 @@ end = struct
| B_eq _ | B_neq _ -> None | B_eq _ | B_neq _ -> None
let fresh_term self ~for_t ~pre ty = let fresh_term self ~for_t ~pre ty =
let u = A.Gensym.fresh_term self.gensym ~pre ty in let u = Gensym.fresh_term self.gensym ~pre ty in
Log.debugf 20 (fun k -> Log.debugf 20 (fun k ->
k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" T.pp_debug u T.pp_debug k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" T.pp_debug u T.pp_debug
for_t); for_t);
@ -139,26 +140,26 @@ end = struct
PA.add_clause PA.add_clause
[ Lit.neg lit; Lit.neg a; b ] [ Lit.neg lit; Lit.neg a; b ]
(if is_xor then (if is_xor then
mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e+" [ t ] mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e+" [ t ]
else else
mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_a ]); mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-e" [ t; t_a ]);
PA.add_clause PA.add_clause
[ Lit.neg lit; Lit.neg b; a ] [ Lit.neg lit; Lit.neg b; a ]
(if is_xor then (if is_xor then
mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-e-" [ t ] mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e-" [ t ]
else else
mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-e" [ t; t_b ]); mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-e" [ t; t_b ]);
PA.add_clause [ lit; a; b ] PA.add_clause [ lit; a; b ]
(if is_xor then (if is_xor then
mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_a ] mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-i" [ t; t_a ]
else else
mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i+" [ t ]); mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i+" [ t ]);
PA.add_clause PA.add_clause
[ lit; Lit.neg a; Lit.neg b ] [ lit; Lit.neg a; Lit.neg b ]
(if is_xor then (if is_xor then
mk_step_ @@ fun () -> A.P.lemma_bool_c "xor-i" [ t; t_b ] mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-i" [ t; t_b ]
else else
mk_step_ @@ fun () -> A.P.lemma_bool_c "eq-i-" [ t ]) mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i-" [ t ])
in in
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
@ -166,23 +167,21 @@ end = struct
| B_bool _ -> () | B_bool _ -> ()
| B_not _ -> () | B_not _ -> ()
| B_and l -> | B_and l ->
let t_subs = Iter.to_list l in
let lit = PA.mk_lit t in let lit = PA.mk_lit t in
let subs = List.map PA.mk_lit t_subs in let subs = List.map PA.mk_lit l in
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
PA.add_clause PA.add_clause
[ Lit.neg lit; u ] [ Lit.neg lit; u ]
(mk_step_ @@ fun () -> A.P.lemma_bool_c "and-e" [ t; t_u ])) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-e" [ t; t_u ]))
t_subs subs; l subs;
PA.add_clause PA.add_clause
(lit :: List.map Lit.neg subs) (lit :: List.map Lit.neg subs)
(mk_step_ @@ fun () -> A.P.lemma_bool_c "and-i" [ t ]) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ])
| B_or l -> | B_or l ->
let t_subs = Iter.to_list l in let subs = List.map PA.mk_lit l in
let subs = List.map PA.mk_lit t_subs in
let lit = PA.mk_lit t in let lit = PA.mk_lit t in
(* add clauses *) (* add clauses *)
@ -190,13 +189,12 @@ end = struct
(fun t_u u -> (fun t_u u ->
PA.add_clause PA.add_clause
[ Lit.neg u; lit ] [ Lit.neg u; lit ]
(mk_step_ @@ fun () -> A.P.lemma_bool_c "or-i" [ t; t_u ])) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-i" [ t; t_u ]))
t_subs subs; l subs;
PA.add_clause (Lit.neg lit :: subs) PA.add_clause (Lit.neg lit :: subs)
(mk_step_ @@ fun () -> A.P.lemma_bool_c "or-e" [ t ]) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ])
| B_imply (t_args, t_u) -> | B_imply (t_args, t_u) ->
(* transform into [¬args \/ u] on the fly *) (* transform into [¬args \/ u] on the fly *)
let t_args = Iter.to_list t_args in
let args = List.map (fun t -> Lit.neg (PA.mk_lit t)) t_args in let args = List.map (fun t -> Lit.neg (PA.mk_lit t)) t_args in
let u = PA.mk_lit t_u in let u = PA.mk_lit t_u in
let subs = u :: args in let subs = u :: args in
@ -209,18 +207,18 @@ end = struct
(fun t_u u -> (fun t_u u ->
PA.add_clause PA.add_clause
[ Lit.neg u; lit ] [ Lit.neg u; lit ]
(mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-i" [ t; t_u ])) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-i" [ t; t_u ]))
(t_u :: t_args) subs; (t_u :: t_args) subs;
PA.add_clause (Lit.neg lit :: subs) PA.add_clause (Lit.neg lit :: subs)
(mk_step_ @@ fun () -> A.P.lemma_bool_c "imp-e" [ t ]) (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ])
| B_ite (a, b, c) -> | B_ite (a, b, c) ->
let lit_a = PA.mk_lit a in let lit_a = PA.mk_lit a in
PA.add_clause PA.add_clause
[ Lit.neg lit_a; PA.mk_lit (eq self.tst t b) ] [ Lit.neg lit_a; PA.mk_lit (eq self.tst t b) ]
(mk_step_ @@ fun () -> A.P.lemma_ite_true ~ite:t); (mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
PA.add_clause PA.add_clause
[ lit_a; PA.mk_lit (eq self.tst t c) ] [ lit_a; PA.mk_lit (eq self.tst t c) ]
(mk_step_ @@ fun () -> A.P.lemma_ite_false ~ite:t) (mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
| B_eq _ | B_neq _ -> () | B_eq _ | B_neq _ -> ()
| B_equiv (a, b) -> equiv_ si ~t ~is_xor:false a b | B_equiv (a, b) -> equiv_ si ~t ~is_xor:false a b
| B_xor (a, b) -> equiv_ si ~t ~is_xor:true a b | B_xor (a, b) -> equiv_ si ~t ~is_xor:true a b

1
src/th-bool-static/Sidekick_th_bool_static.mli
View file

@ -4,6 +4,7 @@
*) *)
module Intf = Intf module Intf = Intf
module Proof_rules = Proof_rules
open Intf open Intf
module type ARG = Intf.ARG module type ARG = Intf.ARG

39
src/th-bool-static/intf.ml
View file

@ -19,46 +19,11 @@ type ('a, 'args) bool_view = ('a, 'args) Bool_view.t =
| B_ite of 'a * 'a * 'a | B_ite of 'a * 'a * 'a
| B_atom of 'a | B_atom of 'a
module type PROOF_RULES = sig
val lemma_bool_tauto : Lit.t Iter.t -> Proof_term.t
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : string -> term list -> Proof_term.t
(** Basic boolean logic lemma for a clause [|- c].
[proof_bool_c b name cs] is the Proof_term.t designated by [name]. *)
val lemma_bool_equiv : term -> term -> Proof_term.t
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : ite:term -> Proof_term.t
(** lemma [a ==> ite a b c = b] *)
val lemma_ite_false : ite:term -> Proof_term.t
(** lemma [¬a ==> ite a b c = c] *)
end
(** Argument to the theory *) (** Argument to the theory *)
module type ARG = sig module type ARG = sig
val view_as_bool : term -> (term, term Iter.t) bool_view val view_as_bool : term -> (term, term list) bool_view
(** Project the term into the boolean view. *) (** Project the term into the boolean view. *)
val mk_bool : Term.store -> (term, term array) bool_view -> term val mk_bool : Term.store -> (term, term list) bool_view -> term
(** Make a term from the given boolean view. *) (** Make a term from the given boolean view. *)
module P : PROOF_RULES
(** Fresh symbol generator.
The theory needs to be able to create new terms with fresh names,
to be used as placeholders for complex formulas during Tseitin
encoding. *)
module Gensym : sig
type t
val create : Term.store -> t
(** New (stateful) generator instance. *)
val fresh_term : t -> pre:string -> ty -> term
(** Make a fresh term of the given type *)
end
end end

19
src/th-bool-static/proof_rules.ml Normal file
View file

@ -0,0 +1,19 @@
open Sidekick_core
type term = Term.t
type lit = Lit.t
let lemma_bool_tauto lits : Proof_term.t =
Proof_term.apply_rule "bool.tauto" ~lits
let lemma_bool_c name terms : Proof_term.t =
Proof_term.apply_rule ("bool.c." ^ name) ~terms
let lemma_bool_equiv t u : Proof_term.t =
Proof_term.apply_rule "bool.equiv" ~terms:[ t; u ]
let lemma_ite_true ~ite : Proof_term.t =
Proof_term.apply_rule "bool.ite.true" ~terms:[ ite ]
let lemma_ite_false ~ite : Proof_term.t =
Proof_term.apply_rule "bool.ite.false" ~terms:[ ite ]

20
src/th-bool-static/proof_rules.mli Normal file
View file

@ -0,0 +1,20 @@
open Sidekick_core
type term = Term.t
type lit = Lit.t
val lemma_bool_tauto : lit list -> Proof_term.t
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : string -> term list -> Proof_term.t
(** Basic boolean logic lemma for a clause [|- c].
[proof_bool_c b name cs] is the Proof_term.t designated by [name]. *)
val lemma_bool_equiv : term -> term -> Proof_term.t
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : ite:term -> Proof_term.t
(** lemma [a ==> ite a b c = b] *)
val lemma_ite_false : ite:term -> Proof_term.t
(** lemma [¬a ==> ite a b c = c] *)