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

refactor(proof): use a suspension but keep uniform Proof_term.data type

Browse source 
this makes proof terms uniformly printable or (de)serializable.
This commit is contained in:
Simon Cruanes 2022-07-31 15:00:27 -04:00
parent dd50ab079e
commit 1edf054104
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
20 changed files with 182 additions and 192 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/cc/CC.ml
View file

@ -2,12 +2,6 @@ open Types_
type view_as_cc = Term.t -> (Const.t, Term.t, Term.t Iter.t) View.t
open struct
(* proof rules *)
module Rules_ = Proof_core
module P = Proof_trace
end
type e_node = E_node.t
(** A node of the congruence closure *)
@ -305,13 +299,13 @@ module Expl_state = struct
(* proof of [\/_i ¬lits[i]] *)
let proof_of_th_lemmas (self : t) (proof : Proof_trace.t) : Proof_term.step_id
=
let p_lits1 = Iter.of_list self.lits |> Iter.map Lit.neg in
let p_lits1 = List.rev_map Lit.neg self.lits in
let p_lits2 =
Iter.of_list self.th_lemmas
|> Iter.map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u)
self.th_lemmas |> List.rev_map (fun (lit_t_u, _, _) -> Lit.neg lit_t_u)
in
let p_cc =
P.add_step proof @@ Rules_.lemma_cc (Iter.append p_lits1 p_lits2)
Proof_trace.add_step proof @@ fun () ->
Proof_core.lemma_cc (List.rev_append p_lits1 p_lits2)
in
let resolve_with_th_proof pr (lit_t_u, sub_proofs, pr_th) =
(* pr_th: [sub_proofs |- t=u].
@ -322,16 +316,16 @@ module Expl_state = struct
(fun pr_th (lit_i, hyps_i) ->
(* [hyps_i |- lit_i] *)
let lemma_i =
P.add_step proof
@@ Rules_.lemma_cc
Iter.(cons lit_i (of_list hyps_i |> map Lit.neg))
Proof_trace.add_step proof @@ fun () ->
Proof_core.lemma_cc (lit_i :: List.rev_map Lit.neg hyps_i)
in
(* resolve [lit_i] away. *)
P.add_step proof
@@ Rules_.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th)
Proof_trace.add_step proof @@ fun () ->
Proof_core.proof_res ~pivot:(Lit.term lit_i) lemma_i pr_th)
pr_th sub_proofs
in
P.add_step proof @@ Rules_.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr
Proof_trace.add_step proof @@ fun () ->
Proof_core.proof_res ~pivot:(Lit.term lit_t_u) pr_th pr
in
(* resolve with theory proofs responsible for some merges, if any. *)
List.fold_left resolve_with_th_proof p_cc self.th_lemmas
@ -590,7 +584,7 @@ and task_merge_ self a b e_ab : unit =
E_node.pp ra E_node.pp a E_node.pp rb E_node.pp b Expl.pp e_ab);
let th = ref false in
(* TODO:
C1: P.true_neq_false
C1: Proof_trace.true_neq_false
C2: lemma [lits |- true=false] (and resolve on theory proofs)
C3: r1 C1 C2
*)

27
src/core/proof_core.ml
View file

@ -6,33 +6,24 @@
type lit = Lit.t
let lemma_cc lits : Proof_term.t = Proof_term.make ~lits "core.lemma-cc"
let lemma_cc lits : Proof_term.data = Proof_term.make_data ~lits "core.lemma-cc"
let define_term t1 t2 =
Proof_term.make ~terms:(Iter.of_list [ t1; t2 ]) "core.define-term"
Proof_term.make_data ~terms:[ t1; t2 ] "core.define-term"
let proof_r1 p1 p2 =
Proof_term.make ~premises:(Iter.of_list [ p1; p2 ]) "core.r1"
let proof_p1 p1 p2 =
Proof_term.make ~premises:(Iter.of_list [ p1; p2 ]) "core.p1"
let proof_r1 p1 p2 = Proof_term.make_data ~premises:[ p1; p2 ] "core.r1"
let proof_p1 p1 p2 = Proof_term.make_data ~premises:[ p1; p2 ] "core.p1"
let proof_res ~pivot p1 p2 =
Proof_term.make ~terms:(Iter.return pivot)
~premises:(Iter.of_list [ p1; p2 ])
"core.res"
Proof_term.make_data ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
let with_defs pr defs =
Proof_term.make ~premises:(Iter.append (Iter.return pr) defs) "core.with-defs"
Proof_term.make_data ~premises:(pr :: defs) "core.with-defs"
let lemma_true t = Proof_term.make ~terms:(Iter.return t) "core.true"
let lemma_true t = Proof_term.make_data ~terms:[ t ] "core.true"
let lemma_preprocess t1 t2 ~using =
Proof_term.make
~terms:(Iter.of_list [ t1; t2 ])
~premises:using "core.preprocess"
Proof_term.make_data ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
let lemma_rw_clause pr ~res ~using =
Proof_term.make
~premises:(Iter.append (Iter.return pr) using)
~lits:res "core.rw-clause"
Proof_term.make_data ~premises:(pr :: using) ~lits:res "core.rw-clause"

