Skip to content

Commit f20e8d7

Browse files
tautschnigtautschnig
authored
Merge pull request #1891 from diffblue/deprecated-exprt-methods
remove exprt::negate, sum, mul, subtract (deprecated since 2011)
2 parents 20fc8d1 + f6890b3 commit f20e8d7

File tree

3 files changed

+126
-231
lines changed

3 files changed

+126
-231
lines changed

‎src/util/expr.cpp

Lines changed: 6 additions & 216 deletions
Original file line numberDiff line numberDiff line change
@@ -9,19 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com
99
/// \file
1010
/// Expression Representation
1111

12+
#include "arith_tools.h"
1213
#include "expr.h"
13-
#include <cassert>
14-
#include <stack>
15-
#include "string2int.h"
16-
#include "mp_arith.h"
14+
#include "expr_iterator.h"
1715
#include "fixedbv.h"
1816
#include "ieee_float.h"
1917
#include "invariant.h"
20-
#include "expr_iterator.h"
18+
#include "mp_arith.h"
2119
#include "rational.h"
2220
#include "rational_tools.h"
23-
#include "arith_tools.h"
2421
#include "std_expr.h"
22+
#include "string2int.h"
23+
24+
#include <stack>
2525

2626
void exprt::move_to_operands(exprt &expr)
2727
{
@@ -157,71 +157,6 @@ void exprt::make_false()
157157
set(ID_value, ID_false);
158158
}
159159

160-
void exprt::negate()
161-
{
162-
const irep_idt &type_id=type().id();
163-
164-
if(type_id==ID_bool)
165-
make_not();
166-
else
167-
{
168-
if(is_constant())
169-
{
170-
const irep_idt &value=get(ID_value);
171-
172-
if(type_id==ID_integer)
173-
{
174-
set(ID_value, integer2string(-string2integer(id2string(value))));
175-
}
176-
else if(type_id==ID_unsignedbv)
177-
{
178-
mp_integer int_value=binary2integer(id2string(value), false);
179-
typet _type=type();
180-
*this=from_integer(-int_value, _type);
181-
}
182-
else if(type_id==ID_signedbv)
183-
{
184-
mp_integer int_value=binary2integer(id2string(value), true);
185-
typet _type=type();
186-
*this=from_integer(-int_value, _type);
187-
}
188-
else if(type_id==ID_fixedbv)
189-
{
190-
fixedbvt fixedbv_value=fixedbvt(to_constant_expr(*this));
191-
fixedbv_value.negate();
192-
*this=fixedbv_value.to_expr();
193-
}
194-
else if(type_id==ID_floatbv)
195-
{
196-
ieee_floatt ieee_float_value=ieee_floatt(to_constant_expr(*this));
197-
ieee_float_value.negate();
198-
*this=ieee_float_value.to_expr();
199-
}
200-
else
201-
{
202-
make_nil();
203-
UNREACHABLE;
204-
}
205-
}
206-
else
207-
{
208-
if(id()==ID_unary_minus)
209-
{
210-
exprt tmp;
211-
DATA_INVARIANT(operands().size()==1,
212-
"Unary minus must have one operand");
213-
tmp.swap(op0());
214-
swap(tmp);
215-
}
216-
else
217-
{
218-
unary_minus_exprt tmp(*this);
219-
swap(tmp);
220-
}
221-
}
222-
}
223-
}
224-
225160
bool exprt::is_boolean() const
226161
{
227162
return type().id()==ID_bool;
@@ -312,151 +247,6 @@ bool exprt::is_one() const
312247
return false;
313248
}
314249

