[Marabou] Support relational constraints between two variables.

src/printers/marabou.ml

@@ -53,6 +53,33 @@ let rec print_term info fmt t =
     Printer.unsupportedTerm t "Not supported by Marabou"
   | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
   | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
+  | Tapp (ls, [ { t_node = Tapp (ls1, []); _ }; { t_node = Tapp (ls2, []); _ } ])
+    -> (
+    (* Marabou accepts only constraints of the form 't1 relop t2' where t1 must
+       be a sequence of variables, each with a {+,-} symbol upfront, while t2
+       must be a single fp constant. If t1 is a single variable and t2 a fp
+       constant, t1 may not exhibit a + symbol.
+
+       Whenever t2 is not a fp constant, t2 needs to be aggregated to t1.
+
+       FIXME: This code handles only t1 and t2 single variables w/o {+,-}
+       symbols as it prints something of the form '+t1 -t2 relop 0'. That is,
+       assumptions on t1 and t2 abound. *)
+    match
+      ( Term.Hls.find_opt info.variables ls1,
+        Term.Hls.find_opt info.variables ls2 )
+    with
+    | Some s1, Some s2 ->
+      if Term.ls_equal ls info.le
+      then Fmt.pf fmt "+%s -%s <= 0" s1 s2
+      else if Term.ls_equal ls info.ge
+      then Fmt.pf fmt "+%s -%s >= 0" s1 s2
+      else if Term.ls_equal ls info.lt
+      then Fmt.pf fmt "+%s -%s < 0" s1 s2
+      else if Term.ls_equal ls info.gt
+      then Fmt.pf fmt "+%s -%s > 0" s1 s2
+      else Printer.unsupportedTerm t "Unknown relational operator"
+    | _ -> Printer.unsupportedTerm t "Unknown variable(s)")
   | Tapp (ls, l) -> (
     match Printer.query_syntax info.info_syn ls.ls_name with
     | Some s -> Printer.syntax_arguments s (print_term info) fmt l

tests/marabou.t

@@ -32,7 +32,13 @@ Test verify
   >      (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
   >      let (y1,y2,_,_,_) = net_apply x1 x2 x3 x4 x5 in
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
+  > 
+  >   goal I: forall x1 x2 x3 x4 x5.
+  >      (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
+  >      let (y1,y2,_,_,_) = net_apply x1 x2 x3 x4 x5 in
+  >      y2 .< y1 \/ y1 .< y2
   > end
   > EOF
   [caisar] Goal G: Unknown ()
   [caisar] Goal H: Unknown ()
+  [caisar] Goal I: Unknown ()