仅从命令gtime获取执行时间

Question

我需要执行一个命令，并获得它的执行时间。我使用的是gtime，但输出与我想要的略有不同。

gtime返回执行结果，然后返回执行时间。我需要将命令的输出(我只需要它是时间)存储在一个变量中，并在以后使用它。有没有办法将命令更改为只获取执行时间？

所以如果我写下下面的命令：

executiontime=$(gtime -f "%U" /Users/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2)
echo "$executiontime"

下面是我得到的输出的一个例子：

sat

(objectives
 (misses_80 1)
)
9.94

Answer 1

要仅从输出中获取可执行时间，您可以通过以下方式修改命令：

executiontime=$(gtime -f "%U" /Users/ouafaelachhab/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2|tail -1)