From c67e44e6543070db6feb117f396d1062486d04a5 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 9 Oct 2020 23:59:38 -0400
Subject: [PATCH] detail

---
 src/core/Sidekick_core.ml               | 1 +
 src/msat-solver/Sidekick_msat_solver.ml | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 4be835fb..bc6ba4ac 100644
--- a/src/core/Sidekick_core.ml
+++ b/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
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index d4db7e44..617837bd 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/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}