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

refactor: update remaining theories for new proof style

Browse source
This commit is contained in:
Simon Cruanes 2022-10-12 22:19:00 -04:00
parent f275129967
commit ad0165242f
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
17 changed files with 138 additions and 151 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
src/th-bool-dyn/Sidekick_th_bool_dyn.ml
View file

@ -65,18 +65,18 @@ end = struct
(* TODO: share this with th-bool-static by way of a library for
boolean simplification? (also handle one-point rule and the likes) *)
let simplify (self : state) (simp : Simplify.t) (t : T.t) :
(T.t * Proof_step.id Iter.t) option =
(T.t * Proof.Step.id Iter.t) option =
let tst = self.tst in
let proof = Simplify.proof simp in
let steps = ref [] in
let add_step_ s = steps := s :: !steps in
let mk_step_ r = Proof_trace.add_step proof r in
let mk_step_ r = Proof.Tracer.add_step proof r in
let add_step_eq a b ~using ~c0 : unit =
add_step_ @@ mk_step_
@@ fun () ->
Proof_core.lemma_rw_clause c0 ~using
Proof.Core_rules.lemma_rw_clause c0 ~using
~res:[ Lit.atom tst (A.mk_bool tst (B_eq (a, b))) ]
in
@ -170,7 +170,7 @@ end = struct
let preprocess_ (self : state) (_p : SMT.Preprocess.t) ~is_sub:_ ~recurse:_
(module PA : SI.PREPROCESS_ACTS) (t : T.t) : T.t option =
Log.debugf 50 (fun k -> k "(@[th-bool.dyn.preprocess@ %a@])" T.pp_debug t);
let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in
let[@inline] mk_step_ r = Proof.Tracer.add_step PA.proof_tracer r in
match A.view_as_bool t with
| B_ite (a, b, c) ->
@ -201,8 +201,6 @@ end = struct
SI.add_clause_permanent solver acts c pr
in
let[@inline] mk_step_ r = Proof_trace.add_step (SI.proof solver) r in
(* handle boolean equality *)
let equiv_ ~is_xor a b : unit =
(* [a xor b] is [(¬a) = b] *)
@ -218,33 +216,37 @@ end = struct
add_axiom
[ Lit.neg lit; Lit.neg a; b ]
(if is_xor then
mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e+" [ t ]
fun () ->
Proof_rules.lemma_bool_c "xor-e+" [ t ]
else
mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "eq-e" [ t; Lit.term a ]);
fun () ->
Proof_rules.lemma_bool_c "eq-e" [ t; Lit.term a ]);
add_axiom
[ Lit.neg lit; Lit.neg b; a ]
(if is_xor then
mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "xor-e-" [ t ]
fun () ->
Proof_rules.lemma_bool_c "xor-e-" [ t ]
else
mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "eq-e" [ t; Lit.term b ]);
fun () ->
Proof_rules.lemma_bool_c "eq-e" [ t; Lit.term b ]);
add_axiom [ lit; a; b ]
(if is_xor then
mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "xor-i" [ t; Lit.term a ]
fun () ->
Proof_rules.lemma_bool_c "xor-i" [ t; Lit.term a ]
else
mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i+" [ t ]);
fun () ->
Proof_rules.lemma_bool_c "eq-i+" [ t ]);
add_axiom
[ lit; Lit.neg a; Lit.neg b ]
(if is_xor then
mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "xor-i" [ t; Lit.term b ]
fun () ->
Proof_rules.lemma_bool_c "xor-i" [ t; Lit.term b ]
else
mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "eq-i-" [ t ])
fun () ->
Proof_rules.lemma_bool_c "eq-i-" [ t ])
in
match v with
@ -254,7 +256,7 @@ end = struct
| B_bool false ->
SI.add_clause_permanent solver acts
[ Lit.neg lit ]
(mk_step_ @@ fun () -> Proof_core.lemma_true (Lit.term lit))
(fun () -> Proof.Core_rules.lemma_true (Lit.term lit))
| _ when expanded self lit -> () (* already done *)
| B_and l ->
let subs = List.map (Lit.atom self.tst) l in
@ -265,14 +267,12 @@ end = struct
(fun sub ->
add_axiom
[ Lit.neg lit; sub ]
( mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "and-e" [ t; Lit.term sub ] ))
(fun () -> Proof_rules.lemma_bool_c "and-e" [ t; Lit.term sub ]))
subs
else (
(* axiom [¬(and …t_i)=> \/_i (¬ t_i)], only in final-check *)
let c = Lit.neg lit :: List.map Lit.neg subs in
add_axiom c
(mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "and-i" [ t ])
add_axiom c (fun () -> Proof_rules.lemma_bool_c "and-i" [ t ])
)
| B_or l ->
let subs = List.map (Lit.atom self.tst) l in
@ -283,13 +283,12 @@ end = struct
(fun sub ->
add_axiom
[ Lit.neg lit; Lit.neg sub ]
( mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "or-i" [ t; Lit.term sub ] ))
(fun () -> Proof_rules.lemma_bool_c "or-i" [ t; Lit.term sub ]))
subs
else (
(* axiom [lit => \/_i subs_i] *)
let c = Lit.neg lit :: subs in
add_axiom c (mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "or-e" [ t ])
add_axiom c (fun () -> Proof_rules.lemma_bool_c "or-e" [ t ])
)
| B_imply (a, b) ->
let a = Lit.atom self.tst a in
@ -297,19 +296,16 @@ end = struct
if Lit.sign lit then (
(* axiom [lit => a => b] *)
let c = [ Lit.neg lit; Lit.neg a; b ] in
add_axiom c
(mk_step_ @@ fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ])
add_axiom c (fun () -> Proof_rules.lemma_bool_c "imp-e" [ t ])
) else if not @@ Lit.sign lit then (
(* propagate [¬ lit => ¬b] and [¬lit => a] *)
add_axiom
[ a; Lit.neg lit ]
( mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "imp-i" [ t; Lit.term a ] );
(fun () -> Proof_rules.lemma_bool_c "imp-i" [ t; Lit.term a ]);
add_axiom
[ Lit.neg b; Lit.neg lit ]
( mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "imp-i" [ t; Lit.term b ] )
(fun () -> Proof_rules.lemma_bool_c "imp-i" [ t; Lit.term b ])
)
| B_ite (a, b, c) ->
assert (T.is_bool b);
@ -319,10 +315,10 @@ end = struct
let lit_a = Lit.atom self.tst a in
add_axiom
[ Lit.neg lit_a; Lit.make_eq self.tst t b ]
(mk_step_ @@ fun () -> Proof_rules.lemma_ite_true ~ite:t);
(fun () -> Proof_rules.lemma_ite_true ~ite:t);
add_axiom
[ Lit.neg lit; lit_a; Lit.make_eq self.tst t c ]
(mk_step_ @@ fun () -> Proof_rules.lemma_ite_false ~ite:t)
(fun () -> Proof_rules.lemma_ite_false ~ite:t)
| B_equiv (a, b) ->
let a = Lit.atom self.tst a in
let b = Lit.atom self.tst b in

1
src/th-bool-dyn/intf.ml
View file

@ -1,4 +1,5 @@
open Sidekick_core
module Proof = Sidekick_proof
module SMT = Sidekick_smt_solver
module Simplify = Sidekick_simplify

21
src/th-bool-dyn/proof_rules.ml
View file

@ -1,19 +1,20 @@
open Sidekick_core
module Proof = Sidekick_proof
type term = Term.t
type lit = Lit.t
let lemma_bool_tauto lits : Proof_term.t =
Proof_term.apply_rule "bool.tauto" ~lits
let lemma_bool_tauto lits : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.tauto" ~lits
let lemma_bool_c name terms : Proof_term.t =
Proof_term.apply_rule ("bool.c." ^ name) ~terms
let lemma_bool_c name terms : Proof.Pterm.t =
Proof.Pterm.apply_rule ("bool.c." ^ name) ~terms
let lemma_bool_equiv t u : Proof_term.t =
Proof_term.apply_rule "bool.equiv" ~terms:[ t; u ]
let lemma_bool_equiv t u : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.equiv" ~terms:[ t; u ]
let lemma_ite_true ~ite : Proof_term.t =
Proof_term.apply_rule "bool.ite.true" ~terms:[ ite ]
let lemma_ite_true ~ite : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.ite.true" ~terms:[ ite ]
let lemma_ite_false ~ite : Proof_term.t =
Proof_term.apply_rule "bool.ite.false" ~terms:[ ite ]
let lemma_ite_false ~ite : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.ite.false" ~terms:[ ite ]

