| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | array_decl_plugin.cpp | 606 bool array_decl_plugin::is_fully_interp(sort * s) const { in is_fully_interp() function in array_decl_plugin
610 if (!m_manager->is_fully_interp(get_array_domain(s, i))) in is_fully_interp()
613 return m_manager->is_fully_interp(get_array_range(s)); in is_fully_interp()
|
| H A D | datatype_decl_plugin.h | 231 bool is_fully_interp(sort * s) const override;
376 bool is_fully_interp(sort * s) const;
|
| H A D | datatype_decl_plugin.cpp | 647 bool plugin::is_fully_interp(sort * s) const { in is_fully_interp() function in datatype::decl::plugin
648 return u().is_fully_interp(s); in is_fully_interp()
671 bool util::is_fully_interp(sort * s) const { in is_fully_interp() function in datatype::util
688 if (!m.is_fully_interp(r)) { in is_fully_interp()
|
| H A D | array_decl_plugin.h | 137 bool is_fully_interp(sort * s) const override;
|
| H A D | recfun_decl_plugin.h | 171 … bool is_fully_interp(sort * s) const override { return false; } // might depend on unin sorts in is_fully_interp() function
|
| H A D | ast.h | 1080 virtual bool is_fully_interp(sort * s) const { return true; } in is_fully_interp() function
1715 bool is_fully_interp(sort * s) const;
|
| H A D | ast.cpp | 2680 bool ast_manager::is_fully_interp(sort * s) const { in is_fully_interp() function in ast_manager
2687 return p->is_fully_interp(s); in is_fully_interp()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | array_decl_plugin.cpp | 606 bool array_decl_plugin::is_fully_interp(sort * s) const { in is_fully_interp() function in array_decl_plugin
610 if (!m_manager->is_fully_interp(get_array_domain(s, i))) in is_fully_interp()
613 return m_manager->is_fully_interp(get_array_range(s)); in is_fully_interp()
|
| H A D | datatype_decl_plugin.h | 234 bool is_fully_interp(sort * s) const override;
373 bool is_fully_interp(sort * s) const;
|
| H A D | recfun_decl_plugin.h | 169 … bool is_fully_interp(sort * s) const override { return false; } // might depend on unin sorts in is_fully_interp() function
|
| H A D | datatype_decl_plugin.cpp | 629 bool plugin::is_fully_interp(sort * s) const { in is_fully_interp() function in datatype::decl::plugin
630 return u().is_fully_interp(s); in is_fully_interp()
644 bool util::is_fully_interp(sort * s) const { in is_fully_interp() function in datatype::util
661 if (!m.is_fully_interp(r)) { in is_fully_interp()
|
| H A D | array_decl_plugin.h | 137 bool is_fully_interp(sort * s) const override;
|
| H A D | ast.h | 1077 virtual bool is_fully_interp(sort * s) const { return true; } in is_fully_interp() function
1778 bool is_fully_interp(sort * s) const;
|
| H A D | ast.cpp | 2758 bool ast_manager::is_fully_interp(sort * s) const { in is_fully_interp() function in ast_manager
2765 return p->is_fully_interp(s); in is_fully_interp()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
| H A D | elim_uncnstr_tactic.cpp | 244 if (!m().is_fully_interp(s)) in process_eq()
689 if (!m().is_fully_interp(c->get_domain(i))) in process_datatype_app()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/ |
| H A D | elim_uncnstr_tactic.cpp | 243 if (!m().is_fully_interp(s)) in process_eq()
688 if (!m().is_fully_interp(c->get_domain(i))) in process_datatype_app()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_model_finder.cpp | 994 if (m.is_fully_interp(ns)) { in add_elem_to_empty_inst_sets()
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | qe_lite.cpp | 619 if (!m.is_fully_interp(s) || !s->get_num_elements().is_infinite()) return false; in is_unconstrained()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | qe_lite.cpp | 619 if (!m.is_fully_interp(s) || !s->get_num_elements().is_infinite()) return false; in is_unconstrained()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_model_finder.cpp | 951 if (m.is_fully_interp(ns)) { in add_elem_to_empty_inst_sets()
|