1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 #ifndef __CPUTIME_H
20 #define __CPUTIME_H
21
22
23 /*
24 * get_cpu_time() returns CPU time (user + system time) used
25 * by the process since its start. Unit = seconds.
26 */
27 extern double get_cpu_time(void);
28
29
30 /*
31 * When printing time differences (t1 - t2),
32 * it may happen that rounding errors cause the difference
33 * to be printed as -0, even though t1 should always be >= t2.
34 * To fix this use time_diff(t1, t2) rather than (t1 - t2)
35 */
time_diff(double t1,double t2)36 static inline double time_diff(double t1, double t2) {
37 double d;
38 d = t1 - t2;
39 return d < 0.00001 ? 0.0 : d;
40 }
41
42 #endif /* __CPUTIME_H */
43