From 57bf44dfb928de615c395bb6930128b33cb641b9 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 4 Apr 2021 18:50:23 -0400 Subject: [PATCH] feat: basic proof production for QF_UF (wip) --- src/cc/Sidekick_cc.ml | 22 ++++++++++++++--- src/core/Sidekick_core.ml | 16 +++++++----- src/main/main.ml | 10 +++++--- src/msat-solver/Sidekick_msat_solver.ml | 3 ++- src/smtlib/Process.ml | 33 ++++++++++++++++++------- src/smtlib/Process.mli | 1 + src/smtlib/Sidekick_smtlib.ml | 7 +----- 7 files changed, 63 insertions(+), 29 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 30f3a67e..7286c1d2 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -373,14 +373,14 @@ module Make (A: CC_ARG) n.n_expl <- FL_none; end - let raise_conflict (cc:t) ~th (acts:actions) (e:lit list) : _ = + let raise_conflict_ (cc:t) ~th (acts:actions) (e:lit list) p : _ = Profile.instant "cc.conflict"; (* clear tasks queue *) Vec.clear cc.pending; Vec.clear cc.combine; List.iter (fun f -> f cc ~th e) cc.on_conflict; Stat.incr cc.count_conflict; - Actions.raise_conflict acts e P.default + Actions.raise_conflict acts e p let[@inline] all_classes cc : repr Iter.t = T_tbl.values cc.tbl @@ -652,7 +652,14 @@ module Make (A: CC_ARG) let lits = explain_decompose cc ~th [] e_ab in let lits = explain_pair cc ~th lits a ra in let lits = explain_pair cc ~th lits b rb in - raise_conflict cc ~th:!th acts (List.rev_map Lit.neg lits) + let proof = + let lits = + Iter.of_list lits + |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit) + in + P.make_cc lits + in + raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof ); (* We will merge [r_from] into [r_into]. we try to ensure that [size ra <= size rb] in general, but always @@ -833,7 +840,14 @@ module Make (A: CC_ARG) let th = ref true in let lits = explain_decompose cc ~th [] expl in let lits = List.rev_map Lit.neg lits in - raise_conflict cc ~th:!th acts lits + let proof = + let lits = + Iter.of_list lits + |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit) + in + P.make_cc lits + in + raise_conflict_ cc ~th:!th acts lits proof let merge cc n1 n2 expl = Log.debugf 5 diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index a93a0616..04057117 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -146,10 +146,11 @@ module type TERM = sig end module type PROOF = sig + type term type t val pp : t Fmt.printer - val default : t + val make_cc : (term*bool) Iter.t -> t end (** Literals @@ -192,9 +193,10 @@ end is inconsistent *) module type CC_ACTIONS = sig module T : TERM - module P : PROOF module Lit : LIT with module T = T + module P : PROOF with type term = T.Term.t + type t (** An action handle. It is used by the congruence closure to perform the actions below. How it performs the actions @@ -220,7 +222,7 @@ end (** Arguments to a congruence closure's implementation *) module type CC_ARG = sig module T : TERM - module P : PROOF + module P : PROOF with type term = T.Term.t module Lit : LIT with module T = T module Actions : CC_ACTIONS with module T=T and module P = P and module Lit = Lit @@ -231,7 +233,7 @@ end (** Signature of the congruence closure *) module type CC_S = sig module T : TERM - module P : PROOF + module P : PROOF with type term = T.Term.t module Lit : LIT with module T = T module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P type term_state = T.Term.state @@ -491,7 +493,7 @@ end new lemmas, propagate literals, access the congruence closure, etc. *) module type SOLVER_INTERNAL = sig module T : TERM - module P : PROOF + module P : PROOF with type term = T.Term.t type ty = T.Ty.t type term = T.Term.t @@ -728,7 +730,8 @@ end Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *) module type SOLVER = sig module T : TERM - module P : PROOF + module P : PROOF with type term = T.Term.t + module Lit : LIT with module T = T module Solver_internal @@ -854,6 +857,7 @@ module type SOLVER = sig type t val check : t -> unit val pp_dot : t Fmt.printer + val pp : t Fmt.printer end type proof = Proof.t diff --git a/src/main/main.ml b/src/main/main.ml index fa77de89..cc2bc7f7 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -21,7 +21,7 @@ exception Out_of_space let file = ref "" let p_cnf = ref false let p_dot_proof = ref "" -let p_proof_print = ref false +let p_proof = ref false let p_model = ref false let check = ref false let time_limit = ref 300. @@ -71,6 +71,8 @@ let argspec = Arg.align [ "--no-restarts", Arg.Clear restarts, " disable restarts"; "--dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file"; "--stat", Arg.Set p_stat, " print statistics"; + "--proof", Arg.Set p_proof, " print proof"; + "--no-proof", Arg.Clear p_proof, " do not print proof"; "--model", Arg.Set p_model, " print model"; "--no-model", Arg.Clear p_model, " do not print model"; "--gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC"; @@ -151,7 +153,8 @@ let main () = Process.th_lra; ] in - Process.Solver.create ~store_proof:!check ~theories tst () () + let store_proof = !check || !p_proof in + Process.Solver.create ~store_proof ~theories tst () () in if !check then ( (* might have to check conflicts *) @@ -171,7 +174,8 @@ let main () = Process.process_stmt ~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ~time:!time_limit ~memory:!size_limit - ?dot_proof ~pp_model:!p_model ~check:!check ~progress:!p_progress + ?dot_proof ~pp_proof:!p_proof ~pp_model:!p_model + ~check:!check ~progress:!p_progress solver) () input with Exit -> diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 3458bf4d..f8d7d287 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -13,7 +13,7 @@ module Log = Msat.Log module type ARG = sig open Sidekick_core module T : TERM - module P : PROOF + module P : PROOF with type term = T.Term.t val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t @@ -435,6 +435,7 @@ module Make(A : ARG) include Sat_solver.Proof module Dot = Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) let pp_dot = Dot.pp + let pp out (_self:t) = Fmt.string out "" (* TODO *) end type proof = Proof.t diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 42d0cee6..8688b932 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -17,11 +17,7 @@ module Solver_arg = struct let cc_view = Term.cc_view let is_valid_literal _ = true - module P = struct - type t = Default - let default=Default - let pp out _ = Fmt.string out "default" - end + module P = Proof end module Solver = Sidekick_msat_solver.Make(Solver_arg) @@ -147,6 +143,7 @@ let solve ?gc:_ ?restarts:_ ?dot_proof + ?(pp_proof=false) ?(pp_model=false) ?(check=false) ?time:_ ?memory:_ ?(progress=false) @@ -179,12 +176,19 @@ let solve let t3 = Sys.time () -. t2 in Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; | Solver.Unsat {proof;_} -> + + let proof_opt = + if check||pp_proof then Lazy.force proof + else None + in + if check then ( - match proof with - | lazy (Some p) -> + match proof_opt with + | Some p -> Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p); | _ -> () ); + begin match dot_proof, proof with | None, _ -> () | Some file, lazy (Some p) -> @@ -197,8 +201,18 @@ let solve Format.pp_print_flush fmt (); 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 -> + Fmt.printf "(@[proof@ %a@])@." Solver.Proof.pp p; + ); + | Solver.Unknown reas -> Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas end @@ -206,7 +220,7 @@ let solve (* process a single statement *) let process_stmt ?hyps - ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?(check=false) + ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_proof ?pp_model ?(check=false) ?time ?memory ?progress (solver:Solver.t) (stmt:Statement.t) : unit or_error = @@ -240,7 +254,8 @@ let process_stmt List.map (fun (sign,t) -> Solver.mk_atom_t solver ~sign t) l in solve - ?gc ?restarts ?dot_proof ~check ?pp_model ?time ?memory ?progress + ?gc ?restarts ?dot_proof ~check ?pp_proof ?pp_model + ?time ?memory ?progress ~assumptions ?hyps solver; E.return() diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 03bec7e2..8779e99f 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -25,6 +25,7 @@ val process_stmt : ?restarts:bool -> ?pp_cnf:bool -> ?dot_proof:string -> + ?pp_proof:bool -> ?pp_model:bool -> ?check:bool -> ?time:float -> diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 370d98ee..8af04dec 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -1,7 +1,6 @@ (** {1 Process Statements} *) module ID = Sidekick_base_term.ID -module Fmt = CCFormat module E = CCResult module Loc = Smtlib_utils.V_2_6.Loc module Parse_ast = Smtlib_utils.V_2_6.Ast @@ -9,11 +8,7 @@ module Process = Process module Solver = Process.Solver module Term = Sidekick_base_term.Term module Stmt = Sidekick_base_term.Statement - -module Proof = struct - type t = Proof_default - let default = Proof_default -end +module Proof = Proof type 'a or_error = ('a, string) CCResult.t