1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 subpaving_mpq.h 7 8 Abstract: 9 10 Subpaving for non-linear arithmetic using rationals 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2012-07-31. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "math/subpaving/subpaving_t.h" 22 #include "util/mpq.h" 23 24 namespace subpaving { 25 26 struct config_mpq { 27 typedef unsynch_mpq_manager numeral_manager; 28 struct exception {}; 29 round_to_minus_infconfig_mpq30 static void round_to_minus_inf(numeral_manager & m) {} round_to_plus_infconfig_mpq31 static void round_to_plus_inf(numeral_manager & m) {} set_roundingconfig_mpq32 static void set_rounding(numeral_manager & m, bool to_plus_info) {} 33 numeral_manager & m_manager; config_mpqconfig_mpq34 config_mpq(numeral_manager & m):m_manager(m) {} mconfig_mpq35 numeral_manager & m() const { return m_manager; } 36 }; 37 38 typedef context_t<config_mpq> context_mpq; 39 40 }; 41 42