54
src/core/proof_core.mli
View file

@ -4,56 +4,56 @@ open Sidekick_core_logic
type lit = Lit.t
val lemma_cc : lit Iter.t -> Proof_term.t
val lemma_cc : lit list -> Proof_term.data
(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
of uninterpreted functions. *)
of uninterpreted functions. *)
val define_term : Term.t -> Term.t -> Proof_term.t
val define_term : Term.t -> Term.t -> Proof_term.data
(** [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] *)
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
val proof_p1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
(** [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. *)
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
val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
(** [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
pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.data
(** [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. *)
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 Iter.t -> Proof_term.t
val with_defs : Proof_term.step_id -> Proof_term.step_id list -> Proof_term.data
(** [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
val lemma_true : Term.t -> Proof_term.data
(** [lemma_true (true) p] asserts the clause [(true)] *)
val lemma_preprocess :
Term.t -> Term.t -> using:Proof_term.step_id Iter.t -> Proof_term.t
Term.t -> Term.t -> using:Proof_term.step_id list -> Proof_term.data
(** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
and that [t] has been preprocessed into [u].
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.
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)]. *)
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 Iter.t ->
using:Proof_term.step_id Iter.t ->
Proof_term.t
res:lit list ->
using:Proof_term.step_id list ->
Proof_term.data
(** [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). *)
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). *)

10
src/core/proof_sat.ml
View file

@ -1,8 +1,10 @@
type lit = Lit.t
let sat_input_clause lits : Proof_term.t = Proof_term.make "sat.input" ~lits
let sat_input_clause lits : Proof_term.data =
Proof_term.make_data "sat.input" ~lits
let sat_redundant_clause lits ~hyps : Proof_term.t =
Proof_term.make "sat.rup" ~lits ~premises:hyps
let sat_redundant_clause lits ~hyps : Proof_term.data =
Proof_term.make_data "sat.rup" ~lits ~premises:(Iter.to_rev_list hyps)
let sat_unsat_core lits : Proof_term.t = Proof_term.make ~lits "sat.unsat-core"
let sat_unsat_core lits : Proof_term.data =
Proof_term.make_data ~lits "sat.unsat-core"

6
src/core/proof_sat.mli
View file

@ -4,12 +4,12 @@ open Proof_term
type lit = Lit.t
val sat_input_clause : lit Iter.t -> Proof_term.t
val sat_input_clause : lit list -> Proof_term.data
(** Emit an input clause. *)
val sat_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> Proof_term.t
val sat_redundant_clause : lit list -> hyps:step_id Iter.t -> Proof_term.data
(** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
The clause must be RUP wrt [hyps]. *)
val sat_unsat_core : lit Iter.t -> Proof_term.t
val sat_unsat_core : lit list -> Proof_term.data
(** TODO: is this relevant here? *)

16
src/core/proof_term.ml
View file

@ -3,18 +3,20 @@ open Sidekick_core_logic
type step_id = Proof_step.id
type lit = Lit.t
type t = {
type data = {
rule_name: string;
lit_args: lit Iter.t;
term_args: Term.t Iter.t;
subst_args: Subst.t Iter.t;
premises: step_id Iter.t;
lit_args: lit list;
term_args: Term.t list;
subst_args: Subst.t list;
premises: step_id list;
}
type t = unit -> data
let pp out _ = Fmt.string out "<proof term>" (* TODO *)
let make ?(lits = Iter.empty) ?(terms = Iter.empty) ?(substs = Iter.empty)
?(premises = Iter.empty) rule_name : t =
let make_data ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
rule_name : data =
{
rule_name;
lit_args = lits;

24
src/core/proof_term.mli
View file

@ -7,20 +7,22 @@ open Sidekick_core_logic
type step_id = Proof_step.id
type lit = Lit.t
type t = {
type data = {
rule_name: string;
lit_args: lit Iter.t;
term_args: Term.t Iter.t;
subst_args: Subst.t Iter.t;
premises: step_id Iter.t;
lit_args: lit list;
term_args: Term.t list;
subst_args: Subst.t list;
premises: step_id list;
}
type t = unit -> data
include Sidekick_sigs.PRINT with type t := t
val make :
?lits:lit Iter.t ->
?terms:Term.t Iter.t ->
?substs:Subst.t Iter.t ->
?premises:step_id Iter.t ->
val make_data :
?lits:lit list ->
?terms:Term.t list ->
?substs:Subst.t list ->
?premises:step_id list ->
string ->
t
data

55
src/sat/solver.ml
View file

@ -467,10 +467,10 @@ let rec proof_of_atom_lvl0_ (self : t) (a : atom) : Proof_step.id =
if !steps = [] then
proof_c2
else
Proof_trace.add_step self.proof
@@ Proof_sat.sat_redundant_clause
(Iter.return (Atom.lit self.store a))
~hyps:Iter.(cons proof_c2 (of_list !steps))
Proof_trace.add_step self.proof @@ fun () ->
Proof_sat.sat_redundant_clause
[ Atom.lit self.store a ]
~hyps:Iter.(cons proof_c2 (of_list !steps))
in
Atom.set_proof_lvl0 self.store a p;
@ -559,11 +559,12 @@ let preprocess_clause_ (self : t) (c : Clause.t) : Clause.t =
k "(@[sat.add-clause.resolved-lvl-0@ :into [@[%a@]]@])"
(Atom.debug_a store) atoms);
let proof =
let lits = Iter.of_array atoms |> Iter.map (Atom.lit store) in
Proof_trace.add_step self.proof
@@ Proof_sat.sat_redundant_clause lits
~hyps:
Iter.(cons (Clause.proof_step self.store c) (of_list !res0_proofs))
Proof_trace.add_step self.proof @@ fun () ->
let lits = Util.array_to_list_map (Atom.lit store) atoms in
let hyps =
Iter.(cons (Clause.proof_step self.store c) (of_list !res0_proofs))
in
Proof_sat.sat_redundant_clause lits ~hyps
in
Clause.make_a store atoms proof ~removable:(Clause.removable store c)
)
@ -1005,10 +1006,9 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit =
assert (cr.cr_backtrack_lvl = 0 && decision_level self = 0);
let p =
Proof_trace.add_step self.proof
@@ Proof_sat.sat_redundant_clause
(Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
~hyps:(Step_vec.to_iter cr.cr_steps)
Proof_trace.add_step self.proof @@ fun () ->
let lits = Util.array_to_list_map (Atom.lit self.store) cr.cr_learnt in
Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps)
in
let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in
Event.emit self.on_learnt uclause;
@ -1022,10 +1022,9 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit =
| _ ->
let fuip = cr.cr_learnt.(0) in
let p =
Proof_trace.add_step self.proof
@@ Proof_sat.sat_redundant_clause
(Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
~hyps:(Step_vec.to_iter cr.cr_steps)
Proof_trace.add_step self.proof @@ fun () ->
let lits = Util.array_to_list_map (Atom.lit self.store) cr.cr_learnt in
Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps)
in
let lclause = Clause.make_a store ~removable:true cr.cr_learnt p in
@ -1741,8 +1740,8 @@ let assume self cnf : unit =
(fun l ->
let atoms = Util.array_of_list_map (make_atom_ self) l in
let proof =
Proof_trace.add_step self.proof
@@ Proof_sat.sat_input_clause (Iter.of_list l)
Proof_trace.add_step self.proof @@ fun () ->
Proof_sat.sat_input_clause l
in
let c = Clause.make_a self.store ~removable:false atoms proof in
Log.debugf 10 (fun k ->
@ -1825,10 +1824,10 @@ let resolve_with_lvl0 (self : t) (c : clause) : clause =
(* no resolution happened *)
else (
let proof =
let lits = Iter.of_list !res |> Iter.map (Atom.lit self.store) in
Proof_trace.add_step self.proof @@ fun () ->
let lits = List.rev_map (Atom.lit self.store) !res in
let hyps = Iter.of_list (Clause.proof_step self.store c :: !lvl0) in
Proof_trace.add_step self.proof
@@ Proof_sat.sat_redundant_clause lits ~hyps
Proof_sat.sat_redundant_clause lits ~hyps
in
Clause.make_l self.store ~removable:false !res proof
)
@ -1861,8 +1860,9 @@ let mk_unsat (self : t) (us : unsat_cause) : _ unsat_state =
(* increasing trail order *)
assert (Atom.equal first @@ List.hd core);
let proof =
let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in
Proof_trace.add_step self.proof @@ Proof_sat.sat_unsat_core lits
Proof_trace.add_step self.proof @@ fun () ->
let lits = List.rev_map (Atom.lit self.store) core in
Proof_sat.sat_unsat_core lits
in
Clause.make_l self.store ~removable:false [] proof)
in
@ -1937,15 +1937,14 @@ let add_clause self (c : Lit.t list) (pr : Proof_step.id) : unit =
let add_input_clause self (c : Lit.t list) =
let pr =
Proof_trace.add_step self.proof
@@ Proof_sat.sat_input_clause (Iter.of_list c)
Proof_trace.add_step self.proof @@ fun () -> Proof_sat.sat_input_clause c
in
add_clause self c pr
let add_input_clause_a self c =
let pr =
Proof_trace.add_step self.proof
@@ Proof_sat.sat_input_clause (Iter.of_array c)
Proof_trace.add_step self.proof @@ fun () ->
Proof_sat.sat_input_clause (Array.to_list c)
in
add_clause_a self c pr

9
src/simplify/sidekick_simplify.ml
View file

@ -1,10 +1,5 @@
open Sidekick_core
open struct
module P = Proof_trace
module Rule_ = Proof_core
end
type t = {
tst: Term.store;
proof: Proof_trace.t;
@ -68,8 +63,8 @@ let normalize (self : t) (t : Term.t) : (Term.t * Proof_step.id) option =
else (
(* proof: [sub_proofs |- t=u] by CC + subproof *)
let step =
P.add_step self.proof
@@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u)
Proof_trace.add_step self.proof @@ fun () ->
Proof_core.lemma_preprocess t u ~using:(Bag.to_list pr_u)
in
Some (u, step)
)

6
src/smt/solver.ml
View file

@ -113,7 +113,7 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
let t_true = Term.true_ tst in
Sat_solver.add_clause self.solver
[ Lit.atom t_true ]
(P.add_step self.proof @@ Rule_.lemma_true t_true));
(P.add_step self.proof @@ fun () -> Rule_.lemma_true t_true));
self
let[@inline] solver self = self.solver
@ -173,9 +173,7 @@ let add_clause_l self c p = add_clause self (CCArray.of_list c) p
let assert_terms self c =
let c = CCList.map Lit.atom c in
let pr_c =
P.add_step self.proof @@ Proof_sat.sat_input_clause (Iter.of_list c)
in
let pr_c = P.add_step self.proof @@ fun () -> Proof_sat.sat_input_clause c in
add_clause_l self c pr_c
let assert_term self t = assert_terms self [ t ]

26
src/smt/solver_internal.ml
View file

@ -1,13 +1,6 @@
open Sigs
module Proof_rules = Sidekick_core.Proof_sat
module P_core_rules = Sidekick_core.Proof_core
module Ty = Term
open struct
module P = Proof_trace
module Rule_ = Proof_core
end
type th_states =
| Ths_nil
| Ths_cons : {
@ -200,7 +193,7 @@ module type ARR = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val to_iter : 'a t -> 'a Iter.t
val to_list : 'a t -> 'a list
end
module Preprocess_clause (A : ARR) = struct
@ -222,16 +215,21 @@ module Preprocess_clause (A : ARR) = struct
pr_c
else (
Stat.incr self.count_preprocess_clause;
P.add_step self.proof
@@ Rule_.lemma_rw_clause pr_c ~res:(A.to_iter c')
~using:(Iter.of_list !steps)
Proof_trace.add_step self.proof @@ fun () ->
Proof_core.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps
)
in
c', pr_c'
end
[@@inline]
module PC_list = Preprocess_clause (CCList)
module PC_list = Preprocess_clause (struct
type 'a t = 'a list
let map = CCList.map
let to_list l = l
end)
module PC_arr = Preprocess_clause (CCArray)
let preprocess_clause = PC_list.top
@ -518,7 +516,9 @@ let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
in
let c = List.rev_append c1 c2 in
let pr = P.add_step self.proof @@ Rule_.lemma_cc (Iter.of_list c) in
let pr =
Proof_trace.add_step self.proof @@ fun () -> Proof_core.lemma_cc c
in
Log.debugf 20 (fun k ->
k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])"

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

@ -36,8 +36,9 @@ end = struct
let add_step_eq a b ~using ~c0 : unit =
add_step_ @@ mk_step_
@@ Proof_core.lemma_rw_clause c0 ~using
~res:(Iter.return (Lit.atom (A.mk_bool tst (B_eq (a, b)))))
@@ fun () ->
Proof_core.lemma_rw_clause c0 ~using
~res:[ Lit.atom (A.mk_bool tst (B_eq (a, b))) ]
in
let[@inline] ret u = Some (u, Iter.of_list !steps) in
@ -81,11 +82,11 @@ end = struct
Option.iter add_step_ prf_a;
(match A.view_as_bool a with
| B_bool true ->
add_step_eq t b ~using:(Iter.of_opt prf_a)
add_step_eq t b ~using:(Option.to_list prf_a)
~c0:(mk_step_ @@ A.P.lemma_ite_true ~ite:t);
ret b
| B_bool false ->
add_step_eq t c ~using:(Iter.of_opt prf_a)
add_step_eq t c ~using:(Option.to_list prf_a)
~c0:(mk_step_ @@ A.P.lemma_ite_false ~ite:t);
ret c
| _ -> None)

2
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -9,7 +9,7 @@ let name = "th-cstor"
module type ARG = sig
val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view
val lemma_cstor : Lit.t Iter.t -> Proof_term.t
val lemma_cstor : Lit.t list -> Proof_term.data
end
module Make (A : ARG) : sig

2
src/th-cstor/Sidekick_th_cstor.mli
View file

@ -7,7 +7,7 @@ type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't
module type ARG = sig
val view_as_cstor : Term.t -> (Const.t, Term.t) cstor_view
val lemma_cstor : Lit.t Iter.t -> Proof_term.t
val lemma_cstor : Lit.t list -> Proof_term.data
end
val make : (module ARG) -> SMT.theory

59
src/th-data/Sidekick_th_data.ml
View file

@ -186,7 +186,7 @@ end = struct
let t1 = E_node.term c1.c_n in
let t2 = E_node.term c2.c_n in
mk_expl t1 t2 @@ Proof_trace.add_step proof
@@ A.P.lemma_cstor_inj t1 t2 i
@@ fun () -> A.P.lemma_cstor_inj t1 t2 i
in
assert (CCArray.length c1.c_args = CCArray.length c2.c_args);
@ -199,7 +199,7 @@ end = struct
let expl =
let t1 = E_node.term c1.c_n and t2 = E_node.term c2.c_n in
mk_expl t1 t2 @@ Proof_trace.add_step proof
@@ A.P.lemma_cstor_distinct t1 t2
@@ fun () -> A.P.lemma_cstor_distinct t1 t2
in
Error (CC.Handler_action.Conflict expl)
@ -332,15 +332,14 @@ end = struct
with exhaustiveness: [|- is-c(t)] *)
let proof =
let pr_isa =
Proof_trace.add_step self.proof
@@ A.P.lemma_isa_split t
(Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t))
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_isa_split t [ Lit.atom (A.mk_is_a self.tst cstor t) ]
and pr_eq_sel =
Proof_trace.add_step self.proof
@@ A.P.lemma_select_cstor ~cstor_t:u t
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_select_cstor ~cstor_t:u t
in
Proof_trace.add_step self.proof
@@ Proof_core.proof_r1 pr_isa pr_eq_sel
Proof_trace.add_step self.proof @@ fun () ->
Proof_core.proof_r1 pr_isa pr_eq_sel
in
Term.Tbl.add self.single_cstor_preproc_done t ();
@ -394,8 +393,8 @@ end = struct
%a@])"
name Term.pp_debug t is_true E_node.pp n Monoid_cstor.pp cstor);
let pr =
Proof_trace.add_step self.proof
@@ A.P.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t
in
let n_bool = CC.n_bool cc is_true in
let expl =
@ -421,8 +420,8 @@ end = struct
assert (i < CCArray.length cstor.c_args);
let u_i = CCArray.get cstor.c_args i in
let pr =
Proof_trace.add_step self.proof
@@ A.P.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t
in
let expl =
Expl.(
@ -458,9 +457,9 @@ end = struct
name Monoid_parents.pp_is_a is_a2 is_true E_node.pp n1 E_node.pp n2
Monoid_cstor.pp c1);
let pr =
Proof_trace.add_step self.proof
@@ A.P.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n)
(E_node.term is_a2.is_a_n)
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n)
(E_node.term is_a2.is_a_n)
in
let n_bool = CC.n_bool cc is_true in
let expl =
@ -487,9 +486,9 @@ end = struct
E_node.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
assert (sel2.sel_idx < CCArray.length c1.c_args);
let pr =
Proof_trace.add_step self.proof
@@ A.P.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n)
(E_node.term sel2.sel_n)
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n)
(E_node.term sel2.sel_n)
in
let u_i = CCArray.get c1.c_args sel2.sel_idx in
let expl =
@ -598,10 +597,13 @@ end = struct
(* conflict: the [path] forms a cycle *)
let path = (n, node) :: path in
let pr =
Proof_trace.add_step self.proof
@@ A.P.lemma_acyclicity
(Iter.of_list path
|> Iter.map (fun (a, b) -> E_node.term a, E_node.term b.repr))
Proof_trace.add_step self.proof @@ fun () ->
let path =
List.rev_map
(fun (a, b) -> E_node.term a, E_node.term b.repr)
path
in
A.P.lemma_acyclicity path
in
let expl =
let subs =
@ -654,7 +656,9 @@ end = struct
Log.debugf 50 (fun k ->
k "(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name
Term.pp_debug u Term.pp_debug rhs Lit.pp lit);
let pr = Proof_trace.add_step self.proof @@ A.P.lemma_isa_sel t in
let pr =
Proof_trace.add_step self.proof @@ fun () -> A.P.lemma_isa_sel t
in
(* merge [u] and [rhs] *)
CC.merge_t (SI.cc solver) u rhs
(Expl.mk_theory u rhs
@ -680,12 +684,11 @@ end = struct
|> Iter.to_rev_list
in
SI.add_clause_permanent solver acts c
(Proof_trace.add_step self.proof
@@ A.P.lemma_isa_split t (Iter.of_list c));
(Proof_trace.add_step self.proof @@ fun () -> A.P.lemma_isa_split t c);
Iter.diagonal_l c (fun (l1, l2) ->
let pr =
Proof_trace.add_step self.proof
@@ A.P.lemma_isa_disj (Lit.neg l1) (Lit.neg l2)
Proof_trace.add_step self.proof @@ fun () ->
A.P.lemma_isa_disj (Lit.neg l1) (Lit.neg l2)
in
SI.add_clause_permanent solver acts [ Lit.neg l1; Lit.neg l2 ] pr)
)

