| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | arith_eq_adapter.cpp | 89 … tout << mk_ismt2_pp(n1->get_owner(), m) << "\n" << mk_ismt2_pp(n2->get_owner(), m) << "\n";); in mk_axioms()
92 app * t1 = n1->get_owner(); in mk_axioms()
93 app * t2 = n2->get_owner(); in mk_axioms()
113 tout << mk_pp(n1->get_owner(), get_manager()) << "\n"; in mk_axioms()
114 tout << mk_pp(n2->get_owner(), get_manager()) << "\n"; in mk_axioms()
130 tout << "mk_detail " << mk_bounded_pp(n1->get_owner(), m, 5) << " " << in mk_axioms()
131 mk_bounded_pp(n2->get_owner(), m, 5) << "\n";); in mk_axioms()
225 …evancy_eh * eh = ctx.mk_relevancy_eh(arith_eq_relevancy_eh(n1->get_owner(), n2->get_owner(), t1_eq… in mk_axioms()
226 ctx.add_relevancy_eh(n1->get_owner(), eh); in mk_axioms()
227 ctx.add_relevancy_eh(n2->get_owner(), eh); in mk_axioms()
[all …]
|
| H A D | seq_offset_eq.cpp | 62 if (!seq.str.is_length(n1->get_owner(), e1)) in len_offset()
65 if (!seq.str.is_length(n2->get_owner(), e2)) in len_offset()
86 if (a.is_numeral(n->get_owner(), val) && val.is_int32() && INT_MIN < val.get_int32()) { in prop_arith_to_len_offset()
87 TRACE("seq", tout << "offset: " << mk_pp(n->get_owner(), m) << "\n";); in prop_arith_to_len_offset()
90 len_offset(next->get_owner(), val.get_int32()); in prop_arith_to_len_offset()
103 !a.is_numeral(n1->get_owner()) && in find()
104 !a.is_numeral(n2->get_owner()) && in find()
110 return !a.is_numeral(r->get_owner()) && m_has_offset_equality.contains(r); in contains()
|
| H A D | theory_array_base.h | 38 void found_unsupported_op(enode* n) { found_unsupported_op(n->get_owner()); } in found_unsupported_op()
39 void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_owner()); } in found_unsupported_op()
53 bool is_store(enode const * n) const { return is_store(n->get_owner()); } in is_store()
54 bool is_map(enode const* n) const { return is_map(n->get_owner()); } in is_map()
55 bool is_select(enode const* n) const { return is_select(n->get_owner()); } in is_select()
56 bool is_const(enode const* n) const { return is_const(n->get_owner()); } in is_const()
57 bool is_as_array(enode const * n) const { return is_as_array(n->get_owner()); } in is_as_array()
58 bool is_default(enode const* n) const { return is_default(n->get_owner()); } in is_default()
59 bool is_array_sort(enode const* n) const { return is_array_sort(n->get_owner()); } in is_array_sort()
60 bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_owner()); } in is_set_has_size()
[all …]
|
| H A D | theory_fpa.cpp | 296 SASSERT(m_fpa_util.is_float(n->get_owner()) || m_fpa_util.is_rm(n->get_owner())); in apply_sort_cnstr()
299 app * owner = n->get_owner(); in apply_sort_cnstr()
330 expr * xe = e_x->get_owner(); in new_eq_eh()
331 expr * ye = e_y->get_owner(); in new_eq_eh()
369 expr * xe = e_x->get_owner(); in new_diseq_eh()
370 expr * ye = e_y->get_owner(); in new_diseq_eh()
539 owner = get_ite_value(n->get_owner()); in mk_value()
660 mk_ismt2_pp(n->get_owner(), m) << std::endl; in display()
667 mk_ismt2_pp(n->get_owner(), m) << std::endl; in display()
672 expr * e = n->get_owner(); in display()
[all …]
|
| H A D | theory_array_full.cpp | 449 app* map = mp->get_owner(); in instantiate_select_map_axiom()
450 app* select = sl->get_owner(); in instantiate_select_map_axiom()
459 … tout << mk_ismt2_pp(sl->get_owner(), m) << "\n" << mk_ismt2_pp(mp->get_owner(), m) << "\n";); in instantiate_select_map_axiom()
516 app* map = mp->get_owner(); in instantiate_default_map_axiom()
547 expr* val = cnst->get_arg(0)->get_owner(); in instantiate_default_const_axiom()
548 expr* def = mk_default(cnst->get_owner()); in instantiate_default_const_axiom()
567 expr* def = mk_default(arr->get_owner()); in instantiate_default_as_array_axiom()
629 sel_args.push_back(cnst->get_owner()); in instantiate_select_const_axiom()
653 SASSERT(is_as_array(arr->get_owner())); in instantiate_select_as_array_axiom()
663 sel_args.push_back(arr->get_owner()); in instantiate_select_as_array_axiom()
[all …]
|
| H A D | smt_model_generator.cpp | 97 sort * s = m.get_sort(r->get_owner()); in mk_value_procs()
101 tout << mk_pp(r->get_owner(), m) << "\n";); in mk_value_procs()
137 expr * n = r->get_owner(); in mk_model_value()
139 sort * s = m.get_sort(r->get_owner()); in mk_model_value()
186 if (m.get_sort(r->get_owner()) != s) in visit_children()
212 tout << mk_pp(n->get_owner(), m) << "\n"; in visit_children()
309 tout << mk_pp(n->get_owner(), m) << "\n"; in mk_values()
310 sort * s = m.get_sort(n->get_owner()); in mk_values()
348 … << mk_pp(child->get_owner(), m) << " " << mk_pp(child->get_root()->get_owner(), m) << "\n";); in mk_values()
362 func_decl * d = n->get_owner()->get_decl(); in mk_values()
[all …]
|
| H A D | smt_context_inv.cpp | 163 … tout << mk_pp(n->get_owner(), m) << "\n" << mk_pp(n2->get_owner(), m) << "\n"; in check_missing_congruence()
174 if (m.is_bool(n->get_owner()) && get_assignment(n) == l_undef) { in check_missing_bool_enode_propagation()
178 … tout << mk_pp(first->get_owner(), m) << "\nassignment: " << get_assignment(first) << "\n" in check_missing_bool_enode_propagation()
179 … << mk_pp(n->get_owner(), m) << "\nassignment: " << get_assignment(n) << "\n";); in check_missing_bool_enode_propagation()
235 if (m.is_bool(e->get_owner())) { in check_eqc_bool_assignment()
238 tout << "#" << e->get_expr_id() << "\n" << mk_pp(e->get_owner(), m) << "\n"; in check_eqc_bool_assignment()
239 tout << "#" << r->get_expr_id() << "\n" << mk_pp(r->get_owner(), m) << "\n"; in check_eqc_bool_assignment()
273 … if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m.is_iff(n->get_owner())) { in check_th_diseq_propagation()
282 << mk_pp(m.get_sort(lhs->get_owner()), m) << "\n";); in check_th_diseq_propagation()
309 << mk_pp(n->get_owner(), m) << "\n" in check_th_diseq_propagation()
[all …]
|
| H A D | theory_array_base.cpp | 97 app * n = e->get_owner(); in assert_store_axiom1_core()
137 …tout << mk_bounded_pp(store->get_owner(), m) << "\n" << mk_bounded_pp(select->get_owner(), m) << "… in assert_store_axiom2_core()
148 sel2_args.push_back(a->get_owner()); in assert_store_axiom2_core()
182 literal ante = mk_eq(idx1->get_owner(), idx2->get_owner(), true); in assert_store_axiom2_core()
189 … tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m); in assert_store_axiom2_core()
316 app * e1 = n1->get_owner(); in assert_extensionality_core()
317 app * e2 = n2->get_owner(); in assert_extensionality_core()
354 app * e1 = n1->get_owner(); in assert_congruent_core()
355 app * e2 = n2->get_owner(); in assert_congruent_core()
575 app * eq = mk_eq_atom(n1->get_owner(), n2->get_owner()); in mk_interface_eqs()
[all …]
|
| /dports/devel/boost-docs/boost_1_72_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/devel/R-cran-BH/BH/inst/include/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/games/frogatto/frogatto-1.3.1/MacOSJet/boost/include/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/databases/percona57-pam-for-mysql/boost_1_59_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/math/stanmath/math-4.2.0/lib/boost_1.75.0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/science/py-scipy/scipy-1.7.1/scipy/_lib/boost/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w);
70 inline PyObject* get_owner(wrapper_base const volatile& w)
|
| /dports/databases/percona57-server/boost_1_59_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/databases/xtrabackup/boost_1_59_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/databases/percona57-client/boost_1_59_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/security/keybase/client-v5.7.1/shared/ios/Pods/boost-for-react-native/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/devel/boost-libs/boost_1_72_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/devel/boost-python-libs/boost_1_72_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/databases/mysql57-client/mysql-5.7.36/boost/boost_1_59_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/databases/mysqlwsrep57-server/boost_1_59_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/math/py-pystan/pystan-2.19.0.0/pystan/stan/lib/stan_math/lib/boost_1.69.0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/devel/hyperscan/boost_1_75_0/boost/python/detail/ |
| H A D | wrapper_base.hpp | 20 inline PyObject* get_owner(wrapper_base const volatile& w);
43 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
65 return wrapper_base_::get_owner(*w); in owner_impl()
70 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|
| /dports/biology/lamarc/lamarc-2.1.8/boost/python/detail/ |
| H A D | wrapper_base.hpp | 21 inline PyObject* get_owner(wrapper_base const volatile& w);
44 friend PyObject* wrapper_base_::get_owner(wrapper_base const volatile& w);
66 return wrapper_base_::get_owner(*w); in owner_impl()
71 inline PyObject* get_owner(wrapper_base const volatile& w) in get_owner() function
|