Home
last modified time | relevance | path

Searched refs:unsynch_mpq_manager (Results 1 – 25 of 110) sorted by relevance

12345

/dports/math/z3/z3-z3-4.8.13/src/math/subpaving/
H A Dsubpaving.cpp63 …context_mpq_wrapper(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_all… in context_mpq_wrapper()
71 unsynch_mpq_manager & qm() const override { return m_ctx.nm(); } in qm()
87 unsynch_mpq_manager & m_qm;
113 unsynch_mpq_manager & qm() const override { return m_qm; } in qm()
145 unsynch_mpq_manager & m_qm;
163 …context_hwf_wrapper(reslimit& lim,f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref cons… in context_hwf_wrapper()
170 unsynch_mpq_manager & qm() const override { return m_qm; } in qm()
203 unsynch_mpq_manager & m_qm;
228 unsynch_mpq_manager & qm() const override { return m_qm; } in qm()
263 …context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_objec… in mk_mpq_context()
[all …]
H A Dsubpaving.h44 virtual unsynch_mpq_manager & qm() const = 0;
113 …context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref…
115 context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref …
116 context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref con…
117 context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref con…
H A Dsubpaving_mpq.h27 typedef unsynch_mpq_manager numeral_manager;
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/subpaving/
H A Dsubpaving.cpp63 …context_mpq_wrapper(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_all… in context_mpq_wrapper()
71 unsynch_mpq_manager & qm() const override { return m_ctx.nm(); } in qm()
87 unsynch_mpq_manager & m_qm;
113 unsynch_mpq_manager & qm() const override { return m_qm; } in qm()
145 unsynch_mpq_manager & m_qm;
163 …context_hwf_wrapper(reslimit& lim,f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref cons… in context_hwf_wrapper()
170 unsynch_mpq_manager & qm() const override { return m_qm; } in qm()
203 unsynch_mpq_manager & m_qm;
228 unsynch_mpq_manager & qm() const override { return m_qm; } in qm()
263 …context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_objec… in mk_mpq_context()
[all …]
H A Dsubpaving.h44 virtual unsynch_mpq_manager & qm() const = 0;
113 …context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref…
115 context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref …
116 context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref con…
117 context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref con…
H A Dsubpaving_mpq.h27 typedef unsynch_mpq_manager numeral_manager;
/dports/math/z3/z3-z3-4.8.13/src/test/
H A Dinterval.cpp236 unsynch_mpq_manager nm; \
257 unsynch_mpq_manager nm; in tst_neg()
272 unsynch_mpq_manager nm; in tst_pw_2()
287 unsynch_mpq_manager nm; in tst_pw_3()
302 unsynch_mpq_manager nm; in tst_root_2()
324 unsynch_mpq_manager nm; in tst_root_3()
344 unsynch_mpq_manager nm; in tst_inv()
363 unsynch_mpq_manager nm; in tst_div()
385 unsynch_mpq_manager qm;
420 unsynch_mpq_manager nm; in tst_pi()
[all …]
H A Dtrigo.cpp30 static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval_manager<im_default… in tst_sine_core()
41 unsynch_mpq_manager nm; in tst_sine()
56 static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interval_manager<im_defau… in tst_cosine_core()
68 unsynch_mpq_manager nm; in tst_cosine()
135 unsynch_mpq_manager nm; in tst_e()
149 unsynch_mpq_manager qm; in tst_e_float()
H A Drcf.cpp24 unsynch_mpq_manager qm; in tst1()
74 unsynch_mpq_manager nm; in tst2()
108 unsynch_mpq_manager nm; in tst_solve()
130 unsynch_mpq_manager nm; in tst_lin_indep()
149 unsynch_mpq_manager qm; in tst_denominators()
H A Dmpq.cpp107 unsynch_mpq_manager m; in tst2()
119 unsynch_mpq_manager m; in set_str_bug()
137 unsynch_mpq_manager m; in tst_prev_power_2()
H A Dalgebraic.cpp45 unsynch_mpq_manager nm; in tst1()
182 unsynch_mpq_manager qm; in tst_refine_mpbq()
217 unsynch_mpq_manager qm; in tst_mpbq_root()
227 unsynch_mpq_manager nm; in tst_wilkinson()
253 unsynch_mpq_manager qm; in tst_dejan()
340 unsynch_mpq_manager qm; in tst_eval_sign()
421 unsynch_mpq_manager qm; in tst_isolate_roots()
493 unsynch_mpq_manager qm; in ex1()
553 unsynch_mpq_manager qm; in tst_root()
567 unsynch_mpq_manager nm; in tst_sturm()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/
H A Dinterval.cpp236 unsynch_mpq_manager nm; \
257 unsynch_mpq_manager nm; in tst_neg()
272 unsynch_mpq_manager nm; in tst_pw_2()
287 unsynch_mpq_manager nm; in tst_pw_3()
302 unsynch_mpq_manager nm; in tst_root_2()
324 unsynch_mpq_manager nm; in tst_root_3()
344 unsynch_mpq_manager nm; in tst_inv()
363 unsynch_mpq_manager nm; in tst_div()
385 unsynch_mpq_manager qm;
420 unsynch_mpq_manager nm; in tst_pi()
[all …]
H A Dtrigo.cpp30 static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval_manager<im_default… in tst_sine_core()
41 unsynch_mpq_manager nm; in tst_sine()
56 static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interval_manager<im_defau… in tst_cosine_core()
68 unsynch_mpq_manager nm; in tst_cosine()
135 unsynch_mpq_manager nm; in tst_e()
149 unsynch_mpq_manager qm; in tst_e_float()
H A Drcf.cpp24 unsynch_mpq_manager qm; in tst1()
74 unsynch_mpq_manager nm; in tst2()
108 unsynch_mpq_manager nm; in tst_solve()
130 unsynch_mpq_manager nm; in tst_lin_indep()
149 unsynch_mpq_manager qm; in tst_denominators()
H A Dmpq.cpp107 unsynch_mpq_manager m; in tst2()
119 unsynch_mpq_manager m; in set_str_bug()
137 unsynch_mpq_manager m; in tst_prev_power_2()
H A Dalgebraic.cpp45 unsynch_mpq_manager nm; in tst1()
182 unsynch_mpq_manager qm; in tst_refine_mpbq()
217 unsynch_mpq_manager qm; in tst_mpbq_root()
227 unsynch_mpq_manager nm; in tst_wilkinson()
253 unsynch_mpq_manager qm; in tst_dejan()
340 unsynch_mpq_manager qm; in tst_eval_sign()
421 unsynch_mpq_manager qm; in tst_isolate_roots()
493 unsynch_mpq_manager qm; in ex1()
553 unsynch_mpq_manager qm; in tst_root()
567 unsynch_mpq_manager nm; in tst_sturm()
/dports/math/z3/z3-z3-4.8.13/src/math/interval/
H A Ddep_intervals.cpp72 if (unsynch_mpq_manager::is_neg(lower(i))) in separated_from_zero_on_lower()
74 if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i)) in separated_from_zero_on_lower()
82 if (unsynch_mpq_manager::is_pos(upper(i))) in separated_from_zero_on_upper()
84 if (unsynch_mpq_manager::is_zero(upper(i)) && !m_config.upper_is_open(i)) in separated_from_zero_on_upper()
H A Ddep_intervals.h35 unsynch_mpq_manager& m_manager;
39 typedef unsynch_mpq_manager numeral_manager;
91 unsynch_mpq_manager::is_zero(a.m_lower) && in is_zero()
92 unsynch_mpq_manager::is_zero(a.m_upper); in is_zero()
145 mutable unsynch_mpq_manager m_num_manager;
151 unsynch_mpq_manager& num_manager() { return m_num_manager; } in num_manager()
152 const unsynch_mpq_manager& num_manager() const { return m_num_manager; } in num_manager()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/interval/
H A Ddep_intervals.cpp72 if (unsynch_mpq_manager::is_neg(lower(i))) in separated_from_zero_on_lower()
74 if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i)) in separated_from_zero_on_lower()
82 if (unsynch_mpq_manager::is_pos(upper(i))) in separated_from_zero_on_upper()
84 if (unsynch_mpq_manager::is_zero(upper(i)) && !m_config.upper_is_open(i)) in separated_from_zero_on_upper()
H A Ddep_intervals.h35 unsynch_mpq_manager& m_manager;
39 typedef unsynch_mpq_manager numeral_manager;
91 unsynch_mpq_manager::is_zero(a.m_lower) && in is_zero()
92 unsynch_mpq_manager::is_zero(a.m_upper); in is_zero()
145 mutable unsynch_mpq_manager m_num_manager;
151 unsynch_mpq_manager& num_manager() { return m_num_manager; } in num_manager()
152 const unsynch_mpq_manager& num_manager() const { return m_num_manager; } in num_manager()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/util/
H A Dmpbq.h63 bool select_integer(unsynch_mpq_manager & qm, mpq const & lower, mpbq const & upper, mpz & r);
64 bool select_integer(unsynch_mpq_manager & qm, mpbq const & lower, mpq const & upper, mpz & r);
65 bool select_integer(unsynch_mpq_manager & qm, mpq const & lower, mpq const & upper, mpz & r);
254 … void select_small_core(unsynch_mpq_manager & qm, mpq const & lower, mpbq const & upper, mpbq & r);
256 … void select_small_core(unsynch_mpq_manager & qm, mpbq const & lower, mpq const & upper, mpbq & r);
258 … void select_small_core(unsynch_mpq_manager & qm, mpq const & lower, mpq const & upper, mpbq & r);
H A Dmpfx.h61 typedef mpq_manager<false> unsynch_mpq_manager; typedef
319 void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
380 void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
/dports/math/z3/z3-z3-4.8.13/src/util/
H A Dmpbq.h63 bool select_integer(unsynch_mpq_manager & qm, mpq const & lower, mpbq const & upper, mpz & r);
64 bool select_integer(unsynch_mpq_manager & qm, mpbq const & lower, mpq const & upper, mpz & r);
65 bool select_integer(unsynch_mpq_manager & qm, mpq const & lower, mpq const & upper, mpz & r);
254 … void select_small_core(unsynch_mpq_manager & qm, mpq const & lower, mpbq const & upper, mpbq & r);
256 … void select_small_core(unsynch_mpq_manager & qm, mpbq const & lower, mpq const & upper, mpbq & r);
258 … void select_small_core(unsynch_mpq_manager & qm, mpq const & lower, mpq const & upper, mpbq & r);
H A Dmpfx.h61 typedef mpq_manager<false> unsynch_mpq_manager; typedef
319 void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
380 void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
H A Dmpff.h68 typedef mpq_manager<false> unsynch_mpq_manager; typedef
387 void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
448 void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);

12345