CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
rational_tools.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Rational Numbers
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "rational_tools.h"
13
14#include "mathematical_types.h"
15#include "rational.h"
16
17static mp_integer power10(size_t i)
18{
19 mp_integer result=1;
20
21 for(; i!=0; i--)
22 result*=10;
23
24 return result;
25}
26
28{
29 if(!expr.is_constant())
30 return true;
31
32 const std::string &value=expr.get_string(ID_value);
33
34 std::string no1, no2;
35 char mode=0;
36
37 for(const char ch : value)
38 {
39 if(isdigit(ch))
40 {
41 if(mode==0)
42 no1+=ch;
43 else
44 no2+=ch;
45 }
46 else if(ch=='/' || ch=='.')
47 {
48 if(mode==0)
49 mode=ch;
50 else
51 return true;
52 }
53 else
54 return true;
55 }
56
57 switch(mode)
58 {
59 case 0:
61 break;
62
63 case '.':
67 break;
68
69 case '/':
72 break;
73
74 default:
75 return true;
76 }
77
78 return false;
79}
80
82{
83 std::string d=integer2string(a.get_numerator());
84 if(a.get_denominator()!=1)
85 d+="/"+integer2string(a.get_denominator());
86 return constant_exprt(d, rational_typet());
87}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
Base class for all expressions.
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
Unbounded, signed rational numbers.
int isdigit(int c)
Definition ctype.c:24
Mathematical types.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
bool to_rational(const exprt &expr, rationalt &rational_value)
static mp_integer power10(size_t i)
constant_exprt from_rational(const rationalt &a)
BigInt mp_integer
Definition smt_terms.h:17