13
src/th-bool-dyn/proof_rules.mli
View file

@ -1,20 +1,21 @@
open Sidekick_core
module Proof = Sidekick_proof
type term = Term.t
type lit = Lit.t
val lemma_bool_tauto : lit list -> Proof_term.t
val lemma_bool_tauto : lit list -> Proof.Pterm.t
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : string -> term list -> Proof_term.t
val lemma_bool_c : string -> term list -> Proof.Pterm.t
(** Basic boolean logic lemma for a clause [|- c].
[proof_bool_c b name cs] is the Proof_term.t designated by [name]. *)
[proof_bool_c b name cs] is the Proof.Pterm.t designated by [name]. *)
val lemma_bool_equiv : term -> term -> Proof_term.t
val lemma_bool_equiv : term -> term -> Proof.Pterm.t
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : ite:term -> Proof_term.t
val lemma_ite_true : ite:term -> Proof.Pterm.t
(** lemma [a ==> ite a b c = b] *)
val lemma_ite_false : ite:term -> Proof_term.t
val lemma_ite_false : ite:term -> Proof.Pterm.t
(** lemma [¬a ==> ite a b c = c] *)

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

@ -55,18 +55,18 @@ end = struct
aux T.Set.empty t
let simplify (self : state) (simp : Simplify.t) (t : T.t) :
(T.t * Proof_step.id Iter.t) option =
(T.t * Proof.step_id Iter.t) option =
let tst = self.tst in
let proof = Simplify.proof simp in
let steps = ref [] in
let add_step_ s = steps := s :: !steps in
let mk_step_ r = Proof_trace.add_step proof r in
let mk_step_ r = Proof.Tracer.add_step proof r in
let add_step_eq a b ~using ~c0 : unit =
add_step_ @@ mk_step_
@@ fun () ->
Proof_core.lemma_rw_clause c0 ~using
Proof.Core_rules.lemma_rw_clause c0 ~using
~res:[ Lit.atom tst (A.mk_bool tst (B_eq (a, b))) ]
in
@ -160,7 +160,7 @@ end = struct
let cnf (self : state) (_preproc : SMT.Preprocess.t) ~is_sub:_ ~recurse
(module PA : SI.PREPROCESS_ACTS) (t : T.t) : T.t option =
Log.debugf 50 (fun k -> k "(@[th-bool.cnf@ %a@])" T.pp t);
let[@inline] mk_step_ r = Proof_trace.add_step PA.proof r in
let[@inline] mk_step_ r = Proof.Tracer.add_step PA.proof_tracer r in
(* handle boolean equality *)
let equiv_ (self : state) ~is_xor ~t ~box_t t_a t_b : unit =

1
src/th-bool-static/intf.ml
View file

@ -1,4 +1,5 @@
open Sidekick_core
module Proof = Sidekick_proof
module SMT = Sidekick_smt_solver
module Simplify = Sidekick_simplify

21
src/th-bool-static/proof_rules.ml
View file

