| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_rule_subsumption_index.cpp | 57 bool rule_subsumption_index::is_subsumed(app * query) { in is_subsumed() function in datalog::rule_subsumption_index
69 bool rule_subsumption_index::is_subsumed(rule * r) { in is_subsumed() function in datalog::rule_subsumption_index
72 if(is_subsumed(head)) { in is_subsumed()
|
| H A D | dl_rule_subsumption_index.h | 57 bool is_subsumed(rule * r);
58 bool is_subsumed(app * query);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_rule_subsumption_index.cpp | 57 bool rule_subsumption_index::is_subsumed(app * query) { in is_subsumed() function in datalog::rule_subsumption_index
69 bool rule_subsumption_index::is_subsumed(rule * r) { in is_subsumed() function in datalog::rule_subsumption_index
72 if(is_subsumed(head)) { in is_subsumed()
|
| H A D | dl_rule_subsumption_index.h | 57 bool is_subsumed(rule * r);
58 bool is_subsumed(app * query);
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_dl_interface.cpp | 67 bool is_subsumed = !old_rules.empty(); in check_reset() local
68 for (unsigned i = 0; is_subsumed && i < new_rules.get_num_rules(); ++i) { in check_reset()
69 is_subsumed = false; in check_reset()
70 for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) { in check_reset()
72 is_subsumed = true; in check_reset()
75 if (!is_subsumed) { in check_reset()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_dl_interface.cpp | 67 bool is_subsumed = !old_rules.empty(); in check_reset() local
68 for (unsigned i = 0; is_subsumed && i < new_rules.get_num_rules(); ++i) { in check_reset()
69 is_subsumed = false; in check_reset()
70 for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) { in check_reset()
72 is_subsumed = true; in check_reset()
75 if (!is_subsumed) { in check_reset()
|
| /dports/math/z3/z3-z3-4.8.13/src/math/hilbert/ |
| H A D | hilbert_basis.h | 137 bool is_subsumed(offset_t idx);
138 bool is_subsumed(offset_t i, offset_t j) const;
|
| H A D | hilbert_basis.cpp | 67 if (*it != static_cast<int>(idx.m_offset) && hb.is_subsumed(idx, offs)) { in find()
861 if (is_subsumed(idx)) { in saturate_orig()
951 if (is_subsumed(idx)) { in saturate()
1122 if (is_subsumed(idx)) { in add_goal()
1135 bool hilbert_basis::is_subsumed(offset_t idx) { in is_subsumed() function in hilbert_basis
1301 bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const { in is_subsumed() function in hilbert_basis
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/math/hilbert/ |
| H A D | hilbert_basis.h | 137 bool is_subsumed(offset_t idx);
138 bool is_subsumed(offset_t i, offset_t j) const;
|
| H A D | hilbert_basis.cpp | 67 if (*it != static_cast<int>(idx.m_offset) && hb.is_subsumed(idx, offs)) { in find()
861 if (is_subsumed(idx)) { in saturate_orig()
951 if (is_subsumed(idx)) { in saturate()
1122 if (is_subsumed(idx)) { in add_goal()
1135 bool hilbert_basis::is_subsumed(offset_t idx) { in is_subsumed() function in hilbert_basis
1301 bool hilbert_basis::is_subsumed(offset_t i, offset_t j) const { in is_subsumed() function in hilbert_basis
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/transforms/ |
| H A D | dl_mk_subsumption_checker.cpp | 134 || subs_index.is_subsumed(tail_atom)) { in transform_rule()
232 if (subs_index.is_subsumed(new_rule)) { in transform_rules()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/transforms/ |
| H A D | dl_mk_subsumption_checker.cpp | 134 || subs_index.is_subsumed(tail_atom)) { in transform_rule()
232 if (subs_index.is_subsumed(new_rule)) { in transform_rules()
|
| /dports/math/minizinc/libminizinc-2.5.5/lib/flatten/ |
| H A D | flatten_call.cpp | 522 bool is_subsumed = false; in flatten_call() local
545 is_subsumed = true; in flatten_call()
574 is_subsumed = true; in flatten_call()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/tab/ |
| H A D | tab_context.cpp | 529 bool is_subsumed(ref<tb::clause>& g, unsigned& subsumer) { in is_subsumed() function in tb::index
1443 if (m_index.is_subsumed(next_clause, subsumer)) { in apply_rule()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/tab/ |
| H A D | tab_context.cpp | 529 bool is_subsumed(ref<tb::clause>& g, unsigned& subsumer) { in is_subsumed() function in tb::index
1443 if (m_index.is_subsumed(next_clause, subsumer)) { in apply_rule()
|