CBMC
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | Static Private Member Functions | Friends | List of all members
constant_interval_exprt Class Reference

Represents an interval of values. More...

#include <interval.h>

+ Inheritance diagram for constant_interval_exprt:
[フレーム]
[legend]
+ Collaboration diagram for constant_interval_exprt:
[フレーム]
[legend]

Public Member Functions

  constant_interval_exprt (exprt lower, exprt upper, typet type)
 
  constant_interval_exprt (const typet &type)
 
  constant_interval_exprt (const exprt &lower, const exprt &upper)
 
bool  is_well_formed () const
 
const exprt &  get_lower () const
 
const exprt &  get_upper () const
 
constant_interval_exprt  handle_constant_unary_expression (const irep_idt &op) const
  SET OF ARITHMETIC OPERATORS.
 
constant_interval_exprt  handle_constant_binary_expression (const constant_interval_exprt &other, const irep_idt &) const
 
constant_interval_exprt  eval (const irep_idt &unary_operator) const
 
constant_interval_exprt  eval (const irep_idt &binary_operator, const constant_interval_exprt &o) const
 
constant_interval_exprt  unary_plus () const
 
constant_interval_exprt  unary_minus () const
 
constant_interval_exprt  typecast (const typet &type) const
 
tvt  is_definitely_true () const
 
tvt  is_definitely_false () const
 
tvt  logical_and (const constant_interval_exprt &o) const
 
tvt  logical_or (const constant_interval_exprt &o) const
 
tvt  logical_xor (const constant_interval_exprt &o) const
 
tvt  logical_not () const
 
constant_interval_exprt  plus (const constant_interval_exprt &o) const
 
constant_interval_exprt  minus (const constant_interval_exprt &other) const
 
constant_interval_exprt  multiply (const constant_interval_exprt &o) const
 
constant_interval_exprt  divide (const constant_interval_exprt &o) const
 
constant_interval_exprt  modulo (const constant_interval_exprt &o) const
 
constant_interval_exprt  left_shift (const constant_interval_exprt &o) const
 
constant_interval_exprt  right_shift (const constant_interval_exprt &o) const
 
constant_interval_exprt  bitwise_not () const
 
constant_interval_exprt  bitwise_xor (const constant_interval_exprt &o) const
 
constant_interval_exprt  bitwise_or (const constant_interval_exprt &o) const
 
constant_interval_exprt  bitwise_and (const constant_interval_exprt &o) const
 
tvt  less_than (const constant_interval_exprt &o) const
 
tvt  greater_than (const constant_interval_exprt &o) const
 
tvt  less_than_or_equal (const constant_interval_exprt &o) const
 
tvt  greater_than_or_equal (const constant_interval_exprt &o) const
 
tvt  equal (const constant_interval_exprt &o) const
 
tvt  not_equal (const constant_interval_exprt &o) const
 
constant_interval_exprt  increment () const
 
constant_interval_exprt  decrement () const
 
bool  is_empty () const
 
bool  is_single_value_interval () const
 
std::string  to_string () const
 
bool  is_top () const
 
bool  is_bottom () const
 
constant_interval_exprt  top () const
 
constant_interval_exprt  bottom () const
 
bool  has_no_lower_bound () const
 
bool  has_no_upper_bound () const
 
min_value_exprt  min () const
 
max_value_exprt  max () const
 
constant_exprt  zero () const
 
bool  is_numeric () const
 
bool  is_int () const
 
bool  is_float () const
 
bool  is_bitvector () const
 
bool  is_signed () const
 
bool  is_unsigned () const
 
bool  contains_zero () const
 
bool  contains (const constant_interval_exprt &interval) const
 
bool  is_positive () const
 
bool  is_zero () const
 
bool  is_negative () const
 
- Public Member Functions inherited from binary_exprt
  binary_exprt (const exprt &_lhs, const irep_idt &_id, exprt _rhs)
 
  binary_exprt (exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
 
exprt &  lhs ()
 
const exprt &  lhs () const
 
exprt &  rhs ()
 
const exprt &  rhs () const
 
const exprt &  op2 () const =delete
 
exprt &  op2 ()=delete
 
const exprt &  op3 () const =delete
 
exprt &  op3 ()=delete
 
exprt &  op0 ()
 
const exprt &  op0 () const
 
exprt &  op1 ()
 
const exprt &  op1 () const
 
- Public Member Functions inherited from exprt
  exprt ()
 
  exprt (const irep_idt &_id)
 
  exprt (irep_idt _id, typet _type)
 
  exprt (irep_idt _id, typet _type, operandst &&_operands)
 
  exprt (const irep_idt &id, typet type, source_locationt loc)
 
typet &  type ()
  Return the type of the expression.
 
const typet &  type () const
 
bool  has_operands () const
  Return true if there is at least one operand.
 
operandst &  operands ()
 
const operandst &  operands () const
 
exprt &  with_source_location (source_locationt location) &
  Add the source location from location, if it is non-nil.
 
exprt &&  with_source_location (source_locationt location) &&
  Add the source location from location, if it is non-nil.
 
exprt &  with_source_location (const exprt &other) &
  Add the source location from other, if it has any.
 
exprt &&  with_source_location (const exprt &other) &&
  Add the source location from other, if it has any.
 
void  reserve_operands (operandst::size_type n)
 
void  copy_to_operands (const exprt &expr)
  Copy the given argument to the end of exprt's operands.
 
void  add_to_operands (const exprt &expr)
  Add the given argument to the end of exprt's operands.
 
void  add_to_operands (exprt &&expr)
  Add the given argument to the end of exprt's operands.
 
void  add_to_operands (exprt &&e1, exprt &&e2)
  Add the given arguments to the end of exprt's operands.
 
void  add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3)
  Add the given arguments to the end of exprt's operands.
 
