CBMC
rational_tools.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Rational Numbers
4 
5 Author: 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 
17 static 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 
27 bool to_rational(const exprt &expr, rationalt &rational_value)
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:
60  rational_value=rationalt(string2integer(no1));
61  break;
62 
63  case '.':
64  rational_value=rationalt(string2integer(no1));
65  rational_value+=
66  rationalt(string2integer(no2))/rationalt(power10(no2.size()));
67  break;
68 
69  case '/':
70  rational_value=rationalt(string2integer(no1));
71  rational_value/=rationalt(string2integer(no2));
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 }
A constant literal expression.
Definition: std_expr.h:3000
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.
const mp_integer & get_denominator() const
Definition: rational.h:90
const mp_integer & get_numerator() const
Definition: rational.h:85
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