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

use named version of Bool_c

Browse source
This commit is contained in:
Simon Cruanes 2021-06-05 17:42:08 -04:00
parent 01e1bfe6e2
commit 8d05387bc9
3 changed files with 24 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/base-term/Proof.ml
View file

@ -49,7 +49,7 @@ type t =
| Bool_true_is_true
| Bool_true_neq_false
| Bool_eq of term * term (* equal by pure boolean reasoning *)
| Bool_c of clause (* boolean tautology *)
| Bool_c of bool_c_name * clause (* boolean tautology *)
| Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
| Ite_false of term
| LRA of clause
@ -59,6 +59,8 @@ type t =
steps: composite_step array; (* last step is the proof *)
}
and bool_c_name = string
and composite_step =
| S_step_c of {
name: string; (* name *)
@ -131,7 +133,7 @@ let ite_false t = Ite_false t
let true_is_true : t = Bool_true_is_true
let true_neq_false : t = Bool_true_neq_false
let bool_eq a b : t = Bool_eq (a,b)
let bool_c c : t = Bool_c c
let bool_c name c : t = Bool_c (name, c)
let hres_l c l : t = Hres (c,l)
let hres_iter c i : t = Hres (c, Iter.to_list i)
@ -166,7 +168,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
| DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us
| Bool_true_is_true | Bool_true_neq_false -> ()
| Bool_eq (t, u) -> f_t t; f_t u
| Bool_c c -> f_clause c
| Bool_c (_,c) -> f_clause c
| Ite_true t | Ite_false t -> f_t t
| LRA c -> f_clause c
| Composite { assumptions; steps } ->
@ -317,7 +319,7 @@ module Quip = struct
| Bool_eq (a,b) ->
Fmt.fprintf out "(@[bool-eq@ %a@ %a@])"
pp_t a pp_t b
| Bool_c c -> Fmt.fprintf out "(@[bool-c@ %a@])" pp_cl c
| Bool_c (name,c) -> Fmt.fprintf out "(@[bool-c %s@ %a@])" name pp_cl c
| Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t t
| Assertion_c c ->
Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c

2
src/base-term/Proof.mli
View file

@ -9,7 +9,7 @@ val isa_disj : ty -> term -> term -> t
val cstor_inj : Cstor.t -> int -> term list -> term list -> t
val bool_eq : term -> term -> t
val bool_c : lit list -> t
val bool_c : string -> lit list -> t
val ite_true : term -> t
val ite_false : term -> t

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

@ -37,7 +37,7 @@ module type ARG = sig
val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t
(** Basic boolean logic for a clause [|- c] *)
val proof_bool_c : S.P.lit list -> S.P.t
val proof_bool_c : string -> S.P.lit list -> S.P.t
val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term
(** Make a term from the given boolean view. *)
@ -209,9 +209,9 @@ module Make(A : ARG) : S with module A = A = struct
let[@inline] pr_def_refl _proxy t = SI.P.(refl t)
(* prove clause [l] by boolean lemma *)
let pr_bool_c _proxy l : SI.P.t =
let pr_bool_c name _proxy l : SI.P.t =
let cl = List.rev_map pr_lit l in
(A.proof_bool_c cl)
(A.proof_bool_c name cl)
(* TODO: polarity? *)
let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
@ -242,16 +242,16 @@ module Make(A : ARG) : S with module A = A = struct
let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
SI.define_const si ~const:t_proxy ~rhs:for_;
let add_clause c =
add_clause c (pr_bool_c t_proxy c)
let add_clause ~elim c =
add_clause c (pr_bool_c (if elim then "eq-e" else "eq-i") t_proxy c)
in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b];
add_clause [Lit.neg proxy; Lit.neg b; a];
add_clause [proxy; a; b];
add_clause [proxy; Lit.neg a; Lit.neg b];
add_clause ~elim:true [Lit.neg proxy; Lit.neg a; b];
add_clause ~elim:true [Lit.neg proxy; Lit.neg b; a];
add_clause ~elim:false [proxy; a; b];
add_clause ~elim:false [proxy; Lit.neg a; Lit.neg b];
proxy, pr_def_refl t_proxy for_
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
@ -266,8 +266,8 @@ module Make(A : ARG) : S with module A = A = struct
lit
in
let add_clause_by_def_ proxy c : unit =
let pr = pr_bool_c proxy c in
let add_clause_by_def_ name proxy c : unit =
let pr = pr_bool_c name proxy c in
add_clause c pr
in
@ -284,9 +284,9 @@ module Make(A : ARG) : S with module A = A = struct
SI.define_const si ~const:t_proxy ~rhs:t;
(* add clauses *)
List.iter
(fun u -> add_clause_by_def_ t_proxy [Lit.neg proxy; u])
(fun u -> add_clause_by_def_ "and-e" t_proxy [Lit.neg proxy; u])
subs;
add_clause_by_def_ t_proxy (proxy :: List.map Lit.neg subs);
add_clause_by_def_ "and-i" t_proxy (proxy :: List.map Lit.neg subs);
proxy, pr_def_refl t_proxy t
| B_or l ->
@ -294,8 +294,8 @@ module Make(A : ARG) : S with module A = A = struct
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
(* add clauses *)
List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs;
add_clause_by_def_ t_proxy (Lit.neg proxy :: subs);
List.iter (fun u -> add_clause_by_def_ "or-i" t_proxy [Lit.neg u; proxy]) subs;
add_clause_by_def_ "or-e" t_proxy (Lit.neg proxy :: subs);
proxy, pr_def_refl t_proxy t
| B_imply (args, u) ->
@ -309,8 +309,8 @@ module Make(A : ARG) : S with module A = A = struct
SI.define_const si ~const:t_proxy ~rhs:t;
(* add clauses *)
List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs;
add_clause_by_def_ t_proxy (Lit.neg proxy :: subs);
List.iter (fun u -> add_clause_by_def_ "imp-i" t_proxy [Lit.neg u; proxy]) subs;
add_clause_by_def_ "imp-e" t_proxy (Lit.neg proxy :: subs);
proxy, pr_def_refl t_proxy t
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t