Add support for properties between vars.

property.ml

@@ -77,11 +77,16 @@ let rec repr t =
     | Float f -> Format.sprintf "float %f" f
   in
   match t with
-  | Atomic (var, cop, cst) ->
+  | Atomic_cst (var, cop, cst) ->
     let var_s = string_of_var var in
     let cop_s = string_of_cop cop in
     let cst_s = string_of_cst cst in
     Format.sprintf "%s %s %s" var_s cop_s cst_s
+  | Atomic_var (var1, cop, var2) ->
+    let var1_s = string_of_var var1 in
+    let cop_s = string_of_cop cop in
+    let var2_s = string_of_var var2 in
+    Format.sprintf "%s %s %s" var1_s cop_s var2_s
   | And (p1, p2) ->
     Format.sprintf "And (%s, %s)" (repr p1) (repr p2)
 

property_parser.mly

@@ -27,7 +27,9 @@ main:
 
 property:
 | var cop cst
-    { Atomic ($1, $2, $3) }
+    { Atomic_cst ($1, $2, $3) }
+| var cop var
+    { Atomic_var ($1, $2, $3) }
 
 var:
 | i = INPUT

property_syntax.mli

@@ -15,5 +15,6 @@ type cst =
   | Float of float
 
 type t =
-  | Atomic of var * cop * cst
+  | Atomic_cst of var * cop * cst
+  | Atomic_var of var * cop * var
   | And of t * t

solver.ml

@@ -33,8 +33,10 @@ let rec pp_property_marabou property =
     | Float f -> Stdlib.string_of_float f
   in
   match property with
-  | Atomic ((Input v | Output v), cop, cst) ->
+  | Atomic_cst ((Input v | Output v), cop, cst) ->
     Format.sprintf "%s %s %s" v (string_of_cop cop) (string_of_cst cst)
+  | Atomic_var ((Input v1 | Output v1), cop, (Input v2 | Output v2)) ->
+    Format.sprintf "%s %s %s" v1 (string_of_cop cop) v2
   | And (p1, p2) ->
     let s1 = pp_property_marabou p1 in
     let s2 = pp_property_marabou p2 in