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 /*
20  * Parser for benchmarks in the SMT-LIB language.
21  */
22 
23 #ifndef __SMT_PARSER_H
24 #define __SMT_PARSER_H
25 
26 #include "parser_utils/parser.h"
27 
28 
29 /*
30  * The result of parsing is stored in the following structure:
31  *
32  * We keep track of whether any function or predicate is declared
33  * (with non-zero arity). This helps detecting incorrect/misleading
34  * logic labels (e.g. the bcnscheduling benchmarks are in QF_UFIDL but
35  * they are actually pure QF_IDL. They don't have functions or
36  * predicates.
37  */
38 typedef enum smt_stat {
39   smt_none,
40   smt_unsat,
41   smt_sat,
42   smt_unknown,
43 } smt_stat_t;
44 
45 
46 typedef struct smt_benchmark_s {
47   char *name;
48   char *logic_name;
49   int32_t logic_parameter; // used only for QF_UFBV[xx]
50   smt_stat_t status;
51   bool has_uf;        // true if the benchmark declares uninterpreted functions or predicates
52   uint32_t nformulas; // number of formulas and assumptions
53   uint32_t fsize;     // size of array formulas
54   term_t *formulas;   // the corresponding terms
55 } smt_benchmark_t;
56 
57 
58 
59 /*
60  * Minimal size of formulas array (allocated on the first addition)
61  */
62 #define MIN_FSIZE 20
63 
64 /*
65  * Maximal number of formulas
66  */
67 #define MAX_FSIZE (UINT32_MAX/sizeof(term_t))
68 
69 
70 /*
71  * Initialize a benchmark structure (all fields are given a default value).
72  */
73 extern void init_benchmark(smt_benchmark_t *bench);
74 
75 /*
76  * Delete: free all allocated memory
77  */
78 extern void delete_benchmark(smt_benchmark_t *bench);
79 
80 /*
81  * return -1 if there's an error, 0 otherwise
82  * if result is 0 then bench is filled in
83  */
84 extern int32_t parse_smt_benchmark(parser_t *parser, smt_benchmark_t *bench);
85 
86 
87 
88 #endif /* __SMT_PARSER_H */
89