| /dports/math/z3/z3-z3-4.8.13/src/ast/ |
| H A D | expr_substitution.cpp | 30 if (unsat_core_enabled()) in init()
81 if (unsat_core_enabled()) { in insert()
99 if (unsat_core_enabled()) { in insert()
117 if (unsat_core_enabled()) { in erase()
145 if (unsat_core_enabled()) in find()
160 if (unsat_core_enabled()) in reset()
169 if (unsat_core_enabled()) in cleanup()
|
| H A D | macro_substitution.cpp | 30 if (unsat_core_enabled()) in init()
64 if (unsat_core_enabled()) in reset()
73 if (unsat_core_enabled()) in cleanup()
96 if (unsat_core_enabled()) { in insert()
114 if (unsat_core_enabled()) { in insert()
132 if (unsat_core_enabled()) { in erase()
177 if (unsat_core_enabled()) in find()
|
| H A D | macro_substitution.h | 43 bool unsat_core_enabled() const { return m_cores_enabled; } in unsat_core_enabled() function
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/ |
| H A D | expr_substitution.cpp | 30 if (unsat_core_enabled()) in init()
81 if (unsat_core_enabled()) { in insert()
99 if (unsat_core_enabled()) { in insert()
117 if (unsat_core_enabled()) { in erase()
145 if (unsat_core_enabled()) in find()
160 if (unsat_core_enabled()) in reset()
169 if (unsat_core_enabled()) in cleanup()
|
| H A D | macro_substitution.cpp | 30 if (unsat_core_enabled()) in init()
64 if (unsat_core_enabled()) in reset()
73 if (unsat_core_enabled()) in cleanup()
96 if (unsat_core_enabled()) { in insert()
114 if (unsat_core_enabled()) { in insert()
132 if (unsat_core_enabled()) { in erase()
177 if (unsat_core_enabled()) in find()
|
| H A D | macro_substitution.h | 43 bool unsat_core_enabled() const { return m_cores_enabled; } in unsat_core_enabled() function
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/ |
| H A D | goal.cpp | 73 m_core_enabled(src.unsat_core_enabled()), in goal()
87 m_core_enabled(src.unsat_core_enabled()), in goal()
134 if (unsat_core_enabled()) in push_back()
142 if (unsat_core_enabled()) in push_back()
305 if (unsat_core_enabled()) in update()
319 if (unsat_core_enabled()) in update()
483 if (unsat_core_enabled()) in shrink()
504 if (unsat_core_enabled()) in elim_true()
560 if (unsat_core_enabled()) in elim_redundancies()
590 if (unsat_core_enabled()) in elim_redundancies()
[all …]
|
| H A D | tactic.cpp | 163 bool cores_enabled = g->unsat_core_enabled(); in check_sat()
231 if (in->unsat_core_enabled()) { in fail_if_unsat_core_generation()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/ |
| H A D | goal.cpp | 73 m_core_enabled(src.unsat_core_enabled()), in goal()
87 m_core_enabled(src.unsat_core_enabled()), in goal()
134 if (unsat_core_enabled()) in push_back()
142 if (unsat_core_enabled()) in push_back()
305 if (unsat_core_enabled()) in update()
319 if (unsat_core_enabled()) in update()
483 if (unsat_core_enabled()) in shrink()
504 if (unsat_core_enabled()) in elim_true()
560 if (unsat_core_enabled()) in elim_redundancies()
590 if (unsat_core_enabled()) in elim_redundancies()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/ufbv/ |
| H A D | macro_finder_tactic.cpp | 46 bool unsat_core_enabled = g->unsat_core_enabled();
66 unsat_core_enabled ? new_deps.get(i) : nullptr);
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/ufbv/ |
| H A D | macro_finder_tactic.cpp | 53 bool unsat_core_enabled = g->unsat_core_enabled(); in operator ()() local
73 unsat_core_enabled ? new_deps.get(i) : nullptr); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/solver/ |
| H A D | solver2tactic.cpp | 37 if (d == nullptr || !g->unsat_core_enabled()) { in extract_clauses_and_dependencies()
140 if (in->unsat_core_enabled()) { in operator ()()
156 if (!in->unsat_core_enabled()) { in operator ()()
|
| H A D | tactic2solver.cpp | 317 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
318 … mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic); in operator ()()
328 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
330 return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); in operator ()()
|
| H A D | combined_solver.cpp | 356 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
357 …return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), in operator ()()
358 … (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/solver/ |
| H A D | solver2tactic.cpp | 37 if (d == nullptr || !g->unsat_core_enabled()) { in extract_clauses_and_dependencies()
140 if (in->unsat_core_enabled()) { in operator ()()
156 if (!in->unsat_core_enabled()) { in operator ()()
|
| H A D | tactic2solver.cpp | 321 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
322 … mk_tactic2solver(m, m_tactic.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, logic); in operator ()()
332 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
334 return mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); in operator ()()
|
| H A D | combined_solver.cpp | 361 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
362 …return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), in operator ()()
363 … (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic), in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/portfolio/ |
| H A D | smt_strategic_solver.cpp | 135 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
164 …ined_solver(mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l), in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/portfolio/ |
| H A D | smt_strategic_solver.cpp | 135 …rams_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol cons… in operator ()() argument
164 …ined_solver(mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l), in operator ()()
|
| /dports/math/z3/z3-z3-4.8.13/src/params/ |
| H A D | context_params.cpp | 189 …r_params(params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) { in get_solver_params() argument
192 unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false); in get_solver_params()
|
| H A D | context_params.h | 62 …er_params(params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/params/ |
| H A D | context_params.cpp | 185 …nst & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) { in get_solver_params() argument
188 unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false); in get_solver_params()
|
| H A D | context_params.h | 62 …onst & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/core/ |
| H A D | propagate_values_tactic.cpp | 82 if (m_goal->unsat_core_enabled()) { in push_result()
152 m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled()); in run()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/core/ |
| H A D | propagate_values_tactic.cpp | 82 if (m_goal->unsat_core_enabled()) { in push_result()
149 m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled()); in run()
|