simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-21 08:46:44 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

large refactor with signature splitting, events, etc.

Browse source
This commit is contained in:
Simon Cruanes 2022-07-18 23:20:07 -04:00
parent b2d0ea2d33
commit f3f0628261
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
55 changed files with 2133 additions and 1823 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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

2
src/base/Base_types.ml
View file

@ -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

5
src/base/ID.mli
View file

@ -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

271
src/base/Proof.ml
View file

@ -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

57
src/base/Proof.mli
View file

@ -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

101
src/base/Proof_dummy.ml
View file

@ -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

43
src/base/Proof_dummy.mli
View file

@ -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

4
src/base/Proof_quip.ml
View file

@ -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

2
src/base/Proof_quip.mli
View file

@ -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

3
src/base/Sidekick_base.ml
View file

@ -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

3
src/base/dune
View file

@ -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))

644
src/cc/Sidekick_cc.ml
View file

File diff suppressed because it is too large Load diff

33
src/cc/Sidekick_cc.mli
View file

@ -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

5
src/cc/plugin/dune Normal file
View file

@ -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))

159
src/cc/plugin/sidekick_cc_plugin.ml Normal file
View file

@ -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

21
src/cc/plugin/sidekick_cc_plugin.mli Normal file
View file

@ -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

568
src/core/Sidekick_core.ml
View file

@ -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

3
src/lra/dune
View file

@ -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))

57
src/lra/sidekick_arith_lra.ml
View file

@ -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

84
src/main/pure_sat_solver.ml
View file

@ -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)

8
src/mini-cc/Sidekick_mini_cc.ml
View file

@ -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

2
src/mini-cc/Sidekick_mini_cc.mli
View file

@ -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 *)

2
src/mini-cc/tests/sidekick_test_minicc.ml
View file

@ -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

18
src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml Normal file
View file

@ -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

6
src/proof-trace/dummy/dune Normal file
View file

@ -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))

23
src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml Normal file
View file

@ -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

6
src/proof-trace/dyn/dune Normal file
View file

@ -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))

24
src/sat/Proof_dummy.ml
View file

@ -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

11
src/sat/Proof_dummy.mli
View file

@ -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

3
src/sat/Sidekick_sat.ml
View file

@ -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

199
src/sat/Solver.ml
View file

@ -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@ @[<hov 2>%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

16
src/sat/Solver.mli
View file

@ -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

92
src/sat/Solver_intf.ml
View file

@ -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 *)

6
src/sat/dune
View file

@ -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))

330
src/sigs/cc/sidekick_sigs_cc.ml
View file

@ -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

10
src/sigs/proof-sat/sidekick_sigs_proof_sat.ml
View file

@ -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

40
src/sigs/proof-trace/sidekick_sigs_proof_trace.ml
View file

@ -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

597
src/sigs/smt/Sidekick_sigs_smt.ml Normal file
View file

@ -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

8
src/sigs/smt/dune Normal file
View file

@ -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))

221
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -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;

2
src/smt-solver/dune
View file

@ -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))

19
src/smtlib/Process.ml
View file

@ -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 "(@[<hv1>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;

2
src/smtlib/Process.mli
View file

@ -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

2
src/tef/Sidekick_tef.real.ml
View file

@ -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)

78
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -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

2
src/th-bool-static/dune
View file

@ -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))

21
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -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 ()

2
src/th-cstor/dune
View file

@ -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))

73
src/th-data/Sidekick_th_data.ml
View file

@ -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;

2
src/th-data/dune
View file

@ -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

34
src/th-data/th_intf.ml
View file

@ -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

3
src/util/Event.ml
View file

@ -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

5
src/util/Event.mli
View file

@ -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

2
src/util/gen/dune Normal file
View file

@ -0,0 +1,2 @@
;(executable
;(name gen_vec))

2
src/util/gen/gen_vec.ml.tmp Normal file
View file

@ -0,0 +1,2 @@
let () =