| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | bv_decl_plugin.cpp | 160 parameter p(bv_size); in get_bv_sort()
170 if (bv_size == 0) { in mk_sort()
173 mk_bv_sort(bv_size); in mk_sort()
192 return decls[bv_size]; in mk_binary()
204 return decls[bv_size]; in mk_unary()
209 if (bv_size == 0) { in mk_int2bv()
257 return decls[bv_size]; in mk_pred()
419 if (bv_size == 0) { in mk_num_decl()
468 int bv_size; in mk_func_decl() local
575 int bv_size; in mk_func_decl() local
[all …]
|
| H A D | bv_decl_plugin.h | 208 void mk_bv_sort(unsigned bv_size);
209 sort * get_bv_sort(unsigned bv_size);
210 func_decl * mk_func_decl(decl_kind k, unsigned bv_size);
215 char const * name, unsigned bv_size);
217 func_decl * mk_comp(unsigned bv_size);
297 bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
378 … rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); } in norm() argument
379 bool has_sign_bit(rational const & n, unsigned bv_size) const;
393 app * mk_numeral(rational const & val, unsigned bv_size) const;
394 …app * mk_numeral(uint64_t u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui6… in mk_numeral() argument
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | bv_decl_plugin.cpp | 160 parameter p(bv_size); in get_bv_sort()
170 if (bv_size == 0) { in mk_sort()
173 mk_bv_sort(bv_size); in mk_sort()
192 return decls[bv_size]; in mk_binary()
204 return decls[bv_size]; in mk_unary()
209 if (bv_size == 0) { in mk_int2bv()
257 return decls[bv_size]; in mk_pred()
419 if (bv_size == 0) { in mk_num_decl()
468 int bv_size; in mk_func_decl() local
575 int bv_size; in mk_func_decl() local
[all …]
|
| H A D | bv_decl_plugin.h | 208 void mk_bv_sort(unsigned bv_size);
209 sort * get_bv_sort(unsigned bv_size);
210 func_decl * mk_func_decl(decl_kind k, unsigned bv_size);
215 char const * name, unsigned bv_size);
217 func_decl * mk_comp(unsigned bv_size);
297 bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
381 … rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); } in norm() argument
382 bool has_sign_bit(rational const & n, unsigned bv_size) const;
395 app * mk_numeral(rational const & val, unsigned bv_size) const;
396 …app * mk_numeral(uint64_t u, unsigned bv_size) const { return mk_numeral(rational(u, rational::ui6… in mk_numeral() argument
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | bv_rewriter.cpp | 993 expr * sign = m_mk_extract(bv_size-1, bv_size-1, arg1); in mk_bv_ashr()
1008 unsigned bv_size; in mk_bv_sdiv_core() local
1055 unsigned bv_size; in mk_bv_udiv_core() local
1112 unsigned bv_size; in mk_bv_srem_core() local
1157 unsigned bv_size; in is_minus_one_core() local
1166 unsigned bv_size; in is_negatable() local
1196 unsigned bv_size; in mk_bv_urem_core() local
1293 unsigned bv_size; in mk_bv_smod_core() local
1561 unsigned bv_size; in mk_sign_extend() local
1972 unsigned bv_size; in mk_bv_not() local
[all …]
|
| H A D | enum2bv_rewriter.cpp | 64 unsigned bv_size = get_bv_size(s); in value2bv() local
65 sort_ref bv_sort(m_bv.mk_sort(bv_size), m); in value2bv()
141 unsigned bv_size = get_bv_size(s); in reduce_arg() local
142 sort_ref bv_sort(m_bv.mk_sort(bv_size), m); in reduce_arg()
145 result = m.mk_var(to_var(a)->get_idx(), m_bv.mk_sort(bv_size)); in reduce_arg()
203 unsigned bv_size = get_bv_size(s); in reduce_quantifier() local
204 sort* bv_sort = m_bv.mk_sort(bv_size); in reduce_quantifier()
245 unsigned bv_size = 1; in get_bv_size() local
246 while ((unsigned)(1 << bv_size) < nc) { in get_bv_size()
247 ++bv_size; in get_bv_size()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | bv_rewriter.cpp | 993 expr * sign = m_mk_extract(bv_size-1, bv_size-1, arg1); in mk_bv_ashr()
1008 unsigned bv_size; in mk_bv_sdiv_core() local
1055 unsigned bv_size; in mk_bv_udiv_core() local
1112 unsigned bv_size; in mk_bv_srem_core() local
1157 unsigned bv_size; in is_minus_one_core() local
1166 unsigned bv_size; in is_negatable() local
1196 unsigned bv_size; in mk_bv_urem_core() local
1293 unsigned bv_size; in mk_bv_smod_core() local
1561 unsigned bv_size; in mk_sign_extend() local
1972 unsigned bv_size; in mk_bv_not() local
[all …]
|
| H A D | enum2bv_rewriter.cpp | 107 unsigned bv_size = get_bv_size(s); in reduce_arg() local
110 result = m.mk_var(to_var(a)->get_idx(), m_bv.mk_sort(bv_size)); in reduce_arg()
117 result = m_bv.mk_numeral(idx, bv_size); in reduce_arg()
128 result = m.mk_fresh_const(f->get_name(), m_bv.mk_sort(bv_size)); in reduce_arg()
131 m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size))); in reduce_arg()
171 unsigned bv_size = get_bv_size(s); in reduce_quantifier() local
172 m_sorts.push_back(m_bv.mk_sort(bv_size)); in reduce_quantifier()
212 unsigned bv_size = 1; in get_bv_size() local
213 while ((unsigned)(1 << bv_size) < nc) { in get_bv_size()
214 ++bv_size; in get_bv_size()
[all …]
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
| H A D | bitvector_theorem_producer.cpp | 4940 int chopSize = bv_size; in liftConcatBVPlus()
5172 int chopSize = bv_size; in chopConcat()
5375 nbits = bv_size - lg; in buildPlusTerm()
5395 bits = bv_size; in buildPlusTerm()
5415 bits = bv_size; in buildPlusTerm()
5416 size = bv_size; in buildPlusTerm()
5481 int bits = bv_size; in buildPlusTerm()
5729 DebugAssert(lsize <= bv_size && rsize <= bv_size, "invariant violated"); in canonBVEQ()
5758 Expr tmp = d_theoryBitvector->newBVExtractExpr(lhs, bv_size-1, bv_size-splitSize); in canonBVEQ()
5933 if (bv_size > 1) { in canonBVEQ()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/util/ |
| H A D | sexpr.cpp | 132 unsigned bv_size = static_cast<sexpr_bv const *>(this)->m_size; in display_atom() local
136 if (bv_size % 4 == 0) { in display_atom()
148 while (sz < bv_size) { in display_atom()
165 while (sz < bv_size) { in display_atom()
276 sexpr * sexpr_manager::mk_bv_numeral(rational const & val, unsigned bv_size, unsigned line, unsigne… in mk_bv_numeral() argument
277 return new (m_allocator.allocate(sizeof(sexpr_bv))) sexpr_bv(val, bv_size, line, pos); in mk_bv_numeral()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/util/ |
| H A D | sexpr.cpp | 132 unsigned bv_size = static_cast<sexpr_bv const *>(this)->m_size; in display_atom() local
136 if (bv_size % 4 == 0) { in display_atom()
148 while (sz < bv_size) { in display_atom()
165 while (sz < bv_size) { in display_atom()
274 sexpr * sexpr_manager::mk_bv_numeral(rational const & val, unsigned bv_size, unsigned line, unsigne… in mk_bv_numeral() argument
275 return new (m_allocator.allocate(sizeof(sexpr_bv))) sexpr_bv(val, bv_size, line, pos); in mk_bv_numeral()
|
| /dports/science/hdf/hdf-4.2.15/hdf/test/ |
| H A D | tbv.c | 56 size=bv_size(b); in test_1()
68 size=bv_size(b); in test_1()
91 size=bv_size(b); in test_2()
121 size=bv_size(b); in test_2()
164 size=bv_size(b); in test_3()
|
| /dports/math/z3/z3-z3-4.8.13/src/model/ |
| H A D | numeral_factory.cpp | 50 app * bv_factory::mk_num_value(rational const & val, unsigned bv_size) { in mk_num_value() argument
51 return numeral_factory::mk_value(val, m_util.mk_sort(bv_size)); in mk_num_value()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/model/ |
| H A D | numeral_factory.cpp | 50 app * bv_factory::mk_num_value(rational const & val, unsigned bv_size) { in mk_num_value() argument
51 return numeral_factory::mk_value(val, m_util.mk_sort(bv_size)); in mk_num_value()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/smtlogics/ |
| H A D | qfnra_tactic.cpp | 26 static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) { in mk_qfnra_sat_solver() argument
28 nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size)); in mk_qfnra_sat_solver()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/smtlogics/ |
| H A D | qfnra_tactic.cpp | 26 static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) { in mk_qfnra_sat_solver() argument
28 nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size)); in mk_qfnra_sat_solver()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/bit_blaster/ |
| H A D | bit_blaster_rewriter.cpp | 153 unsigned bv_size = butil().get_bv_size(t); in get_bits() local
154 for (unsigned i = 0; i < bv_size; i++) { in get_bits()
158 SASSERT(bv_size == out_bits.size()); in get_bits()
225 unsigned bv_size = butil().get_bv_size(s); in mk_const() local
228 for (unsigned i = 0; i < bv_size; i++) { in mk_const()
370 unsigned bv_size = butil().get_bv_size(t); in blast_bv_term() local
371 for (unsigned i = 0; i < bv_size; i++) { in blast_bv_term()
578 unsigned bv_size = butil().get_bv_size(s); in pre_visit() local
580 for (unsigned k = 0; k < bv_size; k++) { in pre_visit()
654 unsigned bv_size = butil().get_bv_size(s); in reduce_quantifier() local
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/bit_blaster/ |
| H A D | bit_blaster_rewriter.cpp | 156 unsigned bv_size = butil().get_bv_size(t); in get_bits() local
157 for (unsigned i = 0; i < bv_size; i++) { in get_bits()
161 SASSERT(bv_size == out_bits.size()); in get_bits()
228 unsigned bv_size = butil().get_bv_size(s); in mk_const() local
231 for (unsigned i = 0; i < bv_size; i++) { in mk_const()
369 unsigned bv_size = butil().get_bv_size(t); in blast_bv_term() local
370 for (unsigned i = 0; i < bv_size; i++) { in blast_bv_term()
574 unsigned bv_size = butil().get_bv_size(s); in pre_visit() local
576 for (unsigned k = 0; k < bv_size; k++) { in pre_visit()
650 unsigned bv_size = butil().get_bv_size(s); in reduce_quantifier() local
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/opt/ |
| H A D | opt_sls_solver.h | 129 unsigned bv_size = maxval.get_num_bits(); in soft2bv() local
130 zero = bv.mk_numeral(rational(0), bv_size); in soft2bv()
133 es.push_back(m.mk_ite(tmp, bv.mk_numeral(den*weights[i], bv_size), zero)); in soft2bv()
136 objective = bv.mk_numeral(0, bv_size); in soft2bv()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/opt/ |
| H A D | opt_sls_solver.h | 129 unsigned bv_size = maxval.get_num_bits(); in soft2bv() local
130 zero = bv.mk_numeral(rational(0), bv_size); in soft2bv()
133 es.push_back(m.mk_ite(tmp, bv.mk_numeral(den*weights[i], bv_size), zero)); in soft2bv()
136 objective = bv.mk_numeral(0, bv_size); in soft2bv()
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | qe_bv_plugin.cpp | 61 unsigned bv_size; in project() local
63 m_bv.is_numeral(val_x, val, bv_size); in project()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | qe_bv_plugin.cpp | 61 unsigned bv_size; in project() local
63 m_bv.is_numeral(val_x, val, bv_size); in project()
|
| /dports/math/py-pysmt/pysmt-0.9.0/examples/sudoku/ |
| H A D | sudoku.py | 30 self.bv_size = int(math.floor(math.log(self.size**2, 2))) + 1
43 return typing.BVType(self.bv_size)
50 return BV(value, self.bv_size)
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/bv/ |
| H A D | bv1_blaster_tactic.cpp | 101 unsigned bv_size = butil().get_bv_size(s); in mk_const() local
102 if (bv_size == 1) { in mk_const()
108 for (unsigned i = 0; i < bv_size; i++) { in mk_const()
120 unsigned bv_size = butil().get_bv_size(t); in blast_bv_term() local
121 if (bv_size == 1) { in blast_bv_term()
125 unsigned i = bv_size; in blast_bv_term()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/bv/ |
| H A D | bv1_blaster_tactic.cpp | 101 unsigned bv_size = butil().get_bv_size(s); in mk_const() local
102 if (bv_size == 1) { in mk_const()
108 for (unsigned i = 0; i < bv_size; i++) { in mk_const()
120 unsigned bv_size = butil().get_bv_size(t); in blast_bv_term() local
121 if (bv_size == 1) { in blast_bv_term()
125 unsigned i = bv_size; in blast_bv_term()
|