From 2810312e2f47586f1ee455eca774e2e913b6f25e Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 22 Feb 2021 21:10:18 -0500
Subject: [PATCH] add simplify to LRA

---
 src/arith/lra/linear_expr.ml        |  1 +
 src/arith/lra/linear_expr_intf.ml   |  1 +
 src/arith/lra/sidekick_arith_lra.ml | 28 +++++++++++++++++++++++++++-
 src/smtlib/Process.ml               |  1 +
 4 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/arith/lra/linear_expr.ml b/src/arith/lra/linear_expr.ml
index ddfda71d..1eb3b091 100644
--- a/src/arith/lra/linear_expr.ml
+++ b/src/arith/lra/linear_expr.ml
@@ -119,6 +119,7 @@ module Make(C : COEFF)(Var : VAR) = struct
     let zero = of_const C.zero
 
     let is_zero e = C.equal C.zero e.const  && Comb.is_empty e.comb
+    let is_const e = Comb.is_empty e.comb
 
     let map2 f g e e' = make (f e.comb e'.comb) (g e.const e'.const)
 
diff --git a/src/arith/lra/linear_expr_intf.ml b/src/arith/lra/linear_expr_intf.ml
index cf0323a9..3e9b5142 100644
--- a/src/arith/lra/linear_expr_intf.ml
+++ b/src/arith/lra/linear_expr_intf.ml
@@ -165,6 +165,7 @@ module type S = sig
     val const : t -> C.t
 
     val is_zero : t -> bool
+    val is_const : t -> bool
 
     val compare : t -> t -> int
     (** Standard comparison function on expressions. *)
diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml
index f02b0ba5..f25440b1 100644
--- a/src/arith/lra/sidekick_arith_lra.ml
+++ b/src/arith/lra/sidekick_arith_lra.ml
@@ -44,6 +44,8 @@ module type ARG = sig
   val view_as_lra : term -> term lra_view
   (** Project the term into the theory view *)
 
+  val mk_bool : S.T.Term.state -> bool -> term
+
   val mk_lra : S.T.Term.state -> term lra_view -> term
   (** Make a term from the given theory view *)
 
@@ -342,6 +344,30 @@ module Make(A : ARG) : S with module A = A = struct
     | LRA_other t when A.has_ty_real t -> None
     | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None
 
+  let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
+    match A.view_as_lra t with
+    | LRA_op _ | LRA_mult _ ->
+      let le = as_linexp_id t in
+      if LE.is_const le then (
+        let c = LE.const le in
+        Some (A.mk_lra self.tst (LRA_const c))
+      ) else None
+    | LRA_pred (pred, l1, l2) ->
+      let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
+      if LE.is_const le then (
+        let c = LE.const le in
+        let is_true = match pred with
+          | Leq -> Q.(c <= zero)
+          | Geq -> Q.(c >= zero)
+          | Lt -> Q.(c < zero)
+          | Gt -> Q.(c > zero)
+          | Eq -> Q.(c = zero)
+          | Neq -> Q.(c <> zero)
+        in
+        Some (A.mk_bool self.tst is_true)
+      ) else None
+    | _ -> None
+
   module Q_map = CCMap.Make(Q)
 
   (* raise conflict from certificate *)
@@ -517,7 +543,7 @@ module Make(A : ARG) : S with module A = A = struct
     Log.debug 2 "(th-lra.setup)";
     let stat = SI.stats si in
     let st = create ~stat (SI.tst si) in
-    (* TODO    SI.add_simplifier si (simplify st); *)
+    SI.add_simplifier si (simplify st);
     SI.add_preprocess si (preproc_lra st);
     SI.on_final_check si (final_check_ st);
     SI.on_partial_check si (partial_check_ st);
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 74fc3cad..489ee2cb 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -317,6 +317,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
 
   let mk_eq = Form.eq
   let mk_lra = T.lra
+  let mk_bool = T.bool
   let view_as_lra t = match T.view t with
     | T.LRA l -> l
     | T.Eq (a,b) when Ty.equal (T.ty a) Ty.real -> LRA_pred (Eq, a, b)