mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
emit many more proof steps
This commit is contained in:
Simon Cruanes
parent
c2b8d93cf4
commit
b5749a1b72
3 changed files with 286 additions and 47 deletions
|
|
@ -128,6 +128,7 @@ let emit_fun_ (self:t) (f:Fun.t) : term_id =
|
|||
let id = alloc_id self in
|
||||
Fun.Tbl.add self.map_fun f id;
|
||||
let f_name = ID.to_string (Fun.id f) in
|
||||
Format.printf "encode fun with name %S@." f_name;
|
||||
emit_step_ self
|
||||
Proof_ser.({ Step.id; view=Fun_decl {Fun_decl.f=f_name}});
|
||||
id
|
||||
|
|
@ -173,6 +174,12 @@ let emit_ (self:t) f : proof_step =
|
|||
id
|
||||
) else dummy_step
|
||||
|
||||
let emit_no_return_ (self:t) f : unit =
|
||||
if enabled self then (
|
||||
let view = f () in
|
||||
emit_step_ self {PS.Step.id=(-1l); view}
|
||||
)
|
||||
|
||||
let[@inline] emit_redundant_clause lits ~hyps (self:t) =
|
||||
emit_ self @@ fun() ->
|
||||
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
|
||||
|
|
@ -190,7 +197,9 @@ let define_term t u (self:t) =
|
|||
let t = emit_term_ self t and u = emit_term_ self u in
|
||||
PS.(Step_view.Expr_def {Expr_def.c=t; rhs=u})
|
||||
|
||||
let proof_p1 _ _ (_pr:t) = dummy_step
|
||||
let proof_p1 rw_with c (self:t) =
|
||||
emit_ self @@ fun() ->
|
||||
PS.(Step_view.Step_proof_p1 {Step_proof_p1.c; rw_with})
|
||||
|
||||
let lemma_preprocess t u ~using (self:t) =
|
||||
emit_ self @@ fun () ->
|
||||
|
|
@ -203,18 +212,40 @@ let lemma_true t (self:t) =
|
|||
let t = emit_term_ self t in
|
||||
PS.(Step_view.Step_true {Step_true.true_=t})
|
||||
|
||||
let lemma_cc _ _ = dummy_step
|
||||
let lemma_rw_clause _ ~using:_ (_pr:t) = dummy_step
|
||||
let lemma_cc lits (self:t) =
|
||||
emit_ self @@ fun () ->
|
||||
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
|
||||
PS.(Step_view.Step_cc {Step_cc.eqns=lits})
|
||||
|
||||
let lemma_rw_clause c ~using (self:t) =
|
||||
emit_ self @@ fun() ->
|
||||
let using = Iter.to_array using in
|
||||
PS.(Step_view.Step_clause_rw {Step_clause_rw.c; using})
|
||||
|
||||
let with_defs _ _ (_pr:t) = dummy_step
|
||||
|
||||
let del_clause _ _ (_pr:t) = ()
|
||||
let emit_unsat_core _ (_pr:t) = dummy_step
|
||||
let emit_unsat _ _ = ()
|
||||
|
||||
let emit_unsat_core _ (_pr:t) = dummy_step (* TODO *)
|
||||
|
||||
let emit_unsat c (self:t) : unit =
|
||||
emit_no_return_ self @@ fun() ->
|
||||
PS.(Step_view.Step_unsat {Step_unsat.c})
|
||||
|
||||
let lemma_lra _ _ = dummy_step
|
||||
|
||||
let lemma_bool_tauto _ _ = dummy_step
|
||||
let lemma_bool_c _ _ _ = dummy_step
|
||||
let lemma_bool_tauto lits (self:t) =
|
||||
emit_ self @@ fun() ->
|
||||
let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
|
||||
PS.(Step_view.Step_bool_tauto {Step_bool_tauto.lits})
|
||||
|
||||
let lemma_bool_c rule (ts:Term.t list) (self:t) =
|
||||
emit_ self @@ fun() ->
|
||||
let exprs = ts |> Util.array_of_list_map (emit_term_ self) in
|
||||
PS.(Step_view.Step_bool_c {Step_bool_c.exprs; rule})
|
||||
|
||||
let lemma_bool_equiv _ _ _ = dummy_step
|
||||
|
||||
let lemma_ite_true ~ite:_ _ = dummy_step
|
||||
let lemma_ite_false ~ite:_ _ = dummy_step
|
||||
|
||||
|
|
|
|||
|
|
@ -36,6 +36,30 @@ type Step_preprocess {
|
|||
using: []ID
|
||||
}
|
||||
|
||||
type Step_clause_rw {
|
||||
c: ID
|
||||
using: []ID
|
||||
}
|
||||
|
||||
type Step_unsat {
|
||||
c: ID
|
||||
}
|
||||
|
||||
# rewrite `c` with the unit clause `rw_with` of the form `t=u` *)
|
||||
type Step_proof_p1 {
|
||||
rw_with: ID
|
||||
c: ID
|
||||
}
|
||||
|
||||
type Step_bool_tauto {
|
||||
lits: []Lit
|
||||
}
|
||||
|
||||
type Step_bool_c {
|
||||
rule: string
|
||||
exprs: []ID
|
||||
}
|
||||
|
||||
type Step_true {
|
||||
true_: ID
|
||||
}
|
||||
|
|
@ -76,10 +100,15 @@ type Expr_app {
|
|||
|
||||
type Step_view
|
||||
( Step_input
|
||||
| Step_unsat
|
||||
| Step_rup
|
||||
| Step_bridge_lit_expr
|
||||
| Step_cc
|
||||
| Step_preprocess
|
||||
| Step_clause_rw
|
||||
| Step_bool_tauto
|
||||
| Step_bool_c
|
||||
| Step_proof_p1
|
||||
| Step_true
|
||||
| Fun_decl
|
||||
| Expr_def
|
||||
|
|
|
|||
|
|
@ -480,6 +480,150 @@ module Step_preprocess = struct
|
|||
|
||||
end
|
||||
|
||||
module Step_clause_rw = struct
|
||||
type t = {
|
||||
c: ID.t;
|
||||
using: ID.t array;
|
||||
}
|
||||
|
||||
(** @raise Bare.Decode.Error in case of error. *)
|
||||
let decode (dec: Bare.Decode.t) : t =
|
||||
let c = ID.decode dec in
|
||||
let using =
|
||||
(let len = Bare.Decode.uint dec in
|
||||
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
|
||||
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
|
||||
{c; using; }
|
||||
|
||||
let encode (enc: Bare.Encode.t) (self: t) : unit =
|
||||
begin
|
||||
ID.encode enc self.c;
|
||||
(let arr = self.using in
|
||||
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
|
||||
Array.iter (fun xi -> ID.encode enc xi) arr);
|
||||
end
|
||||
|
||||
let pp out (self:t) : unit =
|
||||
(fun out x ->
|
||||
begin
|
||||
Format.fprintf out "{ @[";
|
||||
Format.fprintf out "c=%a;@ " ID.pp x.c;
|
||||
Format.fprintf out "using=%a;@ " (Bare.Pp.array ID.pp) x.using;
|
||||
Format.fprintf out "@]}";
|
||||
end) out self
|
||||
|
||||
end
|
||||
|
||||
module Step_unsat = struct
|
||||
type t = {
|
||||
c: ID.t;
|
||||
}
|
||||
|
||||
(** @raise Bare.Decode.Error in case of error. *)
|
||||
let decode (dec: Bare.Decode.t) : t =
|
||||
let c = ID.decode dec in {c; }
|
||||
|
||||
let encode (enc: Bare.Encode.t) (self: t) : unit =
|
||||
begin ID.encode enc self.c; end
|
||||
|
||||
let pp out (self:t) : unit =
|
||||
(fun out x ->
|
||||
begin
|
||||
Format.fprintf out "{ @[";
|
||||
Format.fprintf out "c=%a;@ " ID.pp x.c;
|
||||
Format.fprintf out "@]}";
|
||||
end) out self
|
||||
|
||||
end
|
||||
|
||||
module Step_proof_p1 = struct
|
||||
type t = {
|
||||
rw_with: ID.t;
|
||||
c: ID.t;
|
||||
}
|
||||
|
||||
(** @raise Bare.Decode.Error in case of error. *)
|
||||
let decode (dec: Bare.Decode.t) : t =
|
||||
let rw_with = ID.decode dec in let c = ID.decode dec in {rw_with; c; }
|
||||
|
||||
let encode (enc: Bare.Encode.t) (self: t) : unit =
|
||||
begin ID.encode enc self.rw_with; ID.encode enc self.c; end
|
||||
|
||||
let pp out (self:t) : unit =
|
||||
(fun out x ->
|
||||
begin
|
||||
Format.fprintf out "{ @[";
|
||||
Format.fprintf out "rw_with=%a;@ " ID.pp x.rw_with;
|
||||
Format.fprintf out "c=%a;@ " ID.pp x.c;
|
||||
Format.fprintf out "@]}";
|
||||
end) out self
|
||||
|
||||
end
|
||||
|
||||
module Step_bool_tauto = struct
|
||||
type t = {
|
||||
lits: Lit.t array;
|
||||
}
|
||||
|
||||
(** @raise Bare.Decode.Error in case of error. *)
|
||||
let decode (dec: Bare.Decode.t) : t =
|
||||
let lits =
|
||||
(let len = Bare.Decode.uint dec in
|
||||
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
|
||||
Array.init (Int64.to_int len) (fun _ -> Lit.decode dec)) in
|
||||
{lits; }
|
||||
|
||||
let encode (enc: Bare.Encode.t) (self: t) : unit =
|
||||
begin
|
||||
(let arr = self.lits in
|
||||
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
|
||||
Array.iter (fun xi -> Lit.encode enc xi) arr);
|
||||
end
|
||||
|
||||
let pp out (self:t) : unit =
|
||||
(fun out x ->
|
||||
begin
|
||||
Format.fprintf out "{ @[";
|
||||
Format.fprintf out "lits=%a;@ " (Bare.Pp.array Lit.pp) x.lits;
|
||||
Format.fprintf out "@]}";
|
||||
end) out self
|
||||
|
||||
end
|
||||
|
||||
module Step_bool_c = struct
|
||||
type t = {
|
||||
rule: string;
|
||||
exprs: ID.t array;
|
||||
}
|
||||
|
||||
(** @raise Bare.Decode.Error in case of error. *)
|
||||
let decode (dec: Bare.Decode.t) : t =
|
||||
let rule = Bare.Decode.string dec in
|
||||
let exprs =
|
||||
(let len = Bare.Decode.uint dec in
|
||||
if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
|
||||
Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
|
||||
{rule; exprs; }
|
||||
|
||||
let encode (enc: Bare.Encode.t) (self: t) : unit =
|
||||
begin
|
||||
Bare.Encode.string enc self.rule;
|
||||
(let arr = self.exprs in
|
||||
Bare.Encode.uint enc (Int64.of_int (Array.length arr));
|
||||
Array.iter (fun xi -> ID.encode enc xi) arr);
|
||||
end
|
||||
|
||||
let pp out (self:t) : unit =
|
||||
(fun out x ->
|
||||
begin
|
||||
Format.fprintf out "{ @[";
|
||||
Format.fprintf out "rule=%a;@ " Bare.Pp.string x.rule;
|
||||
Format.fprintf out "exprs=%a;@ " (Bare.Pp.array ID.pp) x.exprs;
|
||||
Format.fprintf out "@]}";
|
||||
end) out self
|
||||
|
||||
end
|
||||
|
||||
module Step_true = struct
|
||||
type t = {
|
||||
true_: ID.t;
|
||||
|
|
@ -686,10 +830,15 @@ end
|
|||
module Step_view = struct
|
||||
type t =
|
||||
| Step_input of Step_input.t
|
||||
| Step_unsat of Step_unsat.t
|
||||
| Step_rup of Step_rup.t
|
||||
| Step_bridge_lit_expr of Step_bridge_lit_expr.t
|
||||
| Step_cc of Step_cc.t
|
||||
| Step_preprocess of Step_preprocess.t
|
||||
| Step_clause_rw of Step_clause_rw.t
|
||||
| Step_bool_tauto of Step_bool_tauto.t
|
||||
| Step_bool_c of Step_bool_c.t
|
||||
| Step_proof_p1 of Step_proof_p1.t
|
||||
| Step_true of Step_true.t
|
||||
| Fun_decl of Fun_decl.t
|
||||
| Expr_def of Expr_def.t
|
||||
|
|
@ -705,18 +854,23 @@ module Step_view = struct
|
|||
let tag = Bare.Decode.uint dec in
|
||||
match tag with
|
||||
| 0L -> Step_input (Step_input.decode dec)
|
||||
| 1L -> Step_rup (Step_rup.decode dec)
|
||||
| 2L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
|
||||
| 3L -> Step_cc (Step_cc.decode dec)
|
||||
| 4L -> Step_preprocess (Step_preprocess.decode dec)
|
||||
| 5L -> Step_true (Step_true.decode dec)
|
||||
| 6L -> Fun_decl (Fun_decl.decode dec)
|
||||
| 7L -> Expr_def (Expr_def.decode dec)
|
||||
| 8L -> Expr_bool (Expr_bool.decode dec)
|
||||
| 9L -> Expr_if (Expr_if.decode dec)
|
||||
| 10L -> Expr_not (Expr_not.decode dec)
|
||||
| 11L -> Expr_eq (Expr_eq.decode dec)
|
||||
| 12L -> Expr_app (Expr_app.decode dec)
|
||||
| 1L -> Step_unsat (Step_unsat.decode dec)
|
||||
| 2L -> Step_rup (Step_rup.decode dec)
|
||||
| 3L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
|
||||
| 4L -> Step_cc (Step_cc.decode dec)
|
||||
| 5L -> Step_preprocess (Step_preprocess.decode dec)
|
||||
| 6L -> Step_clause_rw (Step_clause_rw.decode dec)
|
||||
| 7L -> Step_bool_tauto (Step_bool_tauto.decode dec)
|
||||
| 8L -> Step_bool_c (Step_bool_c.decode dec)
|
||||
| 9L -> Step_proof_p1 (Step_proof_p1.decode dec)
|
||||
| 10L -> Step_true (Step_true.decode dec)
|
||||
| 11L -> Fun_decl (Fun_decl.decode dec)
|
||||
| 12L -> Expr_def (Expr_def.decode dec)
|
||||
| 13L -> Expr_bool (Expr_bool.decode dec)
|
||||
| 14L -> Expr_if (Expr_if.decode dec)
|
||||
| 15L -> Expr_not (Expr_not.decode dec)
|
||||
| 16L -> Expr_eq (Expr_eq.decode dec)
|
||||
| 17L -> Expr_app (Expr_app.decode dec)
|
||||
| _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
|
||||
|
||||
|
||||
|
|
@ -725,41 +879,56 @@ module Step_view = struct
|
|||
| Step_input x ->
|
||||
Bare.Encode.uint enc 0L;
|
||||
Step_input.encode enc x
|
||||
| Step_rup x ->
|
||||
| Step_unsat x ->
|
||||
Bare.Encode.uint enc 1L;
|
||||
Step_unsat.encode enc x
|
||||
| Step_rup x ->
|
||||
Bare.Encode.uint enc 2L;
|
||||
Step_rup.encode enc x
|
||||
| Step_bridge_lit_expr x ->
|
||||
Bare.Encode.uint enc 2L;
|
||||
Bare.Encode.uint enc 3L;
|
||||
Step_bridge_lit_expr.encode enc x
|
||||
| Step_cc x ->
|
||||
Bare.Encode.uint enc 3L;
|
||||
Bare.Encode.uint enc 4L;
|
||||
Step_cc.encode enc x
|
||||
| Step_preprocess x ->
|
||||
Bare.Encode.uint enc 4L;
|
||||
Step_preprocess.encode enc x
|
||||
| Step_true x ->
|
||||
Bare.Encode.uint enc 5L;
|
||||
Step_preprocess.encode enc x
|
||||
| Step_clause_rw x ->
|
||||
Bare.Encode.uint enc 6L;
|
||||
Step_clause_rw.encode enc x
|
||||
| Step_bool_tauto x ->
|
||||
Bare.Encode.uint enc 7L;
|
||||
Step_bool_tauto.encode enc x
|
||||
| Step_bool_c x ->
|
||||
Bare.Encode.uint enc 8L;
|
||||
Step_bool_c.encode enc x
|
||||
| Step_proof_p1 x ->
|
||||
Bare.Encode.uint enc 9L;
|
||||
Step_proof_p1.encode enc x
|
||||
| Step_true x ->
|
||||
Bare.Encode.uint enc 10L;
|
||||
Step_true.encode enc x
|
||||
| Fun_decl x ->
|
||||
Bare.Encode.uint enc 6L;
|
||||
Bare.Encode.uint enc 11L;
|
||||
Fun_decl.encode enc x
|
||||
| Expr_def x ->
|
||||
Bare.Encode.uint enc 7L;
|
||||
Bare.Encode.uint enc 12L;
|
||||
Expr_def.encode enc x
|
||||
| Expr_bool x ->
|
||||
Bare.Encode.uint enc 8L;
|
||||
Bare.Encode.uint enc 13L;
|
||||
Expr_bool.encode enc x
|
||||
| Expr_if x ->
|
||||
Bare.Encode.uint enc 9L;
|
||||
Bare.Encode.uint enc 14L;
|
||||
Expr_if.encode enc x
|
||||
| Expr_not x ->
|
||||
Bare.Encode.uint enc 10L;
|
||||
Bare.Encode.uint enc 15L;
|
||||
Expr_not.encode enc x
|
||||
| Expr_eq x ->
|
||||
Bare.Encode.uint enc 11L;
|
||||
Bare.Encode.uint enc 16L;
|
||||
Expr_eq.encode enc x
|
||||
| Expr_app x ->
|
||||
Bare.Encode.uint enc 12L;
|
||||
Bare.Encode.uint enc 17L;
|
||||
Expr_app.encode enc x
|
||||
|
||||
|
||||
|
|
@ -767,6 +936,8 @@ module Step_view = struct
|
|||
match self with
|
||||
| Step_input x ->
|
||||
Format.fprintf out "(@[Step_input@ %a@])" Step_input.pp x
|
||||
| Step_unsat x ->
|
||||
Format.fprintf out "(@[Step_unsat@ %a@])" Step_unsat.pp x
|
||||
| Step_rup x ->
|
||||
Format.fprintf out "(@[Step_rup@ %a@])" Step_rup.pp x
|
||||
| Step_bridge_lit_expr x ->
|
||||
|
|
@ -775,6 +946,14 @@ module Step_view = struct
|
|||
Format.fprintf out "(@[Step_cc@ %a@])" Step_cc.pp x
|
||||
| Step_preprocess x ->
|
||||
Format.fprintf out "(@[Step_preprocess@ %a@])" Step_preprocess.pp x
|
||||
| Step_clause_rw x ->
|
||||
Format.fprintf out "(@[Step_clause_rw@ %a@])" Step_clause_rw.pp x
|
||||
| Step_bool_tauto x ->
|
||||
Format.fprintf out "(@[Step_bool_tauto@ %a@])" Step_bool_tauto.pp x
|
||||
| Step_bool_c x ->
|
||||
Format.fprintf out "(@[Step_bool_c@ %a@])" Step_bool_c.pp x
|
||||
| Step_proof_p1 x ->
|
||||
Format.fprintf out "(@[Step_proof_p1@ %a@])" Step_proof_p1.pp x
|
||||
| Step_true x ->
|
||||
Format.fprintf out "(@[Step_true@ %a@])" Step_true.pp x
|
||||
| Fun_decl x ->
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue