cprover
constant_interval_exprt Class Reference

Represents an interval of values. More...

#include <interval.h>

+ Inheritance diagram for constant_interval_exprt:
+ Collaboration diagram for constant_interval_exprt:

Public Member Functions

 constant_interval_exprt (const exprt &lower, const exprt &upper, const typet type)
 
 constant_interval_exprt (const constant_interval_exprt &x)
 
 constant_interval_exprt (const exprt &x)
 
 constant_interval_exprt (const typet &type)
 
 constant_interval_exprt (const exprt &lower, const exprt &upper)
 
bool is_well_formed () const
 
bool is_valid_bound (const exprt &expr) const
 
const exprtget_lower () const
 
const exprtget_upper () const
 
constant_interval_exprt handle_constant_unary_expression (const irep_idt &op) const
 SET OF ARITHMETIC OPERATORS. More...
 
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_exprt min () const
 
max_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)
 
exprtlhs ()
 
const exprtlhs () const
 
exprtrhs ()
 
const exprtrhs () const
 
const exprtop2 () const =delete
 
exprtop2 ()=delete
 
const exprtop3 () const =delete
 
exprtop3 ()=delete
 
exprtop0 ()
 
const exprtop0 () const
 
exprtop1 ()
 
const exprtop1 () 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)
 
typettype ()
 Return the type of the expression. More...
 
const typettype () const
 
std::size_t size () const
 Amount of nodes this expression tree contains. More...
 
bool has_operands () const
 Return true if there is at least one operand. More...
 
operandstoperands ()
 
const operandstoperands () const
 
void reserve_operands (operandst::size_type n)
 
void move_to_operands (exprt &expr)
 Move the given argument to the end of exprt's operands. More...
 
void move_to_operands (exprt &e1, exprt &e2)
 Move the given arguments to the end of exprt's operands. More...
 
void move_to_operands (exprt &e1, exprt &e2, exprt &e3)
 Move the given arguments to the end of exprt's operands. More...
 
void copy_to_operands (const exprt &expr)
 Copy the given argument to the end of exprt's operands. More...
 
void add_to_operands (const exprt &expr)
 Add the given argument to the end of exprt's operands. More...
 
void add_to_operands (exprt &&expr)
 Add the given argument to the end of exprt's operands. More...
 
void copy_to_operands (const exprt &e1, const exprt &e2)
 Copy the given arguments to the end of exprt's operands. More...
 
void add_to_operands (const exprt &e1, const exprt &e2)
 Add the given arguments to the end of exprt's operands. More...
 
void add_to_operands (exprt &&e1, exprt &&e2)
 Add the given arguments to the end of exprt's operands. More...
 
void add_to_operands (const exprt &e1, const exprt &e2, const exprt &e3)
 Add the given arguments to the end of exprt's operands. More...
 
void copy_to_operands (const exprt &e1, const exprt &e2, const exprt &e3)
 Copy the given arguments to the end of exprt's operands. More...
 
void add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3)
 Add the given arguments to the end of exprt's operands. More...
 
void make_bool (bool value)
 Replace the expression by a Boolean expression representing value. More...
 
bool is_constant () const
 Return whether the expression is a constant. More...
 
bool is_true () const
 Return whether the expression is a constant representing true. More...
 
bool is_false () const
 Return whether the expression is a constant representing false. More...
 
bool is_zero () const
 Return whether the expression is a constant representing 0. More...
 
bool is_one () const
 Return whether the expression is a constant representing 1. More...
 
bool is_boolean () const
 Return whether the expression represents a Boolean. More...
 
const source_locationtfind_source_location () const
 Get a source_locationt from the expression or from its operands (non-recursively). More...
 
const source_locationtsource_location () const
 
source_locationtadd_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. More...
 
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. More...
 
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_idtid () const
 
const std::string & id_string () const
 
void id (const irep_idt &_data)
 
const ireptfind (const irep_namet &name) const
 
ireptadd (const irep_namet &name)
 
ireptadd (const irep_namet &name, irept irep)
 
const std::string & get_string (const irep_namet &name) const
 
const irep_idtget (const irep_namet &name) const
 
bool get_bool (const irep_namet &name) const
 
signed int get_int (const irep_namet &name) const
 
std::size_t get_size_t (const irep_namet &name) const
 
long long get_long_long (const irep_namet &name) const
 
void set (const irep_namet &name, const irep_idt &value)
 
void set (const irep_namet &name, irept irep)
 
void set (const irep_namet &name, const long long value)
 
void remove (const irep_namet &name)
 
void move_to_sub (irept &irep)
 
void move_to_named_sub (const irep_namet &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 More...
 
bool ordering (const irept &other) const
 defines ordering on the internal representation More...
 
int compare (const irept &i) const
 defines ordering on the internal representation comments are ignored More...
 
void clear ()
 
void make_nil ()
 
subtget_sub ()
 
const subtget_sub () const
 
named_subtget_named_sub ()
 
const named_subtget_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, std::map< irep_namet, 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_treetoperator= (const sharing_treet &irep)
 
sharing_treetoperator= (sharing_treet &&irep)
 
 ~sharing_treet ()
 
const dtread () const
 
dtwrite ()
 

Static Public Member Functions

static constant_interval_exprt tvt_to_interval (const tvt &val)
 
static bool equal (const exprt &a, const exprt &b)
 END SET OF ARITHMETIC OPERATORS. More...
 
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)
 Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked). More...
 
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. More...
 
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) More...
 
- Static Public Member Functions inherited from irept
static bool is_comment (const irep_namet &name)
 
static std::size_t number_of_non_comments (const named_subt &)
 count the number of named_sub elements that are not comments More...
 

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). More...
 
static void append_multiply_expression_max (const exprt &expr, std::vector< exprt > &collection)
 Appends interval bounds that could arise from MAX * expr. More...
 
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. More...
 
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< exprtoperandst
 
- Public Types inherited from irept
using baset = tree_implementationt
 
- Public Types inherited from sharing_treet< irept, std::map< irep_namet, irept > >
using dt = tree_nodet< irept, std::map< irep_namet, 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. More...
 
- Protected Member Functions inherited from expr_protectedt
 expr_protectedt (irep_idt _id, typet _type)
 
 expr_protectedt (irep_idt _id, typet _type, operandst _operands)
 
void make_bool (bool value)
 Replace the expression by a Boolean expression representing value. More...
 
exprtop0 ()
 
const exprtop0 () const
 
exprtop1 ()
 
const exprtop1 () const
 
exprtop2 ()
 
const exprtop2 () const
 
exprtop3 ()
 
const exprtop3 () const
 
- Protected Member Functions inherited from exprt
exprtop0 ()
 
exprtop1 ()
 
exprtop2 ()
 
exprtop3 ()
 
const exprtop0 () const
 
const exprtop1 () const
 
const exprtop2 () const
 
const exprtop3 () const
 
exprtadd_expr (const irep_idt &name)
 
const exprtfind_expr (const irep_idt &name) const
 
- Protected Member Functions inherited from sharing_treet< irept, std::map< irep_namet, irept > >
void detach ()
 
- Static Protected Member Functions inherited from sharing_treet< irept, std::map< irep_namet, 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. More...
 
- Protected Attributes inherited from sharing_treet< irept, std::map< irep_namet, irept > >
dtdata
 
- Static Protected Attributes inherited from sharing_treet< irept, std::map< irep_namet, irept > >
static dt empty_d
 

Detailed Description

Represents an interval of values.

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

Definition at line 55 of file interval.h.

Constructor & Destructor Documentation

◆ constant_interval_exprt() [1/5]

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

Definition at line 58 of file interval.h.

◆ constant_interval_exprt() [2/5]

constant_interval_exprt::constant_interval_exprt ( const constant_interval_exprt x)
inline

Definition at line 67 of file interval.h.

◆ constant_interval_exprt() [3/5]

constant_interval_exprt::constant_interval_exprt ( const exprt x)
inlineexplicit

Definition at line 72 of file interval.h.

◆ constant_interval_exprt() [4/5]

constant_interval_exprt::constant_interval_exprt ( const typet type)
inlineexplicit

Definition at line 77 of file interval.h.

◆ constant_interval_exprt() [5/5]

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

Definition at line 82 of file interval.h.

Member Function Documentation

◆ abs()

exprt constant_interval_exprt::abs ( const exprt expr)
static

Definition at line 1293 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
lowerlhs of multiplication
upperrhs of multiplication
collectionvector of possible values

Definition at line 597 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
exprthe unknown side of multiplication
collectionvector of collected bounds

Definition at line 635 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
minthe side known to be MIN for a given type
otherthe side of unknown value
collectionreference to the vector of collected boundaries

Definition at line 660 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 1731 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 354 of file interval.cpp.

◆ bitwise_not() [1/2]

constant_interval_exprt constant_interval_exprt::bitwise_not ( ) const

Definition at line 364 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 1711 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 1724 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 343 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 1717 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 332 of file interval.cpp.

◆ bottom() [1/2]

constant_interval_exprt constant_interval_exprt::bottom ( ) const

Definition at line 1054 of file interval.cpp.

◆ bottom() [2/2]

constant_interval_exprt constant_interval_exprt::bottom ( const typet type)
static

Definition at line 1044 of file interval.cpp.

◆ contains()

bool constant_interval_exprt::contains ( const constant_interval_exprt interval) const

Definition at line 1420 of file interval.cpp.

◆ contains_extreme() [1/2]

bool constant_interval_exprt::contains_extreme ( const exprt  expr)
static

Definition at line 1823 of file interval.cpp.

◆ contains_extreme() [2/2]

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

Definition at line 1841 of file interval.cpp.

◆ contains_zero()

bool constant_interval_exprt::contains_zero ( ) const

Definition at line 1864 of file interval.cpp.

◆ decrement() [1/2]

constant_interval_exprt constant_interval_exprt::decrement ( ) const

Definition at line 462 of file interval.cpp.

◆ decrement() [2/2]

constant_interval_exprt constant_interval_exprt::decrement ( const constant_interval_exprt a)
static

Definition at line 1787 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 1680 of file interval.cpp.

◆ divide() [2/2]

constant_interval_exprt constant_interval_exprt::divide ( const constant_interval_exprt o) const

Definition at line 134 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 1766 of file interval.cpp.

◆ equal() [2/3]

tvt constant_interval_exprt::equal ( const constant_interval_exprt o) const

Definition at line 429 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 1308 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 811 of file interval.cpp.

◆ eval() [2/2]

constant_interval_exprt constant_interval_exprt::eval ( const irep_idt unary_operator) const

Definition at line 789 of file interval.cpp.

◆ generate_division_expression()

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

Definition at line 680 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 568 of file interval.cpp.

◆ generate_modulo_expression()

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

Definition at line 735 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 895 of file interval.cpp.

◆ get_extreme()

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

Definition at line 493 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 467 of file interval.cpp.

◆ get_lower()

const exprt & constant_interval_exprt::get_lower ( ) const

Definition at line 26 of file interval.cpp.

◆ get_max() [1/2]

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

Definition at line 956 of file interval.cpp.

◆ get_max() [2/2]

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

Definition at line 971 of file interval.cpp.

◆ get_min() [1/2]

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

Definition at line 961 of file interval.cpp.

◆ get_min() [2/2]

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

Definition at line 966 of file interval.cpp.

◆ get_upper()

const exprt & constant_interval_exprt::get_upper ( ) const

Definition at line 31 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 1745 of file interval.cpp.

◆ greater_than() [2/3]

tvt constant_interval_exprt::greater_than ( const constant_interval_exprt o) const

Definition at line 395 of file interval.cpp.

◆ greater_than() [3/3]

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

Definition at line 1398 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 1759 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 423 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 1408 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 947 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 935 of file interval.cpp.

◆ has_no_lower_bound()

bool constant_interval_exprt::has_no_lower_bound ( ) const

Definition at line 1204 of file interval.cpp.

◆ has_no_upper_bound()

bool constant_interval_exprt::has_no_upper_bound ( ) const

Definition at line 1199 of file interval.cpp.

◆ increment() [1/2]

constant_interval_exprt constant_interval_exprt::increment ( ) const

Definition at line 457 of file interval.cpp.

◆ increment() [2/2]

constant_interval_exprt constant_interval_exprt::increment ( const constant_interval_exprt a)
static

Definition at line 1781 of file interval.cpp.

◆ is_bitvector() [1/4]

