mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-10 13:14:09 -05:00
remove dead code
This commit is contained in:
Simon Cruanes
parent
10a4cf4c29
commit
2bb6c94925
1 changed files with 0 additions and 131 deletions
|
|
@ -508,137 +508,6 @@ module Make(A : ARG)
|
|||
(** the parametrized SAT Solver *)
|
||||
module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
|
||||
|
||||
(* TODO: move somewhere else? where it can be used to implement the new
|
||||
proof module?
|
||||
module Pre_proof = struct
|
||||
module SP = Sat_solver.Proof
|
||||
module SC = Sat_solver.Clause
|
||||
|
||||
type t = {
|
||||
solver: Sat_solver.t;
|
||||
msat: Sat_solver.Proof.t;
|
||||
tdefs: (term*term) list; (* term definitions *)
|
||||
p: P.t lazy_t;
|
||||
}
|
||||
|
||||
let to_proof (self:t) : P.t = Lazy.force self.p
|
||||
|
||||
let pp_dot =
|
||||
let module Dot =
|
||||
Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
|
||||
let pp out self = Dot.pp (Sat_solver.store self.solver) out self.msat in
|
||||
Some pp
|
||||
|
||||
(* export to proof {!P.t}, translating Msat-level proof ising:
|
||||
- [stepc 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. (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
|
||||
*)
|
||||
let conv_proof (store:Sat_solver.store) (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t =
|
||||
let assms = ref [] in
|
||||
let steps = ref [] in
|
||||
|
||||
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.t) : string =
|
||||
try SC.Tbl.find n_tbl_ (SP.conclusion p)
|
||||
with Not_found ->
|
||||
Error.errorf
|
||||
"msat-solver.pre-proof.to_proof: cannot find proof step with conclusion %a"
|
||||
(SC.pp store) (SP.conclusion p)
|
||||
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 name = Printf.sprintf "c%d" !n_step in
|
||||
incr n_step;
|
||||
|
||||
SC.Tbl.add n_tbl_ c name;
|
||||
|
||||
(* 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 store a) in
|
||||
P.lit_mk sign t
|
||||
in
|
||||
let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l store 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 store) c
|
||||
in
|
||||
incr n_step;
|
||||
assms := (name, lit) :: !assms;
|
||||
P.ref_by_name name
|
||||
|
||||
| Lemma pr -> pr
|
||||
|
||||
| Duplicate (c, _) ->
|
||||
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 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 = SC.n_atoms store (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 (
|
||||
let pivot = Lit.term (Sat_solver.Atom.formula store pivot) in
|
||||
P.r proof_p' ~pivot
|
||||
)
|
||||
in
|
||||
P.hres_iter proof_init
|
||||
(Iter.of_list steps |> Iter.map tr_step)
|
||||
in
|
||||
|
||||
let step = P.stepc ~name concl pr_step in
|
||||
add_step step;
|
||||
)
|
||||
in
|
||||
|
||||
(* this should traverse from the leaves, so that order of [steps] is correct *)
|
||||
Sat_solver.Proof.fold store tr_node_to_step () msat;
|
||||
let assms = !assms in
|
||||
|
||||
(* gather all term definitions *)
|
||||
let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in
|
||||
P.composite_l ~assms (CCList.append t_defs (List.rev !steps))
|
||||
|
||||
let make solver (msat: Sat_solver.Proof.t) (tdefs: _ list) : t =
|
||||
{ solver; msat; tdefs; p=lazy (conv_proof (Sat_solver.store solver) msat tdefs) }
|
||||
|
||||
let check self = SP.check (Sat_solver.store self.solver) self.msat
|
||||
let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self)
|
||||
let output oc (self:t) = P.Quip.output oc (to_proof self)
|
||||
end
|
||||
*)
|
||||
|
||||
(* main solver state *)
|
||||
type t = {
|
||||
si: Solver_internal.t;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue