add many small sigs libraries

src/sigs/cc/dune

@@ -0,0 +1,9 @@
+
+(library
+ (name sidekick_sigs_cc)
+ (public_name sidekick.sigs.cc)
+ (synopsis "Signatures for the congruence closure")
+ (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.util))

src/sigs/cc/sidekick_sigs_cc.ml

@@ -0,0 +1,548 @@
+(** Main types for congruence closure *)
+
+module View = View
+
+module type TERM = Sidekick_sigs_term.S
+module type LIT = Sidekick_sigs_lit.S
+module type PROOF_TRACE = Sidekick_sigs_proof_trace.S
+
+(** Actions provided to the congruence closure.
+
+    The congruence closure must be able to propagate literals when
+    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
+  type term
+  type lit
+  type proof
+  type proof_step
+
+  val proof : unit -> proof
+
+  val raise_conflict : lit list -> proof_step -> '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).
+      @param pr the proof of [c] being a tautology *)
+
+  val raise_semantic_conflict : lit list -> (bool * term * term) list -> 'a
+  (** [raise_semantic_conflict lits same_val] declares that
+      the conjunction of all [lits] (literals true in current trail) and tuples
+      [{=,≠}, t_i, u_i] implies false.
+
+      The [{=,≠}, t_i, u_i] are pairs of terms with the same value (if [=] / true)
+      or distinct value (if [≠] / false)) in the current model.
+
+      This does not return. It should raise an exception.
+  *)
+
+  val propagate : lit -> reason:(unit -> lit list * proof_step) -> unit
+  (** [propagate lit ~reason pr] declares that [reason() => lit]
+      is a tautology.
+
+      - [reason()] should return a list of literals that are currently true.
+      - [lit] should be a literal of interest (see {!CC_S.set_as_lit}).
+
+      This function might never be called, a congruence closure has the right
+      to not propagate and only trigger conflicts. *)
+end
+
+(** Arguments to a congruence closure's implementation *)
+module type ARG = sig
+  module T : TERM
+  module Lit : LIT with module T = T
+  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 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
+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. *)
+
+  module T : TERM
+  module Lit : LIT with module T = T
+  module Proof_trace : PROOF_TRACE
+
+  type term_store = T.Term.store
+  type term = T.Term.t
+  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 actions =
+    (module ACTIONS
+       with type term = T.Term.t
+        and type lit = Lit.t
+        and type proof = proof
+        and type proof_step = proof_step)
+  (** 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
+      in the partial model built by the solver.
+      The class is represented by a collection of nodes, one of which is
+      distinguished and is called the "representative".
+
+      All information pertaining to the whole equivalence class is stored
+      in this representative's node.
+
+      When two classes become equal (are "merged"), one of the two
+      representatives is picked as the representative of the new class.
+      The new class contains the union of the two old classes' nodes.
+
+      We also allow theories to store additional information in the
+      representative. This information can be used when two classes are
+      merged, to detect conflicts and solve equations à la Shostak.
+  *)
+  module Class : sig
+    type t
+    (** An equivalent class, containing terms that are proved
+        to be equal.
+
+        A value of type [t] points to a particular term, but see
+        {!find} to get the representative of the class. *)
+
+    val term : t -> term
+    (** Term contained in this equivalence class.
+        If [is_root n], then [term n] is the class' representative term. *)
+
+    val equal : t -> t -> bool
+    (** Are two classes {b physically} equal? To check for
+        logical equality, use [CC.Class.equal (CC.find cc n1) (CC.find cc n2)]
+        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. *)
+
+    val is_root : t -> bool
+    (** Is the node a root (ie the representative of its class)?
+        See {!find} to get the root. *)
+
+    val iter_class : t -> t Iter.t
+    (** Traverse the congruence class.
+        Precondition: [is_root n] (see {!find} below) *)
+
+    val iter_parents : t -> t Iter.t
+    (** Traverse the parents of the class.
+        Precondition: [is_root n] (see {!find} below) *)
+
+    type bitfield
+    (** A field in the bitfield of this node. This should only be
+        allocated when a theory is initialized.
+
+        Bitfields are accessed using preallocated keys.
+        See {!CC_S.allocate_bitfield}.
+
+        All fields are initially 0, are backtracked automatically,
+        and are merged automatically when classes are merged. *)
+  end
+
+  (** Explanations
+
+      Explanations are specialized proofs, created by the congruence closure
+      when asked to justify why twp terms are equal. *)
+  module Expl : sig
+    type t
+
+    val pp : t Fmt.printer
+
+    val mk_merge : Class.t -> Class.t -> t
+    (** Explanation: the nodes were explicitly merged *)
+
+    val mk_merge_t : term -> term -> t
+    (** Explanation: the terms were explicitly merged *)
+
+    val mk_lit : lit -> t
+    (** Explanation: we merged [t] and [u] because of literal [t=u],
+        or we merged [t] and [true] because of literal [t],
+        or [t] and [false] because of literal [¬t] *)
+
+    val mk_same_value : Class.t -> Class.t -> t
+
+    val mk_list : t list -> t
+    (** Conjunction of explanations *)
+
+    val mk_theory :
+      term -> term -> (term * term * t list) list -> proof_step -> 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
+        explanations that justify [t_i = u_i] in the current congruence closure.
+
+        The proof [pr] is the theory lemma, of the form
+        [ (t_i = u_i)_i |- t=u ].
+        It is resolved against each [expls_i |- t_i=u_i] obtained from
+        [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
+        where [Gamma] is a subset of the literals asserted into the congruence
+        closure.
+
+        For example for the lemma [a=b] deduced by injectivity
+        from [Some a=Some b] in the theory of datatypes,
+        the arguments would be
+        [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
+        where [pr] is the injectivity lemma [Some a=Some b |- a=b].
+    *)
+  end
+
+  (** Resolved explanations.
+
+      The congruence closure keeps explanations for why terms are in the same
+      class. However these are represented in a compact, cheap form.
+      To use these explanations we need to {b resolve} them into a
+      resolved explanation, typically a list of
+      literals that are true in the current trail and are responsible for
+      merges.
+
+      However, we can also have merged classes because they have the same value
+      in the current model. *)
+  module Resolved_expl : sig
+    type t = {
+      lits: lit list;
+      same_value: (Class.t * Class.t) list;
+      pr: proof -> proof_step;
+    }
+
+    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 *)
+
+  type explanation = Expl.t
+
+  (** {3 Accessors} *)
+
+  val term_store : t -> term_store
+  val proof : t -> proof
+
+  val find : t -> node -> repr
+  (** Current representative *)
+
+  val add_term : t -> term -> node
+  (** Add the term to the congruence closure, if not present already.
+      Will be backtracked. *)
+
+  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
+  (** 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.
+      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").
+
+      There may be restrictions on how many distinct fields are allocated
+      for a given congruence closure (e.g. at most {!Sys.int_size} fields).
+  *)
+
+  val get_bitfield : t -> Class.bitfield -> Class.t -> bool
+  (** Access the bit field of the given node *)
+
+  val set_bitfield : t -> Class.bitfield -> bool -> Class.t -> unit
+  (** 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 *)
+
+  val on_post_merge : t -> ev_on_post_merge -> unit
+  (** Add a function to be called when two classes are merged *)
+
+  val on_new_term : t -> ev_on_new_term -> unit
+  (** Add a function to be called when a new node is created *)
+
+  val on_conflict : t -> ev_on_conflict -> unit
+  (** Called when the congruence closure finds a conflict *)
+
+  val on_propagate : t -> ev_on_propagate -> unit
+  (** Called when the congruence closure propagates a literal *)
+
+  val on_is_subterm : t -> ev_on_is_subterm -> unit
+  (** Called on terms that are subterms of function symbols *)
+
+  val set_as_lit : t -> Class.t -> lit -> unit
+  (** map the given node to a literal. *)
+
+  val find_t : t -> term -> repr
+  (** Current representative of the term.
+      @raise Class.t_found if the term is not already {!add}-ed. *)
+
+  val add_iter : t -> term Iter.t -> unit
+  (** Add a sequence of terms to the congruence closure *)
+
+  val all_classes : t -> repr Iter.t
+  (** All current classes. This is costly, only use if there is no other solution *)
+
+  val assert_lit : t -> lit -> unit
+  (** Given a literal, assume it in the congruence closure and propagate
+      its consequences. Will be backtracked.
+
+      Useful for the theory combination or the SAT solver's functor *)
+
+  val assert_lits : t -> lit Iter.t -> unit
+  (** Addition of many literals *)
+
+  val explain_eq : t -> Class.t -> Class.t -> Resolved_expl.t
+  (** Explain why the two nodes are equal.
+      Fails if they are not, in an unspecified way. *)
+
+  val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
+  (** Raise a conflict with the given explanation.
+      It must be a theory tautology that [expl ==> absurd].
+      To be used in theories.
+
+      This fails in an unspecified way if the explanation, once resolved,
+      satisfies {!Resolved_expl.is_semantic}. *)
+
+  val n_true : t -> Class.t
+  (** Node for [true] *)
+
+  val n_false : t -> Class.t
+  (** Node for [false] *)
+
+  val n_bool : t -> bool -> Class.t
+  (** Node for either true or false *)
+
+  val merge : t -> Class.t -> Class.t -> Expl.t -> unit
+  (** Merge these two nodes given this explanation.
+      It must be a theory tautology that [expl ==> n1 = n2].
+      To be used in theories. *)
+
+  val merge_t : t -> term -> term -> Expl.t -> unit
+  (** Shortcut for adding + merging *)
+
+  val set_model_value : t -> term -> value -> unit
+  (** Set the value of a term in the model. *)
+
+  val with_model_mode : t -> (unit -> 'a) -> 'a
+  (** Enter model combination mode. *)
+
+  val get_model_for_each_class : t -> (repr * Class.t Iter.t * value) Iter.t
+  (** In model combination mode, obtain classes with their values. *)
+
+  val check : t -> actions -> unit
+  (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
+      Will use the {!actions} to propagate literals, declare conflicts, etc. *)
+
+  val push_level : t -> unit
+  (** Push backtracking level *)
+
+  val pop_levels : t -> int -> unit
+  (** Restore to state [n] calls to [push_level] earlier. Used during backtracking. *)
+
+  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: full EGG, also have a function to update the value when
+   the subterms (produced in [of_term]) are updated *)
+
+(** Data attached to the congruence closure classes.
+
+    This helps theories keeping track of some state for each class.
+    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 CC : S
+
+  type t
+  (** Some type with a monoid structure *)
+
+  include Sidekick_sigs.PRINT with type t := t
+
+  val name : string
+  (** name of the monoid structure (short) *)
+
+  val of_term :
+    CC.t -> CC.Class.t -> CC.term -> t option * (CC.Class.t * t) list
+  (** [of_term n t], where [t] is the term annotating node [n],
+      must return [maybe_m, l], where:
+
+      - [maybe_m = Some m] if [t] has monoid value [m];
+        otherwise [maybe_m=None]
+      - [l] is a list of [(u, m_u)] where each [u]'s term
+        is a direct subterm of [t]
+        and [m_u] is the monoid value attached to [u].
+
+      *)
+
+  val merge :
+    CC.t ->
+    CC.Class.t ->
+    t ->
+    CC.Class.t ->
+    t ->
+    CC.Expl.t ->
+    (t, CC.Expl.t) result
+  (** Monoidal combination of two values.
+
+      [merge cc n1 mon1 n2 mon2 expl] returns the result of merging
+      monoid values [mon1] (for class [n1]) and [mon2] (for class [n2])
+      when [n1] and [n2] are merged with explanation [expl].
+
+      @return [Ok mon] if the merge is acceptable, annotating the class of [n1 ∪ n2];
+      or [Error expl'] if the merge is unsatisfiable. [expl'] can then be
+      used to trigger a conflict and undo the merge.
+    *)
+end
+
+(** Stateful plugin holding a per-equivalence-class monoid.
+
+    Helps keep track of monoid state per equivalence class.
+    A theory might use one or more instance(s) of this to
+    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
+
+  val push_level : unit -> unit
+  (** Push backtracking point *)
+
+  val pop_levels : int -> unit
+  (** Pop [n] backtracking points *)
+
+  val n_levels : unit -> int
+
+  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
+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 PL = PLUGIN with module CC = M.CC and module M = M
+
+  type plugin = (module PL)
+
+  val create_and_setup : ?size:int -> M.CC.t -> plugin
+  (** Create a new monoid state *)
+end

src/sigs/cc/view.ml

@@ -0,0 +1,38 @@
+type ('f, 't, 'ts) t =
+  | Bool of bool
+  | App_fun of 'f * 'ts
+  | App_ho of 't * 't
+  | If of 't * 't * 't
+  | Eq of 't * 't
+  | Not of 't
+  | Opaque of 't
+(* do not enter *)
+
+let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
+  match v with
+  | Bool b -> Bool b
+  | App_fun (f, args) -> App_fun (f_f f, f_ts args)
+  | App_ho (f, a) -> App_ho (f_t f, f_t a)
+  | Not t -> Not (f_t t)
+  | If (a, b, c) -> If (f_t a, f_t b, f_t c)
+  | Eq (a, b) -> Eq (f_t a, f_t b)
+  | Opaque t -> Opaque (f_t t)
+
+let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
+  match v with
+  | Bool _ -> ()
+  | App_fun (f, args) ->
+    f_f f;
+    f_ts args
+  | App_ho (f, a) ->
+    f_t f;
+    f_t a
+  | Not t -> f_t t
+  | If (a, b, c) ->
+    f_t a;
+    f_t b;
+    f_t c
+  | Eq (a, b) ->
+    f_t a;
+    f_t b
+  | Opaque t -> f_t t

src/sigs/cc/view.mli

@@ -0,0 +1,33 @@
+(** View terms through the lens of the Congruence Closure *)
+
+(** A view of a term fron the point of view of the congruence closure.
+
+      - ['f] is the type of function symbols
+      - ['t] is the type of terms
+      - ['ts] is the type of sequences of terms (arguments of function application)
+  *)
+type ('f, 't, 'ts) t =
+  | Bool of bool
+  | App_fun of 'f * 'ts
+  | App_ho of 't * 't
+  | If of 't * 't * 't
+  | Eq of 't * 't
+  | Not of 't
+  | Opaque of 't  (** do not enter *)
+
+val map_view :
+  f_f:('a -> 'b) ->
+  f_t:('c -> 'd) ->
+  f_ts:('e -> 'f) ->
+  ('a, 'c, 'e) t ->
+  ('b, 'd, 'f) t
+(** Map function over a view, one level deep.
+    Each function maps over a different type, e.g. [f_t] maps over terms *)
+
+val iter_view :
+  f_f:('a -> unit) ->
+  f_t:('b -> unit) ->
+  f_ts:('c -> unit) ->
+  ('a, 'b, 'c) t ->
+  unit
+(** Iterate over a view, one level deep. *)

src/sigs/lit/dune

@@ -0,0 +1,5 @@
+(library
+ (name sidekick_sigs_lit)
+ (public_name sidekick.sigs.lit)
+ (synopsis "Common definition for literals")
+ (libraries containers iter sidekick.sigs sidekick.sigs.term))

src/sigs/lit/sidekick_sigs_lit.ml

@@ -0,0 +1,45 @@
+(** Literals
+
+    Literals are a pair of a boolean-sorted term, and a sign.
+    Positive literals are the same as their term, and negative literals
+    are the negation of their term.
+
+    The SAT solver deals only in literals and clauses (sets of literals).
+    Everything else belongs in the SMT solver. *)
+
+module type TERM = Sidekick_sigs_term.S
+
+module type S = sig
+  module T : TERM
+  (** Literals depend on terms *)
+
+  type t
+  (** A literal *)
+
+  include Sidekick_sigs.EQ_HASH_PRINT with type t := t
+
+  val term : t -> T.Term.t
+  (** Get the (positive) term *)
+
+  val sign : t -> bool
+  (** Get the sign. A negated literal has sign [false]. *)
+
+  val neg : t -> t
+  (** Take negation of literal. [sign (neg lit) = not (sign lit)]. *)
+
+  val abs : t -> t
+  (** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *)
+
+  val signed_term : t -> T.Term.t * bool
+  (** Return the atom and the sign *)
+
+  val atom : ?sign:bool -> T.Term.store -> T.Term.t -> t
+  (** [atom store t] makes a literal out of a term, possibly normalizing
+      its sign in the process.
+      @param sign if provided, and [sign=false], negate the resulting lit. *)
+
+  val norm_sign : t -> t * bool
+  (** [norm_sign (+t)] is [+t, true],
+      and [norm_sign (-t)] is [+t, false].
+      In both cases the term is positive, and the boolean reflects the initial sign. *)
+end

src/sigs/proof-core/dune

@@ -0,0 +1,6 @@
+(library
+ (name sidekick_sigs_proof_core)
+ (public_name sidekick.sigs.proof.core)
+ (synopsis "Common rules for proof traces")
+ (flags :standard -open Sidekick_util)
+ (libraries containers iter sidekick.util sidekick.sigs))

src/sigs/proof-core/sidekick_sigs_proof_core.ml

@@ -0,0 +1,94 @@
+(** Proof rules for common operations and congruence closure *)
+
+module type S = sig
+  type rule
+  type term
+  type lit
+
+  type step_id
+  (** Identifier for a proof proof_rule (like a unique ID for a clause previously
+      added/proved) *)
+
+  val lemma_cc : lit Iter.t -> rule
+  (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
+      of uninterpreted functions. *)
+
+  val define_term : term -> term -> rule
+  (** [define_term cst u proof] defines the new constant [cst] as being equal
+      to [u].
+      The result is a proof of the clause [cst = u] *)
+
+  val proof_p1 : step_id -> step_id -> rule
+  (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
+      and [p2] proves [C \/ t], is the rule that produces [C \/ u],
+      i.e unit paramodulation. *)
+
+  val proof_r1 : step_id -> step_id -> rule
+  (** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
+      and [p2] proves [C \/ ¬t], is the rule that produces [C \/ u],
+      i.e unit resolution. *)
+
+  val proof_res : pivot:term -> step_id -> step_id -> rule
+  (** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
+      and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
+      is the rule that produces [C \/ D], i.e boolean resolution. *)
+
+  val with_defs : step_id -> step_id Iter.t -> rule
+  (** [with_defs pr defs] specifies that [pr] is valid only in
+      a context where the definitions [defs] are present. *)
+
+  val lemma_true : term -> rule
+  (** [lemma_true (true) p] asserts the clause [(true)] *)
+
+  val lemma_preprocess : term -> term -> using:step_id Iter.t -> rule
+  (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
+      and that [t] has been preprocessed into [u].
+
+      The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
+      closure, and then resolved against the clauses [using] to obtain
+      a unit equality.
+
+      From now on, [t] and [u] will be used interchangeably.
+      @return a rule ID for the clause [(t=u)]. *)
+
+  val lemma_rw_clause :
+    step_id -> res:lit Iter.t -> using:step_id Iter.t -> rule
+  (** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
+      uses the equations [|- p_i = q_i] from [using]
+      to rewrite some literals of [c] into [res]. This is used to preprocess
+      literals of a clause (using {!lemma_preprocess} individually). *)
+end
+
+type ('rule, 'step_id, 'term, 'lit) t =
+  (module S
+     with type rule = 'rule
+      and type step_id = 'step_id
+      and type term = 'term
+      and type lit = 'lit)
+
+(** Make a dummy proof with given types *)
+module Dummy (A : sig
+  type rule
+  type step_id
+  type term
+  type lit
+
+  val dummy_rule : rule
+end) :
+  S
+    with type rule = A.rule
+     and type step_id = A.step_id
+     and type term = A.term
+     and type lit = A.lit = struct
+  include A
+
+  let lemma_cc _ = dummy_rule
+  let define_term _ _ = dummy_rule
+  let proof_p1 _ _ = dummy_rule
+  let proof_r1 _ _ = dummy_rule
+  let proof_res ~pivot:_ _ _ = dummy_rule
+  let with_defs _ _ = dummy_rule
+  let lemma_true _ = dummy_rule
+  let lemma_preprocess _ _ ~using:_ = dummy_rule
+  let lemma_rw_clause _ ~res:_ ~using:_ = dummy_rule
+end

src/sigs/proof-sat/dune

@@ -0,0 +1,6 @@
+(library
+ (name sidekick_sigs_proof_sat)
+ (public_name sidekick.sigs.proof.sat)
+ (synopsis "SAT-solving rules for proof traces")
+ (flags :standard -open Sidekick_util)
+ (libraries containers iter sidekick.util sidekick.sigs))

src/sigs/proof-sat/sidekick_sigs_proof_sat.ml

@@ -0,0 +1,24 @@
+(** Signature for SAT-solver proof emission. *)
+module type S = sig
+  type rule
+  (** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
+
+  type step_id
+  (** identifier for a proof *)
+
+  type lit
+  (** A boolean literal for the proof trace *)
+
+  val sat_input_clause : lit Iter.t -> rule
+  (** Emit an input clause. *)
+
+  val sat_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> rule
+  (** 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? *)
+  *)
+end

src/sigs/proof-trace/dune

@@ -0,0 +1,5 @@
+(library
+ (name sidekick_sigs_proof_trace)
+ (public_name sidekick.sigs.proof-trace)
+ (synopsis "Common definition for proof traces")
+ (libraries containers iter sidekick.sigs sidekick.util))

src/sigs/proof-trace/sidekick_sigs_proof_trace.ml

@@ -0,0 +1,50 @@
+(** Proof traces.
+*)
+
+open Sidekick_util
+
+module type S = 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
+  (** A vector indexed by steps. *)
+
+  (** The proof trace itself.
+
+      A proof trace is a log of all deductive steps taken by the solver,
+      so we can later reconstruct a certificate for proof-checking.
+
+      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 add_unsat : step_id -> unit
+    (** Signal "unsat" result at the given proof *)
+
+    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
+
+  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
+end

src/sigs/sidekick_sigs.ml

@@ -24,4 +24,17 @@ module type PRINT = sig
   val pp : t CCFormat.printer
 end
 
+module type EQ_HASH_PRINT = sig
+  include EQ
+  include HASH with type t := t
+  include PRINT with type t := t
+end
+
+module type EQ_ORD_HASH_PRINT = sig
+  include EQ
+  include ORD with type t := t
+  include HASH with type t := t
+  include PRINT with type t := t
+end
+
 type 'a printer = Format.formatter -> 'a -> unit

src/sigs/term/dune

@@ -0,0 +1,5 @@
+(library
+ (name sidekick_sigs_term)
+ (public_name sidekick.sigs.term)
+ (synopsis "Common definition for terms and types")
+ (libraries containers iter sidekick.sigs))

src/sigs/term/sidekick_sigs_term.ml

@@ -0,0 +1,80 @@
+(** Main representation of Terms and Types *)
+module type S = sig
+  module Fun : Sidekick_sigs.EQ_HASH_PRINT
+  (** A function symbol, like "f" or "plus" or "is_human" or "socrates" *)
+
+  (** Types
+
+      Types should be comparable (ideally, in O(1)), and have
+      at least a boolean type available. *)
+  module Ty : sig
+    include Sidekick_sigs.EQ_HASH_PRINT
+
+    type store
+
+    val bool : store -> t
+    val is_bool : t -> bool
+  end
+
+  (** Term structure.
+
+      Terms should be {b hashconsed}, with perfect sharing.
+      This allows, for example, {!Term.Tbl} and {!Term.iter_dag} to be efficient.
+  *)
+  module Term : sig
+    include Sidekick_sigs.EQ_ORD_HASH_PRINT
+
+    type store
+    (** A store used to create new terms. It is where the hashconsing
+        table should live, along with other all-terms related store. *)
+
+    val ty : t -> Ty.t
+
+    val bool : store -> bool -> t
+    (** build true/false *)
+
+    val as_bool : t -> bool option
+    (** [as_bool t] is [Some true] if [t] is the term [true], and similarly
+        for [false]. For other terms it is [None]. *)
+
+    val abs : store -> t -> t * bool
+    (** [abs t] returns an "absolute value" for the term, along with the
+        sign of [t].
+
+        The idea is that we want to turn [not a] into [(a, false)],
+        or [(a != b)] into [(a=b, false)]. For terms without a negation this
+        should return [(t, true)].
+
+        The store is passed in case a new term needs to be created. *)
+
+    val map_shallow : store -> (t -> t) -> t -> t
+    (** Map function on immediate subterms. This should not be recursive. *)
+
+    val iter_shallow : store -> (t -> unit) -> t -> unit
+    (** Iterate function on immediate subterms. This should not be recursive. *)
+
+    val iter_dag : t -> (t -> unit) -> unit
+    (** [iter_dag t f] calls [f] once on each subterm of [t], [t] included.
+        It must {b not} traverse [t] as a tree, but rather as a
+        perfectly shared DAG.
+
+        For example, in:
+        {[
+          let x = 2 in
+          let y = f x x in
+          let z = g y x in
+          z = z
+        ]}
+
+        the DAG has the following nodes:
+
+        {[ n1: 2
+           n2: f n1 n1
+           n3: g n2 n1
+           n4: = n3 n3
+         ]}
+    *)
+
+    module Tbl : CCHashtbl.S with type key = t
+  end
+end