| /dports/math/z3/z3-z3-4.8.13/examples/tptp/ |
| H A D | tptp5.h | 15 expr_ref_vector m_fmls;
21 m_fmls(m),
26 m_fmls.push_back(fml);
29 unsigned size() const { return m_fmls.size(); }
30 expr*const* data() const { return m_fmls.data(); }
31 expr* operator[](unsigned i) { return m_fmls[i].get(); }
35 m_conjecture_index = m_fmls.size();
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/tptp/ |
| H A D | tptp5.h | 15 expr_ref_vector m_fmls;
21 m_fmls(m),
26 m_fmls.push_back(fml);
29 unsigned size() const { return m_fmls.size(); }
30 expr*const* c_ptr() const { return m_fmls.c_ptr(); }
31 expr* operator[](unsigned i) { return m_fmls[i].get(); }
35 m_conjecture_index = m_fmls.size();
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/solver/ |
| H A D | mus.cpp | 265 expr_ref_vector& m_fmls;
269 m_fmls(fmls1),
277 m_fmls(fmls1),
282 m_fmls(fmls1),
287 m_fmls(fmls1),
292 m_fmls.shrink(m_size);
|
| /dports/math/z3/z3-z3-4.8.13/src/solver/ |
| H A D | mus.cpp | 265 expr_ref_vector& m_fmls; member in mus::imp::scoped_append
269 m_fmls(fmls1), in scoped_append()
277 m_fmls(fmls1), in scoped_append()
282 m_fmls(fmls1), in scoped_append()
287 m_fmls(fmls1), in scoped_append()
292 m_fmls.shrink(m_size); in ~scoped_append()
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/sat_solver/ |
| H A D | inc_sat_solver.cpp | 56 expr_ref_vector m_fmls; member in inc_sat_solver
93 m_fmls(m), in inc_sat_solver()
137 for (expr* f : m_fmls) result->m_fmls.push_back(tr(f)); in translate()
267 m_fmls_lim.push_back(m_fmls.size()); in push_internal()
357 m_fmls.push_back(t); in assert_expr_core()
559 return m_fmls.size(); in get_num_assertions()
567 return m_fmls[idx]; in get_assertion()
904 expr* fml = m_fmls.get(i); in internalize_formulas()
909 m_fmls_head = m_fmls.size(); in internalize_formulas()
1004 if (m_fmls.size() > m_fmls_head) { in get_model_core()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/sat_solver/ |
| H A D | inc_sat_solver.cpp | 55 expr_ref_vector m_fmls; member in inc_sat_solver
92 m_fmls(m), in inc_sat_solver()
136 for (expr* f : m_fmls) result->m_fmls.push_back(tr(f)); in translate()
264 m_fmls_lim.push_back(m_fmls.size()); in push_internal()
327 m_fmls.push_back(t); in assert_expr_core()
529 return m_fmls.size(); in get_num_assertions()
537 return m_fmls[idx]; in get_assertion()
874 expr* fml = m_fmls.get(i); in internalize_formulas()
879 m_fmls_head = m_fmls.size(); in internalize_formulas()
974 if (m_fmls.size() > m_fmls_head) { in get_model_core()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | qe_mbi.cpp | 190 m_fmls(m), in uflia_mbi()
197 m_solver->get_assertions(m_fmls); in uflia_mbi()
198 collect_atoms(m_fmls); in uflia_mbi()
222 dual->assert_expr(mk_not(mk_and(m_fmls))); in get_literals()
438 m_fmls.push_back(clause); in block()
|
| H A D | qe_mbi.h | 117 expr_ref_vector m_fmls; variable
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | qe_mbi.cpp | 190 m_fmls(m), in uflia_mbi()
197 m_solver->get_assertions(m_fmls); in uflia_mbi()
198 collect_atoms(m_fmls); in uflia_mbi()
222 dual->assert_expr(mk_not(mk_and(m_fmls))); in get_literals()
438 m_fmls.push_back(clause); in block()
|
| H A D | qe_mbi.h | 117 expr_ref_vector m_fmls; variable
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_wmaxsat.cpp | 32 m_fmls(m), in theory_wmaxsat()
99 m_fmls.push_back(fml); in assert_weighted()
193 m_fmls.reset(); in reset_local()
|
| H A D | theory_wmaxsat.h | 37 expr_ref_vector m_fmls; // Formulas per soft clause variable
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_wmaxsat.cpp | 32 m_fmls(m), in mtd_probe()
99 m_fmls.push_back(fml); in mtd_probe()
193 m_fmls.reset(); in mtd_probe()
|
| H A D | theory_wmaxsat.h | 37 expr_ref_vector m_fmls; // Formulas per soft clause
|