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