16
src/th-data/th_intf.ml
View file

@ -22,35 +22,35 @@ type ('c, 'ty) data_ty_view =
| Ty_other
module type PROOF_RULES = sig
val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.data
(** [lemma_isa_cstor (d …) (is-c t)] returns the clause
[(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *)
val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.data
(** [lemma_select_cstor (c t1…tn) (sel-c-i t)]
returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *)
val lemma_isa_split : Term.t -> Lit.t Iter.t -> Proof_term.t
val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.data
(** [lemma_isa_split t lits] is the proof of
[is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *)
val lemma_isa_sel : Term.t -> Proof_term.t
val lemma_isa_sel : Term.t -> Proof_term.data
(** [lemma_isa_sel (is-c t)] is the proof of
[is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *)
val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t
val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.data
(** [lemma_isa_disj (is-c t) (is-d t)] is the proof
of [¬ (is-c t) \/ ¬ (is-c t)] *)
val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t
val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.data
(** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of
[c t1…tn = c u1…un |- ti = ui] *)
val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t
val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.data
(** [lemma_isa_distinct (c …) (d …)] is the proof
of the unit clause [|- (c …) ≠ (d …)] *)
val lemma_acyclicity : (Term.t * Term.t) Iter.t -> Proof_term.t
val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.data
(** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
by acyclicity. *)
end

2
src/th-lra/intf.ml
View file

@ -44,7 +44,7 @@ module type ARG = sig
val has_ty_real : Term.t -> bool
(** Does this term have the type [Real] *)
val lemma_lra : Lit.t Iter.t -> Proof_term.t
val lemma_lra : Lit.t list -> Proof_term.data
module Gensym : sig
type t

20
src/th-lra/sidekick_th_lra.ml
View file

@ -248,13 +248,13 @@ module Make (A : ARG) = (* : S with module A = A *) struct
proxy)
let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits =
let pr = Proof_trace.add_step PA.proof @@ A.lemma_lra (Iter.of_list lits) in
let pr = Proof_trace.add_step PA.proof @@ fun () -> A.lemma_lra lits in
let pr =
match using with
| None -> pr
| Some using ->
Proof_trace.add_step PA.proof
@@ Proof_core.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using
Proof_trace.add_step PA.proof @@ fun () ->
Proof_core.lemma_rw_clause pr ~res:lits ~using
in
PA.add_clause lits pr
@ -396,12 +396,12 @@ module Make (A : ARG) = (* : S with module A = A *) struct
let simplify (self : state) (_recurse : _) (t : Term.t) :
(Term.t * Proof_step.id Iter.t) option =
let proof_eq t u =
Proof_trace.add_step self.proof
@@ A.lemma_lra (Iter.return (Lit.atom (Term.eq self.tst t u)))
Proof_trace.add_step self.proof @@ fun () ->
A.lemma_lra [ Lit.atom (Term.eq self.tst t u) ]
in
let proof_bool t ~sign:b =
let lit = Lit.atom ~sign:b t in
Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return lit)
Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
in
match A.view_as_lra t with
@ -467,7 +467,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
|> List.rev_map Lit.neg
in
let pr =
Proof_trace.add_step (SI.proof si) @@ A.lemma_lra (Iter.of_list confl)
Proof_trace.add_step (SI.proof si) @@ fun () -> A.lemma_lra confl
in
SI.raise_conflict si acts confl pr
@ -478,8 +478,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
SI.propagate si acts lit ~reason:(fun () ->
let lits = CCList.flat_map (Tag.to_lits si) reason in
let pr =
Proof_trace.add_step (SI.proof si)
@@ A.lemma_lra Iter.(cons lit (of_list lits))
Proof_trace.add_step (SI.proof si) @@ fun () ->
A.lemma_lra (lit :: lits)
in
CCList.flat_map (Tag.to_lits si) reason, pr)
| _ -> ()
@ -525,7 +525,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
(* [c=0] when [c] is not 0 *)
let lit = Lit.atom ~sign:false @@ Term.eq self.tst t1 t2 in
let pr =
Proof_trace.add_step self.proof @@ A.lemma_lra (Iter.return lit)
Proof_trace.add_step self.proof @@ fun () -> A.lemma_lra [ lit ]
in
SI.add_clause_permanent si acts [ lit ] pr
)

2
src/util/Bag.ml
View file

@ -44,6 +44,8 @@ let rec fold f acc = function
| L x -> f acc x
| N (a, b) -> fold f (fold f acc a) b
let to_list self = fold (fun acc x -> x :: acc) [] self
let[@unroll 2] rec to_iter t yield =
match t with
| E -> ()

1
src/util/Bag.mli
View file

@ -15,6 +15,7 @@ val snoc : 'a t -> 'a -> 'a t
val append : 'a t -> 'a t -> 'a t
val of_iter : 'a Iter.t -> 'a t
val to_iter : 'a t -> 'a Iter.t
val to_list : 'a t -> 'a list
val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
val iter : ('a -> unit) -> 'a t -> unit