diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 05695fe2..75b2f777 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -11,14 +11,16 @@ module Solver_arg = struct module T = Sidekick_base.Solver_arg module Lit = Sidekick_base.Lit - let cc_view = Term.cc_view + let view_as_cc = Term.cc_view let mk_eq = Term.eq let is_valid_literal _ = true - module P = Sidekick_base.Proof + module Proof_trace = Sidekick_base.Proof.Proof_trace + module Rule_core = Sidekick_base.Proof.Rule_core + module Rule_sat = Sidekick_base.Proof.Rule_sat - type proof = P.t - type proof_step = P.proof_step + type step_id = Proof_trace.A.step_id + type rule = Proof_trace.A.rule end module Solver = Sidekick_smt_solver.Make (Solver_arg) @@ -29,7 +31,6 @@ module Th_data = Sidekick_th_data.Make (struct module S = Solver open! Base_types open! Sidekick_th_data - module Proof = Proof module Cstor = Cstor let as_datatype ty = @@ -64,7 +65,7 @@ module Th_data = Sidekick_th_data.Make (struct let ty_is_finite = Ty.finite let ty_set_is_finite = Ty.set_finite - module P = Proof + module P = Proof.Rule_data end) (** Reducing boolean formulas to clauses *) @@ -74,12 +75,7 @@ module Th_bool = Sidekick_th_bool_static.Make (struct type term = S.T.Term.t include Form - - let lemma_bool_tauto = Proof.lemma_bool_tauto - let lemma_bool_c = Proof.lemma_bool_c - let lemma_bool_equiv = Proof.lemma_bool_equiv - let lemma_ite_true = Proof.lemma_ite_true - let lemma_ite_false = Proof.lemma_ite_false + module P = Proof.Rule_bool end) module Gensym = struct diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index f420e075..efd3852b 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -3,7 +3,7 @@ module Vec = Sidekick_util.Vec module Log = Sidekick_util.Log module Fmt = CCFormat -module CC_view = Sidekick_core.CC_view +module CC_view = Sidekick_sigs_cc.View module Proof_ser = Sidekick_base_proof_trace.Proof_ser module Storage = Sidekick_base_proof_trace.Storage diff --git a/src/base/ID.mli b/src/base/ID.mli index 32611ac1..0e96c3fa 100644 --- a/src/base/ID.mli +++ b/src/base/ID.mli @@ -37,10 +37,7 @@ val to_string : t -> string val to_string_full : t -> string (** Printer name and unique counter for this ID. *) -include Intf.EQ with type t := t -include Intf.ORD with type t := t -include Intf.HASH with type t := t -include Intf.PRINT with type t := t +include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t val pp_name : t CCFormat.printer diff --git a/src/base/Proof.ml b/src/base/Proof.ml index 96de480e..86aa110f 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -30,27 +30,13 @@ end (* a step is just a unique integer ID. The actual step is stored in the chunk_stack. *) -type proof_step = Proof_ser.ID.t +type step_id = Proof_ser.ID.t type term_id = Proof_ser.ID.t type lit = Lit.t type term = Term.t -type t = { - mutable enabled: bool; - buf: Buffer.t; - out: Proof_ser.Bare.Encode.t; - mutable storage: Storage.t; - dispose: unit -> unit; - mutable steps_writer: CS.Writer.t; - mutable next_id: int; - map_term: term_id Term.Tbl.t; (* term -> proof ID *) - map_fun: term_id Fun.Tbl.t; -} - -type proof_rule = t -> proof_step - module Step_vec = struct - type elt = proof_step + type elt = step_id type t = elt Vec.t let get = Vec.get @@ -71,6 +57,18 @@ module Step_vec = struct let to_iter = Vec.to_iter end +type t = { + mutable enabled: bool; + buf: Buffer.t; + out: Proof_ser.Bare.Encode.t; + mutable storage: Storage.t; + dispose: unit -> unit; + mutable steps_writer: CS.Writer.t; + mutable next_id: int; + map_term: term_id Term.Tbl.t; (* term -> proof ID *) + map_fun: term_id Fun.Tbl.t; +} + let disable (self : t) : unit = self.enabled <- false; self.storage <- Storage.No_store; @@ -114,7 +112,7 @@ let create ?(config = Config.default) () : t = let empty = create ~config:Config.empty () let iter_steps_backward (self : t) = Storage.iter_steps_backward self.storage -let dummy_step : proof_step = Int32.min_int +let dummy_step : step_id = Int32.min_int let[@inline] enabled (self : t) = self.enabled (* allocate a unique ID to refer to an event in the trace *) @@ -178,119 +176,178 @@ let emit_lit_ (self : t) (lit : Lit.t) : term_id = else Int32.neg t -let emit_ (self : t) f : proof_step = - if enabled self then ( - let view = f () in - let id = alloc_id self in - emit_step_ self { PS.Step.id; view }; - id - ) else - dummy_step - let emit_no_return_ (self : t) f : unit = if enabled self then ( let view = f () in emit_step_ self { PS.Step.id = -1l; view } ) -let[@inline] emit_redundant_clause lits ~hyps (self : t) = - emit_ self @@ fun () -> - let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in - let clause = Proof_ser.{ Clause.lits } in - let hyps = Iter.to_array hyps in - PS.Step_view.Step_rup { res = clause; hyps } +let emit_unsat c (self : t) : unit = + emit_no_return_ self @@ fun () -> PS.(Step_view.Step_unsat { Step_unsat.c }) -let emit_input_clause (lits : Lit.t Iter.t) (self : t) = - emit_ self @@ fun () -> - let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in - PS.(Step_view.Step_input { Step_input.c = { Clause.lits } }) +(** What a rule can return. It can return an existing step, or ask to create + a new one. *) +type rule_res = R_new of PS.Step_view.t | R_old of step_id -let define_term t u (self : t) = - emit_ self @@ fun () -> - let t = emit_term_ self t and u = emit_term_ self u in - PS.(Step_view.Expr_def { Expr_def.c = t; rhs = u }) +type rule = t -> rule_res -let proof_p1 rw_with c (self : t) = - emit_ self @@ fun () -> - PS.(Step_view.Step_proof_p1 { Step_proof_p1.c; rw_with }) - -let proof_r1 unit c (self : t) = - emit_ self @@ fun () -> PS.(Step_view.Step_proof_r1 { Step_proof_r1.c; unit }) - -let proof_res ~pivot c1 c2 (self : t) = - emit_ self @@ fun () -> - let pivot = emit_term_ self pivot in - PS.(Step_view.Step_proof_res { Step_proof_res.c1; c2; pivot }) - -let lemma_preprocess t u ~using (self : t) = - emit_ self @@ fun () -> - let t = emit_term_ self t and u = emit_term_ self u in - let using = using |> Iter.to_array in - PS.(Step_view.Step_preprocess { Step_preprocess.t; u; using }) - -let lemma_true t (self : t) = - emit_ self @@ fun () -> - let t = emit_term_ self t in - PS.(Step_view.Step_true { Step_true.true_ = t }) - -let lemma_cc lits (self : t) = - emit_ self @@ fun () -> - let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in - PS.(Step_view.Step_cc { Step_cc.eqns = lits }) - -let lemma_rw_clause c ~res ~using (self : t) = +let emit_rule_ (self : t) (f : rule) : step_id = if enabled self then ( - let using = Iter.to_array using in - if Array.length using = 0 then - c - (* useless step *) - else - emit_ self @@ fun () -> - let lits = Iter.map (emit_lit_ self) res |> Iter.to_array in - let res = Proof_ser.{ Clause.lits } in - PS.(Step_view.Step_clause_rw { Step_clause_rw.c; res; using }) + match f self with + | R_old id -> id + | R_new view -> + let id = alloc_id self in + emit_step_ self { PS.Step.id; view }; + id ) else dummy_step -(* TODO *) -let with_defs _ _ (_pr : t) = dummy_step +module Proof_trace = struct + module A = struct + type nonrec step_id = step_id + type nonrec rule = rule + + module Step_vec = Step_vec + end + + type nonrec t = t + + let enabled = enabled + let add_step = emit_rule_ + let[@inline] add_unsat self id = emit_unsat id self + let delete _ _ = () +end + +let r_new v = R_new v +let r_old id = R_old id + +module Rule_sat = struct + type nonrec lit = lit + type nonrec step_id = step_id + type nonrec rule = rule + + let sat_redundant_clause lits ~hyps : rule = + fun self -> + let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in + let clause = Proof_ser.{ Clause.lits } in + let hyps = Iter.to_array hyps in + r_new @@ PS.Step_view.Step_rup { res = clause; hyps } + + let sat_input_clause (lits : Lit.t Iter.t) : rule = + fun self -> + let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in + r_new @@ PS.(Step_view.Step_input { Step_input.c = { Clause.lits } }) + + (* TODO *) + let sat_unsat_core _ (_pr : t) = r_old dummy_step +end + +module Rule_core = struct + type nonrec term = term + type nonrec step_id = step_id + type nonrec rule = rule + type nonrec lit = lit + + let sat_redundant_clause lits ~hyps : rule = + fun self -> + let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in + let clause = Proof_ser.{ Clause.lits } in + let hyps = Iter.to_array hyps in + r_new @@ PS.Step_view.Step_rup { res = clause; hyps } + + let define_term t u : rule = + fun self -> + let t = emit_term_ self t and u = emit_term_ self u in + r_new @@ PS.(Step_view.Expr_def { Expr_def.c = t; rhs = u }) + + let proof_p1 rw_with c : rule = + fun _self -> + r_new @@ PS.(Step_view.Step_proof_p1 { Step_proof_p1.c; rw_with }) + + let proof_r1 unit c : rule = + fun _self -> r_new @@ PS.(Step_view.Step_proof_r1 { Step_proof_r1.c; unit }) + + let proof_res ~pivot c1 c2 : rule = + fun self -> + let pivot = emit_term_ self pivot in + r_new @@ PS.(Step_view.Step_proof_res { Step_proof_res.c1; c2; pivot }) + + let lemma_preprocess t u ~using : rule = + fun self -> + let t = emit_term_ self t and u = emit_term_ self u in + let using = using |> Iter.to_array in + r_new @@ PS.(Step_view.Step_preprocess { Step_preprocess.t; u; using }) + + let lemma_true t : rule = + fun self -> + let t = emit_term_ self t in + r_new @@ PS.(Step_view.Step_true { Step_true.true_ = t }) + + let lemma_cc lits : rule = + fun self -> + let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in + r_new @@ PS.(Step_view.Step_cc { Step_cc.eqns = lits }) + + let lemma_rw_clause c ~res ~using : rule = + fun self -> + let using = Iter.to_array using in + if Array.length using = 0 then + r_old c + (* useless step *) + else ( + let lits = Iter.map (emit_lit_ self) res |> Iter.to_array in + let res = Proof_ser.{ Clause.lits } in + r_new @@ PS.(Step_view.Step_clause_rw { Step_clause_rw.c; res; using }) + ) + + (* TODO *) + let with_defs _ _ (_pr : t) = r_old dummy_step +end (* not useful *) let del_clause _ _ (_pr : t) = () -(* TODO *) -let emit_unsat_core _ (_pr : t) = dummy_step +module Rule_bool = struct + type nonrec term = term + type nonrec lit = lit + type nonrec rule = rule -let emit_unsat c (self : t) : unit = - emit_no_return_ self @@ fun () -> PS.(Step_view.Step_unsat { Step_unsat.c }) + let lemma_bool_tauto lits : rule = + fun self -> + let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in + r_new @@ PS.(Step_view.Step_bool_tauto { Step_bool_tauto.lits }) -let lemma_bool_tauto lits (self : t) = - emit_ self @@ fun () -> - let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in - PS.(Step_view.Step_bool_tauto { Step_bool_tauto.lits }) + let lemma_bool_c rule (ts : Term.t list) : rule = + fun self -> + let exprs = Util.array_of_list_map (emit_term_ self) ts in + r_new @@ PS.(Step_view.Step_bool_c { Step_bool_c.exprs; rule }) -let lemma_bool_c rule (ts : Term.t list) (self : t) = - emit_ self @@ fun () -> - let exprs = ts |> Util.array_of_list_map (emit_term_ self) in - PS.(Step_view.Step_bool_c { Step_bool_c.exprs; rule }) + let lemma_bool_equiv _ _ _ = r_old dummy_step + let lemma_ite_true ~ite:_ _ = r_old dummy_step + let lemma_ite_false ~ite:_ _ = r_old dummy_step +end (* TODO *) -let lemma_lra _ _ = dummy_step -let lemma_relax_to_lra _ _ = dummy_step -let lemma_lia _ _ = dummy_step -let lemma_bool_equiv _ _ _ = dummy_step -let lemma_ite_true ~ite:_ _ = dummy_step -let lemma_ite_false ~ite:_ _ = dummy_step -let lemma_isa_cstor ~cstor_t:_ _ (_pr : t) = dummy_step -let lemma_select_cstor ~cstor_t:_ _ (_pr : t) = dummy_step -let lemma_isa_split _ _ (_pr : t) = dummy_step -let lemma_isa_sel _ (_pr : t) = dummy_step -let lemma_isa_disj _ _ (_pr : t) = dummy_step -let lemma_cstor_inj _ _ _ (_pr : t) = dummy_step -let lemma_cstor_distinct _ _ (_pr : t) = dummy_step -let lemma_acyclicity _ (_pr : t) = dummy_step +let lemma_lra _ _ = r_old dummy_step +let lemma_relax_to_lra _ _ = r_old dummy_step +let lemma_lia _ _ = r_old dummy_step + +module Rule_data = struct + type nonrec lit = lit + type nonrec rule = rule + type nonrec term = term + + let lemma_isa_cstor ~cstor_t:_ _ (_pr : t) = r_old dummy_step + let lemma_select_cstor ~cstor_t:_ _ (_pr : t) = r_old dummy_step + let lemma_isa_split _ _ (_pr : t) = r_old dummy_step + let lemma_isa_sel _ (_pr : t) = r_old dummy_step + let lemma_isa_disj _ _ (_pr : t) = r_old dummy_step + let lemma_cstor_inj _ _ _ (_pr : t) = r_old dummy_step + let lemma_cstor_distinct _ _ (_pr : t) = r_old dummy_step + let lemma_acyclicity _ (_pr : t) = r_old dummy_step +end module Unsafe_ = struct - let[@inline] id_of_proof_step_ (p : proof_step) : proof_step = p + let[@inline] id_of_proof_step_ (p : step_id) : step_id = p end diff --git a/src/base/Proof.mli b/src/base/Proof.mli index 50880768..3939fc79 100644 --- a/src/base/Proof.mli +++ b/src/base/Proof.mli @@ -28,39 +28,42 @@ end (** {2 Main Proof API} *) -type t +module Proof_trace : Sidekick_core.PROOF_TRACE + +type t = Proof_trace.t (** A container for the whole proof *) -type proof_step -(** A proof step in the trace. +type step_id = Proof_trace.A.step_id +type rule = Proof_trace.A.rule - The proof will store all steps, and at the end when we find the empty clause - we can filter them to keep only the relevant ones. *) +module Rule_sat : + Sidekick_core.SAT_PROOF_RULES + with type rule = rule + and type lit = Lit.t + and type step_id = step_id -include - Sidekick_core.PROOF - with type t := t - and type proof_step := proof_step +module Rule_core : + Sidekick_core.PROOF_CORE + with type rule = rule + and type lit = Lit.t + and type term = Term.t + and type step_id = step_id + +val lemma_lra : Lit.t Iter.t -> rule +val lemma_relax_to_lra : Lit.t Iter.t -> rule +val lemma_lia : Lit.t Iter.t -> rule + +module Rule_data : + Sidekick_th_data.PROOF_RULES + with type rule = rule and type lit = Lit.t and type term = Term.t -val lemma_lra : Lit.t Iter.t -> proof_rule -val lemma_relax_to_lra : Lit.t Iter.t -> proof_rule -val lemma_lia : Lit.t Iter.t -> proof_rule - -include - Sidekick_th_data.PROOF - with type proof := t - and type proof_step := proof_step - and type lit := Lit.t - and type term := Term.t - -include - Sidekick_th_bool_static.PROOF - with type proof := t - and type proof_step := proof_step - and type lit := Lit.t - and type term := Term.t +module Rule_bool : + Sidekick_th_bool_static.PROOF_RULES + with type rule = rule + and type lit = Lit.t + and type term = Term.t (** {2 Creation} *) @@ -83,5 +86,5 @@ val iter_steps_backward : t -> Proof_ser.Step.t Iter.t a dummy backend. *) module Unsafe_ : sig - val id_of_proof_step_ : proof_step -> Proof_ser.ID.t + val id_of_proof_step_ : step_id -> Proof_ser.ID.t end diff --git a/src/base/Proof_dummy.ml b/src/base/Proof_dummy.ml index 9818b4f0..af268417 100644 --- a/src/base/Proof_dummy.ml +++ b/src/base/Proof_dummy.ml @@ -2,40 +2,75 @@ open Base_types type lit = Lit.t type term = Term.t -type t = unit -type proof_step = unit -type proof_rule = t -> proof_step -module Step_vec = Vec_unit +module Arg = struct + type nonrec rule = unit + type nonrec step_id = unit + + module Step_vec = Vec_unit + + let dummy_step_id = () +end + +include Sidekick_proof_trace_dummy.Make (Arg) + +type rule = A.rule +type step_id = A.step_id let create () : t = () let with_proof _ _ = () -let enabled (_pr : t) = false -let del_clause _ _ (_pr : t) = () -let emit_redundant_clause _ ~hyps:_ _ = () -let emit_input_clause _ _ = () -let define_term _ _ _ = () -let emit_unsat _ _ = () -let proof_p1 _ _ (_pr : t) = () -let proof_r1 _ _ (_pr : t) = () -let proof_res ~pivot:_ _ _ (_pr : t) = () -let emit_unsat_core _ (_pr : t) = () -let lemma_preprocess _ _ ~using:_ (_pr : t) = () -let lemma_true _ _ = () -let lemma_cc _ _ = () -let lemma_rw_clause _ ~res:_ ~using:_ (_pr : t) = () -let with_defs _ _ (_pr : t) = () -let lemma_lra _ _ = () -let lemma_bool_tauto _ _ = () -let lemma_bool_c _ _ _ = () -let lemma_bool_equiv _ _ _ = () -let lemma_ite_true ~ite:_ _ = () -let lemma_ite_false ~ite:_ _ = () -let lemma_isa_cstor ~cstor_t:_ _ (_pr : t) = () -let lemma_select_cstor ~cstor_t:_ _ (_pr : t) = () -let lemma_isa_split _ _ (_pr : t) = () -let lemma_isa_sel _ (_pr : t) = () -let lemma_isa_disj _ _ (_pr : t) = () -let lemma_cstor_inj _ _ _ (_pr : t) = () -let lemma_cstor_distinct _ _ (_pr : t) = () -let lemma_acyclicity _ (_pr : t) = () + +module Rule_sat = struct + type nonrec rule = rule + type nonrec step_id = step_id + type nonrec lit = lit + + let sat_redundant_clause _ ~hyps:_ = () + let sat_input_clause _ = () + let sat_unsat_core _ = () +end + +module Rule_core = struct + type nonrec rule = rule + type nonrec step_id = step_id + type nonrec lit = lit + type nonrec term = term + + let define_term _ _ = () + let proof_p1 _ _ = () + let proof_r1 _ _ = () + let proof_res ~pivot:_ _ _ = () + let lemma_preprocess _ _ ~using:_ = () + let lemma_true _ = () + let lemma_cc _ = () + let lemma_rw_clause _ ~res:_ ~using:_ = () + let with_defs _ _ = () +end + +let lemma_lra _ = () + +module Rule_bool = struct + type nonrec rule = rule + type nonrec lit = lit + + let lemma_bool_tauto _ = () + let lemma_bool_c _ _ = () + let lemma_bool_equiv _ _ = () + let lemma_ite_true ~ite:_ = () + let lemma_ite_false ~ite:_ = () +end + +module Rule_data = struct + type nonrec rule = rule + type nonrec lit = lit + type nonrec term = term + + let lemma_isa_cstor ~cstor_t:_ _ = () + let lemma_select_cstor ~cstor_t:_ _ = () + let lemma_isa_split _ _ = () + let lemma_isa_sel _ = () + let lemma_isa_disj _ _ = () + let lemma_cstor_inj _ _ _ = () + let lemma_cstor_distinct _ _ = () + let lemma_acyclicity _ = () +end diff --git a/src/base/Proof_dummy.mli b/src/base/Proof_dummy.mli index 73620f18..3aca187e 100644 --- a/src/base/Proof_dummy.mli +++ b/src/base/Proof_dummy.mli @@ -2,28 +2,35 @@ open Base_types -include - Sidekick_core.PROOF - with type t = private unit - and type proof_step = private unit +module Arg : + Sidekick_sigs_proof_trace.ARG with type rule = unit and type step_id = unit + +include Sidekick_sigs_proof_trace.S with module A = Arg + +type rule = A.rule +type step_id = A.step_id + +module Rule_sat : + Sidekick_sigs_proof_sat.S with type rule = rule and type lit = Lit.t + +module Rule_core : + Sidekick_core.PROOF_CORE + with type rule = rule and type lit = Lit.t and type term = Term.t -type proof_rule = t -> proof_step - val create : unit -> t -val lemma_lra : Lit.t Iter.t -> proof_rule +val lemma_lra : Lit.t Iter.t -> rule -include - Sidekick_th_data.PROOF - with type proof := t - and type proof_step := proof_step - and type lit := Lit.t - and type term := Term.t +module Rule_data : + Sidekick_th_data.PROOF_RULES + with type rule = rule + and type lit = Lit.t + and type term = Term.t -include - Sidekick_th_bool_static.PROOF - with type proof := t - and type proof_step := proof_step - and type lit := Lit.t +module Rule_bool : + Sidekick_th_bool_static.PROOF_RULES + with type rule = rule + and type lit = Lit.t + and type term = Term.t and type term := Term.t diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index e7b8696a..1b6833f9 100644 --- a/src/base/Proof_quip.ml +++ b/src/base/Proof_quip.ml @@ -8,7 +8,7 @@ type t = P.t module type CONV_ARG = sig val proof : Proof.t - val unsat : Proof.proof_step + val unsat : Proof.step_id end module Make_lazy_tbl (T : sig @@ -318,7 +318,7 @@ end = struct P.composite_a steps end -let of_proof (self : Proof.t) ~(unsat : Proof.proof_step) : P.t = +let of_proof (self : Proof.t) ~(unsat : Proof.step_id) : P.t = let module C = Conv (struct let proof = self let unsat = unsat diff --git a/src/base/Proof_quip.mli b/src/base/Proof_quip.mli index 374a3198..589d6f84 100644 --- a/src/base/Proof_quip.mli +++ b/src/base/Proof_quip.mli @@ -4,7 +4,7 @@ type t -val of_proof : Proof.t -> unsat:Proof.proof_step -> t +val of_proof : Proof.t -> unsat:Proof.step_id -> t type out_format = Sidekick_quip.out_format = Sexp | CSexp diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index a1e65705..bbd89507 100644 --- a/src/base/Sidekick_base.ml +++ b/src/base/Sidekick_base.ml @@ -40,6 +40,3 @@ module Lit = Lit module Proof_dummy = Proof_dummy module Proof = Proof module Proof_quip = Proof_quip - -(* re-export *) -module IArray = IArray diff --git a/src/base/dune b/src/base/dune index 06d7cb19..2846b4e8 100644 --- a/src/base/dune +++ b/src/base/dune @@ -4,5 +4,6 @@ (synopsis "Base term definitions for the standalone SMT solver and library") (libraries containers iter sidekick.core sidekick.util sidekick.lit sidekick-base.proof-trace sidekick.quip sidekick.arith-lra - sidekick.th-bool-static sidekick.th-data sidekick.zarith zarith) + sidekick.th-bool-static sidekick.th-data sidekick.zarith zarith + sidekick.proof-trace.dummy) (flags :standard -w -32 -open Sidekick_util)) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index d2f1ea2f..32792284 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -1,6 +1,30 @@ -include Sidekick_sigs_cc +open Sidekick_sigs_cc +module View = View open View +module type S = sig + include S + + val create : + ?stat:Stat.t -> ?size:[ `Small | `Big ] -> term_store -> proof_trace -> t + (** Create a new congruence closure. + + @param term_store used to be able to create new terms. All terms + interacting with this congruence closure must belong in this term state + as well. *) + + (**/**) + + module Debug_ : sig + val pp : t Fmt.printer + (** Print the whole CC *) + end + + (**/**) +end + +module type ARG = ARG + module Make (A : ARG) : S with module T = A.T @@ -14,8 +38,8 @@ module Make (A : ARG) : open struct (* proof rules *) - module Rules_ = A.CC.Proof_rules - module P = Sidekick_sigs_proof_trace.Utils_ (Proof_trace) + module Rules_ = A.Rule_core + module P = Proof_trace end type term = T.Term.t @@ -23,15 +47,15 @@ module Make (A : ARG) : type term_store = T.Term.store type lit = Lit.t type fun_ = T.Fun.t - type proof = A.Proof_trace.t - type proof_step = A.Proof_trace.step_id + type proof_trace = A.Proof_trace.t + type step_id = A.Proof_trace.A.step_id type actions = - (module ACTIONS + (module DYN_ACTIONS with type term = T.Term.t and type lit = Lit.t - and type proof = proof - and type proof_step = proof_step) + and type proof_trace = proof_trace + and type step_id = step_id) module Bits : sig type t = private int @@ -107,8 +131,7 @@ module Make (A : ARG) : | E_merge_t of term * term | E_congruence of node * node (* caused by normal congruence *) | E_and of explanation * explanation - | E_theory of - term * term * (term * term * explanation list) list * proof_step + | E_theory of term * term * (term * term * explanation list) list * step_id | E_same_val of node * node type repr = node @@ -237,7 +260,7 @@ module Make (A : ARG) : type t = { lits: lit list; same_value: (Class.t * Class.t) list; - pr: proof -> proof_step; + pr: proof_trace -> step_id; } let[@inline] is_semantic (self : t) : bool = @@ -320,7 +343,7 @@ module Make (A : ARG) : type t = { tst: term_store; - proof: proof; + proof: proof_trace; tbl: node T_tbl.t; (* internalization [term -> node] *) signatures_tbl: node Sig_tbl.t; (* map a signature to the corresponding node in some equivalence class. @@ -333,6 +356,7 @@ module Make (A : ARG) : pending: node Vec.t; combine: combine_task Vec.t; t_to_val: (node * value) T_b_tbl.t; + (* TODO: remove this, make it a plugin/EGG instead *) (* [repr -> (t,val)] where [repr = t] and [t := val] in the model *) val_to_t: node T_b_tbl.t; (* [val -> t] where [t := val] in the model *) undo: (unit -> unit) Backtrack_stack.t; @@ -342,12 +366,12 @@ module Make (A : ARG) : true_: node lazy_t; false_: node lazy_t; mutable model_mode: bool; - mutable on_pre_merge: ev_on_pre_merge list; - mutable on_post_merge: ev_on_post_merge list; - mutable on_new_term: ev_on_new_term list; - mutable on_conflict: ev_on_conflict list; - mutable on_propagate: ev_on_propagate list; - mutable on_is_subterm: ev_on_is_subterm list; + on_pre_merge: (t * actions * Class.t * Class.t * Expl.t) Event.Emitter.t; + on_post_merge: (t * actions * Class.t * Class.t) Event.Emitter.t; + on_new_term: (t * Class.t * term) Event.Emitter.t; + on_conflict: ev_on_conflict Event.Emitter.t; + on_propagate: (t * lit * (unit -> lit list * step_id)) Event.Emitter.t; + on_is_subterm: (t * Class.t * term) Event.Emitter.t; count_conflict: int Stat.counter; count_props: int Stat.counter; count_merge: int Stat.counter; @@ -359,75 +383,73 @@ module Make (A : ARG) : several times. See "fast congruence closure and extensions", Nieuwenhuis&al, page 14 *) - and ev_on_pre_merge = t -> actions -> Class.t -> Class.t -> Expl.t -> unit - and ev_on_post_merge = t -> actions -> Class.t -> Class.t -> unit - and ev_on_new_term = t -> Class.t -> term -> unit - and ev_on_conflict = t -> th:bool -> lit list -> unit - and ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit - and ev_on_is_subterm = Class.t -> term -> unit + and ev_on_conflict = { cc: t; th: bool; c: lit list } let[@inline] size_ (r : repr) = r.n_size - let[@inline] n_true cc = Lazy.force cc.true_ - let[@inline] n_false cc = Lazy.force cc.false_ + let[@inline] n_true self = Lazy.force self.true_ + let[@inline] n_false self = Lazy.force self.false_ - let n_bool cc b = + let n_bool self b = if b then - n_true cc + n_true self else - n_false cc + n_false self - let[@inline] term_store cc = cc.tst - let[@inline] proof cc = cc.proof + let[@inline] term_store self = self.tst + let[@inline] proof self = self.proof - let allocate_bitfield ~descr cc = + let allocate_bitfield self ~descr = Log.debugf 5 (fun k -> k "(@[cc.allocate-bit-field@ :descr %s@])" descr); - Bits.mk_field cc.bitgen + Bits.mk_field self.bitgen - let[@inline] on_backtrack cc f : unit = - Backtrack_stack.push_if_nonzero_level cc.undo f + let[@inline] on_backtrack self f : unit = + Backtrack_stack.push_if_nonzero_level self.undo f let[@inline] get_bitfield _cc field n = Class.get_field field n - let set_bitfield cc field b n = + let set_bitfield self field b n = let old = Class.get_field field n in if old <> b then ( - on_backtrack cc (fun () -> Class.set_field field old n); + on_backtrack self (fun () -> Class.set_field field old n); Class.set_field field b n ) (* check if [t] is in the congruence closure. Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) - let[@inline] mem (cc : t) (t : term) : bool = T_tbl.mem cc.tbl t + let[@inline] mem (self : t) (t : term) : bool = T_tbl.mem self.tbl t - (* print full state *) - let pp_full out (cc : t) : unit = - let pp_next out n = Fmt.fprintf out "@ :next %a" Class.pp n.n_next in - let pp_root out n = - if Class.is_root n then - Fmt.string out " :is-root" - else - Fmt.fprintf out "@ :root %a" Class.pp n.n_root - in - let pp_expl out n = - match n.n_expl with - | FL_none -> () - | FL_some e -> - Fmt.fprintf out " (@[:forest %a :expl %a@])" Class.pp e.next Expl.pp - e.expl - in - let pp_n out n = - Fmt.fprintf out "(@[%a%a%a%a@])" Term.pp n.n_term pp_root n pp_next n - pp_expl n - and pp_sig_e out (s, n) = - Fmt.fprintf out "(@[<1>%a@ ~~> %a%a@])" Signature.pp s Class.pp n pp_root - n - in - Fmt.fprintf out - "(@[@{cc.state@}@ (@[:nodes@ %a@])@ (@[:sig-tbl@ %a@])@])" - (Util.pp_iter ~sep:" " pp_n) - (T_tbl.values cc.tbl) - (Util.pp_iter ~sep:" " pp_sig_e) - (Sig_tbl.to_iter cc.signatures_tbl) + module Debug_ = struct + (* print full state *) + let pp out (self : t) : unit = + let pp_next out n = Fmt.fprintf out "@ :next %a" Class.pp n.n_next in + let pp_root out n = + if Class.is_root n then + Fmt.string out " :is-root" + else + Fmt.fprintf out "@ :root %a" Class.pp n.n_root + in + let pp_expl out n = + match n.n_expl with + | FL_none -> () + | FL_some e -> + Fmt.fprintf out " (@[:forest %a :expl %a@])" Class.pp e.next Expl.pp + e.expl + in + let pp_n out n = + Fmt.fprintf out "(@[%a%a%a%a@])" Term.pp n.n_term pp_root n pp_next n + pp_expl n + and pp_sig_e out (s, n) = + Fmt.fprintf out "(@[<1>%a@ ~~> %a%a@])" Signature.pp s Class.pp n + pp_root n + in + Fmt.fprintf out + "(@[@{cc.state@}@ (@[:nodes@ %a@])@ (@[:sig-tbl@ \ + %a@])@])" + (Util.pp_iter ~sep:" " pp_n) + (T_tbl.values self.tbl) + (Util.pp_iter ~sep:" " pp_sig_e) + (Sig_tbl.to_iter self.signatures_tbl) + end (* compute up-to-date signature *) let update_sig (s : signature) : Signature.t = @@ -439,50 +461,50 @@ module Make (A : ARG) : Sig_tbl.get cc.signatures_tbl s (* add to signature table. Assume it's not present already *) - let add_signature cc (s : signature) (n : node) : unit = - assert (not @@ Sig_tbl.mem cc.signatures_tbl s); + let add_signature self (s : signature) (n : node) : unit = + assert (not @@ Sig_tbl.mem self.signatures_tbl s); Log.debugf 50 (fun k -> k "(@[cc.add-sig@ %a@ ~~> %a@])" Signature.pp s Class.pp n); - on_backtrack cc (fun () -> Sig_tbl.remove cc.signatures_tbl s); - Sig_tbl.add cc.signatures_tbl s n + on_backtrack self (fun () -> Sig_tbl.remove self.signatures_tbl s); + Sig_tbl.add self.signatures_tbl s n - let push_pending cc t : unit = + let push_pending self t : unit = Log.debugf 50 (fun k -> k "(@[cc.push-pending@ %a@])" Class.pp t); - Vec.push cc.pending t + Vec.push self.pending t - let merge_classes cc t u e : unit = + let merge_classes self t u e : unit = if t != u && not (same_class t u) then ( Log.debugf 50 (fun k -> k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" Class.pp t Class.pp u Expl.pp e); - Vec.push cc.combine @@ CT_merge (t, u, e) + Vec.push self.combine @@ CT_merge (t, u, e) ) (* re-root the explanation tree of the equivalence class of [n] so that it points to [n]. postcondition: [n.n_expl = None] *) - let[@unroll 2] rec reroot_expl (cc : t) (n : node) : unit = + let[@unroll 2] rec reroot_expl (self : t) (n : node) : unit = match n.n_expl with | FL_none -> () (* already root *) | FL_some { next = u; expl = e_n_u } -> (* reroot to [u], then invert link between [u] and [n] *) - reroot_expl cc u; + reroot_expl self u; u.n_expl <- FL_some { next = n; expl = e_n_u }; n.n_expl <- FL_none - let raise_conflict_ (cc : t) ~th (acts : actions) (e : lit list) - (p : proof_step) : _ = + let raise_conflict_ (cc : t) ~th (acts : actions) (e : lit list) (p : step_id) + : _ = 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; + Event.emit cc.on_conflict { cc; th; c = e }; Stat.incr cc.count_conflict; let (module A) = acts in A.raise_conflict e p - let[@inline] all_classes cc : repr Iter.t = - T_tbl.values cc.tbl |> Iter.filter Class.is_root + let[@inline] all_classes self : repr Iter.t = + T_tbl.values self.tbl |> Iter.filter Class.is_root (* find the closest common ancestor of [a] and [b] in the proof forest. @@ -493,10 +515,10 @@ module Make (A : ARG) : - if [n] is marked, then all the predecessors of [n] from [a] or [b] are marked too. *) - let find_common_ancestor cc (a : node) (b : node) : node = + let find_common_ancestor self (a : node) (b : node) : node = (* catch up to the other node *) let rec find1 a = - if Class.get_field cc.field_marked_explain a then + if Class.get_field self.field_marked_explain a then a else ( match a.n_expl with @@ -507,13 +529,13 @@ module Make (A : ARG) : let rec find2 a b = if Class.equal a b then a - else if Class.get_field cc.field_marked_explain a then + else if Class.get_field self.field_marked_explain a then a - else if Class.get_field cc.field_marked_explain b then + else if Class.get_field self.field_marked_explain b then b else ( - Class.set_field cc.field_marked_explain true a; - Class.set_field cc.field_marked_explain true b; + Class.set_field self.field_marked_explain true a; + Class.set_field self.field_marked_explain true b; match a.n_expl, b.n_expl with | FL_some r1, FL_some r2 -> find2 r1.next r2.next | FL_some r, FL_none -> find1 r.next @@ -525,8 +547,8 @@ module Make (A : ARG) : (* cleanup tags on nodes traversed in [find2] *) let rec cleanup_ n = - if Class.get_field cc.field_marked_explain n then ( - Class.set_field cc.field_marked_explain false n; + if Class.get_field self.field_marked_explain n then ( + Class.set_field self.field_marked_explain false n; match n.n_expl with | FL_none -> () | FL_some { next; _ } -> cleanup_ next @@ -541,7 +563,7 @@ module Make (A : ARG) : type t = { mutable lits: Lit.t list; mutable same_val: (Class.t * Class.t) list; - mutable th_lemmas: (Lit.t * (Lit.t * Lit.t list) list * proof_step) list; + mutable th_lemmas: (Lit.t * (Lit.t * Lit.t list) list * step_id) list; } let create () : t = { lits = []; same_val = []; th_lemmas = [] } @@ -568,7 +590,7 @@ module Make (A : ARG) : () (* proof of [\/_i ¬lits[i]] *) - let proof_of_th_lemmas (self : t) (proof : proof) : proof_step = + let proof_of_th_lemmas (self : t) (proof : proof_trace) : step_id = let p_lits1 = Iter.of_list self.lits |> Iter.map Lit.neg in let p_lits2 = Iter.of_list self.th_lemmas @@ -609,8 +631,8 @@ module Make (A : ARG) : end (* decompose explanation [e] into a list of literals added to [acc] *) - let rec explain_decompose_expl cc (st : Expl_state.t) (e : explanation) : unit - = + let rec explain_decompose_expl self (st : Expl_state.t) (e : explanation) : + unit = Log.debugf 5 (fun k -> k "(@[cc.decompose_expl@ %a@])" Expl.pp e); match e with | E_trivial -> () @@ -619,14 +641,14 @@ module Make (A : ARG) : | Some (App_fun (f1, a1)), Some (App_fun (f2, a2)) -> assert (Fun.equal f1 f2); assert (List.length a1 = List.length a2); - List.iter2 (explain_equal_rec_ cc st) a1 a2 + List.iter2 (explain_equal_rec_ self st) a1 a2 | Some (App_ho (f1, a1)), Some (App_ho (f2, a2)) -> - explain_equal_rec_ cc st f1 f2; - explain_equal_rec_ cc st a1 a2 + explain_equal_rec_ self st f1 f2; + explain_equal_rec_ self st a1 a2 | Some (If (a1, b1, c1)), Some (If (a2, b2, c2)) -> - explain_equal_rec_ cc st a1 a2; - explain_equal_rec_ cc st b1 b2; - explain_equal_rec_ cc st c1 c2 + explain_equal_rec_ self st a1 a2; + explain_equal_rec_ self st b1 b2; + explain_equal_rec_ self st c1 c2 | _ -> assert false) | E_lit lit -> Expl_state.add_lit st lit | E_same_val (n1, n2) -> Expl_state.add_same_val st n1 n2 @@ -634,29 +656,29 @@ module Make (A : ARG) : let sub_proofs = List.map (fun (t_i, u_i, expls_i) -> - let lit_i = A.CC.mk_lit_eq cc.tst t_i u_i in + let lit_i = A.mk_lit_eq self.tst t_i u_i in (* use a separate call to [explain_expls] for each set *) - let sub = explain_expls cc expls_i in + let sub = explain_expls self expls_i in Expl_state.merge st sub; lit_i, sub.lits) expl_sets in - let lit_t_u = A.CC.mk_lit_eq cc.tst t u in + let lit_t_u = A.mk_lit_eq self.tst t u in Expl_state.add_th st lit_t_u sub_proofs pr - | E_merge (a, b) -> explain_equal_rec_ cc st a b + | E_merge (a, b) -> explain_equal_rec_ self st a b | E_merge_t (a, b) -> (* find nodes for [a] and [b] on the fly *) - (match T_tbl.find cc.tbl a, T_tbl.find cc.tbl b with - | a, b -> explain_equal_rec_ cc st a b + (match T_tbl.find self.tbl a, T_tbl.find self.tbl b with + | a, b -> explain_equal_rec_ self st a b | exception Not_found -> Error.errorf "expl: cannot find node(s) for %a, %a" Term.pp a Term.pp b) | E_and (a, b) -> - explain_decompose_expl cc st a; - explain_decompose_expl cc st b + explain_decompose_expl self st a; + explain_decompose_expl self st b - and explain_expls cc (es : explanation list) : Expl_state.t = + and explain_expls self (es : explanation list) : Expl_state.t = let st = Expl_state.create () in - List.iter (explain_decompose_expl cc st) es; + List.iter (explain_decompose_expl self st) es; st and explain_equal_rec_ (cc : t) (st : Expl_state.t) (a : node) (b : node) : @@ -670,7 +692,7 @@ module Make (A : ARG) : (* explain why [a = parent_a], where [a -> ... -> target] in the proof forest *) - and explain_along_path cc (st : Expl_state.t) (a : node) (target : node) : + and explain_along_path self (st : Expl_state.t) (a : node) (target : node) : unit = let rec aux n = if n == target then @@ -679,7 +701,7 @@ module Make (A : ARG) : match n.n_expl with | FL_none -> assert false | FL_some { next = next_n; expl } -> - explain_decompose_expl cc st expl; + explain_decompose_expl self st expl; (* now prove [next_n = target] *) aux next_n ) @@ -687,28 +709,30 @@ module Make (A : ARG) : aux a (* add a term *) - let[@inline] rec add_term_rec_ cc t : node = - try T_tbl.find cc.tbl t with Not_found -> add_new_term_ cc t + let[@inline] rec add_term_rec_ self t : node = + match T_tbl.find self.tbl t with + | n -> n + | exception Not_found -> add_new_term_ self t - (* add [t] to [cc] when not present already *) - and add_new_term_ cc (t : term) : node = - assert (not @@ mem cc t); + (* add [t] when not present already *) + and add_new_term_ self (t : term) : node = + assert (not @@ mem self t); Log.debugf 15 (fun k -> k "(@[cc.add-term@ %a@])" Term.pp t); let n = Class.make t in (* register sub-terms, add [t] to their parent list, and return the corresponding initial signature *) - let sig0 = compute_sig0 cc n in + let sig0 = compute_sig0 self n in n.n_sig0 <- sig0; (* remove term when we backtrack *) - on_backtrack cc (fun () -> + on_backtrack self (fun () -> Log.debugf 30 (fun k -> k "(@[cc.remove-term@ %a@])" Term.pp t); - T_tbl.remove cc.tbl t); + T_tbl.remove self.tbl t); (* add term to the table *) - T_tbl.add cc.tbl t n; + T_tbl.add self.tbl t n; if Option.is_some sig0 then (* [n] might be merged with other equiv classes *) - push_pending cc n; - if not cc.model_mode then List.iter (fun f -> f cc n t) cc.on_new_term; + push_pending self n; + if not self.model_mode then Event.emit self.on_new_term (self, n, t); n (* compute the initial signature of the given node *) @@ -723,13 +747,13 @@ module Make (A : ARG) : let old_parents = sub_r.n_parents in if Bag.is_empty old_parents && not self.model_mode then (* first time it has parents: tell watchers that this is a subterm *) - List.iter (fun f -> f sub u) self.on_is_subterm; + Event.emit self.on_is_subterm (self, sub, u); on_backtrack self (fun () -> sub_r.n_parents <- old_parents); sub_r.n_parents <- Bag.cons n sub_r.n_parents); sub in let[@inline] return x = Some x in - match A.CC.view n.n_term with + match A.view_as_cc n.n_term with | Bool _ | Opaque _ -> None | Eq (a, b) -> let a = deref_sub a in @@ -748,16 +772,16 @@ module Make (A : ARG) : return @@ App_ho (f, a) | If (a, b, c) -> return @@ If (deref_sub a, deref_sub b, deref_sub c) - let[@inline] add_term cc t : node = add_term_rec_ cc t + let[@inline] add_term self t : node = add_term_rec_ self t let mem_term = mem - let set_as_lit cc (n : node) (lit : lit) : unit = + let set_as_lit self (n : node) (lit : lit) : unit = match n.n_as_lit with | Some _ -> () | None -> Log.debugf 15 (fun k -> k "(@[cc.set-as-lit@ %a@ %a@])" Class.pp n Lit.pp lit); - on_backtrack cc (fun () -> n.n_as_lit <- None); + on_backtrack self (fun () -> n.n_as_lit <- None); n.n_as_lit <- Some lit (* is [n] true or false? *) @@ -769,7 +793,7 @@ module Make (A : ARG) : the SAT solver), and [pr] is a proof, including sub-proofs for theory merges. *) let lits_and_proof_of_expl (self : t) (st : Expl_state.t) : - Lit.t list * proof_step = + Lit.t list * step_id = let { Expl_state.lits; th_lemmas = _; same_val } = st in assert (same_val = []); let pr = Expl_state.proof_of_th_lemmas st self.proof in @@ -777,17 +801,17 @@ module Make (A : ARG) : (* main CC algo: add terms from [pending] to the signature table, check for collisions *) - let rec update_tasks (cc : t) (acts : actions) : unit = - while not (Vec.is_empty cc.pending && Vec.is_empty cc.combine) do - while not @@ Vec.is_empty cc.pending do - task_pending_ cc (Vec.pop_exn cc.pending) + let rec update_tasks (self : t) (acts : actions) : unit = + while not (Vec.is_empty self.pending && Vec.is_empty self.combine) do + while not @@ Vec.is_empty self.pending do + task_pending_ self (Vec.pop_exn self.pending) done; - while not @@ Vec.is_empty cc.combine do - task_combine_ cc acts (Vec.pop_exn cc.combine) + while not @@ Vec.is_empty self.combine do + task_combine_ self acts (Vec.pop_exn self.combine) done done - and task_pending_ cc (n : node) : unit = + and task_pending_ self (n : node) : unit = (* check if some parent collided *) match n.n_sig0 with | None -> () (* no-op *) @@ -798,47 +822,47 @@ module Make (A : ARG) : Log.debugf 5 (fun k -> k "(@[cc.pending.eq@ %a@ :r1 %a@ :r2 %a@])" Class.pp n Class.pp a Class.pp b); - merge_classes cc n (n_true cc) expl + merge_classes self n (n_true self) expl ) | Some (Not u) -> (* [u = bool ==> not u = not bool] *) let r_u = find_ u in - if Class.equal r_u (n_true cc) then ( - let expl = Expl.mk_merge u (n_true cc) in - merge_classes cc n (n_false cc) expl - ) else if Class.equal r_u (n_false cc) then ( - let expl = Expl.mk_merge u (n_false cc) in - merge_classes cc n (n_true cc) expl + if Class.equal r_u (n_true self) then ( + let expl = Expl.mk_merge u (n_true self) in + merge_classes self n (n_false self) expl + ) else if Class.equal r_u (n_false self) then ( + let expl = Expl.mk_merge u (n_false self) in + merge_classes self n (n_true self) expl ) | Some s0 -> (* update the signature by using [find] on each sub-node *) let s = update_sig s0 in - (match find_signature cc s with + (match find_signature self s with | None -> (* add to the signature table [sig(n) --> n] *) - add_signature cc s n + add_signature self s n | Some u when Class.equal n u -> () | Some u -> (* [t1] and [t2] must be applications of the same symbol to arguments that are pairwise equal *) assert (n != u); let expl = Expl.mk_congruence n u in - merge_classes cc n u expl) + merge_classes self n u expl) - and[@inline] task_combine_ cc acts = function - | CT_merge (a, b, e_ab) -> task_merge_ cc acts a b e_ab - | CT_set_val (n, v) -> task_set_val_ cc acts n v + and task_combine_ self acts = function + | CT_merge (a, b, e_ab) -> task_merge_ self acts a b e_ab + | CT_set_val (n, v) -> task_set_val_ self acts n v - and task_set_val_ cc acts n v = + and task_set_val_ self acts n v = let repr_n = find_ n in (* - if repr(n) has value [v], do nothing - else if repr(n) has value [v'], semantic conflict - else add [repr(n) -> (n,v)] to cc.t_to_val *) - (match T_b_tbl.get cc.t_to_val repr_n.n_term with + (match T_b_tbl.get self.t_to_val repr_n.n_term with | Some (n', v') when not (Term.equal v v') -> (* semantic conflict *) let expl = [ Expl.mk_merge n n' ] in - let expl_st = explain_expls cc expl in + let expl_st = explain_expls self expl in let lits = expl_st.lits in let tuples = List.rev_map (fun (t, u) -> true, t.n_term, u.n_term) expl_st.same_val @@ -850,33 +874,33 @@ module Make (A : ARG) : (@[existing-val %a@ := %a@])@])" Class.pp n Term.pp v Class.pp n' Term.pp v'); - Stat.incr cc.count_semantic_conflict; + Stat.incr self.count_semantic_conflict; let (module A) = acts in A.raise_semantic_conflict lits tuples | Some _ -> () - | None -> T_b_tbl.add cc.t_to_val repr_n.n_term (n, v)); + | None -> T_b_tbl.add self.t_to_val repr_n.n_term (n, v)); (* now for the reverse map, look in self.val_to_t for [v]. - if present, push a merge command with Expl.mk_same_value - if not, add [v -> n] *) - match T_b_tbl.get cc.val_to_t v with - | None -> T_b_tbl.add cc.val_to_t v n + match T_b_tbl.get self.val_to_t v with + | None -> T_b_tbl.add self.val_to_t v n | Some n' when not (same_class n n') -> - merge_classes cc n n' (Expl.mk_same_value n n') + merge_classes self n n' (Expl.mk_same_value n n') | Some _ -> () (* main CC algo: merge equivalence classes in [st.combine]. @raise Exn_unsat if merge fails *) - and task_merge_ cc acts a b e_ab : unit = + and task_merge_ self acts a b e_ab : unit = let ra = find_ a in let rb = find_ b in if not @@ Class.equal ra rb then ( assert (Class.is_root ra); assert (Class.is_root rb); - Stat.incr cc.count_merge; + Stat.incr self.count_merge; (* check we're not merging [true] and [false] *) if - (Class.equal ra (n_true cc) && Class.equal rb (n_false cc)) - || (Class.equal rb (n_true cc) && Class.equal ra (n_false cc)) + (Class.equal ra (n_true self) && Class.equal rb (n_false self)) + || (Class.equal rb (n_true self) && Class.equal ra (n_false self)) then ( Log.debugf 5 (fun k -> k @@ -890,9 +914,9 @@ module Make (A : ARG) : C3: r1 C1 C2 *) let expl_st = Expl_state.create () in - explain_decompose_expl cc expl_st e_ab; - explain_equal_rec_ cc expl_st a ra; - explain_equal_rec_ cc expl_st b rb; + explain_decompose_expl self expl_st e_ab; + explain_equal_rec_ self expl_st a ra; + explain_equal_rec_ self expl_st b rb; if Expl_state.is_semantic expl_st then ( (* conflict involving some semantic values *) @@ -902,22 +926,22 @@ module Make (A : ARG) : |> List.rev_map (fun (t, u) -> true, Class.term t, Class.term u) in assert (same_val <> []); - Stat.incr cc.count_semantic_conflict; + Stat.incr self.count_semantic_conflict; let (module A) = acts in A.raise_semantic_conflict lits same_val ) else ( (* regular conflict *) - let lits, pr = lits_and_proof_of_expl cc expl_st in - raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr + let lits, pr = lits_and_proof_of_expl self expl_st in + raise_conflict_ self ~th:!th acts (List.rev_map Lit.neg lits) pr ) ); (* We will merge [r_from] into [r_into]. we try to ensure that [size ra <= size rb] in general, but always keep values as representative *) let r_from, r_into = - if n_is_bool_value cc ra then + if n_is_bool_value self ra then rb, ra - else if n_is_bool_value cc rb then + else if n_is_bool_value self rb then ra, rb else if size_ ra > size_ rb then rb, ra @@ -926,13 +950,13 @@ module Make (A : ARG) : in (* when merging terms with [true] or [false], possibly propagate them to SAT *) let merge_bool r1 t1 r2 t2 = - if Class.equal r1 (n_true cc) then - propagate_bools cc acts r2 t2 r1 t1 e_ab true - else if Class.equal r1 (n_false cc) then - propagate_bools cc acts r2 t2 r1 t1 e_ab false + if Class.equal r1 (n_true self) then + propagate_bools self acts r2 t2 r1 t1 e_ab true + else if Class.equal r1 (n_false self) then + propagate_bools self acts r2 t2 r1 t1 e_ab false in - if not cc.model_mode then ( + if not self.model_mode then ( merge_bool ra a rb b; merge_bool rb b ra a ); @@ -942,16 +966,16 @@ module Make (A : ARG) : k "(@[cc.merge@ :from %a@ :into %a@])" Class.pp r_from Class.pp r_into); (* call [on_pre_merge] functions, and merge theory data items *) - if not cc.model_mode then ( + if not self.model_mode then ( (* explanation is [a=ra & e_ab & b=rb] *) let expl = Expl.mk_list [ e_ab; Expl.mk_merge a ra; Expl.mk_merge b rb ] in - List.iter (fun f -> f cc acts r_into r_from expl) cc.on_pre_merge + Event.emit self.on_pre_merge (self, acts, r_into, r_from, expl) ); ((* parents might have a different signature, check for collisions *) - Class.iter_parents r_from (fun parent -> push_pending cc parent); + Class.iter_parents r_from (fun parent -> push_pending self parent); (* for each node in [r_from]'s class, make it point to [r_into] *) Class.iter_class r_from (fun u -> assert (u.n_root == r_from); @@ -968,7 +992,7 @@ module Make (A : ARG) : r_into.n_size <- r_into.n_size + r_from.n_size; r_into.n_bits <- Bits.merge r_into.n_bits r_from.n_bits; (* on backtrack, unmerge classes and restore the pointers to [r_from] *) - on_backtrack cc (fun () -> + on_backtrack self (fun () -> Log.debugf 30 (fun k -> k "(@[cc.undo_merge@ :from %a@ :into %a@])" Class.pp r_from Class.pp r_into); @@ -983,17 +1007,17 @@ module Make (A : ARG) : (* check for semantic values, update the one of [r_into] if [r_from] has a value *) - (match T_b_tbl.get cc.t_to_val r_from.n_term with + (match T_b_tbl.get self.t_to_val r_from.n_term with | None -> () | Some (n_from, v_from) -> - (match T_b_tbl.get cc.t_to_val r_into.n_term with - | None -> T_b_tbl.add cc.t_to_val r_into.n_term (n_from, v_from) + (match T_b_tbl.get self.t_to_val r_into.n_term with + | None -> T_b_tbl.add self.t_to_val r_into.n_term (n_from, v_from) | Some (n_into, v_into) when not (Term.equal v_from v_into) -> (* semantic conflict, including [n_from != n_into] in model *) let expl = [ e_ab; Expl.mk_merge r_from n_from; Expl.mk_merge r_into n_into ] in - let expl_st = explain_expls cc expl in + let expl_st = explain_expls self expl in let lits = expl_st.lits in let tuples = List.rev_map @@ -1008,7 +1032,7 @@ module Make (A : ARG) : (@[n-into %a@ := %a@])@])" Class.pp n_from Term.pp v_from Class.pp n_into Term.pp v_into); - Stat.incr cc.count_semantic_conflict; + Stat.incr self.count_semantic_conflict; let (module A) = acts in A.raise_semantic_conflict lits tuples | Some _ -> ())); @@ -1016,32 +1040,32 @@ module Make (A : ARG) : (* update explanations (a -> b), arbitrarily. Note that here we merge the classes by adding a bridge between [a] and [b], not their roots. *) - reroot_expl cc a; + reroot_expl self a; assert (a.n_expl = FL_none); (* on backtracking, link may be inverted, but we delete the one that bridges between [a] and [b] *) - on_backtrack cc (fun () -> + on_backtrack self (fun () -> match a.n_expl, b.n_expl with | FL_some e, _ when Class.equal e.next b -> a.n_expl <- FL_none | _, FL_some e when Class.equal e.next a -> b.n_expl <- FL_none | _ -> assert false); a.n_expl <- FL_some { next = b; expl = e_ab }; (* call [on_post_merge] *) - if not cc.model_mode then - List.iter (fun f -> f cc acts r_into r_from) cc.on_post_merge + if not self.model_mode then + Event.emit self.on_post_merge (self, acts, r_into, r_from) ) (* we are merging [r1] with [r2==Bool(sign)], so propagate each term [u1] in the equiv class of [r1] that is a known literal back to the SAT solver and which is not the one initially merged. We can explain the propagation with [u1 = t1 =e= t2 = r2==bool] *) - and propagate_bools cc acts r1 t1 r2 t2 (e_12 : explanation) sign : unit = + and propagate_bools self acts r1 t1 r2 t2 (e_12 : explanation) sign : unit = (* explanation for [t1 =e= t2 = r2] *) let half_expl_and_pr = lazy (let st = Expl_state.create () in - explain_decompose_expl cc st e_12; - explain_equal_rec_ cc st r2 t2; + explain_decompose_expl self st e_12; + explain_equal_rec_ self st r2 t2; st) in (* TODO: flag per class, `or`-ed on merge, to indicate if the class @@ -1066,7 +1090,7 @@ module Make (A : ARG) : let (lazy st) = half_expl_and_pr in let st = Expl_state.copy st in (* do not modify shared st *) - explain_equal_rec_ cc st u1 t1; + explain_equal_rec_ self st u1 t1; (* propagate only if this doesn't depend on some semantic values *) if not (Expl_state.is_semantic st) then ( @@ -1075,21 +1099,17 @@ module Make (A : ARG) : let guard = st.lits in (* get a proof of [guard /\ ¬lit] being absurd, to propagate [lit] *) Expl_state.add_lit st (Lit.neg lit); - let _, pr = lits_and_proof_of_expl cc st in + let _, pr = lits_and_proof_of_expl self st in guard, pr in - List.iter (fun f -> f cc lit reason) cc.on_propagate; - Stat.incr cc.count_props; + Event.emit self.on_propagate (self, lit, reason); + Stat.incr self.count_props; let (module A) = acts in A.propagate lit ~reason ) | _ -> ()) - module Debug_ = struct - let pp out _ = Fmt.string out "cc" - end - - let add_iter cc it : unit = it (fun t -> ignore @@ add_term_rec_ cc t) + let add_iter self it : unit = it (fun t -> ignore @@ add_term_rec_ self t) let[@inline] push_level (self : t) : unit = Backtrack_stack.push_level self.undo; @@ -1108,13 +1128,13 @@ module Make (A : ARG) : () (* run [f] in a local congruence closure level *) - let with_model_mode cc f = - assert (not cc.model_mode); - cc.model_mode <- true; - push_level cc; + let with_model_mode self f = + assert (not self.model_mode); + self.model_mode <- true; + push_level self; CCFun.protect f ~finally:(fun () -> - pop_levels cc 1; - cc.model_mode <- false) + pop_levels self 1; + self.model_mode <- false) let get_model_for_each_class self : _ Iter.t = assert self.model_mode; @@ -1127,54 +1147,49 @@ module Make (A : ARG) : (* assert that this boolean literal holds. if a lit is [= a b], merge [a] and [b]; otherwise merge the atom with true/false *) - let assert_lit cc lit : unit = + let assert_lit self lit : unit = let t = Lit.term lit in Log.debugf 15 (fun k -> k "(@[cc.assert-lit@ %a@])" Lit.pp lit); let sign = Lit.sign lit in - match A.CC.view t with + match A.view_as_cc t with | Eq (a, b) when sign -> - let a = add_term cc a in - let b = add_term cc b in + let a = add_term self a in + let b = add_term self b in (* merge [a] and [b] *) - merge_classes cc a b (Expl.mk_lit lit) + merge_classes self a b (Expl.mk_lit lit) | _ -> (* equate t and true/false *) - let rhs = - if sign then - n_true cc - else - n_false cc - in - let n = add_term cc t in + let rhs = n_bool self sign in + let n = add_term self t in (* TODO: ensure that this is O(1). basically, just have [n] point to true/false and thus acquire the corresponding value, so its superterms (like [ite]) can evaluate properly *) (* TODO: use oriented merge (force direction [n -> rhs]) *) - merge_classes cc n rhs (Expl.mk_lit lit) + merge_classes self n rhs (Expl.mk_lit lit) - let[@inline] assert_lits cc lits : unit = Iter.iter (assert_lit cc) lits + let[@inline] assert_lits self lits : unit = Iter.iter (assert_lit self) lits (* raise a conflict *) - let raise_conflict_from_expl cc (acts : actions) expl = + let raise_conflict_from_expl self (acts : actions) expl = Log.debugf 5 (fun k -> k "(@[cc.theory.raise-conflict@ :expl %a@])" Expl.pp expl); let st = Expl_state.create () in - explain_decompose_expl cc st expl; - let lits, pr = lits_and_proof_of_expl cc st in + explain_decompose_expl self st expl; + let lits, pr = lits_and_proof_of_expl self st in let c = List.rev_map Lit.neg lits in let th = st.th_lemmas <> [] in - raise_conflict_ cc ~th acts c pr + raise_conflict_ self ~th acts c pr - let merge cc n1 n2 expl = + let merge self n1 n2 expl = Log.debugf 5 (fun k -> k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" Class.pp n1 Class.pp n2 Expl.pp expl); assert (T.Ty.equal (T.Term.ty n1.n_term) (T.Term.ty n2.n_term)); - merge_classes cc n1 n2 expl + merge_classes self n1 n2 expl - let[@inline] merge_t cc t1 t2 expl = - merge cc (add_term cc t1) (add_term cc t2) expl + let merge_t self t1 t2 expl = + merge self (add_term self t1) (add_term self t2) expl let set_model_value (self : t) (t : term) (v : value) : unit = assert self.model_mode; @@ -1183,23 +1198,21 @@ module Make (A : ARG) : | None -> () (* ignore, th combination not needed *) | Some n -> Vec.push self.combine (CT_set_val (n, v)) - let explain_eq cc n1 n2 : Resolved_expl.t = + let explain_eq self n1 n2 : Resolved_expl.t = let st = Expl_state.create () in - explain_equal_rec_ cc st n1 n2; + explain_equal_rec_ self st n1 n2; (* FIXME: also need to return the proof? *) Expl_state.to_resolved_expl st - let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge - let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge - let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term - let on_conflict cc f = cc.on_conflict <- f :: cc.on_conflict - let on_propagate cc f = cc.on_propagate <- f :: cc.on_propagate - let on_is_subterm cc f = cc.on_is_subterm <- f :: cc.on_is_subterm + let[@inline] on_pre_merge self = Event.of_emitter self.on_pre_merge + let[@inline] on_post_merge self = Event.of_emitter self.on_post_merge + let[@inline] on_new_term self = Event.of_emitter self.on_new_term + let[@inline] on_conflict self = Event.of_emitter self.on_conflict + let[@inline] on_propagate self = Event.of_emitter self.on_propagate + let[@inline] on_is_subterm self = Event.of_emitter self.on_is_subterm - let create ?(stat = Stat.global) ?(on_pre_merge = []) ?(on_post_merge = []) - ?(on_new_term = []) ?(on_conflict = []) ?(on_propagate = []) - ?(on_is_subterm = []) ?(size = `Big) (tst : term_store) (proof : proof) : - t = + let create ?(stat = Stat.global) ?(size = `Big) (tst : term_store) + (proof : proof_trace) : t = let size = match size with | `Small -> 128 @@ -1217,12 +1230,12 @@ module Make (A : ARG) : t_to_val = T_b_tbl.create ~size:32 (); val_to_t = T_b_tbl.create ~size:32 (); model_mode = false; - on_pre_merge; - on_post_merge; - on_new_term; - on_conflict; - on_propagate; - on_is_subterm; + on_pre_merge = Event.Emitter.create (); + on_post_merge = Event.Emitter.create (); + on_new_term = Event.Emitter.create (); + on_conflict = Event.Emitter.create (); + on_propagate = Event.Emitter.create (); + on_is_subterm = Event.Emitter.create (); pending = Vec.create (); combine = Vec.create (); undo = Backtrack_stack.create (); @@ -1240,13 +1253,13 @@ module Make (A : ARG) : ignore (Lazy.force false_ : node); cc - let[@inline] find_t cc t : repr = - let n = T_tbl.find cc.tbl t in + let[@inline] find_t self t : repr = + let n = T_tbl.find self.tbl t in find_ n - let[@inline] check cc acts : unit = + let[@inline] check self acts : unit = Log.debug 5 "(cc.check)"; - update_tasks cc acts + update_tasks self acts let check_inv_enabled_ = true (* XXX NUDGE *) @@ -1273,134 +1286,7 @@ module Make (A : ARG) : ) (* model: return all the classes *) - let get_model (cc : t) : repr Iter.t Iter.t = - check_inv_ cc; - all_classes cc |> Iter.map Class.iter_class -end - -module Make_plugin (M : MONOID_ARG) : PLUGIN_BUILDER with module M = M = struct - module M = M - module CC = M.CC - module Class = CC.Class - module N_tbl = Backtrackable_tbl.Make (Class) - module Expl = CC.Expl - - type term = CC.term - - module type PL = PLUGIN with module CC = M.CC and module M = M - - type plugin = (module PL) - - module Make (A : sig - val size : int option - val cc : CC.t - end) : PL = struct - module M = M - module CC = CC - open A - - (* repr -> value for the class *) - let values : M.t N_tbl.t = N_tbl.create ?size () - - (* bit in CC to filter out quickly classes without value *) - let field_has_value : Class.bitfield = - CC.allocate_bitfield ~descr:("monoid." ^ M.name ^ ".has-value") cc - - let push_level () = N_tbl.push_level values - let pop_levels n = N_tbl.pop_levels values n - let n_levels () = N_tbl.n_levels values - - let mem n = - let res = CC.get_bitfield cc field_has_value n in - assert ( - if res then - N_tbl.mem values n - else - true); - res - - let get n = - if CC.get_bitfield cc field_has_value n then - N_tbl.get values n - else - None - - let on_new_term cc n (t : term) : unit = - (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*) - let maybe_m, l = M.of_term cc n t in - (match maybe_m with - | Some v -> - Log.debugf 20 (fun k -> - k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" M.name Class.pp n - M.pp v); - CC.set_bitfield cc field_has_value true n; - N_tbl.add values n v - | None -> ()); - List.iter - (fun (n_u, m_u) -> - Log.debugf 20 (fun k -> - k "(@[monoid[%s].on-new-term.sub@ :n %a@ :sub-t %a@ :value %a@])" - M.name Class.pp n Class.pp n_u M.pp m_u); - let n_u = CC.find cc n_u in - if CC.get_bitfield cc field_has_value n_u then ( - let m_u' = - try N_tbl.find values n_u - with Not_found -> - Error.errorf "node %a has bitfield but no value" Class.pp n_u - in - match M.merge cc n_u m_u n_u m_u' (Expl.mk_list []) with - | Error expl -> - Error.errorf - "when merging@ @[for node %a@],@ values %a and %a:@ conflict %a" - Class.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp expl - | Ok m_u_merged -> - Log.debugf 20 (fun k -> - k - "(@[monoid[%s].on-new-term.sub.merged@ :n %a@ :sub-t %a@ \ - :value %a@])" - M.name Class.pp n Class.pp n_u M.pp m_u_merged); - N_tbl.add values n_u m_u_merged - ) else ( - (* just add to [n_u] *) - CC.set_bitfield cc field_has_value true n_u; - N_tbl.add values n_u m_u - )) - l; - () - - let iter_all : _ Iter.t = N_tbl.to_iter values - - let on_pre_merge cc acts n1 n2 e_n1_n2 : unit = - match get n1, get n2 with - | Some v1, Some v2 -> - Log.debugf 5 (fun k -> - k - "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ \ - :val2 %a@])@])" - M.name Class.pp n1 M.pp v1 Class.pp n2 M.pp v2); - (match M.merge cc n1 v1 n2 v2 e_n1_n2 with - | Ok v' -> - N_tbl.remove values n2; - (* only keep repr *) - N_tbl.add values n1 v' - | Error expl -> CC.raise_conflict_from_expl cc acts expl) - | None, Some cr -> - CC.set_bitfield cc field_has_value true n1; - N_tbl.add values n1 cr; - N_tbl.remove values n2 (* only keep reprs *) - | Some _, None -> () (* already there on the left *) - | None, None -> () - - (* setup *) - let () = - CC.on_new_term cc on_new_term; - CC.on_pre_merge cc on_pre_merge; - () - end - - let create_and_setup ?size (cc : CC.t) : plugin = - (module Make (struct - let size = size - let cc = cc - end)) + let get_model (self : t) : repr Iter.t Iter.t = + check_inv_ self; + all_classes self |> Iter.map Class.iter_class end diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index ade46641..2ecc963d 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -1,20 +1,33 @@ (** Congruence Closure Implementation *) module View = Sidekick_sigs_cc.View +open Sidekick_sigs_cc -module type TERM = Sidekick_sigs_cc.TERM -module type LIT = Sidekick_sigs_cc.LIT -module type ARG = Sidekick_sigs_cc.ARG -module type S = Sidekick_sigs_cc.S -module type MONOID_ARG = Sidekick_sigs_cc.MONOID_ARG -module type PLUGIN = Sidekick_sigs_cc.PLUGIN -module type PLUGIN_BUILDER = Sidekick_sigs_cc.PLUGIN_BUILDER +module type ARG = ARG + +module type S = sig + include S + + val create : + ?stat:Stat.t -> ?size:[ `Small | `Big ] -> term_store -> proof_trace -> t + (** Create a new congruence closure. + + @param term_store used to be able to create new terms. All terms + interacting with this congruence closure must belong in this term state + as well. *) + + (**/**) + + module Debug_ : sig + val pp : t Fmt.printer + (** Print the whole CC *) + end + + (**/**) +end module Make (A : ARG) : S with module T = A.T and module Lit = A.Lit and module Proof_trace = A.Proof_trace - -(** Create a plugin builder from the given per-class monoid *) -module Make_plugin (M : MONOID_ARG) : PLUGIN_BUILDER with module M = M diff --git a/src/cc/plugin/dune b/src/cc/plugin/dune new file mode 100644 index 00000000..269abd1e --- /dev/null +++ b/src/cc/plugin/dune @@ -0,0 +1,5 @@ +(library + (name Sidekick_cc_plugin) + (public_name sidekick.cc.plugin) + (libraries containers iter sidekick.sigs sidekick.sigs.cc sidekick.util) + (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util)) diff --git a/src/cc/plugin/sidekick_cc_plugin.ml b/src/cc/plugin/sidekick_cc_plugin.ml new file mode 100644 index 00000000..211fd6be --- /dev/null +++ b/src/cc/plugin/sidekick_cc_plugin.ml @@ -0,0 +1,159 @@ +open Sidekick_sigs_cc + +module type EXTENDED_PLUGIN_BUILDER = sig + include MONOID_PLUGIN_BUILDER + + val mem : t -> M.CC.Class.t -> bool + (** Does the CC Class.t have a monoid value? *) + + val get : t -> M.CC.Class.t -> M.t option + (** Get monoid value for this CC Class.t, if any *) + + val iter_all : t -> (M.CC.repr * M.t) Iter.t + + include Sidekick_sigs.BACKTRACKABLE0 with type t := t + include Sidekick_sigs.PRINT with type t := t +end + +module Make (M : MONOID_PLUGIN_ARG) : + EXTENDED_PLUGIN_BUILDER with module M = M = struct + module M = M + module CC = M.CC + module Class = CC.Class + module Cls_tbl = Backtrackable_tbl.Make (Class) + module Expl = CC.Expl + + type term = CC.term + + module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M + + type t = (module DYN_PL_FOR_M) + + module Make (A : sig + val size : int option + val cc : CC.t + end) : DYN_PL_FOR_M = struct + module M = M + module CC = CC + open A + + (* repr -> value for the class *) + let values : M.t Cls_tbl.t = Cls_tbl.create ?size () + + (* bit in CC to filter out quickly classes without value *) + let field_has_value : CC.Class.bitfield = + CC.allocate_bitfield ~descr:("monoid." ^ M.name ^ ".has-value") cc + + let push_level () = Cls_tbl.push_level values + let pop_levels n = Cls_tbl.pop_levels values n + let n_levels () = Cls_tbl.n_levels values + + let mem n = + let res = CC.get_bitfield cc field_has_value n in + assert ( + if res then + Cls_tbl.mem values n + else + true); + res + + let get n = + if CC.get_bitfield cc field_has_value n then + Cls_tbl.get values n + else + None + + let on_new_term cc n (t : term) : unit = + (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*) + let maybe_m, l = M.of_term cc n t in + (match maybe_m with + | Some v -> + Log.debugf 20 (fun k -> + k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" M.name Class.pp n + M.pp v); + CC.set_bitfield cc field_has_value true n; + Cls_tbl.add values n v + | None -> ()); + List.iter + (fun (n_u, m_u) -> + Log.debugf 20 (fun k -> + k "(@[monoid[%s].on-new-term.sub@ :n %a@ :sub-t %a@ :value %a@])" + M.name Class.pp n Class.pp n_u M.pp m_u); + let n_u = CC.find cc n_u in + if CC.get_bitfield cc field_has_value n_u then ( + let m_u' = + try Cls_tbl.find values n_u + with Not_found -> + Error.errorf "node %a has bitfield but no value" Class.pp n_u + in + match M.merge cc n_u m_u n_u m_u' (Expl.mk_list []) with + | Error expl -> + Error.errorf + "when merging@ @[for node %a@],@ values %a and %a:@ conflict %a" + Class.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp expl + | Ok m_u_merged -> + Log.debugf 20 (fun k -> + k + "(@[monoid[%s].on-new-term.sub.merged@ :n %a@ :sub-t %a@ \ + :value %a@])" + M.name Class.pp n Class.pp n_u M.pp m_u_merged); + Cls_tbl.add values n_u m_u_merged + ) else ( + (* just add to [n_u] *) + CC.set_bitfield cc field_has_value true n_u; + Cls_tbl.add values n_u m_u + )) + l; + () + + let iter_all : _ Iter.t = Cls_tbl.to_iter values + + let on_pre_merge cc acts n1 n2 e_n1_n2 : unit = + match get n1, get n2 with + | Some v1, Some v2 -> + Log.debugf 5 (fun k -> + k + "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ \ + :val2 %a@])@])" + M.name Class.pp n1 M.pp v1 Class.pp n2 M.pp v2); + (match M.merge cc n1 v1 n2 v2 e_n1_n2 with + | Ok v' -> + Cls_tbl.remove values n2; + (* only keep repr *) + Cls_tbl.add values n1 v' + | Error expl -> CC.raise_conflict_from_expl cc acts expl) + | None, Some cr -> + CC.set_bitfield cc field_has_value true n1; + Cls_tbl.add values n1 cr; + Cls_tbl.remove values n2 (* only keep reprs *) + | Some _, None -> () (* already there on the left *) + | None, None -> () + + let pp out () : unit = + let pp_e out (t, v) = + Fmt.fprintf out "(@[%a@ :has %a@])" Class.pp t M.pp v + in + Fmt.fprintf out "(@[%a@])" (Fmt.iter pp_e) iter_all + + (* setup *) + let () = + Event.on (CC.on_new_term cc) ~f:(fun (_, r, t) -> on_new_term cc r t); + Event.on (CC.on_pre_merge cc) ~f:(fun (_, acts, ra, rb, expl) -> + on_pre_merge cc acts ra rb expl); + () + end + + let create_and_setup ?size (cc : CC.t) : t = + (module Make (struct + let size = size + let cc = cc + end)) + + let push_level ((module P) : t) = P.push_level () + let pop_levels ((module P) : t) n = P.pop_levels n + let n_levels ((module P) : t) = P.n_levels () + let mem ((module P) : t) t = P.mem t + let get ((module P) : t) t = P.get t + let iter_all ((module P) : t) = P.iter_all + let pp out ((module P) : t) = P.pp out () +end diff --git a/src/cc/plugin/sidekick_cc_plugin.mli b/src/cc/plugin/sidekick_cc_plugin.mli new file mode 100644 index 00000000..f70ae421 --- /dev/null +++ b/src/cc/plugin/sidekick_cc_plugin.mli @@ -0,0 +1,21 @@ +(** Congruence Closure Implementation *) + +open Sidekick_sigs_cc + +module type EXTENDED_PLUGIN_BUILDER = sig + include MONOID_PLUGIN_BUILDER + + val mem : t -> M.CC.Class.t -> bool + (** Does the CC Class.t have a monoid value? *) + + val get : t -> M.CC.Class.t -> M.t option + (** Get monoid value for this CC Class.t, if any *) + + val iter_all : t -> (M.CC.repr * M.t) Iter.t + + include Sidekick_sigs.BACKTRACKABLE0 with type t := t + include Sidekick_sigs.PRINT with type t := t +end + +(** Create a plugin builder from the given per-class monoid *) +module Make (M : MONOID_PLUGIN_ARG) : EXTENDED_PLUGIN_BUILDER with module M = M diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 213ba2fc..5fc40415 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -18,572 +18,8 @@ module type TERM = Sidekick_sigs_term.S module type LIT = Sidekick_sigs_lit.S module type PROOF_TRACE = Sidekick_sigs_proof_trace.S -module type SAT_PROOF = Sidekick_sigs_proof_sat.S +module type SAT_PROOF_RULES = Sidekick_sigs_proof_sat.S (** Signature for SAT-solver proof emission. *) -module type PROOF = Sidekick_sigs_proof_core.S +module type PROOF_CORE = Sidekick_sigs_proof_core.S (** Proofs of unsatisfiability. *) - -(** Registry to extract values *) -module type REGISTRY = sig - type t - type 'a key - - val create_key : unit -> 'a key - (** Call this statically, typically at program initialization, for - each distinct key. *) - - val create : unit -> t - val get : t -> 'a key -> 'a option - val set : t -> 'a key -> 'a -> unit -end - -(** A view of the solver from a theory's point of view. - - Theories should interact with the solver via this module, to assert - new lemmas, propagate literals, access the congruence closure, etc. *) -module type SOLVER_INTERNAL = sig - module T : TERM - module Lit : LIT with module T = T - module Proof_trace : PROOF_TRACE - - type ty = T.Ty.t - type term = T.Term.t - type value = T.Term.t - type term_store = T.Term.store - type ty_store = T.Ty.store - type clause_pool - type proof = Proof_trace.t - type proof_step = Proof_trace.step_id - - type t - (** {3 Main type for a solver} *) - - type solver = t - - val tst : t -> term_store - val ty_st : t -> ty_store - val stats : t -> Stat.t - - val proof : t -> proof - (** Access the proof object *) - - (** {3 Registry} *) - - module Registry : REGISTRY - - val registry : t -> Registry.t - (** A solver contains a registry so that theories can share data *) - - (** {3 Actions for the theories} *) - - type theory_actions - (** Handle that the theories can use to perform actions. *) - - type lit = Lit.t - - (** {3 Congruence Closure} *) - - (** Congruence closure instance *) - module CC : - Sidekick_sigs_cc.S - with module T = T - and module Lit = Lit - and module Proof_trace = Proof_trace - - val cc : t -> CC.t - (** Congruence closure for this solver *) - - (** {3 Simplifiers} *) - - (** Simplify terms *) - module Simplify : sig - type t - - val tst : t -> term_store - val ty_st : t -> ty_store - - val clear : t -> unit - (** Reset internal cache, etc. *) - - val proof : t -> proof - (** Access proof *) - - type hook = t -> term -> (term * proof_step Iter.t) option - (** Given a term, try to simplify it. Return [None] if it didn't change. - - A simple example could be a hook that takes a term [t], - and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, - returns [Some (const (x+y))], and [None] otherwise. - - The simplifier will take care of simplifying the resulting term further, - caching (so that work is not duplicated in subterms), etc. - *) - - val normalize : t -> term -> (term * proof_step) option - (** Normalize a term using all the hooks. This performs - a fixpoint, i.e. it only stops when no hook applies anywhere inside - the term. *) - - val normalize_t : t -> term -> term * proof_step option - (** Normalize a term using all the hooks, along with a proof that the - simplification is correct. - returns [t, ø] if no simplification occurred. *) - end - - type simplify_hook = Simplify.hook - - val add_simplifier : t -> Simplify.hook -> unit - (** Add a simplifier hook for preprocessing. *) - - val simplify_t : t -> term -> (term * proof_step) option - (** Simplify input term, returns [Some u] if some - simplification occurred. *) - - val simp_t : t -> term -> term * proof_step option - (** [simp_t si t] returns [u] even if no simplification occurred - (in which case [t == u] syntactically). - It emits [|- t=u]. - (see {!simplifier}) *) - - (** {3 Preprocessors} - These preprocessors turn mixed, raw literals (possibly simplified) into - literals suitable for reasoning. - Typically some clauses are also added to the solver. *) - - module type PREPROCESS_ACTS = sig - val proof : proof - - val mk_lit : ?sign:bool -> term -> lit - (** [mk_lit t] creates a new literal for a boolean term [t]. *) - - val add_clause : lit list -> proof_step -> unit - (** pushes a new clause into the SAT solver. *) - - val add_lit : ?default_pol:bool -> lit -> unit - (** Ensure the literal will be decided/handled by the SAT solver. *) - end - - type preprocess_actions = (module PREPROCESS_ACTS) - (** Actions available to the preprocessor *) - - type preprocess_hook = t -> preprocess_actions -> term -> unit - (** Given a term, preprocess it. - - The idea is to add literals and clauses to help define the meaning of - the term, if needed. For example for boolean formulas, clauses - for their Tseitin encoding can be added, with the formula acting - as its own proxy symbol. - - @param preprocess_actions actions available during preprocessing. - *) - - val on_preprocess : t -> preprocess_hook -> unit - (** Add a hook that will be called when terms are preprocessed *) - - (** {3 hooks for the theory} *) - - val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'a - (** Give a conflict clause to the solver *) - - val push_decision : t -> theory_actions -> lit -> unit - (** Ask the SAT solver to decide the given literal in an extension of the - current trail. This is useful for theory combination. - If the SAT solver backtracks, this (potential) decision is removed - and forgotten. *) - - val propagate : - t -> theory_actions -> lit -> reason:(unit -> lit list * proof_step) -> unit - (** Propagate a boolean using a unit clause. - [expl => lit] must be a theory lemma, that is, a T-tautology *) - - val propagate_l : t -> theory_actions -> lit -> lit list -> proof_step -> unit - (** Propagate a boolean using a unit clause. - [expl => lit] must be a theory lemma, that is, a T-tautology *) - - val add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unit - (** Add local clause to the SAT solver. This clause will be - removed when the solver backtracks. *) - - val add_clause_permanent : - t -> theory_actions -> lit list -> proof_step -> unit - (** Add toplevel clause to the SAT solver. This clause will - not be backtracked. *) - - val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit - (** Create a literal. This automatically preprocesses the term. *) - - val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit - (** Add the given literal to the SAT solver, so it gets assigned - a boolean value. - @param default_pol default polarity for the corresponding atom *) - - val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit - (** Add the given (signed) bool term to the SAT solver, so it gets assigned - a boolean value *) - - val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'a - (** Raise a conflict with the given congruence closure explanation. - it must be a theory tautology that [expl ==> absurd]. - To be used in theories. *) - - val cc_find : t -> CC.Class.t -> CC.Class.t - (** Find representative of the node *) - - val cc_are_equal : t -> term -> term -> bool - (** Are these two terms equal in the congruence closure? *) - - val cc_merge : - t -> theory_actions -> CC.Class.t -> CC.Class.t -> CC.Expl.t -> unit - (** Merge these two nodes in the congruence closure, given this explanation. - It must be a theory tautology that [expl ==> n1 = n2]. - To be used in theories. *) - - val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unit - (** Merge these two terms in the congruence closure, given this explanation. - See {!cc_merge} *) - - val cc_add_term : t -> term -> CC.Class.t - (** Add/retrieve congruence closure node for this term. - To be used in theories *) - - val cc_mem_term : t -> term -> bool - (** Return [true] if the term is explicitly in the congruence closure. - To be used in theories *) - - val on_cc_pre_merge : - t -> - (CC.t -> theory_actions -> CC.Class.t -> CC.Class.t -> CC.Expl.t -> unit) -> - unit - (** Callback for when two classes containing data for this key are merged (called before) *) - - val on_cc_post_merge : - t -> (CC.t -> theory_actions -> CC.Class.t -> CC.Class.t -> unit) -> unit - (** Callback for when two classes containing data for this key are merged (called after)*) - - val on_cc_new_term : t -> (CC.t -> CC.Class.t -> term -> unit) -> unit - (** Callback to add data on terms when they are added to the congruence - closure *) - - val on_cc_is_subterm : t -> (CC.Class.t -> term -> unit) -> unit - (** Callback for when a term is a subterm of another term in the - congruence closure *) - - val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit - (** Callback called on every CC conflict *) - - val on_cc_propagate : - t -> (CC.t -> lit -> (unit -> lit list * proof_step) -> unit) -> unit - (** Callback called on every CC propagation *) - - val on_partial_check : - t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit - (** Register callbacked to be called with the slice of literals - newly added on the trail. - - This is called very often and should be efficient. It doesn't have - to be complete, only correct. It's given only the slice of - the trail consisting in new literals. *) - - val on_final_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit - (** Register callback to be called during the final check. - - Must be complete (i.e. must raise a conflict if the set of literals is - not satisfiable) and can be expensive. The function - is given the whole trail. - *) - - val on_th_combination : - t -> (t -> theory_actions -> (term * value) Iter.t) -> unit - (** Add a hook called during theory combination. - The hook must return an iterator of pairs [(t, v)] - which mean that term [t] has value [v] in the model. - - Terms with the same value (according to {!Term.equal}) will be - merged in the CC; if two terms with different values are merged, - we get a semantic conflict and must pick another model. *) - - val declare_pb_is_incomplete : t -> unit - (** Declare that, in some theory, the problem is outside the logic fragment - that is decidable (e.g. if we meet proper NIA formulas). - The solver will not reply "SAT" from now on. *) - - (** {3 Model production} *) - - type model_ask_hook = - recurse:(t -> CC.Class.t -> term) -> t -> CC.Class.t -> term option - (** A model-production hook to query values from a theory. - - It takes the solver, a class, and returns - a term for this class. For example, an arithmetic theory - might detect that a class contains a numeric constant, and return - this constant as a model value. - - If no hook assigns a value to a class, a fake value is created for it. - *) - - type model_completion_hook = t -> add:(term -> term -> unit) -> unit - (** A model production hook, for the theory to add values. - The hook is given a [add] function to add bindings to the model. *) - - val on_model : - ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit - (** Add model production/completion hooks. *) -end - -(** User facing view of the solver. - - This is the solver a user of sidekick can see, after instantiating - everything. The user can add some theories, clauses, etc. and asks - the solver to check satisfiability. - - Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *) -module type SOLVER = sig - module T : TERM - module Lit : LIT with module T = T - module Proof_trace : PROOF_TRACE - - (** Internal solver, available to theories. *) - module Solver_internal : - SOLVER_INTERNAL - with module T = T - and module Lit = Lit - and module Proof_trace = Proof_trace - - type t - (** The solver's state. *) - - type solver = t - type term = T.Term.t - type ty = T.Ty.t - type lit = Lit.t - type proof = Proof_trace.t - type proof_step = Proof_trace.step_id - - (** {3 Value registry} *) - - module Registry : REGISTRY - - val registry : t -> Registry.t - (** A solver contains a registry so that theories can share data *) - - (** {3 A theory} - - Theories are abstracted over the concrete implementation of the solver, - so they can work with any implementation. - - Typically a theory should be a functor taking an argument containing - a [SOLVER_INTERNAL] or even a full [SOLVER], - and some additional views on terms, literals, etc. - that are specific to the theory (e.g. to map terms to linear - expressions). - The theory can then be instantiated on any kind of solver for any - term representation that also satisfies the additional theory-specific - requirements. Instantiated theories (ie values of type {!SOLVER.theory}) - can be added to the solver. - *) - module type THEORY = sig - type t - (** The theory's state *) - - val name : string - (** Name of the theory (ideally, unique and short) *) - - val create_and_setup : Solver_internal.t -> t - (** Instantiate the theory's state for the given (internal) solver, - register callbacks, create keys, etc. - - Called once for every solver this theory is added to. *) - - val push_level : t -> unit - (** Push backtracking level. When the corresponding pop is called, - the theory's state should be restored to a state {b equivalent} - to what it was just before [push_level]. - - it does not have to be exactly the same state, it just needs to - be equivalent. *) - - val pop_levels : t -> int -> unit - (** [pop_levels theory n] pops [n] backtracking levels, - restoring [theory] to its state before calling [push_level] n times. *) - end - - type theory = (module THEORY) - (** A theory that can be used for this particular solver. *) - - type 'a theory_p = (module THEORY with type t = 'a) - (** A theory that can be used for this particular solver, with state - of type ['a]. *) - - val mk_theory : - name:string -> - create_and_setup:(Solver_internal.t -> 'th) -> - ?push_level:('th -> unit) -> - ?pop_levels:('th -> int -> unit) -> - unit -> - theory - (** Helper to create a theory. *) - - (** Models - - A model can be produced when the solver is found to be in a - satisfiable state after a call to {!solve}. *) - module Model : sig - type t - - val empty : t - val mem : t -> term -> bool - val find : t -> term -> term option - val eval : t -> term -> term option - val pp : t Fmt.printer - end - - (* TODO *) - module Unknown : sig - type t - - val pp : t CCFormat.printer - - (* - type unknown = - | U_timeout - | U_incomplete - *) - end - - (** {3 Main API} *) - - val stats : t -> Stat.t - val tst : t -> T.Term.store - val ty_st : t -> T.Ty.store - val proof : t -> proof - - val create : - ?stat:Stat.t -> - ?size:[ `Big | `Tiny | `Small ] -> - (* TODO? ?config:Config.t -> *) - proof:proof -> - theories:theory list -> - T.Term.store -> - T.Ty.store -> - unit -> - t - (** Create a new solver. - - It needs a term state and a type state to manipulate terms and types. - All terms and types interacting with this solver will need to come - from these exact states. - - @param store_proof if true, proofs from the SAT solver and theories - are retained and potentially accessible after {!solve} - returns UNSAT. - @param size influences the size of initial allocations. - @param theories theories to load from the start. Other theories - can be added using {!add_theory}. *) - - val add_theory : t -> theory -> unit - (** Add a theory to the solver. This should be called before - any call to {!solve} or to {!add_clause} and the likes (otherwise - the theory will have a partial view of the problem). *) - - val add_theory_p : t -> 'a theory_p -> 'a - (** Add the given theory and obtain its state *) - - val add_theory_l : t -> theory list -> unit - - val mk_lit_t : t -> ?sign:bool -> term -> lit - (** [mk_lit_t _ ~sign t] returns [lit'], - where [lit'] is [preprocess(lit)] and [lit] is - an internal representation of [± t]. - - The proof of [|- lit = lit'] is directly added to the solver's proof. *) - - val add_clause : t -> lit array -> proof_step -> unit - (** [add_clause solver cs] adds a boolean clause to the solver. - Subsequent calls to {!solve} will need to satisfy this clause. *) - - val add_clause_l : t -> lit list -> proof_step -> unit - (** Add a clause to the solver, given as a list. *) - - val assert_terms : t -> term list -> unit - (** Helper that turns each term into an atom, before adding the result - to the solver as an assertion *) - - val assert_term : t -> term -> unit - (** Helper that turns the term into an atom, before adding the result - to the solver as a unit clause assertion *) - - (** Result of solving for the current set of clauses *) - type res = - | Sat of Model.t (** Satisfiable *) - | Unsat of { - unsat_core: unit -> lit Iter.t; - (** Unsat core (subset of assumptions), or empty *) - unsat_proof_step: unit -> proof_step option; - (** Proof step for the empty clause *) - } (** Unsatisfiable *) - | Unknown of Unknown.t - (** Unknown, obtained after a timeout, memory limit, etc. *) - - (* TODO: API to push/pop/clear assumptions, in addition to ~assumptions param *) - - val solve : - ?on_exit:(unit -> unit) list -> - ?check:bool -> - ?on_progress:(t -> unit) -> - ?should_stop:(t -> int -> bool) -> - assumptions:lit list -> - t -> - res - (** [solve s] checks the satisfiability of the clauses added so far to [s]. - @param check if true, the model is checked before returning. - @param on_progress called regularly during solving. - @param assumptions a set of atoms held to be true. The unsat core, - if any, will be a subset of [assumptions]. - @param should_stop a callback regularly called with the solver, - and with a number of "steps" done since last call. The exact notion - of step is not defined, but is guaranteed to increase regularly. - The function should return [true] if it judges solving - must stop (returning [Unknown]), [false] if solving can proceed. - @param on_exit functions to be run before this returns *) - - val last_res : t -> res option - (** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *) - - val push_assumption : t -> lit -> unit - (** Pushes an assumption onto the assumption stack. It will remain - there until it's pop'd by {!pop_assumptions}. *) - - val pop_assumptions : t -> int -> unit - (** [pop_assumptions solver n] removes [n] assumptions from the stack. - It removes the assumptions that were the most - recently added via {!push_assumptions}. - Note that {!check_sat_propagations_only} can call this if it meets - a conflict. *) - - type propagation_result = - | PR_sat - | PR_conflict of { backtracked: int } - | PR_unsat of { unsat_core: unit -> lit Iter.t } - - val check_sat_propagations_only : - assumptions:lit list -> t -> propagation_result - (** [check_sat_propagations_only solver] uses assumptions (including - the [assumptions] parameter, and atoms previously added via {!push_assumptions}) - and boolean+theory propagation to quickly assess satisfiability. - It is not complete; calling {!solve} is required to get an accurate - result. - @returns one of: - - - [PR_sat] if the current state seems satisfiable - - [PR_conflict {backtracked=n}] if a conflict was found and resolved, - leading to backtracking [n] levels of assumptions - - [PR_unsat …] if the assumptions were found to be unsatisfiable, with - the given core. - *) - - (* TODO: allow on_progress to return a bool to know whether to stop? *) - - val pp_stats : t CCFormat.printer - (** Print some statistics. What it prints exactly is unspecified. *) -end diff --git a/src/lra/dune b/src/lra/dune index ffd2ca61..3e1f839c 100644 --- a/src/lra/dune +++ b/src/lra/dune @@ -3,4 +3,5 @@ (public_name sidekick.arith-lra) (synopsis "Solver for LRA (real arithmetic)") (flags :standard -warn-error -a+8 -w -32 -open Sidekick_util) - (libraries containers sidekick.core sidekick.arith sidekick.simplex)) + (libraries containers sidekick.sigs.smt sidekick.arith sidekick.simplex + sidekick.cc.plugin)) diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 344ccd3c..eb8efe82 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -1,9 +1,9 @@ -(** {1 Linear Rational Arithmetic} *) +(** Linear Rational Arithmetic *) (* Reference: http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_LRA *) -open Sidekick_core +open Sidekick_sigs_smt module Predicate = Sidekick_simplex.Predicate module Linear_expr = Sidekick_simplex.Linear_expr module Linear_expr_intf = Sidekick_simplex.Linear_expr_intf @@ -32,7 +32,7 @@ let map_view f (l : _ lra_view) : _ lra_view = | LRA_other x -> LRA_other (f x) module type ARG = sig - module S : Sidekick_core.SOLVER + module S : SOLVER module Z : INT module Q : RATIONAL with type bigint = Z.t @@ -55,7 +55,7 @@ module type ARG = sig val has_ty_real : term -> bool (** Does this term have the type [Real] *) - val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rule + val lemma_lra : S.Lit.t Iter.t -> S.Proof_trace.A.rule module Gensym : sig type t @@ -104,7 +104,11 @@ module Make (A : ARG) : S with module A = A = struct module T = A.S.T.Term module Lit = A.S.Solver_internal.Lit module SI = A.S.Solver_internal - module N = A.S.Solver_internal.CC.N + module N = SI.CC.Class + + open struct + module Pr = SI.Proof_trace + end module Tag = struct type t = Lit of Lit.t | CC_eq of N.t * N.t @@ -171,7 +175,7 @@ module Make (A : ARG) : S with module A = A = struct (* monoid to track linear expressions in congruence classes, to clash on merge *) module Monoid_exprs = struct - module SI = SI + module CC = SI.CC let name = "lra.const" @@ -214,12 +218,12 @@ module Make (A : ARG) : S with module A = A = struct with Confl expl -> Error expl end - module ST_exprs = Sidekick_core.Monoid_of_repr (Monoid_exprs) + module ST_exprs = Sidekick_cc_plugin.Make (Monoid_exprs) type state = { tst: T.store; ty_st: Ty.store; - proof: SI.P.t; + proof: SI.Proof_trace.t; gensym: A.Gensym.t; in_model: unit T.Tbl.t; (* terms to add to model *) encoded_eqs: unit T.Tbl.t; @@ -245,7 +249,7 @@ module Make (A : ARG) : S with module A = A = struct ty_st; proof; in_model = T.Tbl.create 8; - st_exprs = ST_exprs.create_and_setup si; + st_exprs = ST_exprs.create_and_setup (SI.cc si); gensym = A.Gensym.create tst; simp_preds = T.Tbl.create 32; simp_defined = T.Tbl.create 16; @@ -346,12 +350,13 @@ module Make (A : ARG) : S with module A = A = struct proxy) let add_clause_lra_ ?using (module PA : SI.PREPROCESS_ACTS) lits = - let pr = A.lemma_lra (Iter.of_list lits) PA.proof in + let pr = Pr.add_step PA.proof @@ A.lemma_lra (Iter.of_list lits) in let pr = match using with | None -> pr | Some using -> - SI.P.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using PA.proof + Pr.add_step PA.proof + @@ SI.P_core_rules.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using in PA.add_clause lits pr @@ -388,7 +393,7 @@ module Make (A : ARG) : S with module A = A = struct proxy, A.Q.one) (* look for subterms of type Real, for they will need theory combination *) - let on_subterm (self : state) _ (t : T.t) : unit = + let on_subterm (self : state) (t : T.t) : unit = Log.debugf 50 (fun k -> k "(@[lra.cc-on-subterm@ %a@])" T.pp t); match A.view_as_lra t with | LRA_other _ when not (A.has_ty_real t) -> () @@ -408,8 +413,8 @@ module Make (A : ARG) : S with module A = A = struct (* tell the CC this term exists *) let declare_term_to_cc ~sub t = Log.debugf 50 (fun k -> k "(@[lra.declare-term-to-cc@ %a@])" T.pp t); - ignore (SI.CC.add_term (SI.cc si) t : SI.CC.N.t); - if sub then on_subterm self () t + ignore (SI.CC.add_term (SI.cc si) t : N.t); + if sub then on_subterm self t in match A.view_as_lra t with @@ -491,15 +496,14 @@ module Make (A : ARG) : S with module A = A = struct | LRA_other _ -> () let simplify (self : state) (_recurse : _) (t : T.t) : - (T.t * SI.proof_step Iter.t) option = + (T.t * SI.step_id Iter.t) option = let proof_eq t u = - A.lemma_lra - (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) - self.proof + Pr.add_step self.proof + @@ A.lemma_lra (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) in let proof_bool t ~sign:b = let lit = SI.Lit.atom ~sign:b self.tst t in - A.lemma_lra (Iter.return lit) self.proof + Pr.add_step self.proof @@ A.lemma_lra (Iter.return lit) in match A.view_as_lra t with @@ -564,7 +568,7 @@ module Make (A : ARG) : S with module A = A = struct |> CCList.flat_map (Tag.to_lits si) |> List.rev_map SI.Lit.neg in - let pr = A.lemma_lra (Iter.of_list confl) (SI.proof si) in + let pr = Pr.add_step (SI.proof si) @@ A.lemma_lra (Iter.of_list confl) in SI.raise_conflict si acts confl pr let on_propagate_ si acts lit ~reason = @@ -573,7 +577,10 @@ module Make (A : ARG) : S with module A = A = struct (* TODO: more detailed proof certificate *) SI.propagate si acts lit ~reason:(fun () -> let lits = CCList.flat_map (Tag.to_lits si) reason in - let pr = A.lemma_lra Iter.(cons lit (of_list lits)) (SI.proof si) in + let pr = + Pr.add_step (SI.proof si) + @@ A.lemma_lra Iter.(cons lit (of_list lits)) + in CCList.flat_map (Tag.to_lits si) reason, pr) | _ -> () @@ -616,7 +623,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 = SI.Lit.neg @@ SI.mk_lit si acts @@ A.mk_eq self.tst t1 t2 in - let pr = A.lemma_lra (Iter.return lit) self.proof in + let pr = Pr.add_step self.proof @@ A.lemma_lra (Iter.return lit) in SI.add_clause_permanent si acts [ lit ] pr ) ) else ( @@ -791,14 +798,14 @@ module Make (A : ARG) : S with module A = A = struct SI.on_final_check si (final_check_ st); SI.on_partial_check si (partial_check_ st); SI.on_model si ~ask:(model_ask_ st) ~complete:(model_complete_ st); - SI.on_cc_is_subterm si (on_subterm st); - SI.on_cc_pre_merge si (fun si acts n1 n2 expl -> + SI.on_cc_is_subterm si (fun (_, _, t) -> on_subterm st t); + SI.on_cc_pre_merge si (fun (cc, acts, n1, n2, expl) -> match as_const_ (N.term n1), as_const_ (N.term n2) with | Some q1, Some q2 when A.Q.(q1 <> q2) -> (* classes with incompatible constants *) Log.debugf 30 (fun k -> k "(@[lra.merge-incompatible-consts@ %a@ %a@])" N.pp n1 N.pp n2); - SI.CC.raise_conflict_from_expl si acts expl + SI.CC.raise_conflict_from_expl cc acts expl | _ -> ()); SI.on_th_combination si (do_th_combination st); st diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 47df0b09..88206499 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -22,7 +22,13 @@ end (* TODO: on the fly compression *) module Proof : sig - include Sidekick_sat.PROOF with type lit = Lit.t + include Sidekick_sigs_proof_trace.S + + module Rule : + Sidekick_sat.PROOF_RULES + with type lit = Lit.t + and type rule = A.rule + and type step_id = A.step_id type in_memory @@ -51,12 +57,20 @@ end = struct | Inner of in_memory | Out of { oc: out_channel; close: unit -> unit } - type proof_step = unit - type proof_rule = t -> proof_step + module A = struct + type step_id = unit + type rule = t -> unit - module Step_vec = Vec_unit + module Step_vec = Vec_unit + end - let[@inline] enabled pr = + open A + + let[@inline] add_step (self : t) r = r self + let add_unsat _ _ = () + let delete _ _ = () + + let[@inline] enabled (pr : t) = match pr with | Dummy -> false | Inner _ | Out _ -> true @@ -64,29 +78,37 @@ end = struct let[@inline] emit_lits_buf_ buf lits = lits (fun i -> bpf buf "%d " i) let[@inline] emit_lits_out_ oc lits = lits (fun i -> fpf oc "%d " i) - let emit_input_clause lits self = - match self with - | Dummy -> () - | Inner buf -> - bpf buf "i "; - emit_lits_buf_ buf lits; - bpf buf "0\n" - | Out { oc; _ } -> - fpf oc "i "; - emit_lits_out_ oc lits; - fpf oc "0\n" + module Rule = struct + type nonrec lit = lit + type nonrec rule = rule + type nonrec step_id = step_id - let emit_redundant_clause lits ~hyps:_ self = - match self with - | Dummy -> () - | Inner buf -> - bpf buf "r "; - emit_lits_buf_ buf lits; - bpf buf "0\n" - | Out { oc; _ } -> - fpf oc "r "; - emit_lits_out_ oc lits; - fpf oc "0\n" + let sat_input_clause lits self = + match self with + | Dummy -> () + | Inner buf -> + bpf buf "i "; + emit_lits_buf_ buf lits; + bpf buf "0\n" + | Out { oc; _ } -> + fpf oc "i "; + emit_lits_out_ oc lits; + fpf oc "0\n" + + let sat_redundant_clause lits ~hyps:_ self = + match self with + | Dummy -> () + | Inner buf -> + bpf buf "r "; + emit_lits_buf_ buf lits; + bpf buf "0\n" + | Out { oc; _ } -> + fpf oc "r "; + emit_lits_out_ oc lits; + fpf oc "0\n" + + let sat_unsat_core _ _ = () + end let del_clause () lits self = match self with @@ -100,9 +122,6 @@ end = struct emit_lits_out_ oc lits; fpf oc "0\n" - let emit_unsat _ _ = () - let emit_unsat_core _ _ = () - (* lifetime *) let dummy : t = Dummy @@ -153,10 +172,11 @@ module Arg = struct type lit = Lit.t - module Proof = Proof + module Proof_trace = Proof + module Proof_rules = Proof.Rule type proof = Proof.t - type proof_step = Proof.proof_step + type step_id = Proof.A.step_id end module SAT = Sidekick_sat.Make_pure_sat (Arg) diff --git a/src/mini-cc/Sidekick_mini_cc.ml b/src/mini-cc/Sidekick_mini_cc.ml index 444c0f2f..6decc650 100644 --- a/src/mini-cc/Sidekick_mini_cc.ml +++ b/src/mini-cc/Sidekick_mini_cc.ml @@ -5,7 +5,7 @@ module type TERM = Sidekick_sigs_term.S module type ARG = sig module T : TERM - val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t + val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t end module type S = sig @@ -165,7 +165,7 @@ module Make (A : ARG) = struct () let sub_ t k : unit = - match A.cc_view t with + match A.view_as_cc t with | Bool _ | Opaque _ -> () | App_fun (_, args) -> args k | App_ho (f, a) -> @@ -202,7 +202,7 @@ module Make (A : ARG) = struct let compute_sig (self : t) (n : node) : Signature.t option = let[@inline] return x = Some x in - match A.cc_view n.n_t with + match A.view_as_cc n.n_t with | Bool _ | Opaque _ -> None | Eq (a, b) -> let a = find_t_ self a in @@ -318,7 +318,7 @@ module Make (A : ARG) = struct (* API *) let add_lit (self : t) (p : T.t) (sign : bool) : unit = - match A.cc_view p with + match A.view_as_cc p with | Eq (t1, t2) when sign -> let n1 = add_t self t1 in let n2 = add_t self t2 in diff --git a/src/mini-cc/Sidekick_mini_cc.mli b/src/mini-cc/Sidekick_mini_cc.mli index 85d5b588..413d2518 100644 --- a/src/mini-cc/Sidekick_mini_cc.mli +++ b/src/mini-cc/Sidekick_mini_cc.mli @@ -15,7 +15,7 @@ module type TERM = Sidekick_sigs_term.S module type ARG = sig module T : TERM - val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t + val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t end (** Main signature for an instance of the mini congruence closure *) diff --git a/src/mini-cc/tests/sidekick_test_minicc.ml b/src/mini-cc/tests/sidekick_test_minicc.ml index 0d96fd3e..1a3969bb 100644 --- a/src/mini-cc/tests/sidekick_test_minicc.ml +++ b/src/mini-cc/tests/sidekick_test_minicc.ml @@ -4,7 +4,7 @@ module A = Alcotest module CC = Sidekick_mini_cc.Make (struct module T = Sidekick_base.Solver_arg - let cc_view = Term.cc_view + let view_as_cc = Term.cc_view end) module Setup () = struct diff --git a/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml b/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml new file mode 100644 index 00000000..da1d2c0c --- /dev/null +++ b/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml @@ -0,0 +1,18 @@ +module type S = Sidekick_sigs_proof_trace.S + +module type ARG = sig + include Sidekick_sigs_proof_trace.ARG + + val dummy_step_id : step_id +end + +module Make (A : ARG) : S with type t = unit and module A = A = struct + module A = A + + type t = unit + + let enabled _ = false + let add_step _ _ = A.dummy_step_id + let add_unsat _ _ = () + let delete _ _ = () +end diff --git a/src/proof-trace/dummy/dune b/src/proof-trace/dummy/dune new file mode 100644 index 00000000..57140a75 --- /dev/null +++ b/src/proof-trace/dummy/dune @@ -0,0 +1,6 @@ +(library + (name sidekick_proof_trace_dummy) + (public_name sidekick.proof-trace.dummy) + (synopsis "Dummy proof trace that stores nothing") + (libraries sidekick.util sidekick.sigs.proof-trace) + (flags :standard -open Sidekick_util)) diff --git a/src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml b/src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml new file mode 100644 index 00000000..9deee8f7 --- /dev/null +++ b/src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml @@ -0,0 +1,23 @@ +module type ARG = Sidekick_sigs_proof_trace.ARG +module type S = Sidekick_sigs_proof_trace.S + +(** Dynamic version. + + The proof trace is a first-class module that can be provided at runtime. *) +module Make_dyn (A : ARG) : S with module A = A = struct + module A = A + + module type DYN = sig + val enabled : unit -> bool + val add_step : A.rule -> A.step_id + val add_unsat : A.step_id -> unit + val delete : A.step_id -> unit + end + + type t = (module DYN) + + let[@inline] enabled ((module Tr) : t) : bool = Tr.enabled () + let[@inline] add_step ((module Tr) : t) rule : A.step_id = Tr.add_step rule + let[@inline] add_unsat ((module Tr) : t) s : unit = Tr.add_unsat s + let[@inline] delete ((module Tr) : t) s : unit = Tr.delete s +end diff --git a/src/proof-trace/dyn/dune b/src/proof-trace/dyn/dune new file mode 100644 index 00000000..24ca6785 --- /dev/null +++ b/src/proof-trace/dyn/dune @@ -0,0 +1,6 @@ +(library + (name sidekick_proof_trace_dyn) + (public_name sidekick.proof-trace.dyn) + (synopsis "Dynamic version of the proof trace") + (libraries sidekick.util sidekick.sigs.proof-trace) + (flags :standard -open Sidekick_util)) diff --git a/src/sat/Proof_dummy.ml b/src/sat/Proof_dummy.ml index 063e7654..7fe4b9f3 100644 --- a/src/sat/Proof_dummy.ml +++ b/src/sat/Proof_dummy.ml @@ -1,21 +1,17 @@ +(** Dummy proof module for rule=empty *) + module Make (Lit : sig type t end) : - Solver_intf.PROOF + Solver_intf.PROOF_RULES with type lit = Lit.t - and type t = unit - and type proof_step = unit = struct + and type rule = unit + and type step_id = unit = struct type lit = Lit.t - type t = unit - type proof_step = unit - type proof_rule = t -> proof_step + type rule = unit + type step_id = unit - module Step_vec = Vec_unit - - let enabled (_pr : t) = false - let del_clause _ _ (_pr : t) = () - let emit_redundant_clause _ ~hyps:_ _ = () - let emit_input_clause _ _ = () - let emit_unsat _ _ = () - let emit_unsat_core _ (_pr : t) = () + let sat_input_clause _ = () + let sat_redundant_clause _ ~hyps:_ = () + let sat_unsat_core _ = () end diff --git a/src/sat/Proof_dummy.mli b/src/sat/Proof_dummy.mli deleted file mode 100644 index 673a4395..00000000 --- a/src/sat/Proof_dummy.mli +++ /dev/null @@ -1,11 +0,0 @@ -(** Dummy proof module that does nothing. *) - -module Make (Lit : sig - type t -end) : sig - include - Solver_intf.PROOF - with type lit = Lit.t - and type t = unit - and type proof_step = unit -end diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index b64bacf8..2210b271 100644 --- a/src/sat/Sidekick_sat.ml +++ b/src/sat/Sidekick_sat.ml @@ -5,7 +5,8 @@ module Solver_intf = Solver_intf module type S = Solver_intf.S module type LIT = Solver_intf.LIT module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T -module type PROOF = Solver_intf.PROOF +module type PLUGIN_SAT = Solver_intf.PLUGIN_SAT +module type PROOF_RULES = Solver_intf.PROOF_RULES type lbool = Solver_intf.lbool = L_true | L_false | L_undefined diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 75cfa446..08d7d7f0 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -13,10 +13,16 @@ let invalid_argf fmt = Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt module Make (Plugin : PLUGIN) = struct - type lit = Plugin.lit + module Lit = Plugin.Lit + module Proof_trace = Plugin.Proof_trace + module Proof_rules = Plugin.Proof_rules + module Step_vec = Proof_trace.A.Step_vec + + type lit = Plugin.Lit.t type theory = Plugin.t - type proof = Plugin.proof - type proof_step = Plugin.proof_step + type proof_rule = Proof_trace.A.rule + type proof_step = Proof_trace.A.step_id + type proof_trace = Proof_trace.t module Clause_pool_id : sig type t = private int @@ -28,10 +34,6 @@ module Make (Plugin : PLUGIN) = struct let _unsafe_of_int x = x end - module Lit = Plugin.Lit - module Proof = Plugin.Proof - module Step_vec = Proof.Step_vec - (* ### types ### *) (* a boolean variable (positive int) *) @@ -835,7 +837,7 @@ module Make (Plugin : PLUGIN) = struct type t = { store: store; (* atom/var/clause store *) th: theory; (* user defined theory *) - proof: Proof.t; (* the proof object *) + proof: Proof_trace.t; (* the proof object *) (* Clauses are simplified for efficiency purposes. In the following vectors, the comments actually refer to the original non-simplified clause. *) @@ -878,10 +880,11 @@ module Make (Plugin : PLUGIN) = struct temp_step_vec: Step_vec.t; mutable var_incr: float; (* increment for variables' activity *) mutable clause_incr: float; (* increment for clauses' activity *) - mutable on_conflict: (t -> Clause.t -> unit) option; - mutable on_decision: (t -> lit -> unit) option; - mutable on_learnt: (t -> Clause.t -> unit) option; - mutable on_gc: (t -> lit array -> unit) option; + (* FIXME: use event *) + on_conflict: Clause.t Event.Emitter.t; + on_decision: lit Event.Emitter.t; + on_learnt: Clause.t Event.Emitter.t; + on_gc: lit array Event.Emitter.t; stat: Stat.t; n_conflicts: int Stat.counter; n_propagations: int Stat.counter; @@ -930,21 +933,21 @@ module Make (Plugin : PLUGIN) = struct n_propagations = Stat.mk_int stat "sat.n-propagations"; n_restarts = Stat.mk_int stat "sat.n-restarts"; n_minimized_away = Stat.mk_int stat "sat.n-confl-lits-minimized-away"; - on_conflict = None; - on_decision = None; - on_learnt = None; - on_gc = None; + on_conflict = Event.Emitter.create (); + on_decision = Event.Emitter.create (); + on_learnt = Event.Emitter.create (); + on_gc = Event.Emitter.create (); } - let create ?on_conflict ?on_decision ?on_learnt ?on_gc ?(stat = Stat.global) - ?(size = `Big) ~proof (th : theory) : t = + let on_gc self = Event.of_emitter self.on_gc + let on_conflict self = Event.of_emitter self.on_conflict + let on_decision self = Event.of_emitter self.on_decision + let on_learnt self = Event.of_emitter self.on_learnt + + let create ?(stat = Stat.global) ?(size = `Big) ~proof (th : theory) : t = let store = Store.create ~size ~stat () in let max_clauses_learnt = ref 0 in let self = create_ ~max_clauses_learnt ~store ~proof ~stat th in - self.on_decision <- on_decision; - self.on_conflict <- on_conflict; - self.on_learnt <- on_learnt; - self.on_gc <- on_gc; self (* iterate on all learnt clauses, pools included *) @@ -1071,10 +1074,10 @@ module Make (Plugin : PLUGIN) = struct if !steps = [] then proof_c2 else - Proof.emit_redundant_clause - (Iter.return (Atom.lit self.store a)) - ~hyps:Iter.(cons proof_c2 (of_list !steps)) - self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_redundant_clause + (Iter.return (Atom.lit self.store a)) + ~hyps:Iter.(cons proof_c2 (of_list !steps)) in Atom.set_proof_lvl0 self.store a p; @@ -1164,10 +1167,11 @@ module Make (Plugin : PLUGIN) = struct (Atom.debug_a store) atoms); let proof = let lits = Iter.of_array atoms |> Iter.map (Atom.lit store) in - Proof.emit_redundant_clause lits - ~hyps: - Iter.(cons (Clause.proof_step self.store c) (of_list !res0_proofs)) - self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_redundant_clause lits + ~hyps: + Iter.( + cons (Clause.proof_step self.store c) (of_list !res0_proofs)) in Clause.make_a store atoms proof ~removable:(Clause.removable store c) ) @@ -1260,7 +1264,7 @@ module Make (Plugin : PLUGIN) = struct (Clause.debug self.store) c let prove_unsat self (us : clause) : clause = - if Proof.enabled self.proof && Clause.n_atoms self.store us > 0 then ( + if Proof_trace.enabled self.proof && Clause.n_atoms self.store us > 0 then ( (* reduce [c] to an empty clause, all its literals should be false at level 0 *) Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" (Clause.debug self.store) us); @@ -1277,8 +1281,9 @@ module Make (Plugin : PLUGIN) = struct | _ -> assert false); let p_empty = - Proof.emit_redundant_clause Iter.empty ~hyps:(Step_vec.to_iter pvec) - self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_redundant_clause Iter.empty + ~hyps:(Step_vec.to_iter pvec) in Step_vec.clear pvec; let c_empty = Clause.make_l self.store [] ~removable:false p_empty in @@ -1296,11 +1301,9 @@ module Make (Plugin : PLUGIN) = struct match us with | US_false c -> self.unsat_at_0 <- Some c; - (match self.on_learnt with - | Some f -> f self c - | None -> ()); + Event.emit self.on_learnt c; let p = Clause.proof_step self.store c in - Proof.emit_unsat p self.proof; + Proof_trace.add_unsat self.proof p; US_false c | US_local _ -> us in @@ -1405,7 +1408,7 @@ module Make (Plugin : PLUGIN) = struct | Some (Bcp c | Bcp_lazy (lazy c)) -> let c_atoms = Clause.atoms_a store c in assert (Var.equal v (Atom.var c_atoms.(0))); - if Proof.enabled self.proof then + if Proof_trace.enabled self.proof then Step_vec.push steps (Clause.proof_step self.store c); (* check that all the other lits of [c] are marked or redundant *) @@ -1418,7 +1421,7 @@ module Make (Plugin : PLUGIN) = struct | _ when lvl_v2 = 0 -> (* can always remove literals at level 0, but got to update proof properly *) - if Proof.enabled self.proof then ( + if Proof_trace.enabled self.proof then ( let p = proof_of_atom_lvl0_ self (Atom.neg c_atoms.(i)) in Step_vec.push steps p ) @@ -1536,7 +1539,7 @@ module Make (Plugin : PLUGIN) = struct clause); if Clause.removable store clause then clause_bump_activity self clause; - if Proof.enabled self.proof then + if Proof_trace.enabled self.proof then Step_vec.push steps (Clause.proof_step self.store clause); (* visit the current predecessors *) @@ -1548,7 +1551,7 @@ module Make (Plugin : PLUGIN) = struct if Atom.level store q = 0 then ( (* skip [q] entirely, resolved away at level 0 *) assert (Atom.is_false store q); - if Proof.enabled self.proof then ( + if Proof_trace.enabled self.proof then ( let step = proof_of_atom_lvl0_ self (Atom.neg q) in Step_vec.push steps step ) @@ -1639,15 +1642,13 @@ module Make (Plugin : PLUGIN) = struct assert (cr.cr_backtrack_lvl = 0 && decision_level self = 0); let p = - Proof.emit_redundant_clause - (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) - ~hyps:(Step_vec.to_iter cr.cr_steps) - self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_redundant_clause + (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) + ~hyps:(Step_vec.to_iter cr.cr_steps) in let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in - (match self.on_learnt with - | Some f -> f self uclause - | None -> ()); + Event.emit self.on_learnt uclause; if Atom.is_false store fuip then (* incompatible at level 0 *) @@ -1658,19 +1659,17 @@ module Make (Plugin : PLUGIN) = struct | _ -> let fuip = cr.cr_learnt.(0) in let p = - Proof.emit_redundant_clause - (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) - ~hyps:(Step_vec.to_iter cr.cr_steps) - self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_redundant_clause + (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) + ~hyps:(Step_vec.to_iter cr.cr_steps) in let lclause = Clause.make_a store ~removable:true cr.cr_learnt p in add_clause_to_vec_ ~pool self lclause; attach_clause self lclause; clause_bump_activity self lclause; - (match self.on_learnt with - | Some f -> f self lclause - | None -> ()); + Event.emit self.on_learnt lclause; assert cr.cr_is_uip; enqueue_bool self fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)); var_decay_activity self; @@ -2004,7 +2003,7 @@ module Make (Plugin : PLUGIN) = struct let[@inline] current_slice st : _ Solver_intf.acts = let module M = struct - type nonrec proof = proof + type nonrec proof = Proof_trace.t type nonrec proof_step = proof_step type nonrec lit = lit @@ -2022,7 +2021,7 @@ module Make (Plugin : PLUGIN) = struct (* full slice, for [if_sat] final check *) let[@inline] full_slice st : _ Solver_intf.acts = let module M = struct - type nonrec proof = proof + type nonrec proof = Proof_trace.t type nonrec proof_step = proof_step type nonrec lit = lit @@ -2185,14 +2184,8 @@ module Make (Plugin : PLUGIN) = struct mark_dirty_atom (Atom.neg atoms.(0)); (* need to remove from watchlists *) mark_dirty_atom (Atom.neg atoms.(1)); - (match self.on_gc with - | Some f -> - let lits = Clause.lits_a store c in - f self lits - | None -> ()); - Proof.del_clause - (Clause.proof_step store c) - (Clause.lits_iter store c) self.proof + Event.emit self.on_gc (Clause.lits_a store c); + Proof_trace.delete self.proof (Clause.proof_step store c) in let gc_arg = @@ -2281,9 +2274,7 @@ module Make (Plugin : PLUGIN) = struct let current_level = decision_level self in enqueue_bool self atom ~level:current_level Decision; Stat.incr self.n_decisions; - (match self.on_decision with - | Some f -> f self (Atom.lit self.store atom) - | None -> ()); + Event.emit self.on_decision (Atom.lit self.store atom); true ) in @@ -2291,13 +2282,13 @@ module Make (Plugin : PLUGIN) = struct (* do some amount of search, until the number of conflicts or clause learnt reaches the given parameters *) - let search (st : t) ~on_progress ~(max_conflicts : int) : unit = + let search (self : t) ~on_progress ~(max_conflicts : int) : unit = Log.debugf 3 (fun k -> k "(@[sat.search@ :max-conflicts %d@ :max-learnt %d@])" max_conflicts - !(st.max_clauses_learnt)); + !(self.max_clauses_learnt)); let n_conflicts = ref 0 in while true do - match propagate st with + match propagate self with | Some confl -> (* Conflict *) incr n_conflicts; @@ -2305,38 +2296,36 @@ module Make (Plugin : PLUGIN) = struct might 'forget' the initial conflict clause, and only add the analyzed backtrack clause. So in those case, we use add_clause to make sure the initial conflict clause is also added. *) - if Clause.attached st.store confl then - add_boolean_conflict st confl + if Clause.attached self.store confl then + add_boolean_conflict self confl else - add_clause_ ~pool:st.clauses_learnt st confl; - Stat.incr st.n_conflicts; - (match st.on_conflict with - | Some f -> f st confl - | None -> ()) + add_clause_ ~pool:self.clauses_learnt self confl; + Stat.incr self.n_conflicts; + Event.emit self.on_conflict confl | None -> (* No Conflict *) - assert (st.elt_head = AVec.size st.trail); - assert (st.elt_head = st.th_head); + assert (self.elt_head = AVec.size self.trail); + assert (self.elt_head = self.th_head); if max_conflicts > 0 && !n_conflicts >= max_conflicts then ( Log.debug 1 "(sat.restarting)"; - cancel_until st 0; - Stat.incr st.n_restarts; + cancel_until self 0; + Stat.incr self.n_restarts; raise_notrace Restart ); (* if decision_level() = 0 then simplify (); *) let do_gc = - !(st.max_clauses_learnt) > 0 - && cp_size_ st.clauses_learnt - AVec.size st.trail - > !(st.max_clauses_learnt) - || Vec.exists cp_needs_gc_ st.clause_pools + !(self.max_clauses_learnt) > 0 + && cp_size_ self.clauses_learnt - AVec.size self.trail + > !(self.max_clauses_learnt) + || Vec.exists cp_needs_gc_ self.clause_pools in if do_gc then ( - reduce_clause_db st; + reduce_clause_db self; on_progress () ); - let decided = pick_branch_lit ~full:true st in + let decided = pick_branch_lit ~full:true self in if not decided then raise_notrace E_sat done @@ -2401,9 +2390,7 @@ module Make (Plugin : PLUGIN) = struct k "(@[sat.theory-conflict-clause@ %a@])" (Clause.debug self.store) c); Stat.incr self.n_conflicts; - (match self.on_conflict with - | Some f -> f self c - | None -> ()); + Event.emit self.on_conflict c; Delayed_actions.add_clause_learnt self.delayed_actions c; perform_delayed_actions self; on_progress ()) @@ -2414,7 +2401,10 @@ module Make (Plugin : PLUGIN) = struct List.iter (fun l -> let atoms = Util.array_of_list_map (make_atom_ self) l in - let proof = Proof.emit_input_clause (Iter.of_list l) self.proof in + let proof = + Proof_trace.add_step self.proof + @@ Proof_rules.sat_input_clause (Iter.of_list l) + in let c = Clause.make_a self.store ~removable:false atoms proof in Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[%a@]@])" (Clause.debug self.store) @@ -2504,7 +2494,8 @@ module Make (Plugin : PLUGIN) = struct let proof = let lits = Iter.of_list !res |> Iter.map (Atom.lit self.store) in let hyps = Iter.of_list (Clause.proof_step self.store c :: !lvl0) in - Proof.emit_redundant_clause lits ~hyps self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_redundant_clause lits ~hyps in Clause.make_l self.store ~removable:false !res proof ) @@ -2539,7 +2530,8 @@ module Make (Plugin : PLUGIN) = struct assert (Atom.equal first @@ List.hd core); let proof = let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in - Proof.emit_unsat_core lits self.proof + Proof_trace.add_step self.proof + @@ Proof_rules.sat_unsat_core lits in Clause.make_l self.store ~removable:false [] proof) in @@ -2547,7 +2539,7 @@ module Make (Plugin : PLUGIN) = struct in let module M = struct type nonrec lit = lit - type nonrec proof = proof_step + type nonrec proof_step = proof_step type clause = Clause.t let unsat_conflict = unsat_conflict @@ -2615,11 +2607,17 @@ module Make (Plugin : PLUGIN) = struct add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr let add_input_clause self (c : lit list) = - let pr = Proof.emit_input_clause (Iter.of_list c) self.proof in + let pr = + Proof_trace.add_step self.proof + @@ Proof_rules.sat_input_clause (Iter.of_list c) + in add_clause self c pr let add_input_clause_a self c = - let pr = Proof.emit_input_clause (Iter.of_array c) self.proof in + let pr = + Proof_trace.add_step self.proof + @@ Proof_rules.sat_input_clause (Iter.of_array c) + in add_clause_a self c pr (* run [f()] with additional assumptions *) @@ -2693,12 +2691,9 @@ end) [@@inline] [@@specialise] module Make_pure_sat (Plugin : Solver_intf.PLUGIN_SAT) = Make (struct - type lit = Plugin.lit - type proof = Plugin.proof - type proof_step = Plugin.proof_step - module Lit = Plugin.Lit - module Proof = Plugin.Proof + module Proof_trace = Plugin.Proof_trace + module Proof_rules = Plugin.Proof_rules type t = unit diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli index 24be6a99..3a0858d0 100644 --- a/src/sat/Solver.mli +++ b/src/sat/Solver.mli @@ -3,18 +3,14 @@ module type S = Solver_intf.S module Make_pure_sat (Th : Solver_intf.PLUGIN_SAT) : S - with type lit = Th.lit - and module Lit = Th.Lit - and type proof = Th.proof - and type proof_step = Th.proof_step - and module Proof = Th.Proof + with module Lit = Th.Lit + and module Proof_trace = Th.Proof_trace + and module Proof_rules = Th.Proof_rules and type theory = unit module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : S - with type lit = Th.lit - and module Lit = Th.Lit - and type proof = Th.proof - and type proof_step = Th.proof_step - and module Proof = Th.Proof + with module Lit = Th.Lit + and module Proof_trace = Th.Proof_trace + and module Proof_rules = Th.Proof_rules and type theory = Th.t diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index f098011b..e38954a6 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -42,7 +42,7 @@ type 'form sat_state = (module SAT_STATE with type lit = 'form) module type UNSAT_STATE = sig type lit type clause - type proof + type proof_step val unsat_conflict : unit -> clause (** Returns the unsat clause found at the toplevel *) @@ -50,14 +50,14 @@ module type UNSAT_STATE = sig val unsat_assumptions : unit -> lit Iter.t (** Subset of assumptions responsible for "unsat" *) - val unsat_proof : unit -> proof + val unsat_proof : unit -> proof_step end -type ('lit, 'clause, 'proof) unsat_state = +type ('lit, 'clause, 'proof_step) unsat_state = (module UNSAT_STATE with type lit = 'lit and type clause = 'clause - and type proof = 'proof) + and type proof_step = 'proof_step) (** The type of values returned when the solver reaches an UNSAT state. *) type same_sign = bool @@ -65,7 +65,8 @@ type same_sign = bool [true] means the literal stayed the same, [false] that its sign was flipped. *) (** The type of reasons for propagations of a lit [f]. *) -type ('lit, 'proof) reason = Consequence of (unit -> 'lit list * 'proof) +type ('lit, 'proof_step) reason = + | Consequence of (unit -> 'lit list * 'proof_step) [@@unboxed] (** [Consequence (l, p)] means that the lits in [l] imply the propagated lit [f]. The proof should be a proof of the clause "[l] implies [f]". @@ -168,28 +169,21 @@ module type LIT = sig but one returns [false] and the other [true]. *) end -module type PROOF = Sidekick_core.SAT_PROOF +module type PROOF_RULES = Sidekick_sigs_proof_sat.S (** Signature for theories to be given to the CDCL(T) solver *) module type PLUGIN_CDCL_T = sig type t (** The plugin state itself *) - type lit + module Lit : LIT + module Proof_trace : Sidekick_sigs_proof_trace.S - module Lit : LIT with type t = lit - - type proof - (** Proof storage/recording *) - - type proof_step - (** Identifier for a clause precendently added/proved *) - - module Proof : - PROOF - with type t = proof - and type lit = lit - and type proof_step = proof_step + module Proof_rules : + PROOF_RULES + with type lit = Lit.t + and type rule = Proof_trace.A.rule + and type step_id = Proof_trace.A.step_id val push_level : t -> unit (** Create a new backtrack level *) @@ -197,12 +191,14 @@ module type PLUGIN_CDCL_T = sig val pop_levels : t -> int -> unit (** Pop [n] levels of the theory *) - val partial_check : t -> (lit, proof, proof_step) acts -> unit + val partial_check : + t -> (Lit.t, Proof_trace.t, Proof_trace.A.step_id) acts -> unit (** Assume the lits in the slice, possibly using the [slice] to push new lits to be propagated or to raising a conflict or to add new lemmas. *) - val final_check : t -> (lit, proof, proof_step) acts -> unit + val final_check : + t -> (Lit.t, Proof_trace.t, Proof_trace.A.step_id) acts -> unit (** Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; @@ -211,18 +207,14 @@ end (** Signature for pure SAT solvers *) module type PLUGIN_SAT = sig - type lit + module Lit : LIT + module Proof_trace : Sidekick_sigs_proof_trace.S - module Lit : LIT with type t = lit - - type proof - type proof_step - - module Proof : - PROOF - with type t = proof - and type lit = lit - and type proof_step = proof_step + module Proof_rules : + PROOF_RULES + with type lit = Lit.t + and type rule = Proof_trace.A.rule + and type step_id = Proof_trace.A.step_id end exception Resource_exhausted @@ -235,19 +227,20 @@ module type S = sig These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT. *) - type lit - (** literals *) + module Lit : LIT + module Proof_trace : Sidekick_sigs_proof_trace.S - module Lit : LIT with type t = lit + type lit = Lit.t + (** literals *) type clause type theory + type proof_rule = Proof_trace.A.rule + type proof_step = Proof_trace.A.step_id - type proof + type proof_trace = Proof_trace.t (** A representation of a full proof *) - type proof_step - type solver (** The main solver type. *) @@ -279,8 +272,12 @@ module type S = sig (** List of atoms of a clause *) end - (** A module to manipulate proofs. *) - module Proof : PROOF with type lit = lit and type t = proof + (** Proof rules for SAT solving *) + module Proof_rules : + PROOF_RULES + with type lit = lit + and type rule = proof_rule + and type step_id = proof_step (** {2 Main Solver Type} *) @@ -288,13 +285,9 @@ module type S = sig (** Main solver type, containing all state for solving. *) val create : - ?on_conflict:(t -> Clause.t -> unit) -> - ?on_decision:(t -> lit -> unit) -> - ?on_learnt:(t -> Clause.t -> unit) -> - ?on_gc:(t -> lit array -> unit) -> ?stat:Stat.t -> ?size:[ `Tiny | `Small | `Big ] -> - proof:Proof.t -> + proof:proof_trace -> theory -> t (** Create new solver @@ -312,9 +305,14 @@ module type S = sig val stat : t -> Stat.t (** Statistics *) - val proof : t -> proof + val proof : t -> proof_trace (** Access the inner proof *) + val on_conflict : t -> Clause.t Event.t + val on_decision : t -> lit Event.t + val on_learnt : t -> Clause.t Event.t + val on_gc : t -> lit array Event.t + (** {2 Types} *) (** Result type for the solver *) diff --git a/src/sat/dune b/src/sat/dune index 89966075..505da013 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -1,8 +1,6 @@ (library (name sidekick_sat) (public_name sidekick.sat) - (libraries iter sidekick.util sidekick.core) + (libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace) (synopsis "Pure OCaml SAT solver implementation for sidekick") - (flags :standard -warn-error -a+8 -open Sidekick_util) - (ocamlopt_flags :standard -O3 -bin-annot -unbox-closures - -unbox-closures-factor 20)) + (flags :standard -open Sidekick_util)) diff --git a/src/sigs/cc/sidekick_sigs_cc.ml b/src/sigs/cc/sidekick_sigs_cc.ml index 6338b365..5162ba26 100644 --- a/src/sigs/cc/sidekick_sigs_cc.ml +++ b/src/sigs/cc/sidekick_sigs_cc.ml @@ -12,15 +12,15 @@ module type PROOF_TRACE = Sidekick_sigs_proof_trace.S it detects that they are true or false; it must also be able to create conflicts when the set of (dis)equalities is inconsistent *) -module type ACTIONS = sig +module type DYN_ACTIONS = sig type term type lit - type proof - type proof_step + type proof_trace + type step_id - val proof : unit -> proof + val proof_trace : unit -> proof_trace - val raise_conflict : lit list -> proof_step -> 'a + val raise_conflict : lit list -> step_id -> 'a (** [raise_conflict c pr] declares that [c] is a tautology of the theory of congruence. This does not return (it should raise an exception). @@ -37,7 +37,7 @@ module type ACTIONS = sig This does not return. It should raise an exception. *) - val propagate : lit -> reason:(unit -> lit list * proof_step) -> unit + val propagate : lit -> reason:(unit -> lit list * step_id) -> unit (** [propagate lit ~reason pr] declares that [reason() => lit] is a tautology. @@ -55,40 +55,22 @@ module type ARG = sig module Proof_trace : PROOF_TRACE (** Arguments for the congruence closure *) - module CC : sig - val view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) View.t - (** View the term through the lens of the congruence closure *) + val view_as_cc : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) View.t + (** View the term through the lens of the congruence closure *) - val mk_lit_eq : ?sign:bool -> T.Term.store -> T.Term.t -> T.Term.t -> Lit.t - (** [mk_lit_eq store t u] makes the literal [t=u] *) + val mk_lit_eq : ?sign:bool -> T.Term.store -> T.Term.t -> T.Term.t -> Lit.t + (** [mk_lit_eq store t u] makes the literal [t=u] *) - module Proof_rules : - Sidekick_sigs_proof_core.S - with type term = T.Term.t - and type lit = Lit.t - and type step_id = Proof_trace.step_id - and type rule = Proof_trace.rule - end + module Rule_core : + Sidekick_sigs_proof_core.S + with type term = T.Term.t + and type lit = Lit.t + and type step_id = Proof_trace.A.step_id + and type rule = Proof_trace.A.rule end -(** Main congruence closure signature. - - The congruence closure handles the theory QF_UF (uninterpreted - function symbols). - It is also responsible for {i theory combination}, and provides - a general framework for equality reasoning that other - theories piggyback on. - - For example, the theory of datatypes relies on the congruence closure - to do most of the work, and "only" adds injectivity/disjointness/acyclicity - lemmas when needed. - - Similarly, a theory of arrays would hook into the congruence closure and - assert (dis)equalities as needed. -*) -module type S = sig - (** first, some aliases. *) - +(** Collection of input types, and types defined by the congruence closure *) +module type ARGS_CLASSES_EXPL_EVENT = sig module T : TERM module Lit : LIT with module T = T module Proof_trace : PROOF_TRACE @@ -98,22 +80,17 @@ module type S = sig type value = term type fun_ = T.Fun.t type lit = Lit.t - type proof = Proof_trace.t - type proof_step = Proof_trace.step_id + type proof_trace = Proof_trace.t + type step_id = Proof_trace.A.step_id type actions = - (module ACTIONS + (module DYN_ACTIONS with type term = T.Term.t and type lit = Lit.t - and type proof = proof - and type proof_step = proof_step) + and type proof_trace = proof_trace + and type step_id = step_id) (** Actions available to the congruence closure *) - type t - (** The congruence closure object. - It contains a fair amount of state and is mutable - and backtrackable. *) - (** Equivalence classes. An equivalence class is a set of terms that are currently equal @@ -122,7 +99,7 @@ module type S = sig distinguished and is called the "representative". All information pertaining to the whole equivalence class is stored - in this representative's node. + in this representative's Class.t. When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. @@ -140,6 +117,8 @@ module type S = sig A value of type [t] points to a particular term, but see {!find} to get the representative of the class. *) + include Sidekick_sigs.PRINT with type t := t + val term : t -> term (** Term contained in this equivalence class. If [is_root n], then [term n] is the class' representative term. *) @@ -150,14 +129,10 @@ module type S = sig which checks for equality of representatives. *) val hash : t -> int - (** An opaque hash of this node. *) - - val pp : t Fmt.printer - (** Unspecified printing of the node, for example its term, - a unique ID, etc. *) + (** An opaque hash of this Class.t. *) val is_root : t -> bool - (** Is the node a root (ie the representative of its class)? + (** Is the Class.t a root (ie the representative of its class)? See {!find} to get the root. *) val iter_class : t -> t Iter.t @@ -168,6 +143,10 @@ module type S = sig (** Traverse the parents of the class. Precondition: [is_root n] (see {!find} below) *) + (* FIXME: + [@@alert refactor "this should be replaced with a Per_class concept"] + *) + type bitfield (** A field in the bitfield of this node. This should only be allocated when a theory is initialized. @@ -182,11 +161,11 @@ module type S = sig (** Explanations Explanations are specialized proofs, created by the congruence closure - when asked to justify why twp terms are equal. *) + when asked to justify why two terms are equal. *) module Expl : sig type t - val pp : t Fmt.printer + include Sidekick_sigs.PRINT with type t := t val mk_merge : Class.t -> Class.t -> t (** Explanation: the nodes were explicitly merged *) @@ -200,12 +179,12 @@ module type S = sig or [t] and [false] because of literal [¬t] *) val mk_same_value : Class.t -> Class.t -> t + (** The two classes have the same value during model construction *) val mk_list : t list -> t (** Conjunction of explanations *) - val mk_theory : - term -> term -> (term * term * t list) list -> proof_step -> t + val mk_theory : term -> term -> (term * term * t list) list -> step_id -> t (** [mk_theory t u expl_sets pr] builds a theory explanation for why [|- t=u]. It depends on sub-explanations [expl_sets] which are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are @@ -241,28 +220,97 @@ module type S = sig type t = { lits: lit list; same_value: (Class.t * Class.t) list; - pr: proof -> proof_step; + pr: proof_trace -> step_id; } + include Sidekick_sigs.PRINT with type t := t + val is_semantic : t -> bool (** [is_semantic expl] is [true] if there's at least one pair in [expl.same_value]. *) - - val pp : t Fmt.printer end type node = Class.t (** A node of the congruence closure *) type repr = Class.t - (** Node that is currently a representative *) + (** Node that is currently a representative. *) type explanation = Expl.t +end + +(* TODO: can we have that meaningfully? the type of Class.t would depend on + the implementation, so it can't be pre-defined, but nor can it be accessed from + shortcuts from the inside. That means one cannot point to classes from outside + the opened module. + + Potential solution: + - make Expl polymorphic and lift it to toplevel, like View + - do not expose Class, only Term-based API + (** The type for a congruence closure, as a first-class module *) + module type DYN = sig + include ARGS_CLASSES_EXPL_EVENT + include Sidekick_sigs.DYN_BACKTRACKABLE + + val term_store : unit -> term_store + val proof : unit -> proof_trace + val find : node -> repr + val add_term : term -> node + val mem_term : term -> bool + val allocate_bitfield : descr:string -> Class.bitfield + val get_bitfield : Class.bitfield -> Class.t -> bool + val set_bitfield : Class.bitfield -> bool -> Class.t -> unit + val on_event : unit -> event Event.t + val set_as_lit : Class.t -> lit -> unit + val find_t : term -> repr + val add_iter : term Iter.t -> unit + val all_classes : repr Iter.t + val assert_lit : lit -> unit + val assert_lits : lit Iter.t -> unit + val explain_eq : Class.t -> Class.t -> Resolved_expl.t + val raise_conflict_from_expl : actions -> Expl.t -> 'a + val n_true : unit -> Class.t + val n_false : unit -> Class.t + val n_bool : bool -> Class.t + val merge : Class.t -> Class.t -> Expl.t -> unit + val merge_t : term -> term -> Expl.t -> unit + val set_model_value : term -> value -> unit + val with_model_mode : (unit -> 'a) -> 'a + val get_model_for_each_class : (repr * Class.t Iter.t * value) Iter.t + val check : actions -> unit + val push_level : unit -> unit + val pop_levels : int -> unit + val get_model : Class.t Iter.t Iter.t + end +*) + +(** Main congruence closure signature. + + The congruence closure handles the theory QF_UF (uninterpreted + function symbols). + It is also responsible for {i theory combination}, and provides + a general framework for equality reasoning that other + theories piggyback on. + + For example, the theory of datatypes relies on the congruence closure + to do most of the work, and "only" adds injectivity/disjointness/acyclicity + lemmas when needed. + + Similarly, a theory of arrays would hook into the congruence closure and + assert (dis)equalities as needed. +*) +module type S = sig + include ARGS_CLASSES_EXPL_EVENT + + type t + (** The congruence closure object. + It contains a fair amount of state and is mutable + and backtrackable. *) (** {3 Accessors} *) val term_store : t -> term_store - val proof : t -> proof + val proof : t -> proof_trace val find : t -> node -> repr (** Current representative *) @@ -274,66 +322,12 @@ module type S = sig val mem_term : t -> term -> bool (** Returns [true] if the term is explicitly present in the congruence closure *) - (** {3 Events} - - Events triggered by the congruence closure, to which - other plugins can subscribe. *) - - type ev_on_pre_merge = t -> actions -> Class.t -> Class.t -> Expl.t -> unit - (** [ev_on_pre_merge cc acts n1 n2 expl] is called right before [n1] - and [n2] are merged with explanation [expl]. *) - - type ev_on_post_merge = t -> actions -> Class.t -> Class.t -> unit - (** [ev_on_post_merge cc acts n1 n2] is called right after [n1] - and [n2] were merged. [find cc n1] and [find cc n2] will return - the same node. *) - - type ev_on_new_term = t -> Class.t -> term -> unit - (** [ev_on_new_term cc n t] is called whenever a new term [t] - is added to the congruence closure. Its node is [n]. *) - - type ev_on_conflict = t -> th:bool -> lit list -> unit - (** [ev_on_conflict acts ~th c] is called when the congruence - closure triggers a conflict by asserting the tautology [c]. - - @param th true if the explanation for this conflict involves - at least one "theory" explanation; i.e. some of the equations - participating in the conflict are purely syntactic theories - like injectivity of constructors. *) - - type ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit - (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] - is a propagated lemma. See {!CC_ACTIONS.propagate}. *) - - type ev_on_is_subterm = Class.t -> term -> unit - (** [ev_on_is_subterm n t] is called when [n] is a subterm of - another node for the first time. [t] is the term corresponding to - the node [n]. This can be useful for theory combination. *) - - val create : - ?stat:Stat.t -> - ?on_pre_merge:ev_on_pre_merge list -> - ?on_post_merge:ev_on_post_merge list -> - ?on_new_term:ev_on_new_term list -> - ?on_conflict:ev_on_conflict list -> - ?on_propagate:ev_on_propagate list -> - ?on_is_subterm:ev_on_is_subterm list -> - ?size:[ `Small | `Big ] -> - term_store -> - proof -> - t - (** Create a new congruence closure. - - @param term_store used to be able to create new terms. All terms - interacting with this congruence closure must belong in this term state - as well. *) - - val allocate_bitfield : descr:string -> t -> Class.bitfield + val allocate_bitfield : t -> descr:string -> Class.bitfield (** Allocate a new node field (see {!Class.bitfield}). This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using {!set_bitfield} - for each node individually. + for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class"). @@ -349,24 +343,47 @@ module type S = sig (** Set the bitfield for the node. This will be backtracked. See {!Class.bitfield}. *) - (* TODO: remove? this is managed by the solver anyway? *) - val on_pre_merge : t -> ev_on_pre_merge -> unit - (** Add a function to be called when two classes are merged *) + (** {3 Events} - val on_post_merge : t -> ev_on_post_merge -> unit - (** Add a function to be called when two classes are merged *) + Events triggered by the congruence closure, to which + other plugins can subscribe. *) - val on_new_term : t -> ev_on_new_term -> unit - (** Add a function to be called when a new node is created *) + (** Events emitted by the congruence closure when something changes. *) + val on_pre_merge : t -> (t * actions * Class.t * Class.t * Expl.t) Event.t + (** [Ev_on_pre_merge acts n1 n2 expl] is emitted right before [n1] + and [n2] are merged with explanation [expl]. *) - val on_conflict : t -> ev_on_conflict -> unit - (** Called when the congruence closure finds a conflict *) + val on_post_merge : t -> (t * actions * Class.t * Class.t) Event.t + (** [ev_on_post_merge acts n1 n2] is emitted right after [n1] + and [n2] were merged. [find cc n1] and [find cc n2] will return + the same Class.t. *) - val on_propagate : t -> ev_on_propagate -> unit - (** Called when the congruence closure propagates a literal *) + val on_new_term : t -> (t * Class.t * term) Event.t + (** [ev_on_new_term n t] is emitted whenever a new term [t] + is added to the congruence closure. Its Class.t is [n]. *) - val on_is_subterm : t -> ev_on_is_subterm -> unit - (** Called on terms that are subterms of function symbols *) + type ev_on_conflict = { cc: t; th: bool; c: lit list } + (** Event emitted when a conflict occurs in the CC. + + [th] is true if the explanation for this conflict involves + at least one "theory" explanation; i.e. some of the equations + participating in the conflict are purely syntactic theories + like injectivity of constructors. *) + + val on_conflict : t -> ev_on_conflict Event.t + (** [ev_on_conflict {th; c}] is emitted when the congruence + closure triggers a conflict by asserting the tautology [c]. *) + + val on_propagate : t -> (t * lit * (unit -> lit list * step_id)) Event.t + (** [ev_on_propagate lit reason] is emitted whenever [reason() => lit] + is a propagated lemma. See {!CC_ACTIONS.propagate}. *) + + val on_is_subterm : t -> (t * Class.t * term) Event.t + (** [ev_on_is_subterm n t] is emitted when [n] is a subterm of + another Class.t for the first time. [t] is the term corresponding to + the Class.t [n]. This can be useful for theory combination. *) + + (** {3 Misc} *) val set_as_lit : t -> Class.t -> lit -> unit (** map the given node to a literal. *) @@ -440,17 +457,14 @@ module type S = sig val get_model : t -> Class.t Iter.t Iter.t (** get all the equivalence classes so they can be merged in the model *) - - (**/**) - - module Debug_ : sig - val pp : t Fmt.printer - (** Print the whole CC *) - end - - (**/**) end +(* TODO + module type DYN_BUILDER = sig + include ARGS_CLASSES_EXPL_EVENT + end +*) + (* TODO: full EGG, also have a function to update the value when the subterms (produced in [of_term]) are updated *) @@ -460,7 +474,7 @@ end The state of a class is the monoidal combination of the state for each term in the class (for example, the set of terms in the class whose head symbol is a datatype constructor). *) -module type MONOID_ARG = sig +module type MONOID_PLUGIN_ARG = sig module CC : S type t @@ -511,38 +525,32 @@ end aggregate some theory-specific state over all terms, with the information of what terms are already known to be equal potentially saving work for the theory. *) -module type PLUGIN = sig - module CC : S - module M : MONOID_ARG with module CC = CC +module type DYN_MONOID_PLUGIN = sig + module M : MONOID_PLUGIN_ARG + include Sidekick_sigs.DYN_BACKTRACKABLE - val push_level : unit -> unit - (** Push backtracking point *) + val pp : unit Fmt.printer - val pop_levels : int -> unit - (** Pop [n] backtracking points *) + val mem : M.CC.Class.t -> bool + (** Does the CC Class.t have a monoid value? *) - val n_levels : unit -> int + val get : M.CC.Class.t -> M.t option + (** Get monoid value for this CC Class.t, if any *) - val mem : CC.Class.t -> bool - (** Does the CC node have a monoid value? *) - - val get : CC.Class.t -> M.t option - (** Get monoid value for this CC node, if any *) - - val iter_all : (CC.repr * M.t) Iter.t + val iter_all : (M.CC.repr * M.t) Iter.t end (** Builder for a plugin. The builder takes a congruence closure, and instantiate the plugin on it. *) -module type PLUGIN_BUILDER = sig - module M : MONOID_ARG +module type MONOID_PLUGIN_BUILDER = sig + module M : MONOID_PLUGIN_ARG - module type PL = PLUGIN with module CC = M.CC and module M = M + module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M - type plugin = (module PL) + type t = (module DYN_PL_FOR_M) - val create_and_setup : ?size:int -> M.CC.t -> plugin + val create_and_setup : ?size:int -> M.CC.t -> t (** Create a new monoid state *) end diff --git a/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml b/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml index 5e81fafc..c9b20417 100644 --- a/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml +++ b/src/sigs/proof-sat/sidekick_sigs_proof_sat.ml @@ -1,4 +1,5 @@ -(** Signature for SAT-solver proof emission. *) +(** Proof rules for SAT Solver reasoning *) + module type S = sig type rule (** The stored proof (possibly nil, possibly on disk, possibly in memory) *) @@ -16,9 +17,6 @@ module type S = sig (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt [hyps]. *) - (* FIXME: goes in proof trace itself? not exactly a rule… - val sat_unsat_core : lit Iter.t -> rule - (** Produce a proof of the empty clause given this subset of the assumptions. - FIXME: probably needs the list of proof_step that disprove the lits? *) - *) + val sat_unsat_core : lit Iter.t -> rule + (** TODO: is this relevant here? *) end diff --git a/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml b/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml index 012957c3..83ee8d3f 100644 --- a/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml +++ b/src/sigs/proof-trace/sidekick_sigs_proof_trace.ml @@ -3,16 +3,21 @@ open Sidekick_util -module type S = sig +module type ARG = sig type rule type step_id (** Identifier for a tracing step (like a unique ID for a clause previously added/proved) *) - module Step_vec : Vec_sig.BASE with type t = step_id + module Step_vec : Vec_sig.BASE with type elt = step_id (** A vector indexed by steps. *) +end +module type S = sig + module A : ARG + + type t (** The proof trace itself. A proof trace is a log of all deductive steps taken by the solver, @@ -21,30 +26,17 @@ module type S = sig Each step in the proof trace should be a {b valid lemma} (of its theory) or a {b valid consequence} of previous steps. *) - module type PROOF_TRACE = sig - val enabled : unit -> bool - (** Is proof tracing enabled? *) - val add_step : rule -> step_id - (** Create a new step in the trace. *) + val enabled : t -> bool + (** Is proof tracing enabled? *) - val add_unsat : step_id -> unit - (** Signal "unsat" result at the given proof *) + val add_step : t -> A.rule -> A.step_id + (** Create a new step in the trace. *) - val delete : step_id -> unit - (** Forget a step that won't be used in the rest of the trace. - Only useful for performance/memory considerations. *) - end + val add_unsat : t -> A.step_id -> unit + (** Signal "unsat" result at the given proof *) - type t = (module PROOF_TRACE) -end - -module Utils_ (Trace : S) = struct - let[@inline] enabled ((module Tr) : Trace.t) : bool = Tr.enabled () - - let[@inline] add_step ((module Tr) : Trace.t) rule : Trace.step_id = - Tr.add_step rule - - let[@inline] add_unsat ((module Tr) : Trace.t) s : unit = Tr.add_unsat s - let[@inline] delete ((module Tr) : Trace.t) s : unit = Tr.delete s + val delete : t -> A.step_id -> unit + (** Forget a step that won't be used in the rest of the trace. + Only useful for performance/memory considerations. *) end diff --git a/src/sigs/smt/Sidekick_sigs_smt.ml b/src/sigs/smt/Sidekick_sigs_smt.ml new file mode 100644 index 00000000..be68256d --- /dev/null +++ b/src/sigs/smt/Sidekick_sigs_smt.ml @@ -0,0 +1,597 @@ +(** Signature for the main SMT solver types. + + Theories and concrete solvers rely on an environment that defines + several important types: + + - sorts + - terms (to represent logic expressions and formulas) + - a congruence closure instance + - a bridge to some SAT solver + + In this module we collect signatures defined elsewhere and define + the module types for the main SMT solver. +*) + +module type TERM = Sidekick_sigs_term.S +module type LIT = Sidekick_sigs_lit.S +module type PROOF_TRACE = Sidekick_sigs_proof_trace.S + +module type SAT_PROOF_RULES = Sidekick_sigs_proof_sat.S +(** Signature for SAT-solver proof emission. *) + +module type PROOF_CORE = Sidekick_sigs_proof_core.S +(** Proofs of unsatisfiability. *) + +(** Registry to extract values *) +module type REGISTRY = sig + type t + type 'a key + + val create_key : unit -> 'a key + (** Call this statically, typically at program initialization, for + each distinct key. *) + + val create : unit -> t + val get : t -> 'a key -> 'a option + val set : t -> 'a key -> 'a -> unit +end + +(** A view of the solver from a theory's point of view. + + Theories should interact with the solver via this module, to assert + new lemmas, propagate literals, access the congruence closure, etc. *) +module type SOLVER_INTERNAL = sig + module T : TERM + module Lit : LIT with module T = T + module Proof_trace : PROOF_TRACE + + type ty = T.Ty.t + type term = T.Term.t + type value = T.Term.t + type lit = Lit.t + type term_store = T.Term.store + type ty_store = T.Ty.store + type clause_pool + type proof_trace = Proof_trace.t + type step_id = Proof_trace.A.step_id + + type t + (** {3 Main type for a solver} *) + + type solver = t + + val tst : t -> term_store + val ty_st : t -> ty_store + val stats : t -> Stat.t + + val proof : t -> proof_trace + (** Access the proof object *) + + (** {3 Registry} *) + + module Registry : REGISTRY + + val registry : t -> Registry.t + (** A solver contains a registry so that theories can share data *) + + (** {3 Exported Proof rules} *) + + module P_core_rules : + Sidekick_sigs_proof_core.S + with type rule = Proof_trace.A.rule + and type step_id = Proof_trace.A.step_id + and type term = term + and type lit = lit + + (** {3 Actions for the theories} *) + + type theory_actions + (** Handle that the theories can use to perform actions. *) + + (** {3 Congruence Closure} *) + + (** Congruence closure instance *) + module CC : + Sidekick_sigs_cc.S + with module T = T + and module Lit = Lit + and module Proof_trace = Proof_trace + + val cc : t -> CC.t + (** Congruence closure for this solver *) + + (** {3 Simplifiers} *) + + (* TODO: move into its own library *) + + (** Simplify terms *) + module Simplify : sig + type t + + val tst : t -> term_store + val ty_st : t -> ty_store + + val clear : t -> unit + (** Reset internal cache, etc. *) + + val proof : t -> proof_trace + (** Access proof *) + + type hook = t -> term -> (term * step_id Iter.t) option + (** Given a term, try to simplify it. Return [None] if it didn't change. + + A simple example could be a hook that takes a term [t], + and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, + returns [Some (const (x+y))], and [None] otherwise. + + The simplifier will take care of simplifying the resulting term further, + caching (so that work is not duplicated in subterms), etc. + *) + + val normalize : t -> term -> (term * step_id) option + (** Normalize a term using all the hooks. This performs + a fixpoint, i.e. it only stops when no hook applies anywhere inside + the term. *) + + val normalize_t : t -> term -> term * step_id option + (** Normalize a term using all the hooks, along with a proof that the + simplification is correct. + returns [t, ø] if no simplification occurred. *) + end + + type simplify_hook = Simplify.hook + + val add_simplifier : t -> Simplify.hook -> unit + (** Add a simplifier hook for preprocessing. *) + + val simplify_t : t -> term -> (term * step_id) option + (** Simplify input term, returns [Some u] if some + simplification occurred. *) + + val simp_t : t -> term -> term * step_id option + (** [simp_t si t] returns [u] even if no simplification occurred + (in which case [t == u] syntactically). + It emits [|- t=u]. + (see {!simplifier}) *) + + (** {3 Preprocessors} + These preprocessors turn mixed, raw literals (possibly simplified) into + literals suitable for reasoning. + Typically some clauses are also added to the solver. *) + + (* TODO: move into its own sig + library *) + module type PREPROCESS_ACTS = sig + val proof : proof_trace + + val mk_lit : ?sign:bool -> term -> lit + (** [mk_lit t] creates a new literal for a boolean term [t]. *) + + val add_clause : lit list -> step_id -> unit + (** pushes a new clause into the SAT solver. *) + + val add_lit : ?default_pol:bool -> lit -> unit + (** Ensure the literal will be decided/handled by the SAT solver. *) + end + + type preprocess_actions = (module PREPROCESS_ACTS) + (** Actions available to the preprocessor *) + + type preprocess_hook = t -> preprocess_actions -> term -> unit + (** Given a term, preprocess it. + + The idea is to add literals and clauses to help define the meaning of + the term, if needed. For example for boolean formulas, clauses + for their Tseitin encoding can be added, with the formula acting + as its own proxy symbol. + + @param preprocess_actions actions available during preprocessing. + *) + + val on_preprocess : t -> preprocess_hook -> unit + (** Add a hook that will be called when terms are preprocessed *) + + (** {3 hooks for the theory} *) + + val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a + (** Give a conflict clause to the solver *) + + val push_decision : t -> theory_actions -> lit -> unit + (** Ask the SAT solver to decide the given literal in an extension of the + current trail. This is useful for theory combination. + If the SAT solver backtracks, this (potential) decision is removed + and forgotten. *) + + val propagate : + t -> theory_actions -> lit -> reason:(unit -> lit list * step_id) -> unit + (** Propagate a boolean using a unit clause. + [expl => lit] must be a theory lemma, that is, a T-tautology *) + + val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> unit + (** Propagate a boolean using a unit clause. + [expl => lit] must be a theory lemma, that is, a T-tautology *) + + val add_clause_temp : t -> theory_actions -> lit list -> step_id -> unit + (** Add local clause to the SAT solver. This clause will be + removed when the solver backtracks. *) + + val add_clause_permanent : t -> theory_actions -> lit list -> step_id -> unit + (** Add toplevel clause to the SAT solver. This clause will + not be backtracked. *) + + val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit + (** Create a literal. This automatically preprocesses the term. *) + + val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit + (** Add the given literal to the SAT solver, so it gets assigned + a boolean value. + @param default_pol default polarity for the corresponding atom *) + + val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit + (** Add the given (signed) bool term to the SAT solver, so it gets assigned + a boolean value *) + + val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'a + (** Raise a conflict with the given congruence closure explanation. + it must be a theory tautology that [expl ==> absurd]. + To be used in theories. *) + + val cc_find : t -> CC.Class.t -> CC.Class.t + (** Find representative of the node *) + + val cc_are_equal : t -> term -> term -> bool + (** Are these two terms equal in the congruence closure? *) + + val cc_merge : + t -> theory_actions -> CC.Class.t -> CC.Class.t -> CC.Expl.t -> unit + (** Merge these two nodes in the congruence closure, given this explanation. + It must be a theory tautology that [expl ==> n1 = n2]. + To be used in theories. *) + + val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unit + (** Merge these two terms in the congruence closure, given this explanation. + See {!cc_merge} *) + + val cc_add_term : t -> term -> CC.Class.t + (** Add/retrieve congruence closure node for this term. + To be used in theories *) + + val cc_mem_term : t -> term -> bool + (** Return [true] if the term is explicitly in the congruence closure. + To be used in theories *) + + val on_cc_pre_merge : + t -> + (CC.t * CC.actions * CC.Class.t * CC.Class.t * CC.Expl.t -> unit) -> + unit + (** Callback for when two classes containing data for this key are merged (called before) *) + + val on_cc_post_merge : + t -> (CC.t * CC.actions * CC.Class.t * CC.Class.t -> unit) -> unit + (** Callback for when two classes containing data for this key are merged (called after)*) + + val on_cc_new_term : t -> (CC.t * CC.Class.t * term -> unit) -> unit + (** Callback to add data on terms when they are added to the congruence + closure *) + + val on_cc_is_subterm : t -> (CC.t * CC.Class.t * term -> unit) -> unit + (** Callback for when a term is a subterm of another term in the + congruence closure *) + + val on_cc_conflict : t -> (CC.ev_on_conflict -> unit) -> unit + (** Callback called on every CC conflict *) + + val on_cc_propagate : + t -> (CC.t * lit * (unit -> lit list * step_id) -> unit) -> unit + (** Callback called on every CC propagation *) + + val on_partial_check : + t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit + (** Register callbacked to be called with the slice of literals + newly added on the trail. + + This is called very often and should be efficient. It doesn't have + to be complete, only correct. It's given only the slice of + the trail consisting in new literals. *) + + val on_final_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit + (** Register callback to be called during the final check. + + Must be complete (i.e. must raise a conflict if the set of literals is + not satisfiable) and can be expensive. The function + is given the whole trail. + *) + + val on_th_combination : + t -> (t -> theory_actions -> (term * value) Iter.t) -> unit + (** Add a hook called during theory combination. + The hook must return an iterator of pairs [(t, v)] + which mean that term [t] has value [v] in the model. + + Terms with the same value (according to {!Term.equal}) will be + merged in the CC; if two terms with different values are merged, + we get a semantic conflict and must pick another model. *) + + val declare_pb_is_incomplete : t -> unit + (** Declare that, in some theory, the problem is outside the logic fragment + that is decidable (e.g. if we meet proper NIA formulas). + The solver will not reply "SAT" from now on. *) + + (** {3 Model production} *) + + type model_ask_hook = + recurse:(t -> CC.Class.t -> term) -> t -> CC.Class.t -> term option + (** A model-production hook to query values from a theory. + + It takes the solver, a class, and returns + a term for this class. For example, an arithmetic theory + might detect that a class contains a numeric constant, and return + this constant as a model value. + + If no hook assigns a value to a class, a fake value is created for it. + *) + + type model_completion_hook = t -> add:(term -> term -> unit) -> unit + (** A model production hook, for the theory to add values. + The hook is given a [add] function to add bindings to the model. *) + + val on_model : + ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> unit + (** Add model production/completion hooks. *) +end + +(** User facing view of the solver. + + This is the solver a user of sidekick can see, after instantiating + everything. The user can add some theories, clauses, etc. and asks + the solver to check satisfiability. + + Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *) +module type SOLVER = sig + module T : TERM + module Lit : LIT with module T = T + module Proof_trace : PROOF_TRACE + + (** Internal solver, available to theories. *) + module Solver_internal : + SOLVER_INTERNAL + with module T = T + and module Lit = Lit + and module Proof_trace = Proof_trace + + type t + (** The solver's state. *) + + type solver = t + type term = T.Term.t + type ty = T.Ty.t + type lit = Lit.t + type proof_trace = Proof_trace.t + type step_id = Proof_trace.A.step_id + + (** {3 Value registry} *) + + module Registry : REGISTRY + + val registry : t -> Registry.t + (** A solver contains a registry so that theories can share data *) + + (** {3 A theory} + + Theories are abstracted over the concrete implementation of the solver, + so they can work with any implementation. + + Typically a theory should be a functor taking an argument containing + a [SOLVER_INTERNAL] or even a full [SOLVER], + and some additional views on terms, literals, etc. + that are specific to the theory (e.g. to map terms to linear + expressions). + The theory can then be instantiated on any kind of solver for any + term representation that also satisfies the additional theory-specific + requirements. Instantiated theories (ie values of type {!SOLVER.theory}) + can be added to the solver. + *) + module type THEORY = sig + type t + (** The theory's state *) + + val name : string + (** Name of the theory (ideally, unique and short) *) + + val create_and_setup : Solver_internal.t -> t + (** Instantiate the theory's state for the given (internal) solver, + register callbacks, create keys, etc. + + Called once for every solver this theory is added to. *) + + val push_level : t -> unit + (** Push backtracking level. When the corresponding pop is called, + the theory's state should be restored to a state {b equivalent} + to what it was just before [push_level]. + + it does not have to be exactly the same state, it just needs to + be equivalent. *) + + val pop_levels : t -> int -> unit + (** [pop_levels theory n] pops [n] backtracking levels, + restoring [theory] to its state before calling [push_level] n times. *) + end + + type theory = (module THEORY) + (** A theory that can be used for this particular solver. *) + + type 'a theory_p = (module THEORY with type t = 'a) + (** A theory that can be used for this particular solver, with state + of type ['a]. *) + + val mk_theory : + name:string -> + create_and_setup:(Solver_internal.t -> 'th) -> + ?push_level:('th -> unit) -> + ?pop_levels:('th -> int -> unit) -> + unit -> + theory + (** Helper to create a theory. *) + + (** Models + + A model can be produced when the solver is found to be in a + satisfiable state after a call to {!solve}. *) + module Model : sig + type t + + val empty : t + val mem : t -> term -> bool + val find : t -> term -> term option + val eval : t -> term -> term option + val pp : t Fmt.printer + end + + (* TODO *) + module Unknown : sig + type t + + val pp : t CCFormat.printer + + (* + type unknown = + | U_timeout + | U_incomplete + *) + end + + (** {3 Main API} *) + + val stats : t -> Stat.t + val tst : t -> T.Term.store + val ty_st : t -> T.Ty.store + val proof : t -> proof_trace + + val create : + ?stat:Stat.t -> + ?size:[ `Big | `Tiny | `Small ] -> + (* TODO? ?config:Config.t -> *) + proof:proof_trace -> + theories:theory list -> + T.Term.store -> + T.Ty.store -> + unit -> + t + (** Create a new solver. + + It needs a term state and a type state to manipulate terms and types. + All terms and types interacting with this solver will need to come + from these exact states. + + @param store_proof if true, proofs from the SAT solver and theories + are retained and potentially accessible after {!solve} + returns UNSAT. + @param size influences the size of initial allocations. + @param theories theories to load from the start. Other theories + can be added using {!add_theory}. *) + + val add_theory : t -> theory -> unit + (** Add a theory to the solver. This should be called before + any call to {!solve} or to {!add_clause} and the likes (otherwise + the theory will have a partial view of the problem). *) + + val add_theory_p : t -> 'a theory_p -> 'a + (** Add the given theory and obtain its state *) + + val add_theory_l : t -> theory list -> unit + + val mk_lit_t : t -> ?sign:bool -> term -> lit + (** [mk_lit_t _ ~sign t] returns [lit'], + where [lit'] is [preprocess(lit)] and [lit] is + an internal representation of [± t]. + + The proof of [|- lit = lit'] is directly added to the solver's proof. *) + + val add_clause : t -> lit array -> step_id -> unit + (** [add_clause solver cs] adds a boolean clause to the solver. + Subsequent calls to {!solve} will need to satisfy this clause. *) + + val add_clause_l : t -> lit list -> step_id -> unit + (** Add a clause to the solver, given as a list. *) + + val assert_terms : t -> term list -> unit + (** Helper that turns each term into an atom, before adding the result + to the solver as an assertion *) + + val assert_term : t -> term -> unit + (** Helper that turns the term into an atom, before adding the result + to the solver as a unit clause assertion *) + + (** Result of solving for the current set of clauses *) + type res = + | Sat of Model.t (** Satisfiable *) + | Unsat of { + unsat_core: unit -> lit Iter.t; + (** Unsat core (subset of assumptions), or empty *) + unsat_step_id: unit -> step_id option; + (** Proof step for the empty clause *) + } (** Unsatisfiable *) + | Unknown of Unknown.t + (** Unknown, obtained after a timeout, memory limit, etc. *) + + (* TODO: API to push/pop/clear assumptions, in addition to ~assumptions param *) + + val solve : + ?on_exit:(unit -> unit) list -> + ?check:bool -> + ?on_progress:(t -> unit) -> + ?should_stop:(t -> int -> bool) -> + assumptions:lit list -> + t -> + res + (** [solve s] checks the satisfiability of the clauses added so far to [s]. + @param check if true, the model is checked before returning. + @param on_progress called regularly during solving. + @param assumptions a set of atoms held to be true. The unsat core, + if any, will be a subset of [assumptions]. + @param should_stop a callback regularly called with the solver, + and with a number of "steps" done since last call. The exact notion + of step is not defined, but is guaranteed to increase regularly. + The function should return [true] if it judges solving + must stop (returning [Unknown]), [false] if solving can proceed. + @param on_exit functions to be run before this returns *) + + val last_res : t -> res option + (** Last result, if any. Some operations will erase this (e.g. {!assert_term}). *) + + val push_assumption : t -> lit -> unit + (** Pushes an assumption onto the assumption stack. It will remain + there until it's pop'd by {!pop_assumptions}. *) + + val pop_assumptions : t -> int -> unit + (** [pop_assumptions solver n] removes [n] assumptions from the stack. + It removes the assumptions that were the most + recently added via {!push_assumptions}. + Note that {!check_sat_propagations_only} can call this if it meets + a conflict. *) + + type propagation_result = + | PR_sat + | PR_conflict of { backtracked: int } + | PR_unsat of { unsat_core: unit -> lit Iter.t } + + val check_sat_propagations_only : + assumptions:lit list -> t -> propagation_result + (** [check_sat_propagations_only solver] uses assumptions (including + the [assumptions] parameter, and atoms previously added via {!push_assumptions}) + and boolean+theory propagation to quickly assess satisfiability. + It is not complete; calling {!solve} is required to get an accurate + result. + @returns one of: + + - [PR_sat] if the current state seems satisfiable + - [PR_conflict {backtracked=n}] if a conflict was found and resolved, + leading to backtracking [n] levels of assumptions + - [PR_unsat …] if the assumptions were found to be unsatisfiable, with + the given core. + *) + + (* TODO: allow on_progress to return a bool to know whether to stop? *) + + val pp_stats : t CCFormat.printer + (** Print some statistics. What it prints exactly is unspecified. *) +end diff --git a/src/sigs/smt/dune b/src/sigs/smt/dune new file mode 100644 index 00000000..063ba7ce --- /dev/null +++ b/src/sigs/smt/dune @@ -0,0 +1,8 @@ +(library + (name sidekick_sigs_smt) + (public_name sidekick.sigs.smt) + (synopsis "Signatures for the SMT solver") + (flags :standard -open Sidekick_util) + (libraries containers iter sidekick.sigs sidekick.sigs.term + sidekick.sigs.lit sidekick.sigs.proof-trace sidekick.sigs.proof.core + sidekick.sigs.proof.sat sidekick.util sidekick.sigs.cc)) diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 15ba0430..8c44e19a 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -12,18 +12,26 @@ module type ARG = sig open Sidekick_core module T : TERM module Lit : LIT with module T = T + module Proof_trace : PROOF_TRACE - type proof - type proof_step + type step_id = Proof_trace.A.step_id + type rule = Proof_trace.A.rule - module P : - PROOF + module Rule_core : + Sidekick_sigs_proof_core.S with type term = T.Term.t - and type t = proof - and type proof_step = proof_step and type lit = Lit.t + and type step_id = step_id + and type rule = rule - val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t + module Rule_sat : + Sidekick_sigs_proof_sat.S + with type lit = Lit.t + and type step_id = step_id + and type rule = rule + + val view_as_cc : + T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) Sidekick_sigs_cc.View.t val mk_eq : T.Term.store -> T.Term.t -> T.Term.t -> T.Term.t (** [mk_eq store t u] builds the term [t=u] *) @@ -33,9 +41,9 @@ module type ARG = sig a quantifier) *) end -module type S = Sidekick_core.SOLVER +module type S = Sidekick_sigs_smt.SOLVER -module Registry : Sidekick_core.REGISTRY = struct +module Registry : Sidekick_sigs_smt.REGISTRY = struct (* registry keys *) module type KEY = sig type elt @@ -78,24 +86,28 @@ end module Make (A : ARG) : S with module T = A.T - and type proof = A.proof - and type proof_step = A.proof_step and module Lit = A.Lit - and module P = A.P = struct + and module Proof_trace = A.Proof_trace = struct module T = A.T - module P = A.P + module Proof_trace = A.Proof_trace + module Lit = A.Lit module Ty = T.Ty module Term = T.Term - module Lit = A.Lit + + open struct + module P = Proof_trace + module Rule_ = A.Rule_core + end type term = Term.t type ty = Ty.t - type proof = A.proof - type proof_step = A.proof_step type lit = Lit.t + type rule = Proof_trace.A.rule + type step_id = Proof_trace.A.step_id + type proof_trace = Proof_trace.t (* actions from the sat solver *) - type sat_acts = (lit, proof, proof_step) Sidekick_sat.acts + type sat_acts = (lit, Proof_trace.t, step_id) Sidekick_sat.acts type th_combination_conflict = { lits: lit list; @@ -109,48 +121,20 @@ module Make (A : ARG) : exception Semantic_conflict of th_combination_conflict (* the full argument to the congruence closure *) - module CC_actions = struct + module CC_arg = struct module T = T - module P = P module Lit = Lit + module Proof_trace = Proof_trace + module Rule_core = A.Rule_core - type nonrec proof = proof - type nonrec proof_step = proof_step - - let cc_view = A.cc_view + let view_as_cc = A.view_as_cc let[@inline] mk_lit_eq ?sign store t u = A.Lit.atom ?sign store (A.mk_eq store t u) - - module Actions = struct - module T = T - module P = P - module Lit = Lit - - type nonrec proof = proof - type nonrec proof_step = proof_step - type t = sat_acts - - let[@inline] proof (a : t) = - let (module A) = a in - A.proof - - let[@inline] raise_conflict (a : t) lits (pr : proof_step) = - let (module A) = a in - A.raise_conflict lits pr - - let[@inline] raise_semantic_conflict (_ : t) lits semantic = - raise (Semantic_conflict { lits; semantic }) - - let[@inline] propagate (a : t) lit ~reason = - let (module A) = a in - let reason = Sidekick_sat.Consequence reason in - A.propagate lit reason - end end - module CC = Sidekick_cc.Make (CC_actions) - module N = CC.N + module CC = Sidekick_cc.Make (CC_arg) + module N = CC.Class module Model = struct type t = Empty | Map of term Term.Tbl.t @@ -180,19 +164,44 @@ module Make (A : ARG) : (* delayed actions. We avoid doing them on the spot because, when triggered by a theory, they might go back to the theory "too early". *) type delayed_action = - | DA_add_clause of { c: lit list; pr: proof_step; keep: bool } + | DA_add_clause of { c: lit list; pr: step_id; keep: bool } | DA_add_lit of { default_pol: bool option; lit: lit } + let mk_cc_acts_ (pr : P.t) (a : sat_acts) : CC.actions = + let (module A) = a in + + (module struct + module T = T + module Lit = Lit + + type nonrec lit = lit + type nonrec term = term + type nonrec proof_trace = Proof_trace.t + type nonrec step_id = step_id + + let proof_trace () = pr + let[@inline] raise_conflict lits (pr : step_id) = A.raise_conflict lits pr + + let[@inline] raise_semantic_conflict lits semantic = + raise (Semantic_conflict { lits; semantic }) + + let[@inline] propagate lit ~reason = + let reason = Sidekick_sat.Consequence reason in + A.propagate lit reason + end) + (** Internal solver, given to theories and to Msat *) module Solver_internal = struct module T = T - module P = P + module Proof_trace = Proof_trace + module Proof_rules = A.Rule_sat + module P_core_rules = A.Rule_core module Lit = Lit module CC = CC - module N = CC.N + module N = CC.Class - type nonrec proof = proof - type nonrec proof_step = proof_step + type nonrec proof_trace = Proof_trace.t + type nonrec step_id = step_id type term = Term.t type value = term type ty = Ty.t @@ -217,15 +226,15 @@ module Make (A : ARG) : type t = { tst: term_store; ty_st: ty_store; - proof: proof; + proof: proof_trace; mutable hooks: hook list; - (* store [t --> u by proof_steps] in the cache. + (* store [t --> u by step_ids] in the cache. We use a bag for the proof steps because it gives us structural sharing of subproofs. *) - cache: (Term.t * proof_step Bag.t) Term.Tbl.t; + cache: (Term.t * step_id Bag.t) Term.Tbl.t; } - and hook = t -> term -> (term * proof_step Iter.t) option + and hook = t -> term -> (term * step_id Iter.t) option let create tst ty_st ~proof : t = { tst; ty_st; proof; hooks = []; cache = Term.Tbl.create 32 } @@ -236,7 +245,7 @@ module Make (A : ARG) : let add_hook self f = self.hooks <- f :: self.hooks let clear self = Term.Tbl.clear self.cache - let normalize (self : t) (t : Term.t) : (Term.t * proof_step) option = + let normalize (self : t) (t : Term.t) : (Term.t * step_id) option = (* compute and cache normal form of [t] *) let rec loop t : Term.t * _ Bag.t = match Term.Tbl.find self.cache t with @@ -277,7 +286,8 @@ module Make (A : ARG) : else ( (* proof: [sub_proofs |- t=u] by CC + subproof *) let step = - P.lemma_preprocess t u ~using:(Bag.to_iter pr_u) self.proof + P.add_step self.proof + @@ Rule_.lemma_preprocess t u ~using:(Bag.to_iter pr_u) in Some (u, step) ) @@ -291,9 +301,9 @@ module Make (A : ARG) : type simplify_hook = Simplify.hook module type PREPROCESS_ACTS = sig - val proof : proof + val proof : proof_trace val mk_lit : ?sign:bool -> term -> lit - val add_clause : lit list -> proof_step -> unit + val add_clause : lit list -> step_id -> unit val add_lit : ?default_pol:bool -> lit -> unit end @@ -305,7 +315,7 @@ module Make (A : ARG) : tst: Term.store; (** state for managing terms *) ty_st: Ty.store; cc: CC.t lazy_t; (** congruence closure *) - proof: proof; (** proof logger *) + proof: proof_trace; (** proof logger *) registry: Registry.t; mutable on_progress: unit -> unit; mutable on_partial_check: @@ -331,16 +341,11 @@ module Make (A : ARG) : } and preprocess_hook = t -> preprocess_actions -> term -> unit - - and model_ask_hook = - recurse:(t -> CC.N.t -> term) -> t -> CC.N.t -> term option - + and model_ask_hook = recurse:(t -> N.t -> term) -> t -> N.t -> term option and model_completion_hook = t -> add:(term -> term -> unit) -> unit type solver = t - module Proof = P - let[@inline] cc (t : t) = Lazy.force t.cc let[@inline] tst t = t.tst let[@inline] ty_st t = t.ty_st @@ -382,7 +387,7 @@ module Make (A : ARG) : propagate self acts p ~reason:(fun () -> cs, proof) let add_sat_clause_ self (acts : theory_actions) ~keep lits - (proof : proof_step) : unit = + (proof : step_id) : unit = let (module A) = acts in Stat.incr self.count_axiom; A.add_clause ~keep lits proof @@ -395,7 +400,7 @@ module Make (A : ARG) : let delayed_add_lit (self : t) ?default_pol (lit : Lit.t) : unit = Queue.push (DA_add_lit { default_pol; lit }) self.delayed_actions - let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : proof_step) : + let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : unit = Queue.push (DA_add_clause { c; pr; keep }) self.delayed_actions @@ -445,7 +450,7 @@ module Make (A : ARG) : (* simplify literal, then preprocess the result *) let simplify_and_preproc_lit_ (self : t) (lit : Lit.t) : - Lit.t * proof_step option = + Lit.t * step_id option = let t = Lit.term lit in let sign = Lit.sign lit in let u, pr = @@ -476,8 +481,7 @@ module Make (A : ARG) : module Preprocess_clause (A : ARR) = struct (* preprocess a clause's literals, possibly emitting a proof for the preprocessing. *) - let top (self : t) (c : lit A.t) (pr_c : proof_step) : - lit A.t * proof_step = + let top (self : t) (c : lit A.t) (pr_c : step_id) : lit A.t * step_id = let steps = ref [] in (* simplify a literal, then preprocess it *) @@ -493,8 +497,9 @@ module Make (A : ARG) : pr_c else ( Stat.incr self.count_preprocess_clause; - P.lemma_rw_clause pr_c ~res:(A.to_iter c') - ~using:(Iter.of_list !steps) self.proof + P.add_step self.proof + @@ Rule_.lemma_rw_clause pr_c ~res:(A.to_iter c') + ~using:(Iter.of_list !steps) ) in c', pr_c' @@ -510,9 +515,7 @@ module Make (A : ARG) : module type PERFORM_ACTS = sig type t - val add_clause : - solver -> t -> keep:bool -> lit list -> proof_step -> unit - + val add_clause : solver -> t -> keep:bool -> lit list -> step_id -> unit val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit end @@ -542,11 +545,11 @@ module Make (A : ARG) : add_sat_lit_ self acts ?default_pol lit end) - let[@inline] add_clause_temp self _acts c (proof : proof_step) : unit = + let[@inline] add_clause_temp self _acts c (proof : step_id) : unit = let c, proof = preprocess_clause_ self c proof in delayed_add_clause self ~keep:false c proof - let[@inline] add_clause_permanent self _acts c (proof : proof_step) : unit = + let[@inline] add_clause_permanent self _acts c (proof : step_id) : unit = let c, proof = preprocess_clause_ self c proof in delayed_add_clause self ~keep:true c proof @@ -566,12 +569,12 @@ module Make (A : ARG) : let on_partial_check self f = self.on_partial_check <- f :: self.on_partial_check - let on_cc_new_term self f = CC.on_new_term (cc self) f - let on_cc_pre_merge self f = CC.on_pre_merge (cc self) f - let on_cc_post_merge self f = CC.on_post_merge (cc self) f - let on_cc_conflict self f = CC.on_conflict (cc self) f - let on_cc_propagate self f = CC.on_propagate (cc self) f - let on_cc_is_subterm self f = CC.on_is_subterm (cc self) f + let on_cc_new_term self f = Event.on (CC.on_new_term (cc self)) ~f + let on_cc_pre_merge self f = Event.on (CC.on_pre_merge (cc self)) ~f + let on_cc_post_merge self f = Event.on (CC.on_post_merge (cc self)) ~f + let on_cc_conflict self f = Event.on (CC.on_conflict (cc self)) ~f + let on_cc_propagate self f = Event.on (CC.on_propagate (cc self)) ~f + let on_cc_is_subterm self f = Event.on (CC.on_is_subterm (cc self)) ~f let cc_add_term self t = CC.add_term (cc self) t let cc_mem_term self t = CC.mem_term (cc self) t let cc_find self n = CC.find (cc self) n @@ -584,10 +587,12 @@ module Make (A : ARG) : let cc_merge self _acts n1 n2 e = CC.merge (cc self) n1 n2 e let cc_merge_t self acts t1 t2 e = - cc_merge self acts (cc_add_term self t1) (cc_add_term self t2) e + let cc_acts = mk_cc_acts_ self.proof acts in + cc_merge self cc_acts (cc_add_term self t1) (cc_add_term self t2) e let cc_raise_conflict_expl self acts e = - CC.raise_conflict_from_expl (cc self) acts e + let cc_acts = mk_cc_acts_ self.proof acts in + CC.raise_conflict_from_expl (cc self) cc_acts e (** {2 Interface with the SAT solver} *) @@ -698,6 +703,8 @@ module Make (A : ARG) : let check_th_combination_ (self : t) (acts : theory_actions) : (Model.t, th_combination_conflict) result = let cc = cc self in + let cc_acts = mk_cc_acts_ self.proof acts in + (* entier model mode, disabling most of congruence closure *) CC.with_model_mode cc @@ fun () -> let set_val (t, v) : unit = @@ -715,7 +722,7 @@ module Make (A : ARG) : try List.iter add_th_values self.on_th_combination; - CC.check cc acts; + CC.check cc cc_acts; let m = mk_model_ self in Ok m with Semantic_conflict c -> Error c @@ -734,12 +741,14 @@ module Make (A : ARG) : lits); (* transmit to CC *) let cc = cc self in + let cc_acts = mk_cc_acts_ self.proof acts in + if not final then CC.assert_lits cc lits; (* transmit to theories. *) - CC.check cc acts; + CC.check cc cc_acts; if final then ( List.iter (fun f -> f self acts lits) self.on_final_check; - CC.check cc acts; + CC.check cc cc_acts; (match check_th_combination_ self acts with | Ok m -> self.last_model <- Some m @@ -765,7 +774,7 @@ module Make (A : ARG) : in let c = List.rev_append c1 c2 in - let pr = P.lemma_cc (Iter.of_list c) self.proof in + let pr = P.add_step self.proof @@ Rule_.lemma_cc (Iter.of_list c) in Log.debugf 20 (fun k -> k "(@[solver.th-comb.add-semantic-conflict-clause@ %a@])" @@ -882,7 +891,7 @@ module Make (A : ARG) : | Unsat of { unsat_core: unit -> lit Iter.t; (** Unsat core (subset of assumptions), or empty *) - unsat_proof_step: unit -> proof_step option; + unsat_step_id: unit -> step_id option; (** Proof step for the empty clause *) } | Unknown of Unknown.t @@ -946,7 +955,7 @@ module Make (A : ARG) : let t_true = Term.bool tst true in Sat_solver.add_clause self.solver [ Lit.atom tst t_true ] - (P.lemma_true t_true self.proof)); + (P.add_step self.proof @@ Rule_.lemma_true t_true)); self let[@inline] solver self = self.solver @@ -960,8 +969,8 @@ module Make (A : ARG) : let reset_last_res_ self = self.last_res <- None (* preprocess clause, return new proof *) - let preprocess_clause_ (self : t) (c : lit array) (pr : proof_step) : - lit array * proof_step = + let preprocess_clause_ (self : t) (c : lit array) (pr : step_id) : + lit array * step_id = Solver_internal.preprocess_clause_iarray_ self.si c pr let mk_lit_t (self : t) ?sign (t : term) : lit = @@ -974,8 +983,8 @@ module Make (A : ARG) : let pp_stats out (self : t) : unit = Stat.pp_all out (Stat.all @@ stats self) (* add [c], without preprocessing its literals *) - let add_clause_nopreproc_ (self : t) (c : lit array) (proof : proof_step) : - unit = + let add_clause_nopreproc_ (self : t) (c : lit array) (proof : step_id) : unit + = Stat.incr self.count_clause; reset_last_res_ self; Log.debugf 50 (fun k -> @@ -997,7 +1006,7 @@ module Make (A : ARG) : Sat_solver.add_lit solver.solver ?default_pol lit end) - let add_clause (self : t) (c : lit array) (proof : proof_step) : unit = + let add_clause (self : t) (c : lit array) (proof : step_id) : unit = let c, proof = preprocess_clause_ self c proof in add_clause_nopreproc_ self c proof; Perform_delayed_.top self.si self; @@ -1008,7 +1017,9 @@ module Make (A : ARG) : let assert_terms self c = let c = CCList.map (fun t -> Lit.atom (tst self) t) c in - let pr_c = P.emit_input_clause (Iter.of_list c) self.proof in + let pr_c = + P.add_step self.proof @@ A.Rule_sat.sat_input_clause (Iter.of_list c) + in add_clause_l self c pr_c let assert_term self t = assert_terms self [ t ] @@ -1064,9 +1075,9 @@ module Make (A : ARG) : Sat m | Sat_solver.Unsat (module UNSAT) -> let unsat_core () = UNSAT.unsat_assumptions () in - let unsat_proof_step () = Some (UNSAT.unsat_proof ()) in + let unsat_step_id () = Some (UNSAT.unsat_proof ()) in do_on_exit (); - Unsat { unsat_core; unsat_proof_step } + Unsat { unsat_core; unsat_step_id } | exception Resource_exhausted -> Unknown Unknown.U_asked_to_stop in self.last_res <- Some res; diff --git a/src/smt-solver/dune b/src/smt-solver/dune index 1b48ad7d..42a88c50 100644 --- a/src/smt-solver/dune +++ b/src/smt-solver/dune @@ -1,6 +1,6 @@ (library (name Sidekick_smt_solver) (public_name sidekick.smt-solver) - (libraries containers iter sidekick.core sidekick.util sidekick.cc + (libraries containers iter sidekick.sigs.smt sidekick.util sidekick.cc sidekick.sat) (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index fd3dae29..17f685ed 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -65,7 +65,7 @@ module Check_cc = struct let n_calls = Stat.mk_int (Solver.Solver_internal.stats si) "check-cc.call" in - Solver.Solver_internal.on_cc_conflict si (fun cc ~th c -> + Solver.Solver_internal.on_cc_conflict si (fun { cc; th; c } -> if not th then ( Stat.incr n_calls; check_conflict si cc c @@ -193,7 +193,7 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) *) let t3 = Sys.time () -. t2 in Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2 -. t1) t3 - | Solver.Unsat { unsat_proof_step; unsat_core = _ } -> + | Solver.Unsat { unsat_step_id; unsat_core = _ } -> if check then () (* FIXME: check trace? @@ -205,13 +205,13 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) (match proof_file with | Some file -> - (match unsat_proof_step () with + (match unsat_step_id () with | None -> () - | Some unsat_step -> + | Some step_id -> let proof = Solver.proof s in let proof_quip = Profile.with_ "proof.to-quip" @@ fun () -> - Proof_quip.of_proof proof ~unsat:unsat_step + Proof_quip.of_proof proof ~unsat:step_id in Profile.with_ "proof.write-file" @@ fun () -> with_file_out file @@ fun oc -> @@ -248,6 +248,8 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model (* TODO: more? *) in + let add_step r = Solver.Proof_trace.add_step (Solver.proof solver) r in + match stmt with | Statement.Stmt_set_logic logic -> if not @@ List.mem logic known_logics then @@ -281,7 +283,7 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model if pp_cnf then Format.printf "(@[assert@ %a@])@." Term.pp t; let lit = Solver.mk_lit_t solver t in Solver.add_clause solver [| lit |] - (Solver.P.emit_input_clause (Iter.singleton lit) (Solver.proof solver)); + (add_step @@ Proof.Rule_sat.sat_input_clause (Iter.singleton lit)); E.return () | Statement.Stmt_assert_clause c_ts -> if pp_cnf then @@ -291,10 +293,9 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model (* proof of assert-input + preprocessing *) let pr = - let module P = Solver.P in - let proof = Solver.proof solver in let tst = Solver.tst solver in - P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) proof + let lits = Iter.of_list c_ts |> Iter.map (Lit.atom tst) in + add_step @@ Proof.Rule_sat.sat_input_clause lits in Solver.add_clause solver (CCArray.of_list c) pr; diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 544cbc40..1d67b33c 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -8,7 +8,7 @@ module Solver : and type T.Term.store = Term.store and type T.Ty.t = Ty.t and type T.Ty.store = Ty.store - and type proof = Proof.t + and type Proof_trace.t = Proof.t val th_bool : Solver.theory val th_data : Solver.theory diff --git a/src/tef/Sidekick_tef.real.ml b/src/tef/Sidekick_tef.real.ml index 68dc2149..0285da98 100644 --- a/src/tef/Sidekick_tef.real.ml +++ b/src/tef/Sidekick_tef.real.ml @@ -2,7 +2,7 @@ module P = Sidekick_util.Profile let active = lazy - (match Sys.getenv "TEF" with + (match Sys.getenv "TRACE" with | "1" | "true" -> true | _ -> false | exception Not_found -> false) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 14cd7898..b986cc83 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -3,6 +3,8 @@ This handles formulas containing "and", "or", "=>", "if-then-else", etc. *) +open Sidekick_sigs_smt + (** Boolean-oriented view of terms *) type ('a, 'args) bool_view = | B_bool of bool @@ -18,32 +20,31 @@ type ('a, 'args) bool_view = | B_opaque_bool of 'a (* do not enter *) | B_atom of 'a -module type PROOF = sig - type proof - type proof_step +module type PROOF_RULES = sig + type rule type term type lit - val lemma_bool_tauto : lit Iter.t -> proof -> proof_step + val lemma_bool_tauto : lit Iter.t -> rule (** Boolean tautology lemma (clause) *) - val lemma_bool_c : string -> term list -> proof -> proof_step + val lemma_bool_c : string -> term list -> rule (** Basic boolean logic lemma for a clause [|- c]. [proof_bool_c b name cs] is the rule designated by [name]. *) - val lemma_bool_equiv : term -> term -> proof -> proof_step + val lemma_bool_equiv : term -> term -> rule (** Boolean tautology lemma (equivalence) *) - val lemma_ite_true : ite:term -> proof -> proof_step + val lemma_ite_true : ite:term -> rule (** lemma [a ==> ite a b c = b] *) - val lemma_ite_false : ite:term -> proof -> proof_step + val lemma_ite_false : ite:term -> rule (** lemma [¬a ==> ite a b c = c] *) end (** Argument to the theory *) module type ARG = sig - module S : Sidekick_core.SOLVER + module S : SOLVER type term = S.T.Term.t @@ -53,10 +54,9 @@ module type ARG = sig val mk_bool : S.T.Term.store -> (term, term array) bool_view -> term (** Make a term from the given boolean view. *) - include - PROOF - with type proof := S.P.t - and type proof_step := S.P.proof_step + module P : + PROOF_RULES + with type rule := S.Proof_trace.A.rule and type lit := S.Lit.t and type term := S.T.Term.t @@ -107,6 +107,11 @@ module Make (A : ARG) : S with module A = A = struct module Lit = A.S.Solver_internal.Lit module SI = A.S.Solver_internal + (* utils *) + open struct + module Pr = A.S.Proof_trace + end + type state = { tst: T.store; ty_st: Ty.store; gensym: A.Gensym.t } let create tst ty_st : state = { tst; ty_st; gensym = A.Gensym.create tst } @@ -124,23 +129,24 @@ module Make (A : ARG) : S with module A = A = struct | _ -> false let simplify (self : state) (simp : SI.Simplify.t) (t : T.t) : - (T.t * SI.proof_step Iter.t) option = + (T.t * SI.step_id Iter.t) option = let tst = self.tst in let proof = SI.Simplify.proof simp in let steps = ref [] in let add_step_ s = steps := s :: !steps in + let mk_step_ r = Pr.add_step proof r in let add_step_eq a b ~using ~c0 : unit = - add_step_ - @@ SI.P.lemma_rw_clause c0 (SI.Simplify.proof simp) ~using + add_step_ @@ mk_step_ + @@ SI.P_core_rules.lemma_rw_clause c0 ~using ~res:(Iter.return (Lit.atom tst (A.mk_bool tst (B_eq (a, b))))) in let[@inline] ret u = Some (u, Iter.of_list !steps) in (* proof is [t <=> u] *) let ret_bequiv t1 u = - add_step_ @@ A.lemma_bool_equiv t1 u @@ SI.Simplify.proof simp; + add_step_ @@ mk_step_ @@ A.P.lemma_bool_equiv t1 u; ret u in @@ -179,11 +185,11 @@ module Make (A : ARG) : S with module A = A = struct (match A.view_as_bool a with | B_bool true -> add_step_eq t b ~using:(Iter.of_opt prf_a) - ~c0:(A.lemma_ite_true ~ite:t proof); + ~c0:(mk_step_ @@ A.P.lemma_ite_true ~ite:t); ret b | B_bool false -> add_step_eq t c ~using:(Iter.of_opt prf_a) - ~c0:(A.lemma_ite_false ~ite:t proof); + ~c0:(mk_step_ @@ A.P.lemma_ite_false ~ite:t); ret c | _ -> None) | B_equiv (a, b) when is_true a -> ret_bequiv t b @@ -215,6 +221,7 @@ module Make (A : ARG) : S with module A = A = struct let cnf (self : state) (si : SI.t) (module PA : SI.PREPROCESS_ACTS) (t : T.t) : unit = Log.debugf 50 (fun k -> k "(@[th-bool.cnf@ %a@])" T.pp t); + let[@inline] mk_step_ r = Pr.add_step PA.proof r in (* handle boolean equality *) let equiv_ _si ~is_xor ~t t_a t_b : unit = @@ -234,26 +241,26 @@ module Make (A : ARG) : S with module A = A = struct PA.add_clause [ Lit.neg lit; Lit.neg a; b ] (if is_xor then - A.lemma_bool_c "xor-e+" [ t ] PA.proof + mk_step_ @@ A.P.lemma_bool_c "xor-e+" [ t ] else - A.lemma_bool_c "eq-e" [ t; t_a ] PA.proof); + mk_step_ @@ A.P.lemma_bool_c "eq-e" [ t; t_a ]); PA.add_clause [ Lit.neg lit; Lit.neg b; a ] (if is_xor then - A.lemma_bool_c "xor-e-" [ t ] PA.proof + mk_step_ @@ A.P.lemma_bool_c "xor-e-" [ t ] else - A.lemma_bool_c "eq-e" [ t; t_b ] PA.proof); + mk_step_ @@ A.P.lemma_bool_c "eq-e" [ t; t_b ]); PA.add_clause [ lit; a; b ] (if is_xor then - A.lemma_bool_c "xor-i" [ t; t_a ] PA.proof + mk_step_ @@ A.P.lemma_bool_c "xor-i" [ t; t_a ] else - A.lemma_bool_c "eq-i+" [ t ] PA.proof); + mk_step_ @@ A.P.lemma_bool_c "eq-i+" [ t ]); PA.add_clause [ lit; Lit.neg a; Lit.neg b ] (if is_xor then - A.lemma_bool_c "xor-i" [ t; t_b ] PA.proof + mk_step_ @@ A.P.lemma_bool_c "xor-i" [ t; t_b ] else - A.lemma_bool_c "eq-i-" [ t ] PA.proof) + mk_step_ @@ A.P.lemma_bool_c "eq-i-" [ t ]) in (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) @@ -271,11 +278,11 @@ module Make (A : ARG) : S with module A = A = struct (fun t_u u -> PA.add_clause [ Lit.neg lit; u ] - (A.lemma_bool_c "and-e" [ t; t_u ] PA.proof)) + (mk_step_ @@ A.P.lemma_bool_c "and-e" [ t; t_u ])) t_subs subs; PA.add_clause (lit :: List.map Lit.neg subs) - (A.lemma_bool_c "and-i" [ t ] PA.proof) + (mk_step_ @@ A.P.lemma_bool_c "and-i" [ t ]) | B_or l -> let t_subs = Iter.to_list l in let subs = List.map PA.mk_lit t_subs in @@ -286,9 +293,10 @@ module Make (A : ARG) : S with module A = A = struct (fun t_u u -> PA.add_clause [ Lit.neg u; lit ] - (A.lemma_bool_c "or-i" [ t; t_u ] PA.proof)) + (mk_step_ @@ A.P.lemma_bool_c "or-i" [ t; t_u ])) t_subs subs; - PA.add_clause (Lit.neg lit :: subs) (A.lemma_bool_c "or-e" [ t ] PA.proof) + PA.add_clause (Lit.neg lit :: subs) + (mk_step_ @@ A.P.lemma_bool_c "or-e" [ t ]) | B_imply (t_args, t_u) -> (* transform into [¬args \/ u] on the fly *) let t_args = Iter.to_list t_args in @@ -304,18 +312,18 @@ module Make (A : ARG) : S with module A = A = struct (fun t_u u -> PA.add_clause [ Lit.neg u; lit ] - (A.lemma_bool_c "imp-i" [ t; t_u ] PA.proof)) + (mk_step_ @@ A.P.lemma_bool_c "imp-i" [ t; t_u ])) (t_u :: t_args) subs; PA.add_clause (Lit.neg lit :: subs) - (A.lemma_bool_c "imp-e" [ t ] PA.proof) + (mk_step_ @@ A.P.lemma_bool_c "imp-e" [ t ]) | B_ite (a, b, c) -> let lit_a = PA.mk_lit a in PA.add_clause [ Lit.neg lit_a; PA.mk_lit (eq self.tst t b) ] - (A.lemma_ite_true ~ite:t PA.proof); + (mk_step_ @@ A.P.lemma_ite_true ~ite:t); PA.add_clause [ lit_a; PA.mk_lit (eq self.tst t c) ] - (A.lemma_ite_false ~ite:t PA.proof) + (mk_step_ @@ A.P.lemma_ite_false ~ite:t) | B_eq _ | B_neq _ -> () | B_equiv (a, b) -> equiv_ si ~t ~is_xor:false a b | B_xor (a, b) -> equiv_ si ~t ~is_xor:true a b diff --git a/src/th-bool-static/dune b/src/th-bool-static/dune index ae7257a1..0cb1c59f 100644 --- a/src/th-bool-static/dune +++ b/src/th-bool-static/dune @@ -2,4 +2,4 @@ (name sidekick_th_bool_static) (public_name sidekick.th-bool-static) (flags :standard -open Sidekick_util) - (libraries sidekick.core sidekick.util)) + (libraries sidekick.sigs.smt sidekick.util sidekick.cc.plugin)) diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 1a266f26..2aaa9b26 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -1,14 +1,16 @@ (** {1 Theory for constructors} *) +open Sidekick_sigs_smt + type ('c, 't) cstor_view = T_cstor of 'c * 't array | T_other of 't let name = "th-cstor" module type ARG = sig - module S : Sidekick_core.SOLVER + module S : SOLVER val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view - val lemma_cstor : S.proof -> S.Lit.t Iter.t -> unit + val lemma_cstor : S.Lit.t Iter.t -> S.Proof_trace.A.rule end module type S = sig @@ -21,12 +23,12 @@ module Make (A : ARG) : S with module A = A = struct module A = A module SI = A.S.Solver_internal module T = A.S.T.Term - module N = SI.CC.N + module N = SI.CC.Class module Fun = A.S.T.Fun module Expl = SI.CC.Expl module Monoid = struct - module SI = SI + module CC = SI.CC (* associate to each class a unique constructor term in the class (if any) *) type t = { t: T.t; n: N.t; cstor: Fun.t; args: N.t array } @@ -65,16 +67,17 @@ module Make (A : ARG) : S with module A = A = struct Error expl end - module ST = Sidekick_core.Monoid_of_repr (Monoid) + module ST = Sidekick_cc_plugin.Make (Monoid) type t = ST.t - let push_level = ST.push_level - let pop_levels = ST.pop_levels + let push_level ((module P) : t) = P.push_level () + let pop_levels ((module P) : t) n = P.pop_levels n + let n_levels ((module P) : t) = P.n_levels () - let create_and_setup (solver : SI.t) : t = + let create_and_setup (si : SI.t) : t = Log.debug 1 "(setup :th-cstor)"; - let self = ST.create_and_setup ~size:32 solver in + let self = ST.create_and_setup ~size:32 (SI.cc si) in self let theory = A.S.mk_theory ~name ~push_level ~pop_levels ~create_and_setup () diff --git a/src/th-cstor/dune b/src/th-cstor/dune index a76f8ce9..bd39edcf 100644 --- a/src/th-cstor/dune +++ b/src/th-cstor/dune @@ -1,5 +1,5 @@ (library (name Sidekick_th_cstor) (public_name sidekick.th-cstor) - (libraries containers sidekick.core sidekick.util) + (libraries containers sidekick.sigs.smt sidekick.util sidekick.cc.plugin) (flags :standard -open Sidekick_util)) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 672f0aef..736e5fab 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -1,5 +1,6 @@ (** Theory for datatypes. *) +open Sidekick_sigs_smt include Th_intf let name = "th-data" @@ -159,15 +160,19 @@ module Make (A : ARG) : S with module A = A = struct module A = A module SI = A.S.Solver_internal module T = A.S.T.Term - module N = SI.CC.N + module N = SI.CC.Class module Ty = A.S.T.Ty module Expl = SI.CC.Expl module Card = Compute_card (A) + open struct + module Pr = SI.Proof_trace + end + (** Monoid mapping each class to the (unique) constructor it contains, if any *) module Monoid_cstor = struct - module SI = SI + module CC = SI.CC let name = "th-data.cstor" @@ -201,12 +206,13 @@ module Make (A : ARG) : S with module A = A = struct pr in + let proof = SI.CC.proof cc in if A.Cstor.equal c1.c_cstor c2.c_cstor then ( (* same function: injectivity *) let expl_merge i = let t1 = N.term c1.c_n in let t2 = N.term c2.c_n in - mk_expl t1 t2 @@ A.P.lemma_cstor_inj t1 t2 i (SI.CC.proof cc) + mk_expl t1 t2 @@ Pr.add_step proof @@ A.P.lemma_cstor_inj t1 t2 i in assert (CCArray.length c1.c_args = CCArray.length c2.c_args); @@ -217,7 +223,7 @@ module Make (A : ARG) : S with module A = A = struct (* different function: disjointness *) let expl = let t1 = N.term c1.c_n and t2 = N.term c2.c_n in - mk_expl t1 t2 @@ A.P.lemma_cstor_distinct t1 t2 (SI.CC.proof cc) + mk_expl t1 t2 @@ Pr.add_step proof @@ A.P.lemma_cstor_distinct t1 t2 in Error expl @@ -227,7 +233,7 @@ module Make (A : ARG) : S with module A = A = struct (** Monoid mapping each class to the set of is-a/select of which it is the argument *) module Monoid_parents = struct - module SI = SI + module CC = SI.CC let name = "th-data.parents" @@ -291,13 +297,13 @@ module Make (A : ARG) : S with module A = A = struct Ok { parent_is_a; parent_select } end - module ST_cstors = Sidekick_core.Monoid_of_repr (Monoid_cstor) - module ST_parents = Sidekick_core.Monoid_of_repr (Monoid_parents) + module ST_cstors = Sidekick_cc_plugin.Make (Monoid_cstor) + module ST_parents = Sidekick_cc_plugin.Make (Monoid_parents) module N_tbl = Backtrackable_tbl.Make (N) type t = { tst: T.store; - proof: SI.P.t; + proof: SI.Proof_trace.t; cstors: ST_cstors.t; (* repr -> cstor for the class *) parents: ST_parents.t; (* repr -> parents for the class *) cards: Card.t; (* remember finiteness *) @@ -350,11 +356,13 @@ module Make (A : ARG) : S with module A = A = struct with exhaustiveness: [|- is-c(t)] *) let proof = let pr_isa = - A.P.lemma_isa_split t - (Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t)) - self.proof - and pr_eq_sel = A.P.lemma_select_cstor ~cstor_t:u t self.proof in - SI.P.proof_r1 pr_isa pr_eq_sel self.proof + Pr.add_step self.proof + @@ A.P.lemma_isa_split t + (Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t)) + and pr_eq_sel = + Pr.add_step self.proof @@ A.P.lemma_select_cstor ~cstor_t:u t + in + Pr.add_step self.proof @@ SI.P_core_rules.proof_r1 pr_isa pr_eq_sel in T.Tbl.add self.single_cstor_preproc_done t (); @@ -386,7 +394,7 @@ module Make (A : ARG) : S with module A = A = struct N_tbl.add self.to_decide_for_complete_model n () | _ -> () - let on_new_term (self : t) cc (n : N.t) (t : T.t) : unit = + let on_new_term (self : t) ((cc, n, t) : _ * N.t * T.t) : unit = on_new_term_look_at_ty self n t; (* might have to decide [t] *) match A.view_as_data t with @@ -404,7 +412,8 @@ module Make (A : ARG) : S with module A = A = struct %a@])" name T.pp t is_true N.pp n Monoid_cstor.pp cstor); let pr = - A.P.lemma_isa_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) + Pr.add_step self.proof + @@ A.P.lemma_isa_cstor ~cstor_t:(N.term cstor.c_n) t in let n_bool = SI.CC.n_bool cc is_true in SI.CC.merge cc n n_bool @@ -423,7 +432,8 @@ module Make (A : ARG) : S with module A = A = struct assert (i < CCArray.length cstor.c_args); let u_i = CCArray.get cstor.c_args i in let pr = - A.P.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) + Pr.add_step self.proof + @@ A.P.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t in SI.CC.merge cc n u_i Expl.( @@ -439,7 +449,7 @@ module Make (A : ARG) : S with module A = A = struct | Ty_data { cstors } -> cstors | _ -> assert false - let on_pre_merge (self : t) (cc : SI.CC.t) acts n1 n2 expl : unit = + let on_pre_merge (self : t) (cc, acts, n1, n2, expl) : unit = let merge_is_a n1 (c1 : Monoid_cstor.t) n2 (is_a2 : Monoid_parents.is_a) = let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in Log.debugf 50 (fun k -> @@ -449,8 +459,8 @@ module Make (A : ARG) : S with module A = A = struct name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1); let pr = - A.P.lemma_isa_cstor ~cstor_t:(N.term c1.c_n) (N.term is_a2.is_a_n) - self.proof + Pr.add_step self.proof + @@ A.P.lemma_isa_cstor ~cstor_t:(N.term c1.c_n) (N.term is_a2.is_a_n) in let n_bool = SI.CC.n_bool cc is_true in SI.CC.merge cc is_a2.is_a_n n_bool @@ -474,8 +484,8 @@ module Make (A : ARG) : S with module A = A = struct N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); assert (sel2.sel_idx < CCArray.length c1.c_args); let pr = - A.P.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n) - self.proof + Pr.add_step self.proof + @@ A.P.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n) in let u_i = CCArray.get c1.c_args sel2.sel_idx in SI.CC.merge cc sel2.sel_n u_i @@ -578,10 +588,10 @@ module Make (A : ARG) : S with module A = A = struct (* conflict: the [path] forms a cycle *) let path = (n, node) :: path in let pr = - A.P.lemma_acyclicity - (Iter.of_list path - |> Iter.map (fun (a, b) -> N.term a, N.term b.repr)) - self.proof + Pr.add_step self.proof + @@ A.P.lemma_acyclicity + (Iter.of_list path + |> Iter.map (fun (a, b) -> N.term a, N.term b.repr)) in let expl = let subs = @@ -601,7 +611,7 @@ module Make (A : ARG) : S with module A = A = struct Log.debugf 5 (fun k -> k "(@[%s.acyclicity.raise_confl@ %a@ @[:path %a@]@])" name Expl.pp expl pp_path path); - SI.CC.raise_conflict_from_expl cc acts expl + SI.cc_raise_conflict_expl solver acts expl | { flag = New; _ } as node_r -> node_r.flag <- Open; let path = (n, node_r) :: path in @@ -631,7 +641,7 @@ module Make (A : ARG) : S with module A = A = struct Log.debugf 50 (fun k -> k "(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name T.pp u T.pp rhs SI.Lit.pp lit); - let pr = A.P.lemma_isa_sel t self.proof in + let pr = Pr.add_step self.proof @@ A.P.lemma_isa_sel t in SI.cc_merge_t solver acts u rhs (Expl.mk_theory u rhs [ t, N.term (SI.CC.n_true @@ SI.cc solver), [ Expl.mk_lit lit ] ] @@ -656,10 +666,11 @@ module Make (A : ARG) : S with module A = A = struct |> Iter.to_rev_list in SI.add_clause_permanent solver acts c - (A.P.lemma_isa_split t (Iter.of_list c) self.proof); + (Pr.add_step self.proof @@ A.P.lemma_isa_split t (Iter.of_list c)); Iter.diagonal_l c (fun (l1, l2) -> let pr = - A.P.lemma_isa_disj (SI.Lit.neg l1) (SI.Lit.neg l2) self.proof + Pr.add_step self.proof + @@ A.P.lemma_isa_disj (SI.Lit.neg l1) (SI.Lit.neg l2) in SI.add_clause_permanent solver acts [ SI.Lit.neg l1; SI.Lit.neg l2 ] @@ -754,8 +765,8 @@ module Make (A : ARG) : S with module A = A = struct { tst = SI.tst solver; proof = SI.proof solver; - cstors = ST_cstors.create_and_setup ~size:32 solver; - parents = ST_parents.create_and_setup ~size:32 solver; + 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 (); to_decide_for_complete_model = N_tbl.create ~size:16 (); single_cstor_preproc_done = T.Tbl.create 8; diff --git a/src/th-data/dune b/src/th-data/dune index 4ac39554..8f959c7e 100644 --- a/src/th-data/dune +++ b/src/th-data/dune @@ -1,7 +1,7 @@ (library (name Sidekick_th_data) (public_name sidekick.th-data) - (libraries containers sidekick.core sidekick.util) + (libraries containers sidekick.sigs.smt sidekick.util sidekick.cc.plugin) (flags :standard -open Sidekick_util -w -27-32)) ; TODO get warning back diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml index e0cafea7..aa1360d4 100644 --- a/src/th-data/th_intf.ml +++ b/src/th-data/th_intf.ml @@ -1,3 +1,5 @@ +open Sidekick_sigs_smt + (** Datatype-oriented view of terms. - ['c] is the representation of constructors @@ -16,47 +18,46 @@ type ('c, 'ty) data_ty_view = | Ty_data of { cstors: 'c } | Ty_other -module type PROOF = sig +module type PROOF_RULES = sig type term type lit - type proof_step - type proof + type rule - val lemma_isa_cstor : cstor_t:term -> term -> proof -> proof_step + val lemma_isa_cstor : cstor_t:term -> term -> rule (** [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 -> term -> proof -> proof_step + val lemma_select_cstor : cstor_t:term -> term -> rule (** [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 -> lit Iter.t -> proof -> proof_step + val lemma_isa_split : term -> lit Iter.t -> rule (** [lemma_isa_split t lits] is the proof of [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *) - val lemma_isa_sel : term -> proof -> proof_step + val lemma_isa_sel : term -> rule (** [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 -> lit -> proof -> proof_step + val lemma_isa_disj : lit -> lit -> rule (** [lemma_isa_disj (is-c t) (is-d t)] is the proof of [¬ (is-c t) \/ ¬ (is-c t)] *) - val lemma_cstor_inj : term -> term -> int -> proof -> proof_step + val lemma_cstor_inj : term -> term -> int -> rule (** [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 -> term -> proof -> proof_step + val lemma_cstor_distinct : term -> term -> rule (** [lemma_isa_distinct (c …) (d …)] is the proof of the unit clause [|- (c …) ≠ (d …)] *) - val lemma_acyclicity : (term * term) Iter.t -> proof -> proof_step + val lemma_acyclicity : (term * term) Iter.t -> rule (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false] by acyclicity. *) end module type ARG = sig - module S : Sidekick_core.SOLVER + module S : SOLVER (** Constructor symbols. @@ -102,9 +103,8 @@ module type ARG = sig (** Modify the "finite" field (see {!ty_is_finite}) *) module P : - PROOF - with type proof := S.P.t - and type proof_step := S.P.proof_step - and type term := S.T.Term.t - and type lit := S.Lit.t + PROOF_RULES + with type rule = S.Proof_trace.A.rule + and type term = S.T.Term.t + and type lit = S.Lit.t end diff --git a/src/util/Event.ml b/src/util/Event.ml index 4bee61c0..c0805bd2 100644 --- a/src/util/Event.ml +++ b/src/util/Event.ml @@ -10,5 +10,6 @@ module Emitter = struct let create () : _ t = { h = Vec.make 3 nop_handler_ } end -let on self f = Vec.push self.h f +let on self ~f = Vec.push self.h f let of_emitter x = x +let emit = Emitter.emit diff --git a/src/util/Event.mli b/src/util/Event.mli index 12599ef8..da060f10 100644 --- a/src/util/Event.mli +++ b/src/util/Event.mli @@ -4,9 +4,10 @@ type 'a t module Emitter : sig type 'a t - val emit : 'a t -> 'a -> unit val create : unit -> 'a t + val emit : 'a t -> 'a -> unit end -val on : 'a t -> ('a -> unit) -> unit +val on : 'a t -> f:('a -> unit) -> unit val of_emitter : 'a Emitter.t -> 'a t +val emit : 'a Emitter.t -> 'a -> unit diff --git a/src/util/gen/dune b/src/util/gen/dune new file mode 100644 index 00000000..de5cfcf8 --- /dev/null +++ b/src/util/gen/dune @@ -0,0 +1,2 @@ +;(executable +;(name gen_vec)) diff --git a/src/util/gen/gen_vec.ml.tmp b/src/util/gen/gen_vec.ml.tmp new file mode 100644 index 00000000..62cb390a --- /dev/null +++ b/src/util/gen/gen_vec.ml.tmp @@ -0,0 +1,2 @@ + +let () =