1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 subpaving.cpp 7 8 Abstract: 9 10 Subpaving for non-linear arithmetic. 11 This is a wrapper for the different implementations 12 of the subpaving module. 13 This wrapper is the main interface between Z3 other modules and subpaving. 14 Thus, it assumes that polynomials have precise integer coefficients, and 15 bounds are rationals. If a particular implementation uses floats, then 16 internally the bounds are approximated. 17 18 Author: 19 20 Leonardo de Moura (leonardo) 2012-08-07. 21 22 Revision History: 23 24 --*/ 25 #include "math/subpaving/subpaving.h" 26 #include "math/subpaving/subpaving_types.h" 27 #include "math/subpaving/subpaving_mpq.h" 28 #include "math/subpaving/subpaving_mpf.h" 29 #include "math/subpaving/subpaving_hwf.h" 30 #include "math/subpaving/subpaving_mpff.h" 31 #include "math/subpaving/subpaving_mpfx.h" 32 33 namespace subpaving { 34 35 template<typename CTX> 36 class context_wrapper : public context { 37 protected: 38 CTX m_ctx; 39 public: context_wrapper(reslimit & lim,typename CTX::numeral_manager & m,params_ref const & p,small_object_allocator * a)40 context_wrapper(reslimit& lim, typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(lim, m, p, a) {} ~context_wrapper()41 ~context_wrapper() override {} num_vars() const42 unsigned num_vars() const override { return m_ctx.num_vars(); } mk_var(bool is_int)43 var mk_var(bool is_int) override { return m_ctx.mk_var(is_int); } is_int(var x) const44 bool is_int(var x) const override { return m_ctx.is_int(x); } mk_monomial(unsigned sz,power const * pws)45 var mk_monomial(unsigned sz, power const * pws) override { return m_ctx.mk_monomial(sz, pws); } inc_ref(ineq * a)46 void inc_ref(ineq * a) override { m_ctx.inc_ref(reinterpret_cast<typename CTX::ineq*>(a)); } dec_ref(ineq * a)47 void dec_ref(ineq * a) override { m_ctx.dec_ref(reinterpret_cast<typename CTX::ineq*>(a)); } add_clause(unsigned sz,ineq * const * atoms)48 void add_clause(unsigned sz, ineq * const * atoms) override { m_ctx.add_clause(sz, reinterpret_cast<typename CTX::ineq * const *>(atoms)); } display_constraints(std::ostream & out,bool use_star) const49 void display_constraints(std::ostream & out, bool use_star) const override { m_ctx.display_constraints(out, use_star); } set_display_proc(display_var_proc * p)50 void set_display_proc(display_var_proc * p) override { m_ctx.set_display_proc(p); } reset_statistics()51 void reset_statistics() override { m_ctx.reset_statistics(); } collect_statistics(statistics & st) const52 void collect_statistics(statistics & st) const override { m_ctx.collect_statistics(st); } collect_param_descrs(param_descrs & r)53 void collect_param_descrs(param_descrs & r) override { m_ctx.collect_param_descrs(r); } updt_params(params_ref const & p)54 void updt_params(params_ref const & p) override { m_ctx.updt_params(p); } operator ()()55 void operator()() override { m_ctx(); } display_bounds(std::ostream & out) const56 void display_bounds(std::ostream & out) const override { m_ctx.display_bounds(out); } 57 }; 58 59 class context_mpq_wrapper : public context_wrapper<context_mpq> { 60 scoped_mpq m_c; 61 scoped_mpq_vector m_as; 62 public: context_mpq_wrapper(reslimit & lim,unsynch_mpq_manager & m,params_ref const & p,small_object_allocator * a)63 context_mpq_wrapper(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a): 64 context_wrapper<context_mpq>(lim, m, p, a), 65 m_c(m), 66 m_as(m) 67 {} 68 ~context_mpq_wrapper()69 ~context_mpq_wrapper() override {} 70 qm() const71 unsynch_mpq_manager & qm() const override { return m_ctx.nm(); } 72 mk_sum(mpz const & c,unsigned sz,mpz const * as,var const * xs)73 var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { 74 m_as.reserve(sz); 75 for (unsigned i = 0; i < sz; i++) { 76 m_ctx.nm().set(m_as[i], as[i]); 77 } 78 m_ctx.nm().set(m_c, c); 79 return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); 80 } mk_ineq(var x,mpq const & k,bool lower,bool open)81 ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override { 82 return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, k, lower, open)); 83 } 84 }; 85 86 class context_mpf_wrapper : public context_wrapper<context_mpf> { 87 unsynch_mpq_manager & m_qm; 88 scoped_mpf m_c; 89 scoped_mpf_vector m_as; 90 scoped_mpq m_q1, m_q2; 91 92 // Convert the mpz (integer) into a mpf, and throws an exception if the conversion is not precise. int2mpf(mpz const & a,mpf & o)93 void int2mpf(mpz const & a, mpf & o) { 94 m_qm.set(m_q1, a); 95 m_ctx.nm().set(o, m_q1); 96 m_ctx.nm().m().to_rational(o, m_q2); 97 if (!m_qm.eq(m_q1, m_q2)) 98 throw subpaving::exception(); 99 } 100 101 public: context_mpf_wrapper(reslimit & lim,f2n<mpf_manager> & fm,params_ref const & p,small_object_allocator * a)102 context_mpf_wrapper(reslimit& lim, f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a): 103 context_wrapper<context_mpf>(lim, fm, p, a), 104 m_qm(fm.m().mpq_manager()), 105 m_c(fm.m()), 106 m_as(fm.m()), 107 m_q1(m_qm), 108 m_q2(m_qm) { 109 } 110 ~context_mpf_wrapper()111 ~context_mpf_wrapper() override {} 112 qm() const113 unsynch_mpq_manager & qm() const override { return m_qm; } 114 mk_sum(mpz const & c,unsigned sz,mpz const * as,var const * xs)115 var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { 116 try { 117 m_as.reserve(sz); 118 for (unsigned i = 0; i < sz; i++) { 119 int2mpf(as[i], m_as[i]); 120 } 121 int2mpf(c, m_c); 122 return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); 123 } 124 catch (const f2n<mpf_manager>::exception &) { 125 throw subpaving::exception(); 126 } 127 } mk_ineq(var x,mpq const & k,bool lower,bool open)128 ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override { 129 try { 130 f2n<mpf_manager> & m = m_ctx.nm(); 131 if (lower) 132 m.round_to_minus_inf(); 133 else 134 m.round_to_plus_inf(); 135 m.set(m_c, k); 136 return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open)); 137 } 138 catch (const f2n<mpf_manager>::exception &) { 139 throw subpaving::exception(); 140 } 141 } 142 }; 143 144 class context_hwf_wrapper : public context_wrapper<context_hwf> { 145 unsynch_mpq_manager & m_qm; 146 hwf m_c; 147 svector<hwf> m_as; 148 149 // Convert the mpz (integer) into a hwf, and throws an exception if the conversion is not precise. int2hwf(mpz const & a,hwf & o)150 void int2hwf(mpz const & a, hwf & o) { 151 if (!m_qm.is_int64(a)) 152 throw subpaving::exception(); 153 int64_t val = m_qm.get_int64(a); 154 double dval = static_cast<double>(val); 155 m_ctx.nm().set(o, dval); 156 double _dval = m_ctx.nm().m().to_double(o); 157 // TODO check the following test 158 if (static_cast<int64_t>(_dval) != val) 159 throw subpaving::exception(); 160 } 161 162 public: context_hwf_wrapper(reslimit & lim,f2n<hwf_manager> & fm,unsynch_mpq_manager & qm,params_ref const & p,small_object_allocator * a)163 context_hwf_wrapper(reslimit& lim,f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a): 164 context_wrapper<context_hwf>(lim, fm, p, a), 165 m_qm(qm) { 166 } 167 ~context_hwf_wrapper()168 ~context_hwf_wrapper() override {} 169 qm() const170 unsynch_mpq_manager & qm() const override { return m_qm; } 171 mk_sum(mpz const & c,unsigned sz,mpz const * as,var const * xs)172 var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { 173 try { 174 m_as.reserve(sz); 175 for (unsigned i = 0; i < sz; i++) { 176 int2hwf(as[i], m_as[i]); 177 } 178 int2hwf(c, m_c); 179 return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); 180 } 181 catch (const f2n<mpf_manager>::exception &) { 182 throw subpaving::exception(); 183 } 184 } mk_ineq(var x,mpq const & k,bool lower,bool open)185 ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override { 186 try { 187 f2n<hwf_manager> & m = m_ctx.nm(); 188 if (lower) 189 m.round_to_minus_inf(); 190 else 191 m.round_to_plus_inf(); 192 m.set(m_c, k); 193 return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open)); 194 } 195 catch (const f2n<mpf_manager>::exception &) { 196 throw subpaving::exception(); 197 } 198 } 199 }; 200 201 template<typename context_fpoint> 202 class context_fpoint_wrapper : public context_wrapper<context_fpoint> { 203 unsynch_mpq_manager & m_qm; 204 _scoped_numeral<typename context_fpoint::numeral_manager> m_c; 205 _scoped_numeral_vector<typename context_fpoint::numeral_manager> m_as; 206 scoped_mpz m_z1, m_z2; 207 int2fpoint(mpz const & a,typename context_fpoint::numeral & o)208 void int2fpoint(mpz const & a, typename context_fpoint::numeral & o) { 209 m_qm.set(m_z1, a); 210 this->m_ctx.nm().set(o, m_qm, m_z1); 211 this->m_ctx.nm().to_mpz(o, m_qm, m_z2); 212 if (!m_qm.eq(m_z1, m_z2)) 213 throw subpaving::exception(); 214 } 215 216 public: context_fpoint_wrapper(reslimit & lim,typename context_fpoint::numeral_manager & m,unsynch_mpq_manager & qm,params_ref const & p,small_object_allocator * a)217 context_fpoint_wrapper(reslimit& lim, typename context_fpoint::numeral_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a): 218 context_wrapper<context_fpoint>(lim, m, p, a), 219 m_qm(qm), 220 m_c(m), 221 m_as(m), 222 m_z1(m_qm), 223 m_z2(m_qm) { 224 } 225 ~context_fpoint_wrapper()226 ~context_fpoint_wrapper() override {} 227 qm() const228 unsynch_mpq_manager & qm() const override { return m_qm; } 229 mk_sum(mpz const & c,unsigned sz,mpz const * as,var const * xs)230 var mk_sum(mpz const & c, unsigned sz, mpz const * as, var const * xs) override { 231 try { 232 m_as.reserve(sz); 233 for (unsigned i = 0; i < sz; i++) { 234 int2fpoint(as[i], m_as[i]); 235 } 236 int2fpoint(c, m_c); 237 return this->m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); 238 } 239 catch (const typename context_fpoint::numeral_manager::exception &) { 240 throw subpaving::exception(); 241 } 242 } 243 mk_ineq(var x,mpq const & k,bool lower,bool open)244 ineq * mk_ineq(var x, mpq const & k, bool lower, bool open) override { 245 try { 246 typename context_fpoint::numeral_manager & m = this->m_ctx.nm(); 247 if (lower) 248 m.round_to_minus_inf(); 249 else 250 m.round_to_plus_inf(); 251 m.set(m_c, m_qm, k); 252 return reinterpret_cast<ineq*>(this->m_ctx.mk_ineq(x, m_c, lower, open)); 253 } 254 catch (const typename context_fpoint::numeral_manager::exception &) { 255 throw subpaving::exception(); 256 } 257 } 258 }; 259 260 typedef context_fpoint_wrapper<context_mpff> context_mpff_wrapper; 261 typedef context_fpoint_wrapper<context_mpfx> context_mpfx_wrapper; 262 mk_mpq_context(reslimit & lim,unsynch_mpq_manager & m,params_ref const & p,small_object_allocator * a)263 context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) { 264 return alloc(context_mpq_wrapper, lim, m, p, a); 265 } 266 mk_mpf_context(reslimit & lim,f2n<mpf_manager> & m,params_ref const & p,small_object_allocator * a)267 context * mk_mpf_context(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a) { 268 return alloc(context_mpf_wrapper, lim, m, p, a); 269 } 270 mk_hwf_context(reslimit & lim,f2n<hwf_manager> & m,unsynch_mpq_manager & qm,params_ref const & p,small_object_allocator * a)271 context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) { 272 return alloc(context_hwf_wrapper, lim, m, qm, p, a); 273 } 274 mk_mpff_context(reslimit & lim,mpff_manager & m,unsynch_mpq_manager & qm,params_ref const & p,small_object_allocator * a)275 context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) { 276 return alloc(context_mpff_wrapper, lim, m, qm, p, a); 277 } 278 mk_mpfx_context(reslimit & lim,mpfx_manager & m,unsynch_mpq_manager & qm,params_ref const & p,small_object_allocator * a)279 context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) { 280 return alloc(context_mpfx_wrapper, lim, m, qm, p, a); 281 } 282 283 }; 284