bool constant_interval_exprt::is_bitvector ( ) const

Definition at line 1184 of file interval.cpp.

◆ is_bitvector() [2/4]

bool constant_interval_exprt::is_bitvector ( const constant_interval_exprt interval)
static

Definition at line 1153 of file interval.cpp.

◆ is_bitvector() [3/4]

bool constant_interval_exprt::is_bitvector ( const exprt expr)
static

Definition at line 1169 of file interval.cpp.

◆ is_bitvector() [4/4]

bool constant_interval_exprt::is_bitvector ( const typet type)
static

Definition at line 1122 of file interval.cpp.

◆ is_bottom() [1/2]

bool constant_interval_exprt::is_bottom ( ) const

Definition at line 1033 of file interval.cpp.

◆ is_bottom() [2/2]

bool constant_interval_exprt::is_bottom ( const constant_interval_exprt a)
static

Definition at line 1808 of file interval.cpp.

◆ is_definitely_false()

tvt constant_interval_exprt::is_definitely_false ( ) const

Definition at line 221 of file interval.cpp.

◆ is_definitely_true()

tvt constant_interval_exprt::is_definitely_true ( ) const

Definition at line 215 of file interval.cpp.

◆ is_empty() [1/2]

bool constant_interval_exprt::is_empty ( ) const

Definition at line 1848 of file interval.cpp.

◆ is_empty() [2/2]

bool constant_interval_exprt::is_empty ( const constant_interval_exprt a)
static

Definition at line 1792 of file interval.cpp.

◆ is_extreme() [1/2]

bool constant_interval_exprt::is_extreme ( const exprt expr)
static

Definition at line 1189 of file interval.cpp.

◆ is_extreme() [2/2]

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

Definition at line 1194 of file interval.cpp.

◆ is_false()

tvt constant_interval_exprt::is_false ( const constant_interval_exprt a)
static

Definition at line 1928 of file interval.cpp.

◆ is_float() [1/4]

bool constant_interval_exprt::is_float ( ) const

Definition at line 1066 of file interval.cpp.

◆ is_float() [2/4]

bool constant_interval_exprt::is_float ( const constant_interval_exprt interval)
static

Definition at line 1117 of file interval.cpp.

◆ is_float() [3/4]

bool constant_interval_exprt::is_float ( const exprt expr)
static

Definition at line 1112 of file interval.cpp.

◆ is_float() [4/4]

bool constant_interval_exprt::is_float ( const typet type)
static

Definition at line 1097 of file interval.cpp.

◆ is_int() [1/4]

bool constant_interval_exprt::is_int ( ) const

Definition at line 1061 of file interval.cpp.

◆ is_int() [2/4]

bool constant_interval_exprt::is_int ( const constant_interval_exprt interval)
static

Definition at line 1107 of file interval.cpp.

◆ is_int() [3/4]

bool constant_interval_exprt::is_int ( const exprt expr)
static

Definition at line 1102 of file interval.cpp.

◆ is_int() [4/4]

bool constant_interval_exprt::is_int ( const typet type)
static

Definition at line 1092 of file interval.cpp.

◆ is_max() [1/2]

bool constant_interval_exprt::is_max ( const constant_interval_exprt a)
static

Definition at line 1818 of file interval.cpp.

◆ is_max() [2/2]

bool constant_interval_exprt::is_max ( const exprt expr)
static

Definition at line 1209 of file interval.cpp.

◆ is_min() [1/2]

bool constant_interval_exprt::is_min ( const constant_interval_exprt a)
static

Definition at line 1813 of file interval.cpp.

◆ is_min() [2/2]

bool constant_interval_exprt::is_min ( const exprt expr)
static

Definition at line 1214 of file interval.cpp.

◆ is_negative() [1/3]

bool constant_interval_exprt::is_negative ( ) const

Definition at line 1918 of file interval.cpp.

◆ is_negative() [2/3]

bool constant_interval_exprt::is_negative ( const constant_interval_exprt interval)
static

Definition at line 1902 of file interval.cpp.

◆ is_negative() [3/3]

bool constant_interval_exprt::is_negative ( const exprt expr)
static

Definition at line 1273 of file interval.cpp.

◆ is_numeric() [1/4]

bool constant_interval_exprt::is_numeric ( ) const

Definition at line 1076 of file interval.cpp.

◆ is_numeric() [2/4]

bool constant_interval_exprt::is_numeric ( const constant_interval_exprt interval)
static

Definition at line 1086 of file interval.cpp.

◆ is_numeric() [3/4]

bool constant_interval_exprt::is_numeric ( const exprt expr)
static

Definition at line 1081 of file interval.cpp.

◆ is_numeric() [4/4]

bool constant_interval_exprt::is_numeric ( const typet type)
static

Definition at line 1071 of file interval.cpp.

◆ is_positive() [1/3]

bool constant_interval_exprt::is_positive ( ) const

Definition at line 1908 of file interval.cpp.

◆ is_positive() [2/3]

bool constant_interval_exprt::is_positive ( const constant_interval_exprt interval)
static

Definition at line 1891 of file interval.cpp.

◆ is_positive() [3/3]

bool constant_interval_exprt::is_positive ( const exprt expr)
static

Definition at line 1219 of file interval.cpp.

◆ is_signed() [1/4]

bool constant_interval_exprt::is_signed ( ) const

Definition at line 1174 of file interval.cpp.

◆ is_signed() [2/4]

bool constant_interval_exprt::is_signed ( const constant_interval_exprt interval)
static

Definition at line 1142 of file interval.cpp.

◆ is_signed() [3/4]

bool constant_interval_exprt::is_signed ( const exprt expr)
static

Definition at line 1159 of file interval.cpp.

◆ is_signed() [4/4]

bool constant_interval_exprt::is_signed ( const typet type)
static

Definition at line 1129 of file interval.cpp.

◆ is_single_value_interval() [1/2]

bool constant_interval_exprt::is_single_value_interval ( ) const

Definition at line 1858 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 1797 of file interval.cpp.

◆ is_top() [1/2]

bool constant_interval_exprt::is_top ( ) const

Definition at line 1028 of file interval.cpp.

◆ is_top() [2/2]

bool constant_interval_exprt::is_top ( const constant_interval_exprt a)
static

Definition at line 1803 of file interval.cpp.

◆ is_true()

tvt constant_interval_exprt::is_true ( const constant_interval_exprt a)
static

Definition at line 1923 of file interval.cpp.

◆ is_unsigned() [1/4]

bool constant_interval_exprt::is_unsigned ( ) const

Definition at line 1179 of file interval.cpp.

◆ is_unsigned() [2/4]

bool constant_interval_exprt::is_unsigned ( const constant_interval_exprt interval)
static

Definition at line 1147 of file interval.cpp.

◆ is_unsigned() [3/4]

bool constant_interval_exprt::is_unsigned ( const exprt expr)
static

Definition at line 1164 of file interval.cpp.

◆ is_unsigned() [4/4]

bool constant_interval_exprt::is_unsigned ( const typet type)
static

Definition at line 1135 of file interval.cpp.

◆ is_valid_bound()

bool constant_interval_exprt::is_valid_bound ( const exprt expr) const
inline

Definition at line 108 of file interval.h.

◆ is_well_formed()

bool constant_interval_exprt::is_well_formed ( ) const
inline

Definition at line 87 of file interval.h.

◆ is_zero() [1/3]

bool constant_interval_exprt::is_zero ( ) const

Definition at line 1913 of file interval.cpp.

◆ is_zero() [2/3]

bool constant_interval_exprt::is_zero ( const constant_interval_exprt interval)
static

Definition at line 1897 of file interval.cpp.

◆ is_zero() [3/3]

bool constant_interval_exprt::is_zero ( const exprt expr)
static

Definition at line 1244 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 1695 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 299 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 1738 of file interval.cpp.

◆ less_than() [2/3]

tvt constant_interval_exprt::less_than ( const constant_interval_exprt o) const

Definition at line 374 of file interval.cpp.

◆ less_than() [3/3]

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

Definition at line 1351 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 1752 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 401 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 1403 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 1933 of file interval.cpp.

◆ logical_and() [2/2]

tvt constant_interval_exprt::logical_and ( const constant_interval_exprt o) const

Definition at line 263 of file interval.cpp.

◆ logical_not() [1/2]