@ -1,19 +1,20 @@
open Sidekick_core
module Proof = Sidekick_proof
type term = Term.t
type lit = Lit.t
let lemma_bool_tauto lits : Proof_term.t =
Proof_term.apply_rule "bool.tauto" ~lits
let lemma_bool_tauto lits : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.tauto" ~lits
let lemma_bool_c name terms : Proof_term.t =
Proof_term.apply_rule ("bool.c." ^ name) ~terms
let lemma_bool_c name terms : Proof.Pterm.t =
Proof.Pterm.apply_rule ("bool.c." ^ name) ~terms
let lemma_bool_equiv t u : Proof_term.t =
Proof_term.apply_rule "bool.equiv" ~terms:[ t; u ]
let lemma_bool_equiv t u : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.equiv" ~terms:[ t; u ]
let lemma_ite_true ~ite : Proof_term.t =
Proof_term.apply_rule "bool.ite.true" ~terms:[ ite ]
let lemma_ite_true ~ite : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.ite.true" ~terms:[ ite ]
let lemma_ite_false ~ite : Proof_term.t =
Proof_term.apply_rule "bool.ite.false" ~terms:[ ite ]
let lemma_ite_false ~ite : Proof.Pterm.t =
Proof.Pterm.apply_rule "bool.ite.false" ~terms:[ ite ]

11
src/th-bool-static/proof_rules.mli
View file

@ -1,20 +1,21 @@
open Sidekick_core
module Proof = Sidekick_proof
type term = Term.t
type lit = Lit.t
val lemma_bool_tauto : lit list -> Proof_term.t
val lemma_bool_tauto : lit list -> Proof.Pterm.t
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : string -> term list -> Proof_term.t
val lemma_bool_c : string -> term list -> Proof.Pterm.t
(** Basic boolean logic lemma for a clause [|- c].
[proof_bool_c b name cs] is the Proof_term.t designated by [name]. *)
val lemma_bool_equiv : term -> term -> Proof_term.t
val lemma_bool_equiv : term -> term -> Proof.Pterm.t
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : ite:term -> Proof_term.t
val lemma_ite_true : ite:term -> Proof.Pterm.t
(** lemma [a ==> ite a b c = b] *)
val lemma_ite_false : ite:term -> Proof_term.t
val lemma_ite_false : ite:term -> Proof.Pterm.t
(** lemma [¬a ==> ite a b c = c] *)

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

@ -1,4 +1,5 @@
open Sidekick_core
module Proof = Sidekick_proof
module SMT = Sidekick_smt_solver
module SI = SMT.Solver_internal
module T = Term
@ -9,7 +10,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 list -> Proof_term.t
val lemma_cstor : Lit.t list -> Proof.Pterm.t
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 list -> Proof_term.t
val lemma_cstor : Lit.t list -> Sidekick_proof.Pterm.t
end
val make : (module ARG) -> SMT.theory

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

