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

basic proof emission for dyn-trans

Browse source
This commit is contained in:
Simon Cruanes 2021-09-13 06:44:59 -04:00
parent 405d48ac2d
commit d7f09d5b09
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/base-solver/sidekick_base_solver.ml
View file

@ -124,6 +124,7 @@ module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct
| Term.Eq(a,b) -> Some (a,b) | Term.Eq(a,b) -> Some (a,b)
| _ -> None | _ -> None
let mk_eqn tst t u : term = Term.make tst (Term.Eq (t,u)) let mk_eqn tst t u : term = Term.make tst (Term.Eq (t,u))
let proof_trans lits p = Proof_stub.lemma_cc (Iter.of_list lits) p
end) end)
let th_bool : Solver.theory = Th_bool.theory let th_bool : Solver.theory = Th_bool.theory

17
src/th-dyn-trans/Sidekick_th_dyn_trans.ml
View file

@ -7,6 +7,8 @@ module type ARG = sig
val term_as_eqn : Solver.T.Term.store -> term -> (term*term) option val term_as_eqn : Solver.T.Term.store -> term -> (term*term) option
val mk_eqn : Solver.T.Term.store -> term -> term -> term val mk_eqn : Solver.T.Term.store -> term -> term -> term
val proof_trans : Solver.Lit.t list -> Solver.P.t -> unit
end end
module type S = sig module type S = sig
@ -30,7 +32,10 @@ module Make(A: ARG)
| None -> false | None -> false
module Instantiation = struct module Instantiation = struct
(** A deduction [l1 \/ l2 \/ concl],
where [l1] is [t =/ u], [l2] is [u /= v], and [concl] is [t = v] *)
type t = {l1: Lit.t; l2: Lit.t; concl: Lit.t} type t = {l1: Lit.t; l2: Lit.t; concl: Lit.t}
let equal a b = let equal a b =
Lit.equal a.l1 b.l1 && Lit.equal a.l1 b.l1 &&
Lit.equal a.l2 b.l2 && Lit.equal a.l2 b.l2 &&
@ -39,8 +44,8 @@ module Make(A: ARG)
let hash a = CCHash.(combine3 (Lit.hash a.l1) (Lit.hash a.l2) (Lit.hash a.concl)) let hash a = CCHash.(combine3 (Lit.hash a.l1) (Lit.hash a.l2) (Lit.hash a.concl))
let make (tst:Term.store) l1 l2 concl : t = let make (tst:Term.store) l1 l2 concl : t =
assert (Lit.sign l1 && is_eqn_ tst (Lit.term l1)); assert (not (Lit.sign l1) && is_eqn_ tst (Lit.term l1));
assert (Lit.sign l2 && is_eqn_ tst (Lit.term l2)); assert (not (Lit.sign l2) && is_eqn_ tst (Lit.term l2));
assert (Lit.sign concl && is_eqn_ tst (Lit.term concl)); assert (Lit.sign concl && is_eqn_ tst (Lit.term concl));
let l1, l2 = let l1, l2 =
if Term.compare (Lit.term l1) (Lit.term l2) < 0 if Term.compare (Lit.term l1) (Lit.term l2) < 0
@ -85,9 +90,7 @@ module Make(A: ARG)
if not (Term.equal u u') then ( if not (Term.equal u u') then (
(* see if [t=u, t=u' => u=u'] has not been instantiated yet *) (* see if [t=u, t=u' => u=u'] has not been instantiated yet *)
let concl = Lit.atom self.tstore (A.mk_eqn self.tstore u u') in let concl = Lit.atom self.tstore (A.mk_eqn self.tstore u u') in
let inst = let inst = Instantiation.make self.tstore lit lit' concl in
Instantiation.make self.tstore
(Lit.neg lit) (Lit.neg lit') concl in
if not (Inst_tbl.mem self.done_inst inst) then ( if not (Inst_tbl.mem self.done_inst inst) then (
Vec.push candidates (t,u,u',lit,lit',concl) Vec.push candidates (t,u,u',lit,lit',concl)
) )
@ -123,9 +126,11 @@ module Make(A: ARG)
|> Iter.iter |> Iter.iter
(fun (_,_,_,l1,l2,concl) -> (fun (_,_,_,l1,l2,concl) ->
let c = [l1; l2; concl] in let c = [l1; l2; concl] in
(* remember we did that instantiation *)
Inst_tbl.replace self.done_inst (Instantiation.make self.tstore l1 l2 concl) ();
Stat.incr self.stat_inst; Stat.incr self.stat_inst;
Log.debugf 10 (fun k->k "add dyn-trans %a" (Fmt.Dump.list Lit.pp) c); Log.debugf 10 (fun k->k "add dyn-trans %a" (Fmt.Dump.list Lit.pp) c);
let emit_proof p = () in (* TODO *) let emit_proof = A.proof_trans c in
CC.add_clause ~pool:self.cpool cc c emit_proof) CC.add_clause ~pool:self.cpool cc c emit_proof)
end; end;