perf(simplex): optim: no new variable for constraints like a·x <= b

src/arith/lra/linear_expr.ml

@@ -36,6 +36,13 @@ module Make(C : COEFF)(Var : VAR) = struct
 
     let monomial1 x = Var_map.singleton x C.one
 
+    let as_singleton m =
+      if is_empty m then None
+      else (
+        let x, c = Var_map.choose m in
+        if is_empty (Var_map.remove x m) then Some (c, x) else None
+      )
+
     let add c x e =
       let c' = Var_map.get_or ~default:C.zero x e in
       let c' = C.(c + c') in

src/arith/lra/linear_expr_intf.ml

@@ -157,6 +157,9 @@ module type S = sig
     val monomial1 : var -> t
     (** [monome1 v] creates the linear combination [1 * v] *)
 
+    val as_singleton : t -> (C.t * var) option
+    (** [as_singleton l] returns [Some (c,x)] if [l = c * x], [None] otherwise *)
+
     val add : C.t -> var -> t -> t
     (** [add n v t] adds the monome [n * v] to the combination [t]. *)
 

src/arith/lra/predicate.ml

@@ -9,6 +9,14 @@ let neg = function
   | Geq -> Lt
   | Gt -> Leq
 
+let neg_sign = function
+  | Leq -> Geq
+  | Lt -> Gt
+  | Geq -> Leq
+  | Gt -> Lt
+  | Neq -> Neq
+  | Eq -> Eq
+
 let to_string = function
   | Leq -> "=<" | Geq -> ">=" | Lt -> "<"
   | Gt -> ">" | Eq -> "=" | Neq -> "!="

src/arith/lra/simplex.ml

@@ -726,19 +726,35 @@ module Make_full_for_expr(V : VAR_GEN)
 
   (* add a constraint *)
   let add_constr (t:t) (c:constr) (reason:lit) : unit =
-    let (x:var) = V.Fresh.fresh t.param in
     let e, op, q = L.Constr.split c in
-    add_eq t (x, L.Comb.to_list e);
-    begin match op with
-      | Leq -> add_upper_bound t ~strict:false ~reason x q
-      | Geq -> add_lower_bound t ~strict:false ~reason x q
-      | Lt -> add_upper_bound t ~strict:true ~reason x q
-      | Gt -> add_lower_bound t ~strict:true ~reason x q
-      | Eq -> add_bounds t (x,q,q)
-                ~strict_lower:false ~strict_upper:false
-                ~lower_reason:reason ~upper_reason:reason
-      | Neq -> assert false
-    end
+    match L.Comb.as_singleton e with
+    | Some (c0, x0) ->
+      (* no need for a fresh variable, just add constraint on [x0] *)
+      let q = Q.div q c0 in
+      let op = if Q.sign c0 < 0 then Predicate.neg_sign op else op in
+      begin match op with
+        | Leq -> add_upper_bound t ~strict:false ~reason x0 q
+        | Geq -> add_lower_bound t ~strict:false ~reason x0 q
+        | Lt -> add_upper_bound t ~strict:true ~reason x0 q
+        | Gt -> add_lower_bound t ~strict:true ~reason x0 q
+        | Eq -> add_bounds t (x0,q,q)
+                  ~strict_lower:false ~strict_upper:false
+                  ~lower_reason:reason ~upper_reason:reason
+        | Neq -> assert false
+      end
+    | None ->
+      let (x:var) = V.Fresh.fresh t.param in
+      add_eq t (x, L.Comb.to_list e);
+      begin match op with
+        | Leq -> add_upper_bound t ~strict:false ~reason x q
+        | Geq -> add_lower_bound t ~strict:false ~reason x q
+        | Lt -> add_upper_bound t ~strict:true ~reason x q
+        | Gt -> add_lower_bound t ~strict:true ~reason x q
+        | Eq -> add_bounds t (x,q,q)
+                  ~strict_lower:false ~strict_upper:false
+                  ~lower_reason:reason ~upper_reason:reason
+        | Neq -> assert false
+      end
 end
 
 module Make_full(V : VAR_GEN)