Skip to content

Commit

Permalink
remove exprt::negate, sum, mul, subtract (deprecated since 2011)
Browse files Browse the repository at this point in the history
  • Loading branch information
Daniel Kroening committed Mar 4, 2018
1 parent 0d0dca4 commit 4d87ba1
Show file tree
Hide file tree
Showing 3 changed files with 125 additions and 231 deletions.
222 changes: 6 additions & 216 deletions src/util/expr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,19 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com
/// \file
/// Expression Representation

#include "arith_tools.h"
#include "expr.h"
#include <cassert>
#include <stack>
#include "string2int.h"
#include "mp_arith.h"
#include "expr_iterator.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "invariant.h"
#include "expr_iterator.h"
#include "mp_arith.h"
#include "rational.h"
#include "rational_tools.h"
#include "arith_tools.h"
#include "std_expr.h"
#include "string2int.h"

#include <stack>

void exprt::move_to_operands(exprt &expr)
{
Expand Down Expand Up @@ -157,71 +157,6 @@ void exprt::make_false()
set(ID_value, ID_false);
}

void exprt::negate()
{
const irep_idt &type_id=type().id();

if(type_id==ID_bool)
make_not();
else
{
if(is_constant())
{
const irep_idt &value=get(ID_value);

if(type_id==ID_integer)
{
set(ID_value, integer2string(-string2integer(id2string(value))));
}
else if(type_id==ID_unsignedbv)
{
mp_integer int_value=binary2integer(id2string(value), false);
typet _type=type();
*this=from_integer(-int_value, _type);
}
else if(type_id==ID_signedbv)
{
mp_integer int_value=binary2integer(id2string(value), true);
typet _type=type();
*this=from_integer(-int_value, _type);
}
else if(type_id==ID_fixedbv)
{
fixedbvt fixedbv_value=fixedbvt(to_constant_expr(*this));
fixedbv_value.negate();
*this=fixedbv_value.to_expr();
}
else if(type_id==ID_floatbv)
{
ieee_floatt ieee_float_value=ieee_floatt(to_constant_expr(*this));
ieee_float_value.negate();
*this=ieee_float_value.to_expr();
}
else
{
make_nil();
UNREACHABLE;
}
}
else
{
if(id()==ID_unary_minus)
{
exprt tmp;
DATA_INVARIANT(operands().size()==1,
"Unary minus must have one operand");
tmp.swap(op0());
swap(tmp);
}
else
{
unary_minus_exprt tmp(*this);
swap(tmp);
}
}
}
}

bool exprt::is_boolean() const
{
return type().id()==ID_bool;
Expand Down Expand Up @@ -312,151 +247,6 @@ bool exprt::is_one() const
return false;
}

bool exprt::sum(const exprt &expr)
{
if(!is_constant() || !expr.is_constant())
return true;
if(type()!=expr.type())
return true;

const irep_idt &type_id=type().id();

if(type_id==ID_integer || type_id==ID_natural)
{
set(ID_value, integer2string(
string2integer(get_string(ID_value))+
string2integer(expr.get_string(ID_value))));
return false;
}
else if(type_id==ID_rational)
{
rationalt a, b;
if(!to_rational(*this, a) && !to_rational(expr, b))
{
exprt a_plus_b=from_rational(a+b);
set(ID_value, a_plus_b.get_string(ID_value));
return false;
}
}
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
{
set(ID_value, integer2binary(
binary2integer(get_string(ID_value), false)+
binary2integer(expr.get_string(ID_value), false),
unsafe_string2unsigned(type().get_string(ID_width))));
return false;
}
else if(type_id==ID_fixedbv)
{
set(ID_value, integer2binary(
binary2integer(get_string(ID_value), false)+
binary2integer(expr.get_string(ID_value), false),
unsafe_string2unsigned(type().get_string(ID_width))));
return false;
}
else if(type_id==ID_floatbv)
{
ieee_floatt f(to_constant_expr(*this));
f+=ieee_floatt(to_constant_expr(expr));
*this=f.to_expr();
return false;
}

return true;
}

bool exprt::mul(const exprt &expr)
{
if(!is_constant() || !expr.is_constant())
return true;
if(type()!=expr.type())
return true;

const irep_idt &type_id=type().id();

if(type_id==ID_integer || type_id==ID_natural)
{
set(ID_value, integer2string(
string2integer(get_string(ID_value))*
string2integer(expr.get_string(ID_value))));
return false;
}
else if(type_id==ID_rational)
{
rationalt a, b;
if(!to_rational(*this, a) && !to_rational(expr, b))
{
exprt a_mul_b=from_rational(a*b);
set(ID_value, a_mul_b.get_string(ID_value));
return false;
}
}
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
{
// the following works for signed and unsigned integers
set(ID_value, integer2binary(
binary2integer(get_string(ID_value), false)*
binary2integer(expr.get_string(ID_value), false),
unsafe_string2unsigned(type().get_string(ID_width))));
return false;
}
else if(type_id==ID_fixedbv)
{
fixedbvt f(to_constant_expr(*this));
f*=fixedbvt(to_constant_expr(expr));
*this=f.to_expr();
return false;
}
else if(type_id==ID_floatbv)
{
ieee_floatt f(to_constant_expr(*this));
f*=ieee_floatt(to_constant_expr(expr));
*this=f.to_expr();
return false;
}

return true;
}

bool exprt::subtract(const exprt &expr)
{
if(!is_constant() || !expr.is_constant())
return true;

if(type()!=expr.type())
return true;

const irep_idt &type_id=type().id();

if(type_id==ID_integer || type_id==ID_natural)
{
set(ID_value, integer2string(
string2integer(get_string(ID_value))-
string2integer(expr.get_string(ID_value))));
return false;
}
else if(type_id==ID_rational)
{
rationalt a, b;
if(!to_rational(*this, a) && !to_rational(expr, b))
{
exprt a_minus_b=from_rational(a-b);
set(ID_value, a_minus_b.get_string(ID_value));
return false;
}
}
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
{
set(ID_value, integer2binary(
binary2integer(get_string(ID_value), false)-
binary2integer(expr.get_string(ID_value), false),
unsafe_string2unsigned(type().get_string(ID_width))));
return false;
}

return true;
}

const source_locationt &exprt::find_source_location() const
{
const source_locationt &l=source_location();
Expand Down
5 changes: 0 additions & 5 deletions src/util/expr.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,11 +113,6 @@ class exprt:public irept
void make_true();
void make_false();
void make_bool(bool value);
void negate();

bool sum(const exprt &expr);
bool mul(const exprt &expr);
bool subtract(const exprt &expr);

bool is_constant() const;
bool is_true() const;
Expand Down
Loading

0 comments on commit 4d87ba1

Please sign in to comment.