bool  is_constant () const
  Return whether the expression is a constant.
 
bool  is_true () const
  Return whether the expression is a constant representing true.
 
bool  is_false () const
  Return whether the expression is a constant representing false.
 
bool  is_zero () const
  Return whether the expression is a constant representing 0.
 
bool  is_one () const
  Return whether the expression is a constant representing 1.
 
bool  is_boolean () const
  Return whether the expression represents a Boolean.
 
const source_locationt &  find_source_location () const
  Get a source_locationt from the expression or from its operands (non-recursively).
 
const source_locationt &  source_location () const
 
source_locationt &  add_source_location ()
 
void  drop_source_location ()
 
void  visit (class expr_visitort &visitor)
  These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children have been visited.
 
void  visit (class const_expr_visitort &visitor) const
 
void  visit_pre (std::function< void(exprt &)>)
 
void  visit_pre (std::function< void(const exprt &)>) const
 
void  visit_post (std::function< void(exprt &)>)
  These are post-order traversal visitors, i.e., the visitor is executed on a node after its children have been visited.
 
void  visit_post (std::function< void(const exprt &)>) const
 
depth_iteratort  depth_begin ()
 
depth_iteratort  depth_end ()
 
const_depth_iteratort  depth_begin () const
 
const_depth_iteratort  depth_end () const
 
const_depth_iteratort  depth_cbegin () const
 
const_depth_iteratort  depth_cend () const
 
depth_iteratort  depth_begin (std::function< exprt &()> mutate_root) const
 
const_unique_depth_iteratort  unique_depth_begin () const
 
const_unique_depth_iteratort  unique_depth_end () const
 
const_unique_depth_iteratort  unique_depth_cbegin () const
 
const_unique_depth_iteratort  unique_depth_cend () const
 
- Public Member Functions inherited from irept
bool  is_nil () const
 
bool  is_not_nil () const
 
  irept (const irep_idt &_id)
 
  irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
 
  irept ()=default
 
const irep_idt &  id () const
 
const std::string &  id_string () const
 
void  id (const irep_idt &_data)
 
const irept &  find (const irep_idt &name) const
 
irept &  add (const irep_idt &name)
 
irept &  add (const irep_idt &name, irept irep)
 
const std::string &  get_string (const irep_idt &name) const
 
const irep_idt &  get (const irep_idt &name) const
 
bool  get_bool (const irep_idt &name) const
 
signed int  get_int (const irep_idt &name) const
 
std::size_t  get_size_t (const irep_idt &name) const
 
long long  get_long_long (const irep_idt &name) const
 
void  set (const irep_idt &name, const irep_idt &value)
 
void  set (const irep_idt &name, irept irep)
 
void  set (const irep_idt &name, const long long value)
 
void  set_size_t (const irep_idt &name, const std::size_t value)
 
void  remove (const irep_idt &name)
 
void  move_to_sub (irept &irep)
 
void  move_to_named_sub (const irep_idt &name, irept &irep)
 
bool  operator== (const irept &other) const
 
bool  operator!= (const irept &other) const
 
void  swap (irept &irep)
 
bool  operator< (const irept &other) const
  defines ordering on the internal representation
 
bool  ordering (const irept &other) const
  defines ordering on the internal representation
 
int  compare (const irept &i) const
  defines ordering on the internal representation comments are ignored
 
void  clear ()
 
void  make_nil ()
 
subt &  get_sub ()
 
const subt &  get_sub () const
 
named_subt &  get_named_sub ()
 
const named_subt &  get_named_sub () const
 
std::size_t  hash () const
 
std::size_t  full_hash () const
 
bool  full_eq (const irept &other) const
 
std::string  pretty (unsigned indent=0, unsigned max_indent=0) const
 
- Public Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
  sharing_treet (irep_idt _id)
 
  sharing_treet (irep_idt _id, named_subt _named_sub, subt _sub)
 
  sharing_treet ()
 
  sharing_treet (const sharing_treet &irep)
 
  sharing_treet (sharing_treet &&irep)
 
sharing_treet &  operator= (const sharing_treet &irep)
 
sharing_treet &  operator= (sharing_treet &&irep)
 
  ~sharing_treet ()
 
const dt &  read () const
 
dt &  write ()
 

Static Public Member Functions

static constant_interval_exprt  singleton (const exprt &x)
 
static bool  is_valid_bound (const exprt &expr)
 
static constant_interval_exprt  tvt_to_interval (const tvt &val)
 
static bool  equal (const exprt &a, const exprt &b)
  END SET OF ARITHMETIC OPERATORS.
 
static bool  not_equal (const exprt &a, const exprt &b)
 
static bool  less_than (const exprt &a, const exprt &b)
 
static bool  less_than_or_equal (const exprt &a, const exprt &b)
 
static bool  greater_than (const exprt &a, const exprt &b)
 
static bool  greater_than_or_equal (const exprt &a, const exprt &b)
 
static tvt  is_true (const constant_interval_exprt &a)
 
static tvt  is_false (const constant_interval_exprt &a)
 
