mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

rm typedef

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-18 21:20:20 -08:00
parent 036d5c02f4
commit 49b6d5b6fb
2 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/interval/dep_intervals.cpp
View file

@ -172,7 +172,7 @@ template <e_with_deps wd>
dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) { dep_intervals::interval dep_intervals::power(const interval& a, unsigned n) {
interval b; interval b;
if (with_deps == wd) { if (with_deps == wd) {
interval_deps_combine_rule combine_rule; interval_deps combine_rule;
m_imanager.power(a, n, b, combine_rule); m_imanager.power(a, n, b, combine_rule);
combine_deps(a, combine_rule, b); combine_deps(a, combine_rule, b);
} }

6
src/math/interval/dep_intervals.h
View file

@ -37,8 +37,6 @@ private:
public: public:
typedef unsynch_mpq_manager numeral_manager; typedef unsynch_mpq_manager numeral_manager;
typedef bound_deps deps_combine_rule;
typedef deps_combine_rule interval_deps_combine_rule;
struct interval { struct interval {
interval() : interval() :
@ -105,7 +103,7 @@ private:
im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {} im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {}
private: private:
u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const { u_dependency* mk_dependency(interval const& a, interval const& b, bound_deps bd) const {
u_dependency* dep = nullptr; u_dependency* dep = nullptr;
if (dep_in_lower1(bd)) { if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep); dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
@ -122,7 +120,7 @@ private:
return dep; return dep;
} }
u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const { u_dependency* mk_dependency(interval const& a, bound_deps bd) const {
u_dependency* dep = nullptr; u_dependency* dep = nullptr;
if (dep_in_lower1(bd)) { if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep); dep = m_dep_manager.mk_join(dep, a.m_lower_dep);