wip: proof production using BARE for storage

sidekick-base.opam

@@ -17,6 +17,7 @@ depends: [
   "ocaml" { >= "4.04" }
   "sidekick" { = version }
   "zarith" { >= "1.8" } # constraint for infix ops
+  "bare_encoding"
   "alcotest" {with-test}
   "qcheck" {with-test & >= "0.16" }
   "odoc" {with-doc}

src/base/dune

@@ -4,5 +4,12 @@
  (synopsis "Base term definitions for the standalone SMT solver and library")
  (libraries containers sidekick.core sidekick.util sidekick.lit
             sidekick.arith-lra sidekick.th-bool-static
-            sidekick.zarith zarith)
+            sidekick.zarith
+            bare_encoding zarith)
  (flags :standard -w -32 -open Sidekick_util))
+
+(rule
+  (targets proof_ser.ml)
+  (deps proof_ser.bare)
+  (action (run bare-codegen %{deps} -o %{targets})))
+

src/base/proof_ser.bare

@@ -0,0 +1,46 @@
+
+type ProofID int
+type Lit int
+type ExprID int
+
+type Clause {
+  lits: []Lit
+}
+
+# clause, RUP with previous steps
+type Step_rup {
+  res: Clause
+  steps: []ProofID
+}
+
+# lit <-> expr
+type Step_bridge_lit_expr {
+  lit: Lit
+  expr: ExprID
+}
+
+# prove congruence closure lemma `\/_{e\in eqns} e`
+type Step_cc {
+  eqns: []ExprID
+}
+
+# prove t=u using some previous steps and unit equations,
+# and add clause (t=u) with given ID
+type Step_preprocess {
+  t: ExprID
+  u: ExprID
+  using: ProofID
+}
+
+type Step_view
+  ( Step_rup
+  | Step_bridge_lit_expr
+  | Step_cc
+  )
+
+type Step {
+  id: ProofID
+  view: Step_view
+}
+
+