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