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

refactor(proof): merge proof and lemma, add composite proof constructor

Browse source
This commit is contained in:
Simon Cruanes 2021-04-25 21:56:16 -04:00
parent 22d6786c40
commit 502dce503c
7 changed files with 230 additions and 123 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -35,6 +35,7 @@ type t =
| Unspecified
| Sorry (* NOTE: v. bad as we don't even specify the return *)
| Sorry_c of clause
| Named of string (* refers to previously defined clause *)
| Refl of term
| CC_lemma_imply of t list * term * term
| CC_lemma of clause
@ -50,6 +51,23 @@ type t =
| Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
| Ite_false of term
| LRA of clause
| Composite of {
(* some named (atomic) assumptions *)
assumptions: (string * lit) list;
steps: composite_step list; (* last step is the proof *)
}
and composite_step =
| S_define_c of {
name: string; (* name *)
res: clause; (* result of [proof] *)
proof: t; (* sub-proof *)
}
(* TODO: do we need that here? or is it only during printing
that it becomes important?
| S_define_t of string * term (* name this term *)
*)
and hres_step =
| R of { pivot: term; p: t}
@ -62,11 +80,15 @@ let r1 p = R1 p
let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
let p1 p = P1 p
let defc ~name res proof : composite_step =
S_define_c {proof;name;res}
let default=Unspecified
let sorry_c c = Sorry_c (Iter.to_rev_list c)
let sorry_c_l c = Sorry_c c
let sorry = Sorry
let refl t : t = Refl t
let ref_by_name name : t = Named name
let make_cc iter : t = CC_lemma (Iter.to_rev_list iter)
let cc_lemma c : t = CC_lemma (Iter.to_rev_list c)
let cc_imply_l l t u : t = CC_lemma_imply (l, t, u)
@ -74,6 +96,11 @@ let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u)
let assertion t = Assertion t
let assertion_c c = Assertion_c (Iter.to_rev_list c)
let assertion_c_l c = Assertion_c c
let composite_l ?(assms=[]) steps : t =
Composite {assumptions=assms; steps}
let composite_iter ?(assms=[]) steps : t =
let steps = Iter.to_list steps in
Composite {assumptions=assms; steps}
let isa_split ty i = DT_isa_split (ty, Iter.to_rev_list i)
let isa_disj ty t u = DT_isa_disj (ty, t, u)
@ -91,16 +118,24 @@ let hres_iter c i : t = Hres (c, Iter.to_list i)
let lra_l c : t = LRA c
let lra c = LRA (Iter.to_rev_list c)
let rec pp out (self:t) : unit =
let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l in
let pp_cl out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l pp_lit) c in
module Quip = struct
(*
TODO: make sure we print terms properly
TODO: define/use [deft] for printing shared terms
*)
let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l
let pp_cl out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l pp_lit) c
let rec pp_rec out (self:t) : unit =
match self with
| Unspecified -> Fmt.string out "<unspecified>"
| Named s -> Fmt.fprintf out "(ref %s)" s
| CC_lemma l ->
Fmt.fprintf out "(@[cc-lemma@ %a@])" pp_cl l
| CC_lemma_imply (l,t,u) ->
Fmt.fprintf out "(@[cc-lemma-imply@ (@[%a@])@ (@[=@ %a@ %a@])@])"
(pp_l pp) l T.pp t T.pp u
(pp_l pp_rec) l T.pp t T.pp u
| Refl t -> Fmt.fprintf out "(@[refl@ %a@])" T.pp t
| Sorry -> Fmt.string out "sorry"
| Sorry_c c -> Fmt.fprintf out "(@[sorry-c@ %a@])" pp_cl c
@ -111,7 +146,7 @@ let rec pp out (self:t) : unit =
| Assertion_c c ->
Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c
| Hres (c, l) ->
Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp c
Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp_rec c
(pp_l pp_hres_step) l
| DT_isa_split (ty,l) ->
Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])"
@ -124,12 +159,31 @@ let rec pp out (self:t) : unit =
| Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" T.pp t
| Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" T.pp t
| LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c
| Composite {steps; assumptions} ->
let pp_ass out (n,a) = Fmt.fprintf out "(@[assuming@ (name %s) %a@])" n pp_lit a in
Fmt.fprintf out "(@[steps@ (@[%a@])@ (@[%a@])@])"
(pp_l pp_ass) assumptions (pp_l pp_composite_step) steps
and pp_hres_step out = function
and pp_composite_step out = function
| S_define_c {name;res;proof} ->
Fmt.fprintf out "(@[defc %s %a@ %a@])" name pp_cl res pp_rec proof
(*
| S_define_t (name, t) ->
Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t
*)
and pp_hres_step out = function
| R {pivot; p} ->
Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" T.pp pivot pp p
| R1 p -> Fmt.fprintf out "(@[r1@ %a@])" pp p
Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" T.pp pivot pp_rec p
| R1 p -> Fmt.fprintf out "(@[r1@ %a@])" pp_rec p
| P {p; lhs; rhs} ->
Fmt.fprintf out "(@[r@ (@[lhs@ %a@])@ (@[rhs@ %a@])@ %a@])"
T.pp lhs T.pp rhs pp p
| P1 p -> Fmt.fprintf out "(@[p1@ %a@])" pp p
T.pp lhs T.pp rhs pp_rec p
| P1 p -> Fmt.fprintf out "(@[p1@ %a@])" pp_rec p
(* toplevel wrapper *)
let pp out self =
Fmt.fprintf out "(@[quip 1@ %a@])" pp_rec self
end
let pp_debug = Quip.pp_rec