tvt constant_interval_exprt::logical_not ( ) const

Definition at line 281 of file interval.cpp.

◆ logical_not() [2/2]

tvt constant_interval_exprt::logical_not ( const constant_interval_exprt a)
static

Definition at line 1954 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 1940 of file interval.cpp.

◆ logical_or() [2/2]

tvt constant_interval_exprt::logical_or ( const constant_interval_exprt o) const

Definition at line 252 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 1947 of file interval.cpp.

◆ logical_xor() [2/2]

tvt constant_interval_exprt::logical_xor ( const constant_interval_exprt o) const

Definition at line 271 of file interval.cpp.

◆ max()

max_exprt constant_interval_exprt::max ( ) const

Definition at line 1023 of file interval.cpp.

◆ min()

min_exprt constant_interval_exprt::min ( ) const

Definition at line 1018 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 1666 of file interval.cpp.

◆ minus() [2/2]

constant_interval_exprt constant_interval_exprt::minus ( const constant_interval_exprt other) const

Definition at line 111 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 1687 of file interval.cpp.

◆ modulo() [2/2]

constant_interval_exprt constant_interval_exprt::modulo ( const constant_interval_exprt o) const

Definition at line 151 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 1673 of file interval.cpp.

◆ multiply() [2/2]

constant_interval_exprt constant_interval_exprt::multiply ( const constant_interval_exprt o) const

Definition at line 123 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 1773 of file interval.cpp.

◆ not_equal() [2/3]

tvt constant_interval_exprt::not_equal ( const constant_interval_exprt o) const

Definition at line 452 of file interval.cpp.

◆ not_equal() [3/3]

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

Definition at line 1415 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 1659 of file interval.cpp.

◆ plus() [2/2]

constant_interval_exprt constant_interval_exprt::plus ( const constant_interval_exprt o) const

Definition at line 73 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 1702 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 316 of file interval.cpp.

◆ simplified_expr()

exprt constant_interval_exprt::simplified_expr ( exprt  expr)
static

Definition at line 983 of file interval.cpp.

◆ simplified_interval()

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

Definition at line 978 of file interval.cpp.

◆ to_string()

std::string constant_interval_exprt::to_string ( ) const

Definition at line 1429 of file interval.cpp.

◆ top() [1/2]

constant_interval_exprt constant_interval_exprt::top ( ) const

Definition at line 1049 of file interval.cpp.

◆ top() [2/2]

constant_interval_exprt constant_interval_exprt::top ( const typet type)
static

Definition at line 1039 of file interval.cpp.

◆ tvt_to_interval()

constant_interval_exprt constant_interval_exprt::tvt_to_interval ( const tvt val)
static

Definition at line 1959 of file interval.cpp.

◆ typecast()

constant_interval_exprt constant_interval_exprt::typecast ( const typet type) const

Definition at line 1620 of file interval.cpp.

◆ unary_minus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_minus ( ) const

Definition at line 41 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 1614 of file interval.cpp.

◆ unary_plus() [1/2]

constant_interval_exprt constant_interval_exprt::unary_plus ( ) const

Definition at line 36 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 1608 of file interval.cpp.

◆ zero() [1/4]

constant_exprt constant_interval_exprt::zero ( ) const

Definition at line 1013 of file interval.cpp.

◆ zero() [2/4]

constant_exprt constant_interval_exprt::zero ( const constant_interval_exprt interval)
static

Definition at line 1008 of file interval.cpp.

◆ zero() [3/4]

constant_exprt constant_interval_exprt::zero ( const exprt expr)
static

Definition at line 1002 of file interval.cpp.

◆ zero() [4/4]

constant_exprt constant_interval_exprt::zero ( const typet type)
static

Definition at line 993 of file interval.cpp.

Friends And Related Function Documentation

◆ operator!

const constant_interval_exprt operator! ( const constant_interval_exprt lhs)
friend

Definition at line 1588 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%

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 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 1553 of file interval.cpp.

◆ operator+

const constant_interval_exprt 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 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<

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

Definition at line 1490 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 1593 of file interval.cpp.

◆ operator<< [2/2]

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

Definition at line 1436 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>

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

Definition at line 1497 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>>

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^

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

Definition at line 1581 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.


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