simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: add "drup" case to proofs

Browse source
This commit is contained in:
Simon Cruanes 2021-07-20 23:27:11 -04:00
parent 89051fd3ad
commit d53b3c291e
3 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/base/Proof.ml
View file

@ -40,6 +40,7 @@ type t =
| CC_lemma of clause
| Assertion of term
| Assertion_c of clause
| Drup_res of clause
| Hres of t * hres_step list
| Res of term * t * t
| Res1 of t * t
@ -136,6 +137,7 @@ let bool_eq a b : t = Bool_eq (a,b)
let bool_c name c : t = Bool_c (name, c)
let nn c : t = Nn c
let drup_res c : t = Drup_res c
let hres_l p l : t =
let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
if l=[] then p else Hres (p,l)
@ -159,6 +161,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
| CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u
| CC_lemma c | Assertion_c c -> f_clause c
| Assertion t -> f_t t
| Drup_res c -> f_clause c
| Hres (i, l) ->
f_p i;
List.iter
@ -402,6 +405,7 @@ module Quip = struct
| Nn p -> l[a"nn";pp_rec p]
| Assertion t -> l[a"assert";pp_t t]
| Assertion_c c -> l[a"assert-c";pp_cl c]
| Drup_res c -> l[a"drup";pp_cl c]
| Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)]
| Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2]
| Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2]

4
src/cc/Sidekick_cc.ml
View file

@ -600,10 +600,10 @@ module Make (A: CC_ARG)
let rec update_tasks (cc:t) (acts:actions) : unit =
while not (Vec.is_empty cc.pending && Vec.is_empty cc.combine) do
while not @@ Vec.is_empty cc.pending do
task_pending_ cc (Vec.pop cc.pending);
task_pending_ cc (Vec.pop_exn cc.pending);
done;
while not @@ Vec.is_empty cc.combine do
task_combine_ cc acts (Vec.pop cc.combine);
task_combine_ cc acts (Vec.pop_exn cc.combine);
done;
done

1
src/core/Sidekick_core.ml
View file

@ -197,6 +197,7 @@ module type PROOF = sig
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t (* named clause, see {!defc} *)
val assertion_c_l : lit list -> t
val drup_res : lit list -> t (* assert clause and let DRUP take care of it *)
val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *)
val hres_l : t -> hres_step list -> t (* hyper-res *)
val res : pivot:term -> t -> t -> t (* resolution with pivot *)