detail

src/core/Sidekick_core.ml

@@ -98,6 +98,7 @@ module type LIT = sig
   val term : t -> T.Term.t
   val sign : t -> bool
   val neg : t -> t
+  val abs : t -> t
 
   val equal : t -> t -> bool
   val hash : t -> int

src/msat-solver/Sidekick_msat_solver.ml

@@ -38,6 +38,7 @@ module Make(A : ARG)
 
     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 make ~sign t = {lit_sign=sign; lit_term=t}