2
src/cc/Sidekick_cc.ml
View file

@ -169,7 +169,7 @@ module Make (A: CC_ARG)
| E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
| E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
| E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
| E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp p
| E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp_debug p
| E_and (a,b) ->
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b

49
src/core/Sidekick_core.ml
View file

@ -149,7 +149,6 @@ module type PROOF = sig
type term
type ty
type t
val pp : t Fmt.printer
type hres_step
(** hyper-resolution steps: resolution, unit resolution;
@ -178,8 +177,12 @@ module type PROOF = sig
val neq : term -> term -> lit
val not : lit -> lit
type composite_step
val defc : name:string -> lit list -> t -> composite_step
val assertion : term -> t
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 hres_iter : t -> hres_step Iter.t -> t (* hyper-res *)
val hres_l : t -> hres_step list -> t (* hyper-res *)
@ -189,6 +192,8 @@ module type PROOF = sig
val cc_lemma : lit Iter.t -> t (* equality tautology, unsigned *)
val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *)
val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *)
val composite_iter : ?assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?assms:(string * lit) list -> composite_step list -> t
val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
val sorry_c : lit Iter.t -> t
[@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
@ -196,6 +201,13 @@ module type PROOF = sig
val sorry_c_l : lit list -> t
val default : t [@@alert cstor "do not use default constructor"]
val pp_debug : t Fmt.printer
module Quip : sig
val pp : t Fmt.printer
(** Printer in Quip format (experimental) *)
end
end
(** Literals
@ -810,7 +822,7 @@ module type SOLVER = sig
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
type lemma = P.t
type proof = P.t
(** {3 A theory}
@ -915,19 +927,6 @@ module type SOLVER = sig
*)
end
(** {3 Proof type}
The representation of a full proof, including toplevel steps
with intermediate, named, clauses. Each clause is justified by
a {!P.t} lemma. *)
module Proof : sig
type t
val check : t -> unit
val pp_dot : t Fmt.printer
val pp : t Fmt.printer
end
type proof = Proof.t
(** {3 Main API} *)
val stats : t -> Stat.t
@ -980,11 +979,29 @@ module type SOLVER = sig
val add_clause_l : t -> Atom.t list -> P.t -> unit
(** Same as {!add_clause} but with a list of atoms. *)
(** {2 Internal representation of proofs}
A type or state convertible into {!P.t} *)
module Pre_proof : sig
type t
val pp : t Fmt.printer
val pp_dot : t Fmt.printer option
(** Optional printer into DOT/graphviz *)
val check : t -> unit
(** Check the proof (to an unspecified level of confidence;
this can be a no-op). May fail. *)
val to_proof : t -> P.t
end
(** Result of solving for the current set of clauses *)
type res =
| Sat of Model.t (** Satisfiable *)
| Unsat of {
proof: proof option lazy_t; (** proof of unsat *)
proof: Pre_proof.t option lazy_t; (** proof of unsat *)
unsat_core: Atom.t list lazy_t; (** subset of assumptions responsible for unsat *)
} (** Unsatisfiable *)
| Unknown of Unknown.t

4
src/lra/sidekick_arith_lra.ml
View file

@ -58,8 +58,8 @@ module type ARG = sig
(** Does this term have the type [Real] *)
(** TODO: more accurate certificates *)
val proof_lra : S.P.lit Iter.t -> S.lemma
val proof_lra_l : S.P.lit list -> S.lemma
val proof_lra : S.P.lit Iter.t -> S.P.t
val proof_lra_l : S.P.lit list -> S.P.t
module Gensym : sig
type t

148
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -36,7 +36,7 @@ module Make(A : ARG)
module Term = T.Term
type term = Term.t
type ty = Ty.t
type lemma = P.t
type proof = P.t
module Lit_ = struct
module T = T
@ -344,7 +344,7 @@ module Make(A : ARG)
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
Log.debugf 10
(fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])"
Lit.pp lit Lit.pp lit' P.pp p);
Lit.pp lit Lit.pp lit' P.Quip.pp p);
lit', p
(* add a clause using [acts] *)
@ -504,93 +504,129 @@ module Make(A : ARG)
module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
module Atom = Sat_solver.Atom
module Proof = struct
include Sat_solver.Proof
module Pre_proof = struct
module SP = Sat_solver.Proof
module SC = Sat_solver.Clause
type t = {
msat: Sat_solver.proof;
p: P.t lazy_t;
}
let to_proof (self:t) : P.t = Lazy.force self.p
let pp_dot =
let module Dot =
Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in
Dot.pp
let pp out self = Dot.pp out self.msat in
Some pp
(* TODO: instead export to regular proof, which must get:
(* export to proof {!P.t}, translating Msat-level proof ising:
- [defc name cl proof] to bind [name] to given clause and proof
- [deft name t] to define [name] as a shortcut for [t] (tseitin, etc.).
Checker will always expand these.
Checker will always expand these. (TODO)
- [steps <defc>+] for a structure proof with definitions, returning last one
- [subproof (assms <lit>* ) (proof)] which uses [proof] to get
clause [c] under given assumptions (each assm is a lit),
and return [-a1 \/ … \/ -an \/ c], discharging assumptions
proof must provide a mutable builder for "steps" which is passed along
in main solver context so that theories can use it for their global
definitions. This is also what resolution should use to translate the proof.
*)
let pp out (self:t) : unit =
let n_step = ref 0 in
let n_tbl_ = SC.Tbl.create 32 in (* node.concl -> unique idx *)
let conv_proof (msat:Sat_solver.proof) : P.t =
let assms = ref [] in
let steps = ref [] in
let find_idx_of_proof_ (p:t) : int =
try SC.Tbl.find n_tbl_ (conclusion p)
let n_step = ref 0 in
let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *)
(* name of an already processed proof node *)
let find_proof_name (p:Sat_solver.proof) : string =
try SC.Tbl.find n_tbl_ (SP.conclusion p)
with Not_found ->
Error.errorf "proof print: cannot find proof step with conclusion %a" SC.pp (conclusion p)
Error.errorf
"msat-solver.pre-proof.to_proof: cannot find proof step with conclusion %a"
SC.pp (SP.conclusion p)
in
let pp_node () n_init : unit =
let {conclusion=c; step} = n_init in
let add_step s = steps := s :: !steps in
(* convert [n_init] into a proof step and adds it to [steps] *)
let tr_node_to_step () (n_init:SP.proof_node) : unit =
let {SP.conclusion=c; step} = n_init in
if SC.Tbl.mem n_tbl_ c then ()
else (
let idx = !n_step in
let name = Printf.sprintf "c%d" !n_step in
incr n_step;
SC.Tbl.add n_tbl_ c idx;
SC.Tbl.add n_tbl_ c name;
let atoms = Sat_solver.Clause.atoms_l c in
let pp_atom out a =
let lit = Sat_solver.Atom.formula a in
let sign = if Sat_solver.Atom.sign a then "+" else "-" in
Fmt.fprintf out "(@[%s %a@])" sign T.Term.pp (Lit.term lit)
(* build conclusion of proof step *)
let tr_atom a : P.lit =
let sign = Sat_solver.Atom.sign a in
let t = Lit.term (Sat_solver.Atom.formula a) in
P.lit_st (t,sign)
in
let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l c in
(* proof for the node *)
let pr_step : P.t =
match step with
| SP.Hypothesis pr -> pr (* FIXME: should this have a special rule? *)
| SP.Assumption ->
(* push into assumptions and introduce a name for it *)
let name = Printf.sprintf "a%d" !n_step in
let lit = match concl with
| [l] -> l
| _ -> Error.errorf "assumption with non-unit clause %a" SC.pp c
in
incr n_step;
assms := (name, lit) :: !assms;
P.ref_by_name name
| Lemma pr -> pr
let pp_step out (s:step) : unit =
match s with
| Hypothesis l ->
Fmt.fprintf out "(@[hyp@ %a@])" P.pp l
| Assumption -> Fmt.string out "assumption"
| Lemma l -> Fmt.fprintf out "(@[lemma@ %a@])" P.pp l
| Duplicate (c, _) ->
let n = find_idx_of_proof_ c in
Fmt.fprintf out "(@[dedup@ c%d@])" n
let n = find_proof_name c in
let p = P.ref_by_name n in
(* NOTE: we do not represent this form of transformation for now.
Quip should be able to process clauses as sets. *)
p
| Hyper_res { hr_init=init; hr_steps=steps } ->
let n_init = find_idx_of_proof_ init in
let pp_step out (pivot,p') =
let unit_res =
Array.length (SC.atoms (conclusion p')) = 1 in
let n_p' = find_idx_of_proof_ p' in
if unit_res then (
Fmt.fprintf out "(@[r1 c%d@])" n_p'
let proof_init = P.ref_by_name @@ find_proof_name init in
let tr_step (pivot,p') : P.hres_step =
(* unit resolution? *)
let is_r1_step = Array.length (SC.atoms (SP.conclusion p')) = 1 in
let proof_p' = P.ref_by_name @@ find_proof_name p' in
if is_r1_step then (
P.r1 proof_p'
) else (
Fmt.fprintf out "(@[r c%d@ :pivot %a@])" n_p' pp_atom pivot
let pivot = Lit.term (Sat_solver.Atom.formula pivot) in
P.r proof_p' ~pivot
)
in
Fmt.fprintf out "(@[hres@ c%d@ (@[%a@])@])"
n_init Fmt.(list ~sep:(return "@ ") pp_step) steps
P.hres_iter proof_init
(Iter.of_list steps |> Iter.map tr_step)
in
Fmt.fprintf out "@ (@[defc c%d@ (@[cl %a@])@ (@[<1>src@ %a@])@])"
idx Fmt.(list ~sep:(return "@ ") pp_atom) atoms
pp_step step;
let step = P.defc ~name concl pr_step in
add_step step;
)
in
Fmt.fprintf out "(@[<v>quip 1";
Sat_solver.Proof.fold pp_node () self;
Fmt.fprintf out "@])";
()
(* this should traverse from the leaves, so that order of [steps] is correct *)
Sat_solver.Proof.fold tr_node_to_step () msat;
let assms = !assms in
P.composite_l ~assms (List.rev !steps)
let make (msat: Sat_solver.proof) : t =
{ msat; p=lazy (conv_proof msat) }
let check self = SP.check self.msat
let pp out (self:t) = P.Quip.pp out (to_proof self)
end
type proof = Proof.t
(* main solver state *)
type t = {
si: Solver_internal.t;
@ -747,7 +783,7 @@ module Make(A : ARG)
type res =
| Sat of Model.t
| Unsat of {
proof: proof option lazy_t;
proof: Pre_proof.t option lazy_t;
unsat_core: Atom.t list lazy_t;
}
| Unknown of Unknown.t
@ -761,7 +797,7 @@ module Make(A : ARG)
let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit =
Stat.incr self.count_clause;
Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])"
(Util.pp_iarray Atom.pp) c P.pp proof);
(Util.pp_iarray Atom.pp) c P.pp_debug proof);
let pb = Profile.begin_ "add-clause" in
Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof;
Profile.exit pb
@ -860,7 +896,7 @@ module Make(A : ARG)
try
let pr = us.get_proof () in
if check then Sat_solver.Proof.check pr;
Some pr
Some (Pre_proof.make pr)
with Msat.Solver_intf.No_proof -> None
) in
let unsat_core = lazy (us.Msat.unsat_assumptions ()) in

12
src/smtlib/Process.ml
View file

@ -185,19 +185,18 @@ let solve
if check then (
match proof_opt with
| Some p ->
Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
Profile.with_ "unsat.check" (fun () -> Solver.Pre_proof.check p);
| _ -> ()
);
begin match dot_proof, proof with
| None, _ -> ()
| Some file, lazy (Some p) ->
begin match dot_proof, proof, Solver.Pre_proof.pp_dot with
| Some file, lazy (Some p), Some pp_dot ->
Profile.with_ "dot.proof" @@ fun () ->
CCIO.with_out file
(fun oc ->
Log.debugf 1 (fun k->k "write proof into `%s`" file);
let fmt = Format.formatter_of_out_channel oc in
Solver.Proof.pp_dot fmt p;
pp_dot fmt p;
Format.pp_print_flush fmt (); flush oc)
| _ -> ()
end;
@ -210,7 +209,8 @@ let solve
match proof_opt with
| None -> Error.errorf "cannot print proof, none was generated"
| Some p ->
Fmt.printf "(@[proof@ %a@])@." Solver.Proof.pp p;
let p = Solver.Pre_proof.to_proof p in
Fmt.printf "(@[proof@ %a@])@." Solver.P.Quip.pp p;
);
| Solver.Unknown reas ->

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

@ -317,7 +317,7 @@ module Make(A : ARG) : S with module A = A = struct
| Some (u, pr_t_u) ->
Log.debugf 5
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])"
T.pp t T.pp u SI.P.pp pr_t_u);
T.pp t T.pp u SI.P.Quip.pp pr_t_u);
SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
());
end;