mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
wip: refactor(core): remove proof representation from core
This commit is contained in:
Simon Cruanes
parent
82727cd7ad
commit
842a7de435
14 changed files with 14 additions and 404 deletions
|
|
@ -17,6 +17,7 @@ module Fmt = CCFormat
|
|||
(** {2 Re-exports from core-logic} *)
|
||||
|
||||
module Const = Sidekick_core_logic.Const
|
||||
module Str_const = Sidekick_core_logic.Str_const
|
||||
|
||||
module Term = struct
|
||||
include Sidekick_core_logic.Term
|
||||
|
|
@ -24,10 +25,9 @@ module Term = struct
|
|||
include T_printer
|
||||
module Tracer = T_tracer
|
||||
module Trace_reader = T_trace_reader
|
||||
module Ref = T_ref
|
||||
end
|
||||
|
||||
module Gensym = Gensym
|
||||
|
||||
(** {2 view} *)
|
||||
|
||||
module Bool_view = Bool_view
|
||||
|
|
@ -38,14 +38,20 @@ module Default_cc_view = Default_cc_view
|
|||
|
||||
module Bvar = Sidekick_core_logic.Bvar
|
||||
module Lit = Lit
|
||||
module Proof_step = Proof_step
|
||||
module Proof_core = Proof_core
|
||||
module Proof_sat = Proof_sat
|
||||
module Proof_trace = Proof_trace
|
||||
module Proof_term = Proof_term
|
||||
module Subst = Sidekick_core_logic.Subst
|
||||
module Var = Sidekick_core_logic.Var
|
||||
module Box = Box
|
||||
module Clause_tracer = Clause_tracer
|
||||
module Gensym = Gensym
|
||||
|
||||
exception Resource_exhausted
|
||||
|
||||
(** {2 Const decoders for traces} *)
|
||||
|
||||
let const_decoders =
|
||||
List.flatten
|
||||
[
|
||||
Sidekick_core_logic.T_builtins.const_decoders;
|
||||
T_ref.const_decoders;
|
||||
Box.const_decoders;
|
||||
]
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
module Tr = Sidekick_trace
|
||||
|
||||
class type t =
|
||||
object
|
||||
method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
|
||||
method delete_clause : id:int -> Lit.t Iter.t -> unit
|
||||
method unsat_clause : id:int -> Tr.Entry_id.t
|
||||
method encode_lit : Lit.t -> Ser_value.t
|
||||
end
|
||||
|
||||
class dummy : t =
|
||||
object
|
||||
method assert_clause ~id:_ _ = Tr.Entry_id.dummy
|
||||
method delete_clause ~id:_ _ = ()
|
||||
method unsat_clause ~id:_ = Tr.Entry_id.dummy
|
||||
method encode_lit _ = Ser_value.null
|
||||
end
|
||||
|
||||
let dummy : t = new dummy
|
||||
let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c
|
||||
|
||||
let assert_clause' (self : #t) ~id c : unit =
|
||||
ignore (self#assert_clause ~id c : Tr.Entry_id.t)
|
||||
|
||||
let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id
|
||||
|
||||
let unsat_clause' (self : #t) ~id : unit =
|
||||
ignore (self#unsat_clause ~id : Tr.Entry_id.t)
|
||||
|
||||
let delete_clause (self : #t) ~id c = self#delete_clause ~id c
|
||||
let encode_lit (self : #t) lit = self#encode_lit lit
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
(** Tracer for clauses and literals *)
|
||||
|
||||
module Tr = Sidekick_trace
|
||||
|
||||
(** Tracer for clauses. *)
|
||||
class type t =
|
||||
object
|
||||
method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
|
||||
method delete_clause : id:int -> Lit.t Iter.t -> unit
|
||||
method unsat_clause : id:int -> Tr.Entry_id.t
|
||||
method encode_lit : Lit.t -> Ser_value.t
|
||||
end
|
||||
|
||||
class dummy : t
|
||||
|
||||
val dummy : t
|
||||
(** Dummy tracer, recording nothing. *)
|
||||
|
||||
val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t
|
||||
val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit
|
||||
val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit
|
||||
val unsat_clause : #t -> id:int -> Tr.Entry_id.t
|
||||
val unsat_clause' : #t -> id:int -> unit
|
||||
val encode_lit : #t -> Lit.t -> Ser_value.t
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
(* FIXME
|
||||
open Proof_trace
|
||||
|
||||
type lit = Lit.t
|
||||
*)
|
||||
|
||||
type lit = Lit.t
|
||||
|
||||
let lemma_cc lits : Proof_term.t = Proof_term.apply_rule ~lits "core.lemma-cc"
|
||||
|
||||
let define_term t1 t2 =
|
||||
Proof_term.apply_rule ~terms:[ t1; t2 ] "core.define-term"
|
||||
|
||||
let proof_r1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.r1"
|
||||
let proof_p1 p1 p2 = Proof_term.apply_rule ~premises:[ p1; p2 ] "core.p1"
|
||||
|
||||
let proof_res ~pivot p1 p2 =
|
||||
Proof_term.apply_rule ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
|
||||
|
||||
let with_defs pr defs =
|
||||
Proof_term.apply_rule ~premises:(pr :: defs) "core.with-defs"
|
||||
|
||||
let lemma_true t = Proof_term.apply_rule ~terms:[ t ] "core.true"
|
||||
|
||||
let lemma_preprocess t1 t2 ~using =
|
||||
Proof_term.apply_rule ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
|
||||
|
||||
let lemma_rw_clause pr ~res ~using =
|
||||
Proof_term.apply_rule ~premises:(pr :: using) ~lits:res "core.rw-clause"
|
||||
|
|
@ -1,59 +0,0 @@
|
|||
(** Core proofs for SMT and congruence closure. *)
|
||||
|
||||
open Sidekick_core_logic
|
||||
|
||||
type lit = Lit.t
|
||||
|
||||
val lemma_cc : lit list -> Proof_term.t
|
||||
(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
|
||||
of uninterpreted functions. *)
|
||||
|
||||
val define_term : Term.t -> Term.t -> Proof_term.t
|
||||
(** [define_term cst u proof] defines the new constant [cst] as being equal
|
||||
to [u].
|
||||
The result is a proof of the clause [cst = u] *)
|
||||
|
||||
val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
|
||||
(** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
|
||||
and [p2] proves [C \/ t], is the Proof_term.t that produces [C \/ u],
|
||||
i.e unit paramodulation. *)
|
||||
|
||||
val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
|
||||
(** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
|
||||
and [p2] proves [C \/ ¬t], is the Proof_term.t that produces [C \/ u],
|
||||
i.e unit resolution. *)
|
||||
|
||||
val proof_res :
|
||||
pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
|
||||
(** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
|
||||
and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
|
||||
is the Proof_term.t that produces [C \/ D], i.e boolean resolution. *)
|
||||
|
||||
val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.t
|
||||
(** [with_defs pr defs] specifies that [pr] is valid only in
|
||||
a context where the definitions [defs] are present. *)
|
||||
|
||||
val lemma_true : Term.t -> Proof_term.t
|
||||
(** [lemma_true (true) p] asserts the clause [(true)] *)
|
||||
|
||||
val lemma_preprocess :
|
||||
Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.t
|
||||
(** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
|
||||
and that [t] has been preprocessed into [u].
|
||||
|
||||
The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
|
||||
closure, and then resolved against the clauses [using] to obtain
|
||||
a unit equality.
|
||||
|
||||
From now on, [t] and [u] will be used interchangeably.
|
||||
@return a Proof_term.t ID for the clause [(t=u)]. *)
|
||||
|
||||
val lemma_rw_clause :
|
||||
Proof_term.step_id ->
|
||||
res:lit list ->
|
||||
using:Proof_term.step_id list ->
|
||||
Proof_term.t
|
||||
(** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
|
||||
uses the equations [|- p_i = q_i] from [using]
|
||||
to rewrite some literals of [c] into [res]. This is used to preprocess
|
||||
literals of a clause (using {!lemma_preprocess} individually). *)
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
type lit = Lit.t
|
||||
|
||||
let sat_input_clause lits : Proof_term.t =
|
||||
Proof_term.apply_rule "sat.input" ~lits
|
||||
|
||||
let sat_redundant_clause lits ~hyps : Proof_term.t =
|
||||
Proof_term.apply_rule "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps)
|
||||
|
||||
let sat_unsat_core lits : Proof_term.t =
|
||||
Proof_term.apply_rule ~lits "sat.unsat-core"
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
(** SAT-solver proof emission. *)
|
||||
|
||||
open Proof_term
|
||||
|
||||
type lit = Lit.t
|
||||
|
||||
val sat_input_clause : lit list -> Proof_term.t
|
||||
(** Emit an input clause. *)
|
||||
|
||||
val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.t
|
||||
(** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
|
||||
The clause must be RUP wrt [hyps]. *)
|
||||
|
||||
val sat_unsat_core : lit list -> Proof_term.t
|
||||
(** TODO: is this relevant here? *)
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
type id = int32
|
||||
|
||||
let pp = Fmt.int32
|
||||
|
|
@ -1,44 +0,0 @@
|
|||
open Sidekick_core_logic
|
||||
|
||||
type step_id = Proof_step.id
|
||||
type local_ref = int
|
||||
type lit = Lit.t
|
||||
|
||||
type rule_apply = {
|
||||
rule_name: string;
|
||||
lit_args: lit list;
|
||||
term_args: Term.t list;
|
||||
subst_args: Subst.t list;
|
||||
premises: step_id list;
|
||||
indices: int list;
|
||||
}
|
||||
|
||||
type t =
|
||||
| P_ref of step_id
|
||||
| P_local of local_ref
|
||||
| P_let of (local_ref * t) list * t
|
||||
| P_apply of rule_apply
|
||||
|
||||
type delayed = unit -> t
|
||||
|
||||
let pp out _ = Fmt.string out "<proof term>" (* TODO *)
|
||||
|
||||
let local_ref id = P_local id
|
||||
let ref_ id = P_ref id
|
||||
|
||||
let let_ bs r =
|
||||
match bs with
|
||||
| [] -> r
|
||||
| _ -> P_let (bs, r)
|
||||
|
||||
let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
|
||||
?(indices = []) rule_name : t =
|
||||
P_apply
|
||||
{
|
||||
rule_name;
|
||||
lit_args = lits;
|
||||
subst_args = substs;
|
||||
term_args = terms;
|
||||
premises;
|
||||
indices;
|
||||
}
|
||||
|
|
@ -1,41 +0,0 @@
|
|||
(** Proof terms.
|
||||
|
||||
A proof term is the description of a reasoning step, that yields a clause. *)
|
||||
|
||||
open Sidekick_core_logic
|
||||
|
||||
type step_id = Proof_step.id
|
||||
type local_ref = int
|
||||
type lit = Lit.t
|
||||
|
||||
type rule_apply = {
|
||||
rule_name: string;
|
||||
lit_args: lit list;
|
||||
term_args: Term.t list;
|
||||
subst_args: Subst.t list;
|
||||
premises: step_id list;
|
||||
indices: int list;
|
||||
}
|
||||
|
||||
type t =
|
||||
| P_ref of step_id
|
||||
| P_local of local_ref (** Local reference, in a let *)
|
||||
| P_let of (local_ref * t) list * t
|
||||
| P_apply of rule_apply
|
||||
|
||||
type delayed = unit -> t
|
||||
|
||||
include Sidekick_sigs.PRINT with type t := t
|
||||
|
||||
val ref_ : step_id -> t
|
||||
val local_ref : local_ref -> t
|
||||
val let_ : (local_ref * t) list -> t -> t
|
||||
|
||||
val apply_rule :
|
||||
?lits:lit list ->
|
||||
?terms:Term.t list ->
|
||||
?substs:Subst.t list ->
|
||||
?premises:step_id list ->
|
||||
?indices:int list ->
|
||||
string ->
|
||||
t
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
type lit = Lit.t
|
||||
type step_id = Proof_step.id
|
||||
|
||||
module Step_vec = struct
|
||||
type elt = step_id
|
||||
type t = elt Vec.t
|
||||
|
||||
let get = Vec.get
|
||||
let size = Vec.size
|
||||
let iter = Vec.iter
|
||||
let iteri = Vec.iteri
|
||||
let create ?cap:_ () = Vec.create ()
|
||||
let clear = Vec.clear
|
||||
let copy = Vec.copy
|
||||
let is_empty = Vec.is_empty
|
||||
let push = Vec.push
|
||||
let fast_remove = Vec.fast_remove
|
||||
let filter_in_place = Vec.filter_in_place
|
||||
let ensure_size v len = Vec.ensure_size v ~elt:0l len
|
||||
let pop = Vec.pop_exn
|
||||
let set = Vec.set
|
||||
let shrink = Vec.shrink
|
||||
let to_iter = Vec.to_iter
|
||||
end
|
||||
|
||||
module type DYN = sig
|
||||
val enabled : unit -> bool
|
||||
val add_step : Proof_term.delayed -> step_id
|
||||
val add_unsat : step_id -> unit
|
||||
val delete : step_id -> unit
|
||||
val close : unit -> unit
|
||||
end
|
||||
|
||||
type t = (module DYN)
|
||||
|
||||
let[@inline] enabled ((module Tr) : t) : bool = Tr.enabled ()
|
||||
let[@inline] add_step ((module Tr) : t) rule : step_id = Tr.add_step rule
|
||||
let[@inline] add_unsat ((module Tr) : t) s : unit = Tr.add_unsat s
|
||||
let[@inline] delete ((module Tr) : t) s : unit = Tr.delete s
|
||||
let[@inline] close ((module Tr) : t) : unit = Tr.close ()
|
||||
let make (d : (module DYN)) : t = d
|
||||
let dummy_step_id : step_id = -1l
|
||||
|
||||
let dummy : t =
|
||||
(module struct
|
||||
let enabled () = false
|
||||
let add_step _ = dummy_step_id
|
||||
let add_unsat _ = ()
|
||||
let delete _ = ()
|
||||
let close _ = ()
|
||||
end)
|
||||
|
|
@ -1,65 +0,0 @@
|
|||
(** Proof traces.
|
||||
|
||||
A proof trace is a log of all the deductive reasoning steps made by
|
||||
the SMT solver and other reasoning components. It essentially stores
|
||||
a DAG of all these steps, where each step points (via {!step_id})
|
||||
to its premises.
|
||||
*)
|
||||
|
||||
type lit = Lit.t
|
||||
|
||||
type step_id = Proof_step.id
|
||||
(** Identifier for a tracing step (like a unique ID for a clause previously
|
||||
added/proved) *)
|
||||
|
||||
module Step_vec : Vec_sig.BASE with type elt = step_id
|
||||
(** A vector indexed by steps. *)
|
||||
|
||||
(** {2 Traces} *)
|
||||
|
||||
type t
|
||||
(** The proof trace itself.
|
||||
|
||||
A proof trace is a log of all deductive steps taken by the solver,
|
||||
so we can later reconstruct a certificate for proof-checking.
|
||||
|
||||
Each step in the proof trace should be a {b valid
|
||||
lemma} (of its theory) or a {b valid consequence} of previous steps.
|
||||
*)
|
||||
|
||||
val enabled : t -> bool
|
||||
(** Is proof tracing enabled? *)
|
||||
|
||||
val add_step : t -> Proof_term.delayed -> step_id
|
||||
(** Create a new step in the trace. *)
|
||||
|
||||
val add_unsat : t -> step_id -> unit
|
||||
(** Signal "unsat" result at the given proof *)
|
||||
|
||||
val delete : t -> step_id -> unit
|
||||
(** Forget a step that won't be used in the rest of the trace.
|
||||
Only useful for performance/memory considerations. *)
|
||||
|
||||
val close : t -> unit
|
||||
(** [close p] closes the proof, and can dispose of underlying resources *)
|
||||
|
||||
(** {2 Dummy backend} *)
|
||||
|
||||
val dummy_step_id : step_id
|
||||
|
||||
val dummy : t
|
||||
(** Dummy proof trace, logs nothing. *)
|
||||
|
||||
(* TODO: something that just logs on stderr? or uses "Log"? *)
|
||||
|
||||
(** {2 Dynamic interface} *)
|
||||
|
||||
module type DYN = sig
|
||||
val enabled : unit -> bool
|
||||
val add_step : Proof_term.delayed -> step_id
|
||||
val add_unsat : step_id -> unit
|
||||
val delete : step_id -> unit
|
||||
val close : unit -> unit
|
||||
end
|
||||
|
||||
val make : (module DYN) -> t
|
||||
|
|
@ -3,18 +3,6 @@ module Tr = Sidekick_trace
|
|||
module T = Term
|
||||
|
||||
type term_ref = Tr.entry_id
|
||||
|
||||
type Tr.entry_view +=
|
||||
| T_ty of int
|
||||
| T_app of term_ref * term_ref
|
||||
| T_var of string * term_ref
|
||||
| T_bvar of int * term_ref
|
||||
| T_const of { c: Const.view; c_ops: Const.Ops.t; ty: term_ref }
|
||||
| T_lam of { v_name: string; v_ty: term_ref; body: term_ref }
|
||||
| T_pi of { v_name: string; v_ty: term_ref; body: term_ref }
|
||||
(* FIXME: remove when we decode *)
|
||||
[@@ocaml.warning "-38"]
|
||||
|
||||
type state = { sink: Tr.Sink.t; emitted: Tr.Entry_id.t T.Weak_map.t }
|
||||
|
||||
let emit_term_ (self : state) (t : Term.t) =
|
||||
|
|
|
|||
|
|
@ -8,19 +8,7 @@
|
|||
open Sidekick_core_logic
|
||||
module Tr = Sidekick_trace
|
||||
|
||||
type term_ref = Tr.entry_id
|
||||
|
||||
type Tr.entry_view +=
|
||||
private
|
||||
| T_ty of int
|
||||
| T_app of term_ref * term_ref
|
||||
| T_var of string * term_ref
|
||||
| T_bvar of int * term_ref
|
||||
| T_const of { c: Const.view; c_ops: Const.Ops.t; ty: term_ref }
|
||||
| T_lam of { v_name: string; v_ty: term_ref; body: term_ref }
|
||||
| T_pi of { v_name: string; v_ty: term_ref; body: term_ref }
|
||||
(* FIXME: remove *)
|
||||
[@@ocaml.warning "-38"]
|
||||
type term_ref = T_ref.t
|
||||
|
||||
class type t =
|
||||
object
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue