feat(core): concrete lit, proof traces, proof terms

src/core/Sidekick_core.ml

@@ -3,7 +3,7 @@
     Theories and concrete solvers rely on an environment that defines
     several important types:
 
-    - sorts
+      - types
     - terms (to represent logic expressions and formulas)
     - a congruence closure instance
     - a bridge to some SAT solver
@@ -14,12 +14,18 @@
 
 module Fmt = CCFormat
 
-module type TERM = Sidekick_sigs_term.S
+(* re-export *)
-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
+module Const = Sidekick_core_logic.Const
-(** Signature for SAT-solver proof emission. *)
 
-module type PROOF_CORE = Sidekick_sigs_proof_core.S
+module Term = struct
-(** Proofs of unsatisfiability. *)
+  include Sidekick_core_logic.Term
+  include Sidekick_core_logic.T_builtins
+end
+
+module Var = Sidekick_core_logic.Var
+module Bvar = Sidekick_core_logic.Bvar
+module Subst = Sidekick_core_logic.Subst
+module Proof_trace = Proof_trace
+module Proof_sat = Proof_sat
+module Proof_core = Proof_core

src/core/dune

@@ -2,6 +2,4 @@
  (name Sidekick_core)
  (public_name sidekick.core)
  (flags :standard -open Sidekick_util)
- (libraries containers iter sidekick.util sidekick.sigs.proof-trace
+ (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic))
-   sidekick.sigs.term sidekick.sigs.lit sidekick.sigs.proof.sat
-   sidekick.sigs.proof.core sidekick.sigs.cc))

src/core/lit.ml

@@ -0,0 +1,40 @@
+open Sidekick_core_logic
+module T = Term
+
+type term = T.t
+type t = { lit_term: term; lit_sign: bool }
+
+let[@inline] neg l = { l with lit_sign = not l.lit_sign }
+let[@inline] sign t = t.lit_sign
+let[@inline] abs t = { t with lit_sign = true }
+let[@inline] term (t : t) : term = t.lit_term
+let[@inline] signed_term t = term t, sign t
+let make ~sign t = { lit_sign = sign; lit_term = t }
+
+let atom ?(sign = true) (t : term) : t =
+  let sign', t = T_builtins.abs t in
+  let sign =
+    if not sign' then
+      not sign
+    else
+      sign
+  in
+  make ~sign t
+
+let equal a b = a.lit_sign = b.lit_sign && T.equal a.lit_term b.lit_term
+
+let hash a =
+  let sign = a.lit_sign in
+  CCHash.combine3 2 (CCHash.bool sign) (T.hash a.lit_term)
+
+let pp out l =
+  if l.lit_sign then
+    T.pp_debug out l.lit_term
+  else
+    Format.fprintf out "(@[@<1>¬@ %a@])" T.pp_debug l.lit_term
+
+let norm_sign l =
+  if l.lit_sign then
+    l, true
+  else
+    neg l, false

src/core/lit.mli

@@ -0,0 +1,42 @@
+(** 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. *)
+
+open Sidekick_core_logic
+
+type term = Term.t
+
+type t
+(** A literal *)
+
+include Sidekick_sigs.EQ_HASH_PRINT with type t := t
+
+val term : t -> term
+(** 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 -> term * bool
+(** Return the atom and the sign *)
+
+val atom : ?sign:bool -> term -> 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. *)

src/core/proof_core.ml

@@ -0,0 +1,38 @@
+(* FIXME
+   open Proof_trace
+
+   type lit = Lit.t
+*)
+
+type lit = Lit.t
+
+let lemma_cc lits : Proof_term.t = Proof_term.make ~lits "core.lemma-cc"
+
+let define_term t1 t2 =
+  Proof_term.make ~terms:(Iter.of_list [ t1; t2 ]) "core.define-term"
+
+let proof_r1 p1 p2 =
+  Proof_term.make ~premises:(Iter.of_list [ p1; p2 ]) "core.r1"
+
+let proof_p1 p1 p2 =
+  Proof_term.make ~premises:(Iter.of_list [ p1; p2 ]) "core.p1"
+
+let proof_res ~pivot p1 p2 =
+  Proof_term.make ~terms:(Iter.return pivot)
+    ~premises:(Iter.of_list [ p1; p2 ])
+    "core.res"
+
+let with_defs pr defs =
+  Proof_term.make ~premises:(Iter.append (Iter.return pr) defs) "core.with-defs"
+
+let lemma_true t = Proof_term.make ~terms:(Iter.return t) "core.true"
+
+let lemma_preprocess t1 t2 ~using =
+  Proof_term.make
+    ~terms:(Iter.of_list [ t1; t2 ])
+    ~premises:using "core.preprocess"
+
+let lemma_rw_clause pr ~res ~using =
+  Proof_term.make
+    ~premises:(Iter.append (Iter.return pr) using)
+    ~lits:res "core.rw-clause"

src/core/proof_core.mli

@@ -0,0 +1,59 @@
+(** Core proofs for SMT and congruence closure. *)
+
+open Sidekick_core_logic
+
+type lit = Lit.t
+
+val lemma_cc : lit Iter.t -> Proof_term.t
+(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
+       of uninterpreted functions. *)
+
+val define_term : Term.t -> Term.t -> Proof_term.t
+(** [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 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
+(** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
+       and [p2] proves [C \/ t], is the Proof_term.t that produces [C \/ u],
+       i.e unit paramodulation. *)
+
+val proof_r1 : Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
+(** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
+       and [p2] proves [C \/ ¬t], is the Proof_term.t that produces [C \/ u],
+       i.e unit resolution. *)
+
+val proof_res :
+  pivot:Term.t -> Proof_term.step_id -> Proof_term.step_id -> Proof_term.t
+(** [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 Proof_term.t that produces [C \/ D], i.e boolean resolution. *)
+
+val with_defs : Proof_term.step_id -> Proof_term.step_id Iter.t -> Proof_term.t
+(** [with_defs pr defs] specifies that [pr] is valid only in
+       a context where the definitions [defs] are present. *)
+
+val lemma_true : Term.t -> Proof_term.t
+(** [lemma_true (true) p] asserts the clause [(true)] *)
+
+val lemma_preprocess :
+  Term.t -> Term.t -> using:Proof_term.step_id Iter.t -> Proof_term.t
+(** [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 Proof_term.t ID for the clause [(t=u)]. *)
+
+val lemma_rw_clause :
+  Proof_term.step_id ->
+  res:lit Iter.t ->
+  using:Proof_term.step_id Iter.t ->
+  Proof_term.t
+(** [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). *)

src/core/proof_sat.ml

@@ -0,0 +1,8 @@
+type lit = Lit.t
+
+let sat_input_clause lits : Proof_term.t = Proof_term.make "sat.input" ~lits
+
+let sat_redundant_clause lits ~hyps : Proof_term.t =
+  Proof_term.make "sat.rup" ~lits ~premises:hyps
+
+let sat_unsat_core lits : Proof_term.t = Proof_term.make ~lits "sat.unsat-core"

src/core/proof_sat.mli

@@ -0,0 +1,15 @@
+(** SAT-solver proof emission. *)
+
+open Proof_term
+
+type lit = Lit.t
+
+val sat_input_clause : lit Iter.t -> Proof_term.t
+(** Emit an input clause. *)
+
+val sat_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> Proof_term.t
+(** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
+    The clause must be RUP wrt [hyps]. *)
+
+val sat_unsat_core : lit Iter.t -> Proof_term.t
+(** TODO: is this relevant here? *)

src/core/proof_term.ml

@@ -0,0 +1,24 @@
+open Sidekick_core_logic
+
+type step_id = int32
+type lit = Lit.t
+
+type t = {
+  rule_name: string;
+  lit_args: lit Iter.t;
+  term_args: Term.t Iter.t;
+  subst_args: Subst.t Iter.t;
+  premises: step_id Iter.t;
+}
+
+let pp out _ = Fmt.string out "<proof term>" (* TODO *)
+
+let make ?(lits = Iter.empty) ?(terms = Iter.empty) ?(substs = Iter.empty)
+    ?(premises = Iter.empty) rule_name : t =
+  {
+    rule_name;
+    lit_args = lits;
+    subst_args = substs;
+    term_args = terms;
+    premises;
+  }

src/core/proof_term.mli

@@ -0,0 +1,26 @@
+(** Proof terms.
+
+  A proof term is the description of a reasoning step, that yields a clause. *)
+
+open Sidekick_core_logic
+
+type step_id = int32
+type lit = Lit.t
+
+type t = {
+  rule_name: string;
+  lit_args: lit Iter.t;
+  term_args: Term.t Iter.t;
+  subst_args: Subst.t Iter.t;
+  premises: step_id Iter.t;
+}
+
+include Sidekick_sigs.PRINT with type t := t
+
+val make :
+  ?lits:lit Iter.t ->
+  ?terms:Term.t Iter.t ->
+  ?substs:Subst.t Iter.t ->
+  ?premises:step_id Iter.t ->
+  string ->
+  t

src/core/proof_trace.ml

@@ -0,0 +1,49 @@
+type lit = Lit.t
+type step_id = int32
+type proof_term = Proof_term.t
+
+module Step_vec = struct
+  type elt = step_id
+  type t = elt Vec.t
+
+  let get = Vec.get
+  let size = Vec.size
+  let iter = Vec.iter
+  let iteri = Vec.iteri
+  let create ?cap:_ () = Vec.create ()
+  let clear = Vec.clear
+  let copy = Vec.copy
+  let is_empty = Vec.is_empty
+  let push = Vec.push
+  let fast_remove = Vec.fast_remove
+  let filter_in_place = Vec.filter_in_place
+  let ensure_size v len = Vec.ensure_size v ~elt:0l len
+  let pop = Vec.pop_exn
+  let set = Vec.set
+  let shrink = Vec.shrink
+  let to_iter = Vec.to_iter
+end
+
+module type DYN = sig
+  val enabled : unit -> bool
+  val add_step : proof_term -> step_id
+  val add_unsat : step_id -> unit
+  val delete : 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 : 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
+let make (d : (module DYN)) : t = d
+let dummy_step_id : step_id = -1l
+
+let dummy : t =
+  (module struct
+    let enabled () = false
+    let add_step _ = dummy_step_id
+    let add_unsat _ = ()
+    let delete _ = ()
+  end)

src/core/proof_trace.mli

@@ -0,0 +1,65 @@
+(** Proof traces.
+
+    A proof trace is a log of all the deductive reasoning steps made by
+    the SMT solver and other reasoning components. It essentially stores
+    a DAG of all these steps, where each step points (via {!step_id})
+    to its premises.
+*)
+
+open Sidekick_core_logic
+
+type lit = Lit.t
+
+type step_id = Proof_term.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 elt = step_id
+(** A vector indexed by steps. *)
+
+type proof_term = Proof_term.t
+
+(** {2 Traces} *)
+
+type t
+(** 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.
+*)
+
+val enabled : t -> bool
+(** Is proof tracing enabled? *)
+
+val add_step : t -> proof_term -> step_id
+(** Create a new step in the trace. *)
+
+val add_unsat : t -> step_id -> unit
+(** Signal "unsat" result at the given proof *)
+
+val delete : t -> step_id -> unit
+(** Forget a step that won't be used in the rest of the trace.
+    Only useful for performance/memory considerations. *)
+
+(** {2 Dummy backend} *)
+
+val dummy_step_id : step_id
+
+val dummy : t
+(** Dummy proof trace, logs nothing. *)
+
+(* TODO: something that just logs on stderr? or uses "Log"? *)
+
+(** {2 Dynamic interface} *)
+
+module type DYN = sig
+  val enabled : unit -> bool
+  val add_step : proof_term -> step_id
+  val add_unsat : step_id -> unit
+  val delete : step_id -> unit
+end
+
+val make : (module DYN) -> t