315-
bool exprt::sum(const exprt &expr)
316-
{
317-
if(!is_constant() || !expr.is_constant())
318-
return true;
319-
if(type()!=expr.type())
320-
return true;
321-
322-
const irep_idt &type_id=type().id();
323-
324-
if(type_id==ID_integer || type_id==ID_natural)
325-
{
326-
set(ID_value, integer2string(
327-
string2integer(get_string(ID_value))+
328-
string2integer(expr.get_string(ID_value))));
329-
return false;
330-
}
331-
else if(type_id==ID_rational)
332-
{
333-
rationalt a, b;
334-
if(!to_rational(*this, a) && !to_rational(expr, b))
335-
{
336-
exprt a_plus_b=from_rational(a+b);
337-
set(ID_value, a_plus_b.get_string(ID_value));
338-
return false;
339-
}
340-
}
341-
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
342-
{
343-
set(ID_value, integer2binary(
344-
binary2integer(get_string(ID_value), false)+
345-
binary2integer(expr.get_string(ID_value), false),
346-
unsafe_string2unsigned(type().get_string(ID_width))));
347-
return false;
348-
}
349-
else if(type_id==ID_fixedbv)
350-
{
351-
set(ID_value, integer2binary(
352-
binary2integer(get_string(ID_value), false)+
353-
binary2integer(expr.get_string(ID_value), false),
354-
unsafe_string2unsigned(type().get_string(ID_width))));
355-
return false;
356-
}
357-
else if(type_id==ID_floatbv)
358-
{
359-
ieee_floatt f(to_constant_expr(*this));
360-
f+=ieee_floatt(to_constant_expr(expr));
361-
*this=f.to_expr();
362-
return false;
363-
}
364-
365-
return true;
366-
}
367-
368-
bool exprt::mul(const exprt &expr)
369-
{
370-
if(!is_constant() || !expr.is_constant())
371-
return true;
372-
if(type()!=expr.type())
373-
return true;
374-
375-
const irep_idt &type_id=type().id();
376-
377-
if(type_id==ID_integer || type_id==ID_natural)
378-
{
379-
set(ID_value, integer2string(
380-
string2integer(get_string(ID_value))*
381-
string2integer(expr.get_string(ID_value))));
382-
return false;
383-
}
384-
else if(type_id==ID_rational)
385-
{
386-
rationalt a, b;
387-
if(!to_rational(*this, a) && !to_rational(expr, b))
388-
{
389-
exprt a_mul_b=from_rational(a*b);
390-
set(ID_value, a_mul_b.get_string(ID_value));
391-
return false;
392-
}
393-
}
394-
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
395-
{
396-
// the following works for signed and unsigned integers
397-
set(ID_value, integer2binary(
398-
binary2integer(get_string(ID_value), false)*
399-
binary2integer(expr.get_string(ID_value), false),
400-
unsafe_string2unsigned(type().get_string(ID_width))));
401-
return false;
402-
}
403-
else if(type_id==ID_fixedbv)
404-
{
405-
fixedbvt f(to_constant_expr(*this));
406-
f*=fixedbvt(to_constant_expr(expr));
407-
*this=f.to_expr();
408-
return false;
409-
}
410-
else if(type_id==ID_floatbv)
411-
{
412-
ieee_floatt f(to_constant_expr(*this));
413-
f*=ieee_floatt(to_constant_expr(expr));
414-
*this=f.to_expr();
415-
return false;
416-
}
417-
418-
return true;
419-
}
420-
421-
bool exprt::subtract(const exprt &expr)
422-
{
423-
if(!is_constant() || !expr.is_constant())
424-
return true;
425-
426-
if(type()!=expr.type())
427-
return true;
428-
429-
const irep_idt &type_id=type().id();
430-
431-
if(type_id==ID_integer || type_id==ID_natural)
432-
{
433-
set(ID_value, integer2string(
434-
string2integer(get_string(ID_value))-
435-
string2integer(expr.get_string(ID_value))));
436-
return false;
437-
}
438-
else if(type_id==ID_rational)
439-
{
440-
rationalt a, b;
441-
if(!to_rational(*this, a) && !to_rational(expr, b))
442-
{
443-
exprt a_minus_b=from_rational(a-b);
444-
set(ID_value, a_minus_b.get_string(ID_value));
445-
return false;
446-
}
447-
}
448-
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
449-
{
450-
set(ID_value, integer2binary(
451-
binary2integer(get_string(ID_value), false)-
452-
binary2integer(expr.get_string(ID_value), false),
453-
unsafe_string2unsigned(type().get_string(ID_width))));
454-
return false;
455-
}
456-
457-
return true;
458-
}
459-
460250
const source_locationt &exprt::find_source_location() const
461251
{
462252
const source_locationt &l=source_location();

‎src/util/expr.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -113,11 +113,6 @@ class exprt:public irept
113113
void make_true();
114114
void make_false();
115115
void make_bool(bool value);
116-
void negate();
117-
118-
bool sum(const exprt &expr);
119-
bool mul(const exprt &expr);
120-
bool subtract(const exprt &expr);
121116

122117
bool is_constant() const;
123118
bool is_true() const;

0 commit comments

Comments
 (0)