Merge pull request #1074 from daniel-larraz/mult-two-polys-error

Handle non-linear terms gracefully in to_presburger

src/qe/poly.ml

@@ -16,6 +16,8 @@
 
 *)
 
+exception Not_in_LIA
+
 type psummand = Numeral.t * (Var.t option)
 
 type poly = psummand list
@@ -370,7 +372,8 @@ let multiply_two_polys (pt1: poly) (pt2: poly) : poly =
     | _, [(i, None)] -> poly_times_num pt1 i
 
     | _ ->
-      failwith "Can only multiply two polys when at least one of them is constant."
+      (* failwith "Can only multiply two polys when at least one of them is constant." *)
+      raise Not_in_LIA
 
 (*
 (* Multiply up a list of presburger terms of at least one element. *)

src/qe/poly.mli

@@ -23,6 +23,8 @@
     @author Ruoyu Zhang
 *)
 
+exception Not_in_LIA
+
 (** psummand is a constant or a variable with coefficient *)
 type psummand = Numeral.t * (Var.t option)
 

src/qe/presburger.ml

@@ -88,7 +88,10 @@ let multiply_iformula_list (ifl: iformula list) : poly =
       List.fold_left 
         (fun accum e ->
           match accum, e with
-            | pl1, (Poly pl2) -> multiply_two_polys pl1 pl2
+            | pl1, (Poly pl2) -> (
+              try multiply_two_polys pl1 pl2
+              with Poly.Not_in_LIA -> raise Not_in_LIA
+            )
             | _ -> 
               failwith "multiply_iformula_list can only multiply polynomials.")
         pl 

tests/regression/success/mult_two_polys.lus

@@ -0,0 +1,24 @@
+node s2 (n: int) returns (x: int);
+var n0: int;
+let
+  n0 = n -> pre n0;
+  x = n0 -> pre x + n0;
+tel
+
+node s3 (n: int) returns (x: int);
+var mult: int;
+var n0: int;
+let
+  mult = 1 -> pre mult + 1;
+  n0 = n -> pre n0;
+  x = n0 * mult;
+tel
+
+node check_s3 (n: int) returns (x: bool);
+var x1: int;
+var x2: int;
+let 
+  x1 = s2(n);
+  x2 = s3(n);
+  check x1 = x2;
+tel