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 * CONDITIONALS 21 */ 22 23 /* 24 * By a conditional, we mean a generalization of if-then-else to 25 * multiple conditions. Something semantically equivalent to 26 * 27 * if c1 then t1 28 * if c2 then t2 29 * ... 30 * if c_n then t_n 31 * else t_0 32 * 33 * provided the conditions c_1 ... c_n are pairwise disjoint (i.e. 34 * for any i/=j, c_i /\ c_j is false). This is a common pattern 35 * that's normally written using nested if-then-elses. 36 * 37 * Converting a nested if-then-else to a conditional leads to 38 * a nicer conversion to CNF. 39 */ 40 41 #ifndef __CONDITIONALS_H 42 #define __CONDITIONALS_H 43 44 45 #include <stdint.h> 46 47 #include "terms/terms.h" 48 49 50 /* 51 * Data structure to represent conditionals 52 * - terms = pointer to the relevant term table 53 * - nconds = number of pairs [c_i, t_i] 54 * - size = size of the pair array 55 * - defval = default value = t_0 56 * - array of pairs condition, value 57 * where both conditions and value are terms 58 */ 59 typedef struct cond_pair_s { 60 term_t cond; 61 term_t val; 62 } cond_pair_t; 63 64 typedef struct conditional_s { 65 term_table_t *terms; 66 cond_pair_t *pair; 67 term_t defval; 68 uint32_t nconds; 69 uint32_t size; 70 } conditional_t; 71 72 #define DEF_CONDITIONAL_SIZE 10 73 #define MAX_CONDITIONAL_SIZE (UINT32_MAX/sizeof(cond_pair_t)) 74 75 76 /* 77 * Initialize: 78 * - empty pair array 79 * - defval = NULL_TERM 80 */ 81 extern void init_conditional(conditional_t *d, term_table_t *terms); 82 83 /* 84 * Delete: free the array 85 */ 86 extern void delete_conditional(conditional_t *d); 87 88 /* 89 * Reset: reset defval to NULL_TERM and nconds to 0, but don't 90 * delete the array 91 */ 92 extern void reset_conditional(conditional_t *d); 93 94 95 96 /* 97 * Convert term t to a conditional; store the result in d 98 * - d is reset first 99 * - t must be a valid term defined in d->terms 100 * - if t is not an if-then-else term, the result is 101 * d->nconds = 0 102 * d->defval = t 103 * - if t is (ite c a b) then the conversion depends on whether 104 * a or b is an if-then-else term. 105 */ 106 extern void convert_term_to_conditional(conditional_t *d, term_t t); 107 108 109 /* 110 * Variant: convert (if c a b) to a conditional 111 */ 112 extern void convert_ite_to_conditional(conditional_t *d, term_t c, term_t a, term_t b); 113 114 115 116 #endif /* __CONDITIONALS_H */ 117