@ -2,6 +2,7 @@
open Sidekick_core
open Sidekick_cc
module Proof = Sidekick_proof
include Th_intf
module SI = SMT.Solver_internal
module Model_builder = SMT.Model_builder
@ -174,7 +175,7 @@ end = struct
Some { c_n = n; c_cstor = cstor; c_args = args }, []
| _ -> None, []
let merge cc state n1 c1 n2 c2 e_n1_n2 : _ result =
let merge _cc state n1 c1 n2 c2 e_n1_n2 : _ result =
Log.debugf 5 (fun k ->
k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" name E_node.pp
n1 pp c1 E_node.pp n2 pp c2);
@ -189,14 +190,12 @@ end = struct
pr
in
let proof = CC.proof cc in
if A.Cstor.equal c1.c_cstor c2.c_cstor then (
(* same function: injectivity *)
let expl_merge i =
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
@@ fun () -> Proof_rules.lemma_cstor_inj t1 t2 i
mk_expl t1 t2 @@ fun () -> Proof_rules.lemma_cstor_inj t1 t2 i
in
assert (List.length c1.c_args = List.length c2.c_args);
@ -212,8 +211,7 @@ end = struct
(* different function: disjointness *)
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
@@ fun () -> Proof_rules.lemma_cstor_distinct t1 t2
mk_expl t1 t2 @@ fun () -> Proof_rules.lemma_cstor_distinct t1 t2
in
Stat.incr state.n_conflict;
@ -297,7 +295,7 @@ end = struct
type t = {
tst: Term.store;
proof: Proof_trace.t;
proof: Proof.Tracer.t;
cstors: ST_cstors.t; (* repr -> cstor for the class *)
parents: ST_parents.t; (* repr -> parents for the class *)
cards: Card.t; (* remember finiteness *)
@ -353,15 +351,15 @@ end = struct
with exhaustiveness: [|- is-c(t)] *)
let proof =
let pr_isa =
Proof_trace.add_step self.proof @@ fun () ->
Proof.Tracer.add_step self.proof @@ fun () ->
Proof_rules.lemma_isa_split t
[ Lit.atom self.tst (A.mk_is_a self.tst cstor t) ]
and pr_eq_sel =
Proof_trace.add_step self.proof @@ fun () ->
Proof.Tracer.add_step self.proof @@ fun () ->
Proof_rules.lemma_select_cstor ~cstor_t:u t
in
Proof_trace.add_step self.proof @@ fun () ->
Proof_core.proof_r1 pr_isa pr_eq_sel
Proof.Tracer.add_step self.proof @@ fun () ->
Proof.Core_rules.proof_r1 pr_isa pr_eq_sel
in
Term.Tbl.add self.single_cstor_preproc_done t ();
@ -416,8 +414,7 @@ end = struct
"(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor \
%a@])"
name Term.pp_debug t is_true E_node.pp n Monoid_cstor.pp cstor);
let pr =
Proof_trace.add_step self.proof @@ fun () ->
let pr () =
Proof_rules.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t
in
let n_bool = CC.n_bool cc is_true in
@ -443,8 +440,7 @@ end = struct
E_node.pp n i A.Cstor.pp c_t);
assert (i < List.length cstor.c_args);
let u_i = List.nth cstor.c_args i in
let pr =
Proof_trace.add_step self.proof @@ fun () ->
let pr () =
Proof_rules.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t
in
let expl =
@ -480,8 +476,7 @@ end = struct
:sub-cstor %a@])"
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 @@ fun () ->
let pr () =
Proof_rules.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n)
(E_node.term is_a2.is_a_n)
in
@ -509,8 +504,7 @@ end = struct
k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name
E_node.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
assert (sel2.sel_idx < List.length c1.c_args);
let pr =
Proof_trace.add_step self.proof @@ fun () ->
let pr () =
Proof_rules.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n)
(E_node.term sel2.sel_n)
in
@ -618,8 +612,7 @@ end = struct
| { flag = Open; cstor_n; _ } as node ->
(* conflict: the [path] forms a cycle *)
let path = (n, node) :: path in
let pr =
Proof_trace.add_step self.proof @@ fun () ->
let pr () =
let path =
List.rev_map
(fun (a, b) -> E_node.term a, E_node.term b.repr)
@ -677,10 +670,7 @@ 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 @@ fun () ->
Proof_rules.lemma_isa_sel t
in
let pr () = Proof_rules.lemma_isa_sel t in
(* merge [u] and [rhs] *)
CC.merge_t (SI.cc solver) u rhs
(Expl.mk_theory u rhs
@ -706,14 +696,10 @@ end = struct
(* TODO: set default polarity, depending on n° of args? *)
lit)
in
SI.add_clause_permanent solver acts c
( Proof_trace.add_step self.proof @@ fun () ->
Proof_rules.lemma_isa_split t c );
SI.add_clause_permanent solver acts c (fun () ->
Proof_rules.lemma_isa_split t c);
Iter.diagonal_l c (fun (l1, l2) ->
let pr =
Proof_trace.add_step self.proof @@ fun () ->
Proof_rules.lemma_isa_disj (Lit.neg l1) (Lit.neg l2)
in
let pr () = Proof_rules.lemma_isa_disj (Lit.neg l1) (Lit.neg l2) in
SI.add_clause_permanent solver acts [ Lit.neg l1; Lit.neg l2 ] pr)
)
@ -789,10 +775,11 @@ end = struct
early *)
let create_and_setup ~id:_ (solver : SI.t) : t =
let proof = (SI.tracer solver :> Proof.Tracer.t) in
let self =
{
tst = SI.tst solver;
proof = SI.proof solver;
proof;
cstors = ST_cstors.create_and_setup ~size:32 (SI.cc solver);
parents = ST_parents.create_and_setup ~size:32 (SI.cc solver);
to_decide = N_tbl.create ~size:16 ();

33
src/th-data/proof_rules.ml
View file

@ -1,27 +1,28 @@
open Sidekick_core
module Proof = Sidekick_proof
let lemma_isa_cstor ~cstor_t t : Proof_term.t =
Proof_term.apply_rule ~terms:[ cstor_t; t ] "data.isa-cstor"
let lemma_isa_cstor ~cstor_t t : Proof.Pterm.t =
Proof.Pterm.apply_rule ~terms:[ cstor_t; t ] "data.isa-cstor"
let lemma_select_cstor ~cstor_t t : Proof_term.t =
Proof_term.apply_rule ~terms:[ cstor_t; t ] "data.select-cstor"
let lemma_select_cstor ~cstor_t t : Proof.Pterm.t =
Proof.Pterm.apply_rule ~terms:[ cstor_t; t ] "data.select-cstor"
let lemma_isa_split t lits : Proof_term.t =
Proof_term.apply_rule ~terms:[ t ] ~lits "data.isa-split"
let lemma_isa_split t lits : Proof.Pterm.t =
Proof.Pterm.apply_rule ~terms:[ t ] ~lits "data.isa-split"
let lemma_isa_sel t : Proof_term.t =
Proof_term.apply_rule ~terms:[ t ] "data.isa-sel"
let lemma_isa_sel t : Proof.Pterm.t =
Proof.Pterm.apply_rule ~terms:[ t ] "data.isa-sel"
let lemma_isa_disj l1 l2 : Proof_term.t =
Proof_term.apply_rule ~lits:[ l1; l2 ] "data.isa-disj"
let lemma_isa_disj l1 l2 : Proof.Pterm.t =
Proof.Pterm.apply_rule ~lits:[ l1; l2 ] "data.isa-disj"
let lemma_cstor_inj t1 t2 i : Proof_term.t =
Proof_term.apply_rule ~terms:[ t1; t2 ] ~indices:[ i ] "data.cstor-inj"
let lemma_cstor_inj t1 t2 i : Proof.Pterm.t =
Proof.Pterm.apply_rule ~terms:[ t1; t2 ] ~indices:[ i ] "data.cstor-inj"
let lemma_cstor_distinct t1 t2 : Proof_term.t =
Proof_term.apply_rule ~terms:[ t1; t2 ] "data.cstor-distinct"
let lemma_cstor_distinct t1 t2 : Proof.Pterm.t =
Proof.Pterm.apply_rule ~terms:[ t1; t2 ] "data.cstor-distinct"
let lemma_acyclicity ts : Proof_term.t =
Proof_term.apply_rule
let lemma_acyclicity ts : Proof.Pterm.t =
Proof.Pterm.apply_rule
~terms:(CCList.flat_map (fun (t1, t2) -> [ t1; t2 ]) ts)
"data.acyclicity"

17
src/th-data/proof_rules.mli
View file

@ -1,33 +1,34 @@
open Sidekick_core
module Proof = Sidekick_proof
val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t
val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof.Pterm.t
(** [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.Pterm.t
(** [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 list -> Proof_term.t
val lemma_isa_split : Term.t -> Lit.t list -> Proof.Pterm.t
(** [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.Pterm.t
(** [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.Pterm.t
(** [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.Pterm.t
(** [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.Pterm.t
(** [lemma_isa_distinct (c …) (d …)] is the proof
of the unit clause [|- (c …) ≠ (d …)] *)
val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.t
val lemma_acyclicity : (Term.t * Term.t) list -> Proof.Pterm.t
(** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
by acyclicity. *)

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

@ -1,5 +1,6 @@
open Sidekick_core
module SMT = Sidekick_smt_solver
module Proof = Sidekick_proof
module Predicate = Sidekick_simplex.Predicate
module Linear_expr = Sidekick_simplex.Linear_expr
module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf

3
src/th-lra/proof_rules.ml
View file

@ -1,3 +1,4 @@
open Sidekick_core
module Proof = Sidekick_proof
let lemma_lra lits : Proof_term.t = Proof_term.apply_rule "lra.lemma" ~lits
let lemma_lra lits : Proof.Pterm.t = Proof.Pterm.apply_rule "lra.lemma" ~lits

4
src/th-lra/proof_rules.mli
View file

@ -1,5 +1,5 @@
open Sidekick_core
module Proof = Sidekick_proof
val lemma_lra : Lit.t list -> Proof_term.t
val lemma_lra : Lit.t list -> Proof.Pterm.t
(** List of literals [l1…ln] where [¬l1 /\ … /\ ¬ln] is LRA-unsat *)

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

@ -125,7 +125,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
type state = {
tst: Term.store;
proof: Proof_trace.t;
proof: Proof.Tracer.t;
gensym: Gensym.t;
in_model: unit Term.Tbl.t; (* terms to add to model *)
encoded_eqs: unit Term.Tbl.t;
@ -145,7 +145,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
let create (si : SI.t) : state =
let stat = SI.stats si in
let proof = SI.proof si in
let proof = (SI.tracer si :> Proof.Tracer.t) in
let tst = SI.tst si in
{
tst;
@ -255,14 +255,15 @@ module Make (A : ARG) = (* : S with module A = A *) struct
let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits =
let pr =
Proof_trace.add_step PA.proof @@ fun () -> Proof_rules.lemma_lra lits
Proof.Tracer.add_step PA.proof_tracer @@ fun () ->
Proof_rules.lemma_lra lits
in
let pr =
match using with
| None -> pr
| Some using ->
Proof_trace.add_step PA.proof @@ fun () ->
Proof_core.lemma_rw_clause pr ~res:lits ~using
Proof.Tracer.add_step PA.proof_tracer @@ fun () ->
Proof.Core_rules.lemma_rw_clause pr ~res:lits ~using
in
PA.add_clause lits pr
@ -405,14 +406,15 @@ 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 =
(Term.t * Proof.Step.id Iter.t) option =
let proof_eq t u =
Proof_trace.add_step self.proof @@ fun () ->
Proof.Tracer.add_step self.proof @@ fun () ->
Proof_rules.lemma_lra [ Lit.atom self.tst (Term.eq self.tst t u) ]
in
let proof_bool t ~sign:b =
let lit = Lit.atom ~sign:b self.tst t in
Proof_trace.add_step self.proof @@ fun () -> Proof_rules.lemma_lra [ lit ]
Proof.Tracer.add_step self.proof @@ fun () ->
Proof_rules.lemma_lra [ lit ]
in
match A.view_as_lra t with
@ -477,10 +479,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
|> CCList.flat_map (Tag.to_lits si)
|> List.rev_map Lit.neg
in
let pr =
Proof_trace.add_step (SI.proof si) @@ fun () ->
Proof_rules.lemma_lra confl
in
let pr () = Proof_rules.lemma_lra confl in
Stat.incr self.n_conflict;
SI.raise_conflict si acts confl pr
@ -491,10 +490,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
Stat.incr self.n_propagate;
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) @@ fun () ->
Proof_rules.lemma_lra (lit :: lits)
in
let pr () = Proof_rules.lemma_lra (lit :: lits) in
CCList.flat_map (Tag.to_lits si) reason, pr)
| _ -> ()
@ -538,10 +534,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
if A.Q.(le_const <> zero) then (
(* [c=0] when [c] is not 0 *)
let lit = Lit.atom ~sign:false self.tst @@ Term.eq self.tst t1 t2 in
let pr =
Proof_trace.add_step self.proof @@ fun () ->
Proof_rules.lemma_lra [ lit ]
in
let pr () = Proof_rules.lemma_lra [ lit ] in
SI.add_clause_permanent si acts [ lit ] pr
)
) else (