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 * BOOLEAN VARIABLES AND LITERALS
21 */
22
23 #ifndef __SMT_CORE_BASE_TYPES_H
24 #define __SMT_CORE_BASE_TYPES_H
25
26 #include <stdint.h>
27 #include <stdbool.h>
28 #include <assert.h>
29
30
31 /*
32 * Boolean variables: integers between 0 and nvars - 1
33 * Literals: integers between 0 and 2nvar - 1.
34 *
35 * For a variable x, the positive literal is 2x, the negative
36 * literal is 2x + 1.
37 *
38 * -1 is a special marker for both variables and literals
39 *
40 * Two literals representing the constant true/false are created
41 * when the solver is initialized.
42 */
43 typedef int32_t bvar_t;
44 typedef int32_t literal_t;
45
46 enum {
47 // markers
48 null_bvar = -1,
49 null_literal = -1,
50
51 // boolean constants
52 const_bvar = 0,
53 true_literal = 0,
54 false_literal = 1,
55 };
56
57
58 /*
59 * Maximal number of boolean variables
60 */
61 #define MAX_VARIABLES (INT32_MAX >> 2)
62
63 /*
64 * Conversions from variables to literals
65 */
pos_lit(bvar_t x)66 static inline literal_t pos_lit(bvar_t x) {
67 return x<<1;
68 }
69
neg_lit(bvar_t x)70 static inline literal_t neg_lit(bvar_t x) {
71 return (x<<1) | 1;
72 }
73
74 /*
75 * mk_lit(x, 0) = pos_lit(x)
76 * mk_lit(x, 1) = neg_lit(x)
77 */
mk_lit(bvar_t x,uint32_t sign)78 static inline literal_t mk_lit(bvar_t x, uint32_t sign) {
79 assert((sign & ~1) == 0);
80 return (x<<1)|sign;
81 }
82
83
84 /*
85 * Extract variable and sign
86 */
var_of(literal_t l)87 static inline bvar_t var_of(literal_t l) {
88 return l>>1;
89 }
90
sign_of_lit(literal_t l)91 static inline uint32_t sign_of_lit(literal_t l) {
92 return ((uint32_t) l) & 1;
93 }
94
95
96 // true if l has positive polarity (i.e., l = pos_lit(x))
is_pos(literal_t l)97 static inline bool is_pos(literal_t l) {
98 return !(l & 1);
99 }
100
is_neg(literal_t l)101 static inline bool is_neg(literal_t l) {
102 return (l & 1);
103 }
104
105
106 // negation of literal l
not(literal_t l)107 static inline literal_t not(literal_t l) {
108 return l ^ 1;
109 }
110
111 // check whether l1 and l2 are opposite
opposite(literal_t l1,literal_t l2)112 static inline bool opposite(literal_t l1, literal_t l2) {
113 return (l1 ^ l2) == 1;
114 }
115
116
117 /*
118 * add polarity tt to l:
119 * - if tt is true return l
120 * - if tt is false, return (not l)
121 */
signed_literal(literal_t l,bool tt)122 static inline literal_t signed_literal(literal_t l, bool tt) {
123 return l ^ (((int32_t) tt) ^ 1);
124 }
125
126
127 /*
128 * Variant of mk_lit that takes a boolean polarity instead of
129 * a sign:
130 * - mk_signed_lit(x, true) = mk_lit(x, 0) = pos_lit(x)
131 * - mk_signed_lit(x, false) = mk_lit(x, 1) = neg_lit(x)
132 */
mk_signed_lit(bvar_t x,bool tt)133 static inline literal_t mk_signed_lit(bvar_t x, bool tt) {
134 return (x << 1) | (tt ^ 1);
135 }
136
137
138 /*
139 * Remove the sign of l (i.e., force the sign bit to 0)
140 * - if l is pos_lit(x) return l
141 * - if l is neg_lit(x) return not(l)
142 */
unsigned_literal(literal_t l)143 static inline literal_t unsigned_literal(literal_t l) {
144 return l & ~1;
145 }
146
147
148 /*
149 * Conversion from boolean to literals
150 * - bool2literal(true) = true_literal
151 * - bool2literal(false) = false_literal
152 */
bool2literal(bool tt)153 static inline literal_t bool2literal(bool tt) {
154 return ((int32_t) tt) ^ 1;
155 }
156
157
158
159 /*
160 * Assignment values for a literal or variable
161 * - we use four values to encode the truth value of x
162 * when x is assigned, and the preferred value when x is
163 * not assigned.
164 * - value[x] is interpreted as follows
165 * VAL_UNDEF_FALSE = 0b00 --> x not assigned, preferred value = false
166 * VAL_UNDEF_TRUE = 0b01 --> x not assigned, preferred value = true
167 * VAL_FALSE = 0b10 --> x assigned false
168 * VAL_TRUE = 0b11 --> x assigned true
169 *
170 * The preferred value is used when x is selected as a decision variable.
171 * Then we assign x to true or false depending on the preferred value.
172 * This is done by setting bit 1 in value[x].
173 */
174 typedef enum bval {
175 VAL_UNDEF_FALSE = 0,
176 VAL_UNDEF_TRUE = 1,
177 VAL_FALSE = 2,
178 VAL_TRUE = 3,
179 } bval_t;
180
181
182 /*
183 * Check on boolean values
184 */
bval_is_undef(bval_t v)185 static inline bool bval_is_undef(bval_t v) { // bit 1 is unset
186 return (v & 2) == 0;
187 }
188
bval_is_def(bval_t v)189 static inline bool bval_is_def(bval_t v) { // bit 1 is set
190 return (v & 2) != 0;
191 }
192
193
194 // check whether val is val_undef_true or val_true
true_preferred(bval_t val)195 static inline bool true_preferred(bval_t val) {
196 return (val & 0x1) != 0;
197 }
198
199 // opposite value of v: flip the low order bit
opposite_val(bval_t val)200 static inline bval_t opposite_val(bval_t val) {
201 return val ^ 1;
202 }
203
204 /*
205 * Convert to a Boolean (extract the low-order bit)
206 */
bval2bool(bval_t v)207 static inline bool bval2bool(bval_t v) {
208 return v & 1;
209 }
210
211
212 #endif /* __SMT_CORE_BASE_TYPES_H */
213