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