wip: LRA

src/smtlib/Process.ml

@@ -301,10 +301,28 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   include Form
 end)
 
-module Th_lra = Sidekick_th_lra.Make(struct
+module Th_lra = Sidekick_lra.Make(struct
   module S = Solver
   type term = S.T.Term.t
+
   let view_as_lra _ = assert false (* TODO *)
+
+  let mk_lra _ = assert false
+
+  module Gensym = struct
+    type t = {
+      tst: T.state;
+      mutable fresh: int;
+    }
+
+    let create tst : t = {tst; fresh=0}
+
+    let fresh_term (self:t) ~pre (ty:Ty.t) : T.t =
+      let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in
+      self.fresh <- 1 + self.fresh;
+      let id = ID.make name in
+      T.const self.tst @@ Fun.mk_undef_const id ty
+  end
 end)
 
 let th_bool : Solver.theory = Th_bool.theory

src/th-lra/Sidekick_lra.ml

@@ -159,7 +159,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   (* preprocess linear expressions away *)
   let preproc_lra self si ~mk_lit ~add_clause (t:T.t) : T.t option =
-    let tst = SI.tst si in
+    let _tst = SI.tst si in
     match A.view_as_lra t with
     | LRA_pred (_pre, _t1, _t2) ->
       assert false (* TODO: define a bool variable *)
@@ -261,8 +261,11 @@ module Make(A : ARG) : S with module A = A = struct
       |> Iter.map CC.N.term
     in
     let cnf_of t =
+      assert false
+      (*
       cnf self si t
         ~mk_lit:(SI.mk_lit si acts) ~add_clause:(SI.add_clause_permanent si acts)
+    *)
     in
     begin
       all_terms

src/th-lra/dune

@@ -3,5 +3,5 @@
   (name sidekick_lra)
   (public_name sidekick.th-lra)
   (optional) ; only if deps present
-  (flags :standard -open Sidekick_util)
+  (flags :standard -warn-error -a+8 -open Sidekick_util)
   (libraries containers sidekick.core zarith funarith.zarith funarith))