static tvt  logical_and (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  logical_or (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  logical_xor (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  logical_not (const constant_interval_exprt &a)
 
static constant_interval_exprt  unary_plus (const constant_interval_exprt &a)
 
static constant_interval_exprt  unary_minus (const constant_interval_exprt &a)
 
static constant_interval_exprt  plus (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  minus (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  multiply (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  divide (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  modulo (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  left_shift (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  right_shift (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  bitwise_not (const constant_interval_exprt &a)
 
static constant_interval_exprt  bitwise_xor (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  bitwise_or (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  bitwise_and (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  less_than (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  greater_than (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  less_than_or_equal (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  greater_than_or_equal (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  equal (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static tvt  not_equal (const constant_interval_exprt &a, const constant_interval_exprt &b)
 
static constant_interval_exprt  increment (const constant_interval_exprt &a)
 
static constant_interval_exprt  decrement (const constant_interval_exprt &a)
 
static bool  is_empty (const constant_interval_exprt &a)
 
static bool  is_single_value_interval (const constant_interval_exprt &a)
 
static bool  is_top (const constant_interval_exprt &a)
 
static bool  is_bottom (const constant_interval_exprt &a)
 
static bool  is_min (const constant_interval_exprt &a)
 
static bool  is_max (const constant_interval_exprt &a)
 
static constant_interval_exprt  top (const typet &type)
 
static constant_interval_exprt  bottom (const typet &type)
 
static bool  is_min (const exprt &expr)
 
static bool  is_max (const exprt &expr)
 
static constant_exprt  zero (const typet &type)
 
static constant_exprt  zero (const exprt &expr)
 
static constant_exprt  zero (const constant_interval_exprt &interval)
 
static constant_interval_exprt  get_extremes (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs, const irep_idt &operation)
 
static exprt  get_extreme (std::vector< exprt > values, bool min=true)
 
static exprt  get_max (const exprt &a, const exprt &b)
 
static exprt  get_min (const exprt &a, const exprt &b)
 
static exprt  get_min (std::vector< exprt > &values)
 
static exprt  get_max (std::vector< exprt > &values)
 
static constant_interval_exprt  simplified_interval (exprt &l, exprt &r)
 
static exprt  simplified_expr (exprt expr)
 
static bool  is_numeric (const typet &type)
 
static bool  is_numeric (const exprt &expr)
 
static bool  is_numeric (const constant_interval_exprt &interval)
 
static bool  is_int (const typet &type)
 
static bool  is_int (const exprt &expr)
 
static bool  is_int (const constant_interval_exprt &interval)
 
static bool  is_float (const typet &type)
 
static bool  is_float (const exprt &expr)
 
static bool  is_float (const constant_interval_exprt &interval)
 
static bool  is_bitvector (const typet &type)
 
static bool  is_bitvector (const constant_interval_exprt &interval)
 
static bool  is_bitvector (const exprt &expr)
 
static bool  is_signed (const typet &type)
 
static bool  is_signed (const exprt &expr)
 
static bool  is_signed (const constant_interval_exprt &interval)
 
static bool  is_unsigned (const typet &type)
 
static bool  is_unsigned (const exprt &expr)
 
static bool  is_unsigned (const constant_interval_exprt &interval)
 
static bool  is_extreme (const exprt &expr)
 
static bool  is_extreme (const exprt &expr1, const exprt &expr2)
 
static bool  contains_extreme (const exprt expr)
 
static bool  contains_extreme (const exprt expr1, const exprt expr2)
 
static bool  is_positive (const exprt &expr)
 
static bool  is_positive (const constant_interval_exprt &interval)
 
static bool  is_zero (const exprt &expr)
 
static bool  is_zero (const constant_interval_exprt &interval)
 
static bool  is_negative (const exprt &expr)
 
static bool  is_negative (const constant_interval_exprt &interval)
 
static exprt  abs (const exprt &expr)
 
- Static Public Member Functions inherited from binary_exprt
static void  check (const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
 
static void  validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
 
- Static Public Member Functions inherited from exprt
static void  check (const exprt &, const validation_modet=validation_modet::INVARIANT)
  Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked).
 
static void  validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
  Check that the expression is well-formed, assuming that its subexpressions and type have all ready been checked for well-formedness.
 
static void  validate_full (const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
  Check that the expression is well-formed (full check, including checks of all subexpressions and the type)
 
- Static Public Member Functions inherited from irept
static bool  is_comment (const irep_idt &name)
 
static std::size_t  number_of_non_comments (const named_subt &)
  count the number of named_sub elements that are not comments
 

Static Private Member Functions

static void  generate_expression (const exprt &lhs, const exprt &rhs, const irep_idt &operation, std::vector< exprt > &collection)
 
static void  append_multiply_expression (const exprt &lower, const exprt &upper, std::vector< exprt > &collection)
  Adds all possible values that may arise from multiplication (more than one, in case of past the type boundary results).
 
static void  append_multiply_expression_max (const exprt &expr, std::vector< exprt > &collection)
  Appends interval bounds that could arise from MAX * expr.
 
static void  append_multiply_expression_min (const exprt &min, const exprt &other, std::vector< exprt > &collection)
  Appends interval bounds that could arise from MIN * other.
 
static exprt  generate_division_expression (const exprt &lhs, const exprt &rhs)
 
static exprt  generate_modulo_expression (const exprt &lhs, const exprt &rhs)
 
static exprt  generate_shift_expression (const exprt &lhs, const exprt &rhs, const irep_idt &operation)
 

Friends

bool  operator< (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
bool  operator> (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
bool  operator<= (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
bool  operator>= (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
bool  operator== (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
bool  operator!= (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator+ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator- (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator/ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator* (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator% (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator! (const constant_interval_exprt &lhs)
 
const constant_interval_exprt  operator& (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator| (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator^ (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator<< (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
const constant_interval_exprt  operator>> (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
std::ostream &  operator<< (std::ostream &out, const constant_interval_exprt &i)
 

Additional Inherited Members

- Public Types inherited from exprt
typedef std::vector< exprt >  operandst
 
- Public Types inherited from irept
using  baset = tree_implementationt
 
- Public Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
using  dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true >
 
using  subt = typename dt::subt
 
using  named_subt = typename dt::named_subt
 
using  tree_implementationt = sharing_treet
  Used to refer to this class from derived classes.
 
- Protected Member Functions inherited from expr_protectedt
  expr_protectedt (irep_idt _id, typet _type)
 
  expr_protectedt (irep_idt _id, typet _type, operandst _operands)
 
exprt &  op0 ()
 
const exprt &  op0 () const
 
exprt &  op1 ()
 
const exprt &  op1 () const
 
exprt &  op2 ()
 
const exprt &  op2 () const
 
exprt &  op3 ()
 
const exprt &  op3 () const
 
- Protected Member Functions inherited from exprt
exprt &  op0 ()
 
exprt &  op1 ()
 
exprt &  op2 ()
 
exprt &  op3 ()
 
const exprt &  op0 () const
 
const exprt &  op1 () const
 
const exprt &  op2 () const
 
const exprt &  op3 () const
 
exprt &  add_expr (const irep_idt &name)
 
const exprt &  find_expr (const irep_idt &name) const
 
- Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
void  detach ()
 
- Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
static void  remove_ref (dt *old_data)
 
static void  nonrecursive_destructor (dt *old_data)
  Does the same as remove_ref, but using an explicit stack instead of recursion.
 
- Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
dt *  data
 
- Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >
static dt  empty_d
 

Detailed Description

Represents an interval of values.

Bounds should be constant expressions or min_value_exprt for the lower bound or max_value_exprt for the upper bound Also, lower bound should always be <= upper bound

Definition at line 51 of file interval.h.

Constructor & Destructor Documentation

◆  constant_interval_exprt() [1/3]

constant_interval_exprt::constant_interval_exprt ( exprt  lower,
exprt  upper,
typet  type 
)
inline

Definition at line 54 of file interval.h.

◆  constant_interval_exprt() [2/3]

constant_interval_exprt::constant_interval_exprt ( const typet &  type )
inlineexplicit

Definition at line 64 of file interval.h.

◆  constant_interval_exprt() [3/3]

constant_interval_exprt::constant_interval_exprt ( const exprt &  lower,
const exprt &  upper 
)
inline

Definition at line 72 of file interval.h.

Member Function Documentation

◆  abs()

exprt constant_interval_exprt::abs ( const exprt &  expr )
static

Definition at line 1300 of file interval.cpp.

◆  append_multiply_expression()

void constant_interval_exprt::append_multiply_expression ( const exprt &  lower,
const exprt &  upper,
std::vector< exprt > &  collection 
)
staticprivate

Adds all possible values that may arise from multiplication (more than one, in case of past the type boundary results).

Parameters
lower lhs of multiplication
upper rhs of multiplication
collection vector of possible values

Definition at line 601 of file interval.cpp.

◆  append_multiply_expression_max()

void constant_interval_exprt::append_multiply_expression_max ( const exprt &  expr,
std::vector< exprt > &  collection 
)
staticprivate

Appends interval bounds that could arise from MAX * expr.

Accommodates for overflows by over-approximating.

Parameters
expr the unknown side of multiplication
collection vector of collected bounds

Definition at line 639 of file interval.cpp.

◆  append_multiply_expression_min()

void constant_interval_exprt::append_multiply_expression_min ( const exprt &  min,
const exprt &  other,
std::vector< exprt > &  collection 
)
staticprivate

Appends interval bounds that could arise from MIN * other.

Accommodates for overflows by over-approximating.

Parameters
min the side known to be MIN for a given type
other the side of unknown value
collection reference to the vector of collected boundaries

Definition at line 664 of file interval.cpp.

◆  bitwise_and() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_and ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1738 of file interval.cpp.

◆  bitwise_and() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_and ( const constant_interval_exprt &  o ) const

Definition at line 356 of file interval.cpp.

◆  bitwise_not() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_not ( ) const

Definition at line 366 of file interval.cpp.

◆  bitwise_not() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_not ( const constant_interval_exprt &  a )
static

Definition at line 1718 of file interval.cpp.

◆  bitwise_or() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_or ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1731 of file interval.cpp.

◆  bitwise_or() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_or ( const constant_interval_exprt &  o ) const

Definition at line 345 of file interval.cpp.

◆  bitwise_xor() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_xor ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1724 of file interval.cpp.

◆  bitwise_xor() [2/2]

constant_interval_exprt constant_interval_exprt::bitwise_xor ( const constant_interval_exprt &  o ) const

Definition at line 334 of file interval.cpp.

◆  bottom() [1/2]

constant_interval_exprt constant_interval_exprt::bottom ( ) const

Definition at line 1058 of file interval.cpp.

◆  bottom() [2/2]

constant_interval_exprt constant_interval_exprt::bottom ( const typet &  type )
static

Definition at line 1048 of file interval.cpp.

◆  contains()

bool constant_interval_exprt::contains ( const constant_interval_exprt &  interval ) const

Definition at line 1427 of file interval.cpp.

◆  contains_extreme() [1/2]

bool constant_interval_exprt::contains_extreme ( const exprt  expr )
static

Definition at line 1830 of file interval.cpp.

◆  contains_extreme() [2/2]

bool constant_interval_exprt::contains_extreme ( const exprt  expr1,
const exprt  expr2 
)
static

Definition at line 1848 of file interval.cpp.

◆  contains_zero()

bool constant_interval_exprt::contains_zero ( ) const

Definition at line 1871 of file interval.cpp.

◆  decrement() [1/2]

constant_interval_exprt constant_interval_exprt::decrement ( ) const

Definition at line 465 of file interval.cpp.

◆  decrement() [2/2]

constant_interval_exprt constant_interval_exprt::decrement ( const constant_interval_exprt &  a )
static

Definition at line 1794 of file interval.cpp.

◆  divide() [1/2]

constant_interval_exprt constant_interval_exprt::divide ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1687 of file interval.cpp.

◆  divide() [2/2]

constant_interval_exprt constant_interval_exprt::divide ( const constant_interval_exprt &  o ) const

Definition at line 135 of file interval.cpp.

◆  equal() [1/3]

tvt constant_interval_exprt::equal ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1773 of file interval.cpp.

◆  equal() [2/3]

tvt constant_interval_exprt::equal ( const constant_interval_exprt &  o ) const

Definition at line 431 of file interval.cpp.

◆  equal() [3/3]

bool constant_interval_exprt::equal ( const exprt &  a,
const exprt &  b 
)
static

END SET OF ARITHMETIC OPERATORS.

Definition at line 1315 of file interval.cpp.

◆  eval() [1/2]

constant_interval_exprt constant_interval_exprt::eval ( const irep_idt &  binary_operator,
const constant_interval_exprt &  o 
) const

Definition at line 815 of file interval.cpp.

◆  eval() [2/2]

constant_interval_exprt constant_interval_exprt::eval ( const irep_idt &  unary_operator ) const

Definition at line 793 of file interval.cpp.

◆  generate_division_expression()

exprt constant_interval_exprt::generate_division_expression ( const exprt &  lhs,
const exprt &  rhs 
)
staticprivate

Definition at line 684 of file interval.cpp.

◆  generate_expression()

void constant_interval_exprt::generate_expression ( const exprt &  lhs,
const exprt &  rhs,
const irep_idt &  operation,
std::vector< exprt > &  collection 
)
staticprivate

Definition at line 572 of file interval.cpp.

◆  generate_modulo_expression()

exprt constant_interval_exprt::generate_modulo_expression ( const exprt &  lhs,
const exprt &  rhs 
)
staticprivate

Definition at line 739 of file interval.cpp.

◆  generate_shift_expression()

exprt constant_interval_exprt::generate_shift_expression ( const exprt &  lhs,
const exprt &  rhs,
const irep_idt &  operation 
)
staticprivate

Definition at line 899 of file interval.cpp.

◆  get_extreme()

exprt constant_interval_exprt::get_extreme ( std::vector< exprt >  values,
bool  min = true  
)
static

Definition at line 497 of file interval.cpp.

◆  get_extremes()

constant_interval_exprt constant_interval_exprt::get_extremes ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs,
const irep_idt &  operation 
)
static

Definition at line 471 of file interval.cpp.

◆  get_lower()

const exprt & constant_interval_exprt::get_lower ( ) const

Definition at line 27 of file interval.cpp.

◆  get_max() [1/2]

exprt constant_interval_exprt::get_max ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 960 of file interval.cpp.

◆  get_max() [2/2]

exprt constant_interval_exprt::get_max ( std::vector< exprt > &  values )
static

Definition at line 975 of file interval.cpp.

◆  get_min() [1/2]

exprt constant_interval_exprt::get_min ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 965 of file interval.cpp.

◆  get_min() [2/2]

exprt constant_interval_exprt::get_min ( std::vector< exprt > &  values )
static

Definition at line 970 of file interval.cpp.

◆  get_upper()

const exprt & constant_interval_exprt::get_upper ( ) const

Definition at line 32 of file interval.cpp.

◆  greater_than() [1/3]

tvt constant_interval_exprt::greater_than ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1752 of file interval.cpp.

◆  greater_than() [2/3]

tvt constant_interval_exprt::greater_than ( const constant_interval_exprt &  o ) const

Definition at line 397 of file interval.cpp.

◆  greater_than() [3/3]

bool constant_interval_exprt::greater_than ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 1405 of file interval.cpp.

◆  greater_than_or_equal() [1/3]

tvt constant_interval_exprt::greater_than_or_equal ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1766 of file interval.cpp.

◆  greater_than_or_equal() [2/3]

tvt constant_interval_exprt::greater_than_or_equal ( const constant_interval_exprt &  o ) const

Definition at line 425 of file interval.cpp.

◆  greater_than_or_equal() [3/3]

bool constant_interval_exprt::greater_than_or_equal ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 1415 of file interval.cpp.

◆  handle_constant_binary_expression()

constant_interval_exprt constant_interval_exprt::handle_constant_binary_expression ( const constant_interval_exprt &  other,
const irep_idt &  op 
) const

Definition at line 951 of file interval.cpp.

◆  handle_constant_unary_expression()

constant_interval_exprt constant_interval_exprt::handle_constant_unary_expression ( const irep_idt &  op ) const

SET OF ARITHMETIC OPERATORS.

Definition at line 939 of file interval.cpp.

◆  has_no_lower_bound()

bool constant_interval_exprt::has_no_lower_bound ( ) const

Definition at line 1211 of file interval.cpp.

◆  has_no_upper_bound()

bool constant_interval_exprt::has_no_upper_bound ( ) const

Definition at line 1206 of file interval.cpp.

◆  increment() [1/2]

constant_interval_exprt constant_interval_exprt::increment ( ) const

Definition at line 459 of file interval.cpp.

◆  increment() [2/2]

constant_interval_exprt constant_interval_exprt::increment ( const constant_interval_exprt &  a )
static

Definition at line 1788 of file interval.cpp.

◆  is_bitvector() [1/4]

bool constant_interval_exprt::is_bitvector ( ) const

Definition at line 1191 of file interval.cpp.

◆  is_bitvector() [2/4]

bool constant_interval_exprt::is_bitvector ( const constant_interval_exprt &  interval )
static

Definition at line 1160 of file interval.cpp.

◆  is_bitvector() [3/4]

bool constant_interval_exprt::is_bitvector ( const exprt &  expr )
static

Definition at line 1176 of file interval.cpp.

◆  is_bitvector() [4/4]

bool constant_interval_exprt::is_bitvector ( const typet &  type )
static

Definition at line 1126 of file interval.cpp.

◆  is_bottom() [1/2]

bool constant_interval_exprt::is_bottom ( ) const

Definition at line 1037 of file interval.cpp.

◆  is_bottom() [2/2]

bool constant_interval_exprt::is_bottom ( const constant_interval_exprt &  a )
static

Definition at line 1815 of file interval.cpp.

◆  is_definitely_false()

tvt constant_interval_exprt::is_definitely_false ( ) const

Definition at line 223 of file interval.cpp.

◆  is_definitely_true()

tvt constant_interval_exprt::is_definitely_true ( ) const

Definition at line 217 of file interval.cpp.

◆  is_empty() [1/2]

bool constant_interval_exprt::is_empty ( ) const

Definition at line 1855 of file interval.cpp.

◆  is_empty() [2/2]

bool constant_interval_exprt::is_empty ( const constant_interval_exprt &  a )
static

Definition at line 1799 of file interval.cpp.

◆  is_extreme() [1/2]

bool constant_interval_exprt::is_extreme ( const exprt &  expr )
static

Definition at line 1196 of file interval.cpp.

◆  is_extreme() [2/2]

bool constant_interval_exprt::is_extreme ( const exprt &  expr1,
const exprt &  expr2 
)
static

Definition at line 1201 of file interval.cpp.

◆  is_false()

tvt constant_interval_exprt::is_false ( const constant_interval_exprt &  a )
static

Definition at line 1935 of file interval.cpp.

◆  is_float() [1/4]

bool constant_interval_exprt::is_float ( ) const

Definition at line 1070 of file interval.cpp.

◆  is_float() [2/4]

bool constant_interval_exprt::is_float ( const constant_interval_exprt &  interval )
static

Definition at line 1121 of file interval.cpp.

◆  is_float() [3/4]

bool constant_interval_exprt::is_float ( const exprt &  expr )
static

Definition at line 1116 of file interval.cpp.

◆  is_float() [4/4]

bool constant_interval_exprt::is_float ( const typet &  type )
static

Definition at line 1101 of file interval.cpp.

◆  is_int() [1/4]

bool constant_interval_exprt::is_int ( ) const

Definition at line 1065 of file interval.cpp.

◆  is_int() [2/4]

bool constant_interval_exprt::is_int ( const constant_interval_exprt &  interval )
static

Definition at line 1111 of file interval.cpp.

◆  is_int() [3/4]

bool constant_interval_exprt::is_int ( const exprt &  expr )
static

Definition at line 1106 of file interval.cpp.

◆  is_int() [4/4]

bool constant_interval_exprt::is_int ( const typet &  type )
static

Definition at line 1096 of file interval.cpp.

◆  is_max() [1/2]

bool constant_interval_exprt::is_max ( const constant_interval_exprt &  a )
static

Definition at line 1825 of file interval.cpp.

◆  is_max() [2/2]

bool constant_interval_exprt::is_max ( const exprt &  expr )
static

Definition at line 1216 of file interval.cpp.

◆  is_min() [1/2]

bool constant_interval_exprt::is_min ( const constant_interval_exprt &  a )
static

Definition at line 1820 of file interval.cpp.

◆  is_min() [2/2]

bool constant_interval_exprt::is_min ( const exprt &  expr )
static

Definition at line 1221 of file interval.cpp.

◆  is_negative() [1/3]

bool constant_interval_exprt::is_negative ( ) const

Definition at line 1925 of file interval.cpp.

◆  is_negative() [2/3]

bool constant_interval_exprt::is_negative ( const constant_interval_exprt &  interval )
static

Definition at line 1909 of file interval.cpp.

◆  is_negative() [3/3]

bool constant_interval_exprt::is_negative ( const exprt &  expr )
static

Definition at line 1280 of file interval.cpp.

◆  is_numeric() [1/4]

bool constant_interval_exprt::is_numeric ( ) const

Definition at line 1080 of file interval.cpp.

◆  is_numeric() [2/4]

bool constant_interval_exprt::is_numeric ( const constant_interval_exprt &  interval )
static

Definition at line 1090 of file interval.cpp.

◆  is_numeric() [3/4]

bool constant_interval_exprt::is_numeric ( const exprt &  expr )
static

Definition at line 1085 of file interval.cpp.

◆  is_numeric() [4/4]

bool constant_interval_exprt::is_numeric ( const typet &  type )
static

Definition at line 1075 of file interval.cpp.

◆  is_positive() [1/3]

bool constant_interval_exprt::is_positive ( ) const

Definition at line 1915 of file interval.cpp.

◆  is_positive() [2/3]

bool constant_interval_exprt::is_positive ( const constant_interval_exprt &  interval )
static

Definition at line 1898 of file interval.cpp.

◆  is_positive() [3/3]

bool constant_interval_exprt::is_positive ( const exprt &  expr )
static

Definition at line 1226 of file interval.cpp.

◆  is_signed() [1/4]

bool constant_interval_exprt::is_signed ( ) const

Definition at line 1181 of file interval.cpp.

◆  is_signed() [2/4]

bool constant_interval_exprt::is_signed ( const constant_interval_exprt &  interval )
static

Definition at line 1149 of file interval.cpp.

◆  is_signed() [3/4]

bool constant_interval_exprt::is_signed ( const exprt &  expr )
static

Definition at line 1166 of file interval.cpp.

◆  is_signed() [4/4]

bool constant_interval_exprt::is_signed ( const typet &  type )
static

Definition at line 1134 of file interval.cpp.

◆  is_single_value_interval() [1/2]

bool constant_interval_exprt::is_single_value_interval ( ) const

Definition at line 1865 of file interval.cpp.

◆  is_single_value_interval() [2/2]

bool constant_interval_exprt::is_single_value_interval ( const constant_interval_exprt &  a )
static

Definition at line 1804 of file interval.cpp.

◆  is_top() [1/2]

bool constant_interval_exprt::is_top ( ) const

Definition at line 1032 of file interval.cpp.

◆  is_top() [2/2]

bool constant_interval_exprt::is_top ( const constant_interval_exprt &  a )
static

Definition at line 1810 of file interval.cpp.

◆  is_true()

tvt constant_interval_exprt::is_true ( const constant_interval_exprt &  a )
static

Definition at line 1930 of file interval.cpp.

◆  is_unsigned() [1/4]

bool constant_interval_exprt::is_unsigned ( ) const

Definition at line 1186 of file interval.cpp.

◆  is_unsigned() [2/4]

bool constant_interval_exprt::is_unsigned ( const constant_interval_exprt &  interval )
static

Definition at line 1154 of file interval.cpp.

◆  is_unsigned() [3/4]

bool constant_interval_exprt::is_unsigned ( const exprt &  expr )
static

Definition at line 1171 of file interval.cpp.

◆  is_unsigned() [4/4]

bool constant_interval_exprt::is_unsigned ( const typet &  type )
static

Definition at line 1141 of file interval.cpp.

◆  is_valid_bound()

static bool constant_interval_exprt::is_valid_bound ( const exprt &  expr )
inlinestatic

Definition at line 104 of file interval.h.

◆  is_well_formed()

bool constant_interval_exprt::is_well_formed ( ) const
inline

Definition at line 78 of file interval.h.

◆  is_zero() [1/3]

bool constant_interval_exprt::is_zero ( ) const

Definition at line 1920 of file interval.cpp.

◆  is_zero() [2/3]

bool constant_interval_exprt::is_zero ( const constant_interval_exprt &  interval )
static

Definition at line 1904 of file interval.cpp.

◆  is_zero() [3/3]

bool constant_interval_exprt::is_zero ( const exprt &  expr )
static

Definition at line 1251 of file interval.cpp.

◆  left_shift() [1/2]

constant_interval_exprt constant_interval_exprt::left_shift ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1702 of file interval.cpp.

◆  left_shift() [2/2]

constant_interval_exprt constant_interval_exprt::left_shift ( const constant_interval_exprt &  o ) const

Definition at line 301 of file interval.cpp.

◆  less_than() [1/3]

tvt constant_interval_exprt::less_than ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1745 of file interval.cpp.

◆  less_than() [2/3]

tvt constant_interval_exprt::less_than ( const constant_interval_exprt &  o ) const

Definition at line 376 of file interval.cpp.

◆  less_than() [3/3]

bool constant_interval_exprt::less_than ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 1358 of file interval.cpp.

◆  less_than_or_equal() [1/3]

tvt constant_interval_exprt::less_than_or_equal ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1759 of file interval.cpp.

◆  less_than_or_equal() [2/3]

tvt constant_interval_exprt::less_than_or_equal ( const constant_interval_exprt &  o ) const

Definition at line 403 of file interval.cpp.

◆  less_than_or_equal() [3/3]

bool constant_interval_exprt::less_than_or_equal ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 1410 of file interval.cpp.

◆  logical_and() [1/2]

tvt constant_interval_exprt::logical_and ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1940 of file interval.cpp.

◆  logical_and() [2/2]

tvt constant_interval_exprt::logical_and ( const constant_interval_exprt &  o ) const

Definition at line 265 of file interval.cpp.

◆  logical_not() [1/2]

tvt constant_interval_exprt::logical_not ( ) const

Definition at line 283 of file interval.cpp.

◆  logical_not() [2/2]

tvt constant_interval_exprt::logical_not ( const constant_interval_exprt &  a )
static

Definition at line 1961 of file interval.cpp.

◆  logical_or() [1/2]

tvt constant_interval_exprt::logical_or ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1947 of file interval.cpp.

◆  logical_or() [2/2]

tvt constant_interval_exprt::logical_or ( const constant_interval_exprt &  o ) const

Definition at line 254 of file interval.cpp.

◆  logical_xor() [1/2]

tvt constant_interval_exprt::logical_xor ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1954 of file interval.cpp.

◆  logical_xor() [2/2]

tvt constant_interval_exprt::logical_xor ( const constant_interval_exprt &  o ) const

Definition at line 273 of file interval.cpp.

◆  max()

max_value_exprt constant_interval_exprt::max ( ) const

Definition at line 1027 of file interval.cpp.

◆  min()

min_value_exprt constant_interval_exprt::min ( ) const

Definition at line 1022 of file interval.cpp.

◆  minus() [1/2]

constant_interval_exprt constant_interval_exprt::minus ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1673 of file interval.cpp.

◆  minus() [2/2]

constant_interval_exprt constant_interval_exprt::minus ( const constant_interval_exprt &  other ) const

Definition at line 112 of file interval.cpp.

◆  modulo() [1/2]

constant_interval_exprt constant_interval_exprt::modulo ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1694 of file interval.cpp.

◆  modulo() [2/2]

constant_interval_exprt constant_interval_exprt::modulo ( const constant_interval_exprt &  o ) const

Definition at line 152 of file interval.cpp.

◆  multiply() [1/2]

constant_interval_exprt constant_interval_exprt::multiply ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1680 of file interval.cpp.

◆  multiply() [2/2]

constant_interval_exprt constant_interval_exprt::multiply ( const constant_interval_exprt &  o ) const

Definition at line 124 of file interval.cpp.

◆  not_equal() [1/3]

tvt constant_interval_exprt::not_equal ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1780 of file interval.cpp.

◆  not_equal() [2/3]

tvt constant_interval_exprt::not_equal ( const constant_interval_exprt &  o ) const

Definition at line 454 of file interval.cpp.

◆  not_equal() [3/3]

bool constant_interval_exprt::not_equal ( const exprt &  a,
const exprt &  b 
)
static

Definition at line 1422 of file interval.cpp.

◆  plus() [1/2]

constant_interval_exprt constant_interval_exprt::plus ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1666 of file interval.cpp.

◆  plus() [2/2]

constant_interval_exprt constant_interval_exprt::plus ( const constant_interval_exprt &  o ) const

Definition at line 74 of file interval.cpp.

◆  right_shift() [1/2]

constant_interval_exprt constant_interval_exprt::right_shift ( const constant_interval_exprt &  a,
const constant_interval_exprt &  b 
)
static

Definition at line 1709 of file interval.cpp.

◆  right_shift() [2/2]

constant_interval_exprt constant_interval_exprt::right_shift ( const constant_interval_exprt &  o ) const

Definition at line 318 of file interval.cpp.

◆  simplified_expr()

exprt constant_interval_exprt::simplified_expr ( exprt  expr )
static

Definition at line 987 of file interval.cpp.

◆  simplified_interval()

constant_interval_exprt constant_interval_exprt::simplified_interval ( exprt &  l,
exprt &  r 
)
static

Definition at line 982 of file interval.cpp.

◆  singleton()

static constant_interval_exprt constant_interval_exprt::singleton ( const exprt &  x )
inlinestatic

Definition at line 99 of file interval.h.

◆  to_string()

std::string constant_interval_exprt::to_string ( ) const

Definition at line 1436 of file interval.cpp.

◆  top() [1/2]

constant_interval_exprt constant_interval_exprt::top ( ) const

Definition at line 1053 of file interval.cpp.

◆  top() [2/2]

constant_interval_exprt constant_interval_exprt::top ( const typet &  type )
static

Definition at line 1043 of file interval.cpp.

◆  tvt_to_interval()

constant_interval_exprt constant_interval_exprt::tvt_to_interval ( const tvt &  val )
static

Definition at line 1966 of file interval.cpp.

◆  typecast()

constant_interval_exprt constant_interval_exprt::typecast ( const typet &  type ) const

Definition at line 1627 of file interval.cpp.

◆  unary_minus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_minus ( ) const

Definition at line 42 of file interval.cpp.

◆  unary_minus() [2/2]

constant_interval_exprt constant_interval_exprt::unary_minus ( const constant_interval_exprt &  a )
static

Definition at line 1621 of file interval.cpp.

◆  unary_plus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_plus ( ) const

Definition at line 37 of file interval.cpp.

◆  unary_plus() [2/2]

constant_interval_exprt constant_interval_exprt::unary_plus ( const constant_interval_exprt &  a )
static

Definition at line 1615 of file interval.cpp.

◆  zero() [1/4]

constant_exprt constant_interval_exprt::zero ( ) const

Definition at line 1017 of file interval.cpp.

◆  zero() [2/4]

constant_exprt constant_interval_exprt::zero ( const constant_interval_exprt &  interval )
static

Definition at line 1012 of file interval.cpp.

◆  zero() [3/4]

constant_exprt constant_interval_exprt::zero ( const exprt &  expr )
static

Definition at line 1006 of file interval.cpp.

◆  zero() [4/4]

constant_exprt constant_interval_exprt::zero ( const typet &  type )
static

Definition at line 997 of file interval.cpp.

Friends And Related Symbol Documentation

◆  operator!

const constant_interval_exprt operator! ( const constant_interval_exprt &  lhs )
friend

Definition at line 1595 of file interval.cpp.

◆  operator!=

bool operator!= ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1532 of file interval.cpp.

◆  operator%

const constant_interval_exprt operator% ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1567 of file interval.cpp.

◆  operator&

const constant_interval_exprt operator& ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1574 of file interval.cpp.

◆  operator*

const constant_interval_exprt operator* ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1560 of file interval.cpp.

◆  operator+

const constant_interval_exprt operator+ ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1539 of file interval.cpp.

◆  operator-

const constant_interval_exprt operator- ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1546 of file interval.cpp.

◆  operator/

const constant_interval_exprt operator/ ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1553 of file interval.cpp.

◆  operator<

bool operator< ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1497 of file interval.cpp.

◆  operator<< [1/2]

const constant_interval_exprt operator<< ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1600 of file interval.cpp.

◆  operator<< [2/2]

std::ostream & operator<< ( std::ostream &  out,
const constant_interval_exprt &  i 
)
friend

Definition at line 1443 of file interval.cpp.

◆  operator<=

bool operator<= ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1511 of file interval.cpp.

◆  operator==

bool operator== ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1525 of file interval.cpp.

◆  operator>

bool operator> ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1504 of file interval.cpp.

◆  operator>=

bool operator>= ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1518 of file interval.cpp.

◆  operator>>

const constant_interval_exprt operator>> ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1607 of file interval.cpp.

◆  operator^

const constant_interval_exprt operator^ ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1588 of file interval.cpp.

◆  operator|

const constant_interval_exprt operator| ( const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
friend

Definition at line 1581 of file interval.cpp.

The documentation for this class was generated from the following files:

AltStyle によって変換されたページ (->オリジナル) /