mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-24 02:16:41 -05:00
refactor(proof): new serialization; faster implem
This commit is contained in:
Simon Cruanes
parent
19e083c682
commit
2eee760e29
9 changed files with 207 additions and 121 deletions
|
|
@ -287,6 +287,7 @@ module Ty : sig
|
|||
val bool : state -> t
|
||||
val real : state -> t
|
||||
val atomic : def -> t list -> t
|
||||
val id_of_def : def -> ID.t
|
||||
|
||||
val atomic_uninterpreted : ID.t -> t
|
||||
|
||||
|
|
@ -399,6 +400,10 @@ end = struct
|
|||
make_ (Ty_atomic {def; args; finite=true;})
|
||||
|
||||
let atomic_uninterpreted id = atomic (Ty_uninterpreted id) []
|
||||
let id_of_def = function
|
||||
| Ty_uninterpreted id -> id
|
||||
| Ty_def {id;_} -> id
|
||||
| Ty_data {data} -> data.data_id
|
||||
|
||||
let is_bool t =
|
||||
match t.ty_view with | Ty_bool -> true | _ -> false
|
||||
|
|
@ -1095,6 +1100,7 @@ module Cstor = struct
|
|||
cstor_ty_as_data: data;
|
||||
cstor_ty: ty lazy_t;
|
||||
}
|
||||
let id c = c.cstor_id
|
||||
let ty_args c =
|
||||
Lazy.force c.cstor_args |> Iter.of_list |> Iter.map Select.ty
|
||||
let equal = eq_cstor
|
||||
|
|
|
|||
|
|
@ -292,113 +292,202 @@ end
|
|||
|
||||
Print to a format for checking by an external tool *)
|
||||
module Quip = struct
|
||||
module type OUT = sig
|
||||
type out
|
||||
type printer = out -> unit
|
||||
val l : printer list -> printer
|
||||
val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer
|
||||
(* list of steps, should be printed vertically if possible *)
|
||||
val a : string -> printer
|
||||
end
|
||||
|
||||
(*
|
||||
TODO: make sure we print terms properly
|
||||
*)
|
||||
|
||||
(* TODO: print into a buffer, without Format (should be faster) *)
|
||||
(* TODO: print as C-sexp *)
|
||||
module Make(Out : OUT) = struct
|
||||
open Out
|
||||
|
||||
let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l
|
||||
let pp_a ppx out l = Fmt.(array ~sep:(return "@ ") ppx) out l
|
||||
let pp_cl ~pp_t out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l (pp_lit_with ~pp_t)) c
|
||||
let rec pp_t sharing (t:Term.t) : printer =
|
||||
match T.Tbl.find_opt sharing.Compress.terms t with
|
||||
| Some (Named (N_s s)) -> a s(* use the newly introduced name *)
|
||||
| Some (Named (N_t t)) -> pp_t sharing t (* use name *)
|
||||
| _ -> pp_t_nonshare_root sharing t
|
||||
|
||||
let rec pp_rec (sharing:Compress.sharing_info) out (self:t) : unit =
|
||||
let pp_rec = pp_rec sharing in
|
||||
let pp_t = pp_t sharing in
|
||||
let pp_cl = pp_cl ~pp_t in
|
||||
match self with
|
||||
| Unspecified -> Fmt.string out "<unspecified>"
|
||||
| Named s -> Fmt.fprintf out "(ref %s)" s
|
||||
| CC_lemma l ->
|
||||
Fmt.fprintf out "(@[cc-lemma@ %a@])" pp_cl l
|
||||
| CC_lemma_imply (l,t,u) ->
|
||||
Fmt.fprintf out "(@[cc-lemma-imply@ (@[%a@])@ (@[=@ %a@ %a@])@])"
|
||||
(pp_l pp_rec) l pp_t t pp_t u
|
||||
| Refl t -> Fmt.fprintf out "(@[refl@ %a@])" pp_t t
|
||||
| Sorry -> Fmt.string out "sorry"
|
||||
| Sorry_c c -> Fmt.fprintf out "(@[sorry-c@ %a@])" pp_cl c
|
||||
| Bool_true_is_true -> Fmt.string out "true-is-true"
|
||||
| Bool_true_neq_false -> Fmt.string out "(@[!= T F@])"
|
||||
| Bool_eq (a,b) ->
|
||||
Fmt.fprintf out "(@[bool-eq@ %a@ %a@])"
|
||||
pp_t a pp_t b
|
||||
| Bool_c (name,ts) ->
|
||||
Fmt.fprintf out "(@[bool-c %s@ %a@])" name (pp_l pp_t) ts
|
||||
| Nn p -> Fmt.fprintf out "(@[nn@ %a@])" pp_rec p
|
||||
| Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t t
|
||||
| Assertion_c c ->
|
||||
Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c
|
||||
| Hres (c, l) ->
|
||||
Fmt.fprintf out "(@[hres@ (@[init@ %a@])@ %a@])" pp_rec c
|
||||
(pp_l (pp_hres_step sharing)) l
|
||||
| DT_isa_split (ty,l) ->
|
||||
Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])"
|
||||
Ty.pp ty (pp_l pp_t) l
|
||||
| DT_isa_disj (ty,t,u) ->
|
||||
Fmt.fprintf out "(@[dt.isa.disj@ (@[ty %a@])@ %a@ %a@])"
|
||||
Ty.pp ty pp_t t pp_t u
|
||||
| DT_cstor_inj (c,i,ts,us) ->
|
||||
Fmt.fprintf out "(@[dt.cstor.inj %d@ (@[%a@ %a@])@ (@[%a@ %a@])@])"
|
||||
i Cstor.pp c (pp_l pp_t) ts Cstor.pp c (pp_l pp_t) us
|
||||
| Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" pp_t t
|
||||
| Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" pp_t t
|
||||
| LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c
|
||||
| Composite {steps; assumptions} ->
|
||||
let pp_ass out (n,a) =
|
||||
Fmt.fprintf out "(@[assuming@ (name %s) %a@])" n (pp_lit_with ~pp_t) a in
|
||||
Fmt.fprintf out "(@[steps@ (@[%a@])@ (@[<hv>%a@])@])"
|
||||
(pp_l pp_ass) assumptions (pp_a (pp_composite_step sharing)) steps
|
||||
and pp_t_nonshare_root sharing t =
|
||||
let pp_t = pp_t sharing in
|
||||
match Term.view t with
|
||||
| Bool true -> a"true"
|
||||
| Bool false -> a"false"
|
||||
| App_fun (c, args) when IArray.is_empty args -> a (ID.to_string (id_of_fun c))
|
||||
| App_fun (c, args) ->
|
||||
l(a (ID.to_string (id_of_fun c)) :: IArray.to_list_map pp_t args)
|
||||
| Eq (t,u) -> l[a"=";pp_t t;pp_t u]
|
||||
| Not u -> l[a"not";pp_t u]
|
||||
| Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3]
|
||||
| LRA lra ->
|
||||
begin match lra with
|
||||
| LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2]
|
||||
| LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2]
|
||||
| LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x]
|
||||
| LRA_const q -> a(Q.to_string q)
|
||||
| LRA_simplex_var v -> pp_t v
|
||||
| LRA_simplex_pred (v, op, q) ->
|
||||
l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)]
|
||||
| LRA_other x -> pp_t x
|
||||
end
|
||||
|
||||
and pp_t sharing out (t:T.t) =
|
||||
match T.Tbl.find_opt sharing.Compress.terms t with
|
||||
| Some (Named (N_s s)) ->
|
||||
Fmt.string out s (* use the newly introduced name *)
|
||||
| Some (Named (N_t t)) -> pp_t sharing out t (* use name *)
|
||||
| _ -> pp_t_noshare_root sharing out t
|
||||
let rec pp_ty ty : printer =
|
||||
match Ty.view ty with
|
||||
| Ty_bool -> a"Bool"
|
||||
| Ty_real -> a"Real"
|
||||
| Ty_atomic {def;args=[];finite=_} ->
|
||||
let id = Ty.id_of_def def in
|
||||
a(ID.to_string id)
|
||||
| Ty_atomic {def;args;finite=_} ->
|
||||
let id = Ty.id_of_def def in
|
||||
l(a(ID.to_string id)::List.map pp_ty args)
|
||||
|
||||
and pp_t_noshare_root sharing out t =
|
||||
Base_types.pp_term_view_gen ~pp_id:ID.pp_name
|
||||
~pp_t:(pp_t sharing) out (T.view t)
|
||||
let pp_l ppx xs = l (List.map ppx xs)
|
||||
let pp_lit ~pp_t lit = match lit with
|
||||
| L_a(b,t) -> l[a(if b then"+" else"-");pp_t t]
|
||||
| L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]]
|
||||
let pp_cl ~pp_t c =
|
||||
l (a "cl" :: List.map (pp_lit ~pp_t) c)
|
||||
|
||||
and pp_composite_step sharing out step =
|
||||
let pp_t = pp_t sharing in
|
||||
let pp_cl = pp_cl ~pp_t in
|
||||
match step with
|
||||
| S_step_c {name;res;proof} ->
|
||||
Fmt.fprintf out "(@[stepc %s@ %a@ %a@])" name pp_cl res (pp_rec sharing) proof
|
||||
| S_define_t (c,rhs) ->
|
||||
Fmt.fprintf out "(@[deft@ %a@ %a@])"
|
||||
Term.pp c (pp_t_noshare_root sharing) rhs
|
||||
| S_define_t_name (c,rhs) ->
|
||||
Fmt.fprintf out "(@[deft@ %s@ %a@])"
|
||||
c (pp_t_noshare_root sharing) rhs
|
||||
let rec pp_rec (sharing:Compress.sharing_info) (self:t) : printer =
|
||||
let pp_rec = pp_rec sharing in
|
||||
let pp_t = pp_t sharing in
|
||||
let pp_cl = pp_cl ~pp_t in
|
||||
match self with
|
||||
| Unspecified -> a "<unspecified>"
|
||||
| Named s -> l[a "@"; a s]
|
||||
| CC_lemma c -> l[a"ccl"; pp_cl c]
|
||||
| CC_lemma_imply (hyps,t,u) ->
|
||||
l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u]
|
||||
| Refl t -> l[a"refl"; pp_t t]
|
||||
| Sorry -> a"sorry"
|
||||
| Sorry_c c -> l[a"sorry-c"; pp_cl c]
|
||||
| Bool_true_is_true -> a"true-is-true"
|
||||
| Bool_true_neq_false -> a"true-neq-false"
|
||||
| Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2]
|
||||
| Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts)
|
||||
| Nn p -> l[a"nn";pp_rec p]
|
||||
| Assertion t -> l[a"assert";pp_t t]
|
||||
| Assertion_c c -> l[a"assert-c";pp_cl c]
|
||||
| Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)]
|
||||
| DT_isa_split (ty,cs) ->
|
||||
l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)]
|
||||
| DT_isa_disj (ty,t,u) ->
|
||||
l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u]
|
||||
| DT_cstor_inj (c,i,ts,us) ->
|
||||
l[a"dt.cstor.inj";a(ID.to_string(Cstor.id c));
|
||||
a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)]
|
||||
| Ite_true t -> l[a"ite-true"; pp_t t]
|
||||
| Ite_false t -> l[a"ite-false"; pp_t t]
|
||||
| LRA c -> l[a"lra";pp_cl c]
|
||||
| Composite {steps; assumptions} ->
|
||||
let pp_ass (n,ass) : printer =
|
||||
l[a"assuming";a n;pp_lit ~pp_t ass] in
|
||||
l[a"steps";l(List.map pp_ass assumptions);
|
||||
iter_toplist (pp_composite_step sharing) (Iter.of_array steps)]
|
||||
|
||||
(*
|
||||
| S_define_t (name, t) ->
|
||||
Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t
|
||||
*)
|
||||
and pp_composite_step sharing step : printer =
|
||||
let pp_t = pp_t sharing in
|
||||
let pp_cl = pp_cl ~pp_t in
|
||||
match step with
|
||||
| S_step_c {name;res;proof} ->
|
||||
l[a"stepc";a name;pp_cl res;pp_rec sharing proof]
|
||||
| S_define_t (c,rhs) ->
|
||||
(* disable sharing for [rhs], otherwise it'd print [c] *)
|
||||
l[a"deft";pp_t c; pp_t_nonshare_root sharing rhs]
|
||||
| S_define_t_name (c,rhs) ->
|
||||
l[a"deft";a c; pp_t_nonshare_root sharing rhs]
|
||||
|
||||
and pp_hres_step sharing out = function
|
||||
| R {pivot; p} ->
|
||||
Fmt.fprintf out "(@[r@ (@[pivot@ %a@])@ %a@])" (pp_t sharing) pivot (pp_rec sharing) p
|
||||
| R1 p -> Fmt.fprintf out "(@[r1@ %a@])" (pp_rec sharing) p
|
||||
| P {p; lhs; rhs} ->
|
||||
Fmt.fprintf out "(@[r@ (@[lhs@ %a@])@ (@[rhs@ %a@])@ %a@])"
|
||||
(pp_t sharing) lhs (pp_t sharing) rhs (pp_rec sharing) p
|
||||
| P1 p -> Fmt.fprintf out "(@[p1@ %a@])" (pp_rec sharing) p
|
||||
(*
|
||||
| S_define_t (name, t) ->
|
||||
Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t
|
||||
*)
|
||||
|
||||
(* toplevel wrapper *)
|
||||
let pp out self =
|
||||
(* find sharing *)
|
||||
let sharing = Profile.with1 "proof.find-sharing" Compress.find_sharing self in
|
||||
(* introduce names *)
|
||||
let self = Profile.with2 "proof.rename" Compress.rename sharing self in
|
||||
(* now print *)
|
||||
Fmt.fprintf out "(@[quip 1@ %a@])" (pp_rec sharing) self
|
||||
and pp_hres_step sharing = function
|
||||
| R {pivot; p} -> l[a"r";pp_t sharing pivot; pp_rec sharing p]
|
||||
| R1 p -> l[a"r1";pp_rec sharing p]
|
||||
| P {p; lhs; rhs} ->
|
||||
l[a"r"; pp_t sharing lhs; pp_t sharing rhs; pp_rec sharing p]
|
||||
| P1 p -> l[a"p1"; pp_rec sharing p]
|
||||
|
||||
let pp_debug out self : unit =
|
||||
pp_rec Compress.no_sharing out self
|
||||
(* toplevel wrapper *)
|
||||
let pp self : printer =
|
||||
(* find sharing *)
|
||||
let sharing = Profile.with1 "proof.find-sharing" Compress.find_sharing self in
|
||||
(* introduce names *)
|
||||
let self = Profile.with2 "proof.rename" Compress.rename sharing self in
|
||||
(* now print *)
|
||||
l[a"quip"; a"1"; pp_rec sharing self]
|
||||
|
||||
let pp_debug ~sharing self : printer =
|
||||
if sharing then pp self
|
||||
else pp_rec Compress.no_sharing self
|
||||
end
|
||||
|
||||
module Out_csexp = struct
|
||||
type out = out_channel
|
||||
type printer = out -> unit
|
||||
let l prs out =
|
||||
output_char out '(';
|
||||
List.iter (fun x->x out) prs;
|
||||
output_char out ')'
|
||||
let a s out = Printf.fprintf out "%d:%s" (String.length s) s
|
||||
let iter_toplist f it out =
|
||||
output_char out '(';
|
||||
it (fun x -> f x out);
|
||||
output_char out ')'
|
||||
end
|
||||
|
||||
module Out_sexp = struct
|
||||
type out = out_channel
|
||||
type printer = out -> unit
|
||||
let l prs out =
|
||||
output_char out '(';
|
||||
List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs;
|
||||
output_char out ')'
|
||||
let a =
|
||||
let buf = Buffer.create 128 in
|
||||
fun s out ->
|
||||
Buffer.clear buf;
|
||||
CCSexp.to_buf buf (`Atom s);
|
||||
Buffer.output_buffer out buf
|
||||
let iter_toplist f it out =
|
||||
output_char out '(';
|
||||
let first=ref true in
|
||||
it (fun x -> if !first then first := false else output_char out '\n'; f x out);
|
||||
output_char out ')'
|
||||
end
|
||||
|
||||
let output oc (self:t) : unit =
|
||||
(* canonical sexp *)
|
||||
if true then (
|
||||
let module M = Make(Out_sexp) in M.pp self oc
|
||||
) else (
|
||||
let module M = Make(Out_csexp) in M.pp self oc
|
||||
)
|
||||
end
|
||||
|
||||
let pp_debug = Quip.pp_debug
|
||||
let pp_debug ~sharing out p =
|
||||
let module Out = struct
|
||||
type out = Format.formatter
|
||||
type printer = out -> unit
|
||||
let l prs out =
|
||||
Fmt.fprintf out "(@[";
|
||||
List.iteri(fun i x -> if i>0 then Fmt.fprintf out "@ "; x out) prs;
|
||||
Fmt.fprintf out "@])"
|
||||
let a s out = Fmt.string out s
|
||||
let iter_toplist f it out =
|
||||
Fmt.fprintf out "(@[<v>";
|
||||
let first=ref true in
|
||||
it (fun x -> if !first then first := false else Fmt.fprintf out "@ "; f x out);
|
||||
Fmt.fprintf out "@])"
|
||||
end
|
||||
in
|
||||
let module M = Quip.Make(Out) in
|
||||
M.pp_debug ~sharing p out
|
||||
|
|
|
|||
|
|
@ -169,7 +169,7 @@ module Make (A: CC_ARG)
|
|||
| E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
|
||||
| E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
|
||||
| E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
|
||||
| E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp_debug p
|
||||
| E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" (P.pp_debug ~sharing:false) p
|
||||
| E_and (a,b) ->
|
||||
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
|
||||
|
||||
|
|
|
|||
|
|
@ -209,10 +209,10 @@ module type PROOF = sig
|
|||
|
||||
val default : t [@@alert cstor "do not use default constructor"]
|
||||
|
||||
val pp_debug : t Fmt.printer
|
||||
val pp_debug : sharing:bool -> t Fmt.printer
|
||||
|
||||
module Quip : sig
|
||||
val pp : t Fmt.printer
|
||||
val output : out_channel -> t -> unit
|
||||
(** Printer in Quip format (experimental) *)
|
||||
end
|
||||
end
|
||||
|
|
@ -1004,7 +1004,10 @@ module type SOLVER = sig
|
|||
module Pre_proof : sig
|
||||
type t
|
||||
|
||||
val pp : t Fmt.printer
|
||||
val output : out_channel -> t -> unit
|
||||
(** Output onto a channel, efficiently *)
|
||||
|
||||
val pp_debug : t Fmt.printer
|
||||
|
||||
val pp_dot : t Fmt.printer option
|
||||
(** Optional printer into DOT/graphviz *)
|
||||
|
|
|
|||
|
|
@ -177,7 +177,7 @@ let main () =
|
|||
Process.process_stmt
|
||||
~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file
|
||||
~time:!time_limit ~memory:!size_limit
|
||||
?dot_proof ~pp_proof:!p_proof ~pp_model:!p_model
|
||||
?dot_proof ~pp_model:!p_model
|
||||
~check:!check ~progress:!p_progress
|
||||
solver)
|
||||
() input
|
||||
|
|
|
|||
|
|
@ -352,7 +352,7 @@ module Make(A : ARG)
|
|||
if not (Lit.equal lit lit') then (
|
||||
Log.debugf 10
|
||||
(fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])"
|
||||
Lit.pp lit Lit.pp lit' P.pp_debug p);
|
||||
Lit.pp lit Lit.pp lit' (P.pp_debug ~sharing:false) p);
|
||||
);
|
||||
|
||||
lit', p
|
||||
|
|
@ -639,7 +639,8 @@ module Make(A : ARG)
|
|||
{ msat; tdefs; p=lazy (conv_proof msat tdefs) }
|
||||
|
||||
let check self = SP.check self.msat
|
||||
let pp out (self:t) = P.Quip.pp out (to_proof self)
|
||||
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 *)
|
||||
|
|
@ -828,7 +829,7 @@ module Make(A : ARG)
|
|||
let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit =
|
||||
Stat.incr self.count_clause;
|
||||
Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])"
|
||||
(Util.pp_iarray Atom.pp) c P.pp_debug proof);
|
||||
(Util.pp_iarray Atom.pp) c (P.pp_debug ~sharing:false) proof);
|
||||
let pb = Profile.begin_ "add-clause" in
|
||||
Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof;
|
||||
Profile.exit pb
|
||||
|
|
|
|||
|
|
@ -143,7 +143,6 @@ let solve
|
|||
?gc:_
|
||||
?restarts:_
|
||||
?dot_proof
|
||||
?(pp_proof=false)
|
||||
?(pp_model=false)
|
||||
?proof_file
|
||||
?(check=false)
|
||||
|
|
@ -179,7 +178,7 @@ let solve
|
|||
| Solver.Unsat {proof;_} ->
|
||||
|
||||
let proof_opt =
|
||||
if check||pp_proof then Lazy.force proof
|
||||
if check||CCOpt.is_some proof_file then Lazy.force proof
|
||||
else None
|
||||
in
|
||||
|
||||
|
|
@ -207,24 +206,13 @@ let solve
|
|||
Profile.with_ "proof.write-file" @@ fun () ->
|
||||
let p = Profile.with1 "proof.mk-proof" Solver.Pre_proof.to_proof p in
|
||||
CCIO.with_out file
|
||||
(fun oc ->
|
||||
let fmt = Format.formatter_of_out_channel oc in
|
||||
Fmt.fprintf fmt "%a@." Proof.Quip.pp p);
|
||||
(fun oc -> Proof.Quip.output oc p; flush oc)
|
||||
| _ -> ()
|
||||
end;
|
||||
|
||||
let t3 = Sys.time () -. t2 in
|
||||
Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
|
||||
|
||||
(* TODO: allow to print proof into a file, more realistic for checking *)
|
||||
if pp_proof then (
|
||||
match proof_opt with
|
||||
| None -> Error.errorf "cannot print proof, none was generated"
|
||||
| Some p ->
|
||||
let p = Solver.Pre_proof.to_proof p in
|
||||
Fmt.printf "(@[proof@ %a@])@." Solver.P.Quip.pp p;
|
||||
);
|
||||
|
||||
| Solver.Unknown reas ->
|
||||
Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
|
||||
end
|
||||
|
|
@ -233,7 +221,7 @@ let solve
|
|||
let process_stmt
|
||||
?hyps
|
||||
?gc ?restarts ?(pp_cnf=false)
|
||||
?dot_proof ?pp_proof ?proof_file ?pp_model ?(check=false)
|
||||
?dot_proof ?proof_file ?pp_model ?(check=false)
|
||||
?time ?memory ?progress
|
||||
(solver:Solver.t)
|
||||
(stmt:Statement.t) : unit or_error =
|
||||
|
|
@ -272,7 +260,7 @@ let process_stmt
|
|||
l
|
||||
in
|
||||
solve
|
||||
?gc ?restarts ?dot_proof ~check ?pp_proof ?proof_file ?pp_model
|
||||
?gc ?restarts ?dot_proof ~check ?proof_file ?pp_model
|
||||
?time ?memory ?progress
|
||||
~assumptions ?hyps
|
||||
solver;
|
||||
|
|
|
|||
|
|
@ -25,7 +25,6 @@ val process_stmt :
|
|||
?restarts:bool ->
|
||||
?pp_cnf:bool ->
|
||||
?dot_proof:string ->
|
||||
?pp_proof:bool ->
|
||||
?proof_file:string ->
|
||||
?pp_model:bool ->
|
||||
?check:bool ->
|
||||
|
|
|
|||
|
|
@ -360,7 +360,7 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
| Some (u, pr_t_u) ->
|
||||
Log.debugf 5
|
||||
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])"
|
||||
T.pp t T.pp u SI.P.Quip.pp pr_t_u);
|
||||
T.pp t T.pp u (SI.P.pp_debug ~sharing:false) pr_t_u);
|
||||
SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
|
||||
());
|
||||
end;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue