Lines Matching defs:btor
42 static BoolectorSort get_sort(Btor *btor, struct symbol *type, struct position pos)
48 return boolector_bitvec_sort(btor, type->bit_size);
51 static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
62 return boolector_consth(btor, s, buff);
65 n = boolector_var(btor, s, show_pseudo(pseudo));
74 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
78 BoolectorSort s = get_sort(btor, type, insn->pos);
80 return mkvar(btor, s, arg);
83 static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s)
85 int old = boolector_get_width(btor, s);
87 return boolector_uext(btor, s, new - old);
90 static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s)
92 int old = boolector_get_width(btor, s);
94 return boolector_sext(btor, s, new - old);
97 static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s)
99 int old = boolector_get_width(btor, s);
101 return boolector_slice(btor, s, old - new - 1, 0);
104 static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
108 a = mkvar(btor, s, insn->src1);
109 b = mkvar(btor, s, insn->src2);
113 case OP_ADD: t = boolector_add(btor, a, b); break;
114 case OP_SUB: t = boolector_sub(btor, a, b); break;
115 case OP_MUL: t = boolector_mul(btor, a, b); break;
116 case OP_AND: t = boolector_and(btor, a, b); break;
117 case OP_OR: t = boolector_or (btor, a, b); break;
118 case OP_XOR: t = boolector_xor(btor, a, b); break;
119 case OP_SHL: t = boolector_sll(btor, a, b); break;
120 case OP_LSR: t = boolector_srl(btor, a, b); break;
121 case OP_ASR: t = boolector_sra(btor, a, b); break;
122 case OP_DIVS: t = boolector_sdiv(btor, a, b); break;
123 case OP_DIVU: t = boolector_udiv(btor, a, b); break;
124 case OP_MODS: t = boolector_srem(btor, a, b); break;
125 case OP_MODU: t = boolector_urem(btor, a, b); break;
126 case OP_SET_EQ: t = zext(btor, insn, boolector_eq(btor, a, b)); break;
127 case OP_SET_NE: t = zext(btor, insn, boolector_ne(btor, a, b)); break;
128 case OP_SET_LT: t = zext(btor, insn, boolector_slt(btor, a, b)); break;
129 case OP_SET_LE: t = zext(btor, insn, boolector_slte(btor, a, b)); break;
130 case OP_SET_GE: t = zext(btor, insn, boolector_sgte(btor, a, b)); break;
131 case OP_SET_GT: t = zext(btor, insn, boolector_sgt(btor, a, b)); break;
132 case OP_SET_B: t = zext(btor, insn, boolector_ult(btor, a, b)); break;
133 case OP_SET_BE: t = zext(btor, insn, boolector_ulte(btor, a, b)); break;
134 case OP_SET_AE: t = zext(btor, insn, boolector_ugte(btor, a, b)); break;
135 case OP_SET_A: t = zext(btor, insn, boolector_ugt(btor, a, b)); break;
143 static void binop(Btor *btor, struct instruction *insn)
145 BoolectorSort s = get_sort(btor, insn->type, insn->pos);
146 binary(btor, s, insn);
149 static void icmp(Btor *btor, struct instruction *insn)
151 BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
152 binary(btor, s, insn);
155 static void unop(Btor *btor, struct instruction *insn)
157 BoolectorSort s = get_sort(btor, insn->type, insn->pos);
160 a = mkvar(btor, s, insn->src1);
164 case OP_NEG: t = boolector_neg(btor, a); break;
165 case OP_NOT: t = boolector_not(btor, a); break;
166 case OP_SEXT: t = sext(btor, insn, a); break;
167 case OP_ZEXT: t = zext(btor, insn, a); break;
168 case OP_TRUNC: t = slice(btor, insn, a); break;
176 static void ternop(Btor *btor, struct instruction *insn)
178 BoolectorSort s = get_sort(btor, insn->type, insn->pos);
181 a = mkvar(btor, s, insn->src1);
182 b = mkvar(btor, s, insn->src2);
183 c = mkvar(btor, s, insn->src3);
188 z = boolector_zero(btor, s);
189 d = boolector_ne(btor, a, z);
190 t = boolector_cond(btor, d, b, c);
199 static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
201 BoolectorNode *a = get_arg(btor, insn, 0);
202 BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
203 BoolectorNode *n = boolector_ne(btor, a, z);
204 BoolectorNode *p = boolector_and(btor, *pre, n);
209 static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
211 char model_format[] = "btor";
214 n = boolector_implies(btor, p, n);
215 boolector_assert(btor, boolector_not(btor, n));
216 res = boolector_sat(btor);
223 boolector_dump_btor(btor, stdout);
224 boolector_print_model(btor, model_format, stdout);
233 static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
235 BoolectorNode *a = get_arg(btor, insn, 0);
236 BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
237 BoolectorNode *n = boolector_ne(btor, a, z);
238 return check_btor(btor, pre, n, insn);
241 static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
243 BoolectorNode *a = get_arg(btor, insn, 0);
244 BoolectorNode *b = get_arg(btor, insn, 1);
245 BoolectorNode *n = boolector_eq(btor, a, b);
246 return check_btor(btor, pre, n, insn);
265 static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
271 return add_precondition(btor, pre, insn);
273 return check_assert(btor, *pre, insn);
275 return check_equal(btor, *pre, insn);
277 return check_const(btor, insn);
283 Btor *btor = boolector_new();
284 BoolectorNode *pre = boolector_true(btor);
288 boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
289 boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
300 binop(btor, insn);
303 icmp(btor, insn);
306 unop(btor, insn);
309 ternop(btor, insn);
312 rc &= check_call(btor, &pre, insn);
325 boolector_release_all(btor);
326 boolector_delete(btor);