Searched refs:A_f_i (Results 1 – 4 of 4) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/doc/ |
| H A D | design_recfuns.md | 14 - a list of cases `A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]`.
15 When `A_f_i[t1…tn]` becomes true in the model, `f(t1…tn)` is said to be
16 *unfolded* and the clause `A_f_i[t1…tn] => f(t1…tn) = rhs_i[t1…tn]`
18 - a list of constraints `Γ_f_i[x1…xn] <=> A_f_i[x1…xn]`
19 that states when `A_f_i[x1…xn]` should be true, depending on inputs `x1…xn`.
21 immediately add all the `Γ_f_i[t1…tn] <=> A_f_i[t1…tn]` as auxiliary clauses
24 where each `A_f_i[x1…xn]` is a special new predicate representing the
52 Whenever `A_f_i[t1…tn]` becomes true (for any `f`), we increment
55 where `Γ` is the conjunction of all `A_f_i[t1…tn]` true in the trail.
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/doc/ |
| H A D | design_recfuns.md | 14 - a list of cases `A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]`.
15 When `A_f_i[t1…tn]` becomes true in the model, `f(t1…tn)` is said to be
16 *unfolded* and the clause `A_f_i[t1…tn] => f(t1…tn) = rhs_i[t1…tn]`
18 - a list of constraints `Γ_f_i[x1…xn] <=> A_f_i[x1…xn]`
19 that states when `A_f_i[x1…xn]` should be true, depending on inputs `x1…xn`.
21 immediately add all the `Γ_f_i[t1…tn] <=> A_f_i[t1…tn]` as auxiliary clauses
24 where each `A_f_i[x1…xn]` is a special new predicate representing the
52 Whenever `A_f_i[t1…tn]` becomes true (for any `f`), we increment
55 where `Γ` is the conjunction of all `A_f_i[t1…tn]` true in the trail.
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_model_finder.cpp | 1219 node* A_f_i = s.get_A_f_i(m_f, m_arg_i); in populate_inst_sets() local
1233 A_f_i->insert(arg, e_arg->get_generation()); in populate_inst_sets()
1290 node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); in populate_inst_sets() local
1292 if (A_f_i == S_j) { in populate_inst_sets()
1318 if (A_f_i->is_mono_proj()) in populate_inst_sets()
1321 A_f_i->set_mono_proj(); in populate_inst_sets()
1358 node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); in populate_inst_sets2() local
1361 if (A_f_i != S_j) { in populate_inst_sets2()
1365 copy_instances<false>(A_f_i, S_j, s); in populate_inst_sets2()
1366 copy_instances<true>(S_j, A_f_i, s); in populate_inst_sets2()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_model_finder.cpp | 1167 node* A_f_i = s.get_A_f_i(m_f, m_arg_i); in populate_inst_sets() local
1181 A_f_i->insert(arg, e_arg->get_generation()); in populate_inst_sets()
1238 node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); in populate_inst_sets() local
1240 if (A_f_i == S_j) { in populate_inst_sets()
1266 if (A_f_i->is_mono_proj()) in populate_inst_sets()
1269 A_f_i->set_mono_proj(); in populate_inst_sets()
1306 node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); in populate_inst_sets2() local
1309 if (A_f_i != S_j) { in populate_inst_sets2()
1313 copy_instances<false>(A_f_i, S_j, s); in populate_inst_sets2()
1314 copy_instances<true>(S_j, A_f_i, s); in populate_inst_sets2()
[all …]
|