cprover
bv_utilst Class Reference

#include <bv_utils.h>

Collaboration diagram for bv_utilst:
[legend]

Public Types

enum  representationt { representationt::SIGNED, representationt::UNSIGNED }
 
enum  shiftt { shiftt::LEFT, shiftt::LRIGHT, shiftt::ARIGHT }
 

Public Member Functions

 bv_utilst (propt &_prop)
 
bvt build_constant (const mp_integer &i, std::size_t width)
 
bvt incrementer (const bvt &op, literalt carry_in)
 
bvt inc (const bvt &op)
 
void incrementer (bvt &op, literalt carry_in, literalt &carry_out)
 
bvt negate (const bvt &op)
 
bvt negate_no_overflow (const bvt &op)
 
bvt absolute_value (const bvt &op)
 
literalt overflow_negate (const bvt &op)
 
bvt inverted (const bvt &op)
 
literalt full_adder (const literalt a, const literalt b, const literalt carry_in, literalt &carry_out)
 
literalt carry (literalt a, literalt b, literalt c)
 
bvt add_sub (const bvt &op0, const bvt &op1, bool subtract)
 
bvt add_sub (const bvt &op0, const bvt &op1, literalt subtract)
 
bvt add_sub_no_overflow (const bvt &op0, const bvt &op1, bool subtract, representationt rep)
 
bvt add (const bvt &op0, const bvt &op1)
 
bvt sub (const bvt &op0, const bvt &op1)
 
literalt overflow_add (const bvt &op0, const bvt &op1, representationt rep)
 
literalt overflow_sub (const bvt &op0, const bvt &op1, representationt rep)
 
literalt carry_out (const bvt &op0, const bvt &op1, literalt carry_in)
 
bvt shift (const bvt &op, const shiftt shift, std::size_t distance)
 
bvt shift (const bvt &op, const shiftt shift, const bvt &distance)
 
bvt unsigned_multiplier (const bvt &op0, const bvt &op1)
 
bvt signed_multiplier (const bvt &op0, const bvt &op1)
 
bvt multiplier (const bvt &op0, const bvt &op1, representationt rep)
 
bvt multiplier_no_overflow (const bvt &op0, const bvt &op1, representationt rep)
 
bvt divider (const bvt &op0, const bvt &op1, representationt rep)
 
bvt remainder (const bvt &op0, const bvt &op1, representationt rep)
 
void divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem, representationt rep)
 
void signed_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
 
void unsigned_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
 
literalt equal (const bvt &op0, const bvt &op1)
 Bit-blasting ID_equal and use in other encodings. More...
 
literalt is_zero (const bvt &op)
 
literalt is_not_zero (const bvt &op)
 
literalt is_int_min (const bvt &op)
 
literalt is_one (const bvt &op)
 
literalt is_all_ones (const bvt &op)
 
literalt lt_or_le (bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep)
 To provide a bitwise model of < or <=. More...
 
literalt rel (const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
 
literalt unsigned_less_than (const bvt &bv0, const bvt &bv1)
 
literalt signed_less_than (const bvt &bv0, const bvt &bv1)
 
bool is_constant (const bvt &bv)
 
bvt extension (const bvt &bv, std::size_t new_size, representationt rep)
 
bvt sign_extension (const bvt &bv, std::size_t new_size)
 
bvt zero_extension (const bvt &bv, std::size_t new_size)
 
bvt zeros (std::size_t new_size) const
 
void set_equal (const bvt &a, const bvt &b)
 
void cond_implies_equal (literalt cond, const bvt &a, const bvt &b)
 
bvt cond_negate (const bvt &bv, const literalt cond)
 
bvt select (literalt s, const bvt &a, const bvt &b)
 If s is true, selects a otherwise selects b. More...
 
bvt concatenate (const bvt &a, const bvt &b) const
 
literalt verilog_bv_has_x_or_z (const bvt &)
 
bvt verilog_bv_normal_bits (const bvt &)
 

Static Public Member Functions

static literalt sign_bit (const bvt &op)
 
static bvt extract (const bvt &a, std::size_t first, std::size_t last)
 
static bvt extract_msb (const bvt &a, std::size_t n)
 
static bvt extract_lsb (const bvt &a, std::size_t n)
 

Protected Member Functions

void adder (bvt &sum, const bvt &op, literalt carry_in, literalt &carry_out)
 
void adder_no_overflow (bvt &sum, const bvt &op, bool subtract, representationt rep)
 
void adder_no_overflow (bvt &sum, const bvt &op)
 
bvt unsigned_multiplier_no_overflow (const bvt &op0, const bvt &op1)
 
bvt signed_multiplier_no_overflow (const bvt &op0, const bvt &op1)
 
bvt cond_negate_no_overflow (const bvt &bv, const literalt cond)
 
bvt wallace_tree (const std::vector< bvt > &pps)
 

Protected Attributes

proptprop
 

Detailed Description

Definition at line 26 of file bv_utils.h.

Member Enumeration Documentation

§ representationt

Enumerator
SIGNED 
UNSIGNED 

Definition at line 31 of file bv_utils.h.

§ shiftt

enum bv_utilst::shiftt
strong
Enumerator
LEFT 
LRIGHT 
ARIGHT 

Definition at line 71 of file bv_utils.h.

Constructor & Destructor Documentation

§ bv_utilst()

bv_utilst::bv_utilst ( propt _prop)
inlineexplicit

Definition at line 29 of file bv_utils.h.

Member Function Documentation

§ absolute_value()

bvt bv_utilst::absolute_value ( const bvt op)

§ add()

§ add_sub() [1/2]

bvt bv_utilst::add_sub ( const bvt op0,
const bvt op1,
bool  subtract 
)

Definition at line 339 of file bv_utils.cpp.

References adder(), carry_out(), const_literal(), and inverted().

Referenced by add(), float_utilst::add_sub(), boolbvt::convert_add_sub(), inc(), and sub().

§ add_sub() [2/2]

bvt bv_utilst::add_sub ( const bvt op0,
const bvt op1,
literalt  subtract 
)

Definition at line 354 of file bv_utils.cpp.

References adder(), carry_out(), inverted(), and select().

§ add_sub_no_overflow()

bvt bv_utilst::add_sub_no_overflow ( const bvt op0,
const bvt op1,
bool  subtract,
representationt  rep 
)

Definition at line 328 of file bv_utils.cpp.

References adder_no_overflow().

Referenced by boolbvt::convert_add_sub(), and inc().

§ adder()

void bv_utilst::adder ( bvt sum,
const bvt op,
literalt  carry_in,
literalt carry_out 
)
protected

Definition at line 297 of file bv_utils.cpp.

References full_adder().

Referenced by add_sub(), and adder_no_overflow().

§ adder_no_overflow() [1/2]

void bv_utilst::adder_no_overflow ( bvt sum,
const bvt op,
bool  subtract,
representationt  rep 
)
protected

§ adder_no_overflow() [2/2]

void bv_utilst::adder_no_overflow ( bvt sum,
const bvt op 
)
protected

Definition at line 450 of file bv_utils.cpp.

References adder(), carry_out(), const_literal(), propt::l_set_to_false(), and prop.

§ build_constant()

§ carry()

§ carry_out()

literalt bv_utilst::carry_out ( const bvt op0,
const bvt op1,
literalt  carry_in 
)

§ concatenate()

bvt bv_utilst::concatenate ( const bvt a,
const bvt b 
) const

§ cond_implies_equal()

void bv_utilst::cond_implies_equal ( literalt  cond,
const bvt a,
const bvt b 
)

§ cond_negate()

bvt bv_utilst::cond_negate ( const bvt bv,
const literalt  cond 
)

§ cond_negate_no_overflow()

bvt bv_utilst::cond_negate_no_overflow ( const bvt bv,
const literalt  cond 
)
protected

§ divider() [1/2]

bvt bv_utilst::divider ( const bvt op0,
const bvt op1,
representationt  rep 
)
inline

§ divider() [2/2]

void bv_utilst::divider ( const bvt op0,
const bvt op1,
bvt res,
bvt rem,
representationt  rep 
)

Definition at line 854 of file bv_utils.cpp.

References propt::has_set_to(), prop, SIGNED, signed_divider(), UNSIGNED, and unsigned_divider().

§ equal()

§ extension()

bvt bv_utilst::extension ( const bvt bv,
std::size_t  new_size,
representationt  rep 
)

§ extract()

bvt bv_utilst::extract ( const bvt a,
std::size_t  first,
std::size_t  last 
)
static

§ extract_lsb()

bvt bv_utilst::extract_lsb ( const bvt a,
std::size_t  n 
)
static

Definition at line 70 of file bv_utils.cpp.

Referenced by zeros().

§ extract_msb()

bvt bv_utilst::extract_msb ( const bvt a,
std::size_t  n 
)
static

Definition at line 58 of file bv_utils.cpp.

Referenced by float_utilst::normalization_shift(), and zeros().

§ full_adder()

literalt bv_utilst::full_adder ( const literalt  a,
const literalt  b,
const literalt  carry_in,
literalt carry_out 
)

§ inc()

§ incrementer() [1/2]

bvt bv_utilst::incrementer ( const bvt op,
literalt  carry_in 
)

Definition at line 553 of file bv_utils.cpp.

References carry_out().

Referenced by inc(), negate(), float_utilst::round_fraction(), and boolbvt::type_conversion().

§ incrementer() [2/2]

void bv_utilst::incrementer ( bvt op,
literalt  carry_in,
literalt carry_out 
)

Definition at line 538 of file bv_utils.cpp.

References Forall_literals, propt::land(), propt::lxor(), and prop.

§ inverted()

bvt bv_utilst::inverted ( const bvt op)

§ is_all_ones()

literalt bv_utilst::is_all_ones ( const bvt op)
inline

§ is_constant()

bool bv_utilst::is_constant ( const bvt bv)

§ is_int_min()

literalt bv_utilst::is_int_min ( const bvt op)
inline

Definition at line 143 of file bv_utils.h.

References is_one(), and is_zero().

Referenced by overflow_sub().

§ is_not_zero()

literalt bv_utilst::is_not_zero ( const bvt op)
inline

Definition at line 140 of file bv_utils.h.

References propt::lor(), and prop.

Referenced by float_utilst::div(), and unsigned_divider().

§ is_one()

literalt bv_utilst::is_one ( const bvt op)

Definition at line 26 of file bv_utils.cpp.

References is_zero(), propt::land(), and prop.

Referenced by bv_refinementt::convert_mult(), and is_int_min().

§ is_zero()

§ lt_or_le()

literalt bv_utilst::lt_or_le ( bool  or_equal,
const bvt bv0,
const bvt bv1,
representationt  rep 
)

To provide a bitwise model of < or <=.

parameters: bvts for each input and whether they are signed and whether
a model of < or <= is required.
Returns
A literalt that models the value of the comparison.

Definition at line 1128 of file bv_utils.cpp.

References carry(), carry_out(), propt::cnf_handled_well(), const_literal(), equal(), Forall_literals, propt::has_set_to(), inverted(), propt::l_set_to_true(), propt::lcnf(), propt::lequal(), propt::lor(), propt::lxor(), propt::new_variable(), prop, SIGNED, and UNSIGNED.

Referenced by is_all_ones(), rel(), signed_less_than(), unsigned_divider(), and unsigned_less_than().

§ multiplier()

bvt bv_utilst::multiplier ( const bvt op0,
const bvt op1,
representationt  rep 
)

§ multiplier_no_overflow()

bvt bv_utilst::multiplier_no_overflow ( const bvt op0,
const bvt op1,
representationt  rep 
)

§ negate()

bvt bv_utilst::negate ( const bvt op)

§ negate_no_overflow()

bvt bv_utilst::negate_no_overflow ( const bvt op)

Definition at line 521 of file bv_utils.cpp.

References propt::l_set_to(), negate(), overflow_negate(), and prop.

Referenced by boolbvt::convert_unary_minus(), and inc().

§ overflow_add()

literalt bv_utilst::overflow_add ( const bvt op0,
const bvt op1,
representationt  rep 
)

§ overflow_negate()

literalt bv_utilst::overflow_negate ( const bvt op)

§ overflow_sub()

literalt bv_utilst::overflow_sub ( const bvt op0,
const bvt op1,
representationt  rep 
)

§ rel()

literalt bv_utilst::rel ( const bvt bv0,
irep_idt  id,
const bvt bv1,
representationt  rep 
)

Definition at line 1262 of file bv_utils.cpp.

References equal(), and lt_or_le().

Referenced by boolbvt::convert_bv_rel(), bv_pointerst::convert_rest(), and is_all_ones().

§ remainder()

bvt bv_utilst::remainder ( const bvt op0,
const bvt op1,
representationt  rep 
)
inline

Definition at line 90 of file bv_utils.h.

References divider(), equal(), signed_divider(), and unsigned_divider().

Referenced by bv_refinementt::check_SAT().

§ select()

§ set_equal()

void bv_utilst::set_equal ( const bvt a,
const bvt b 
)

Definition at line 35 of file bv_utils.cpp.

References prop, and propt::set_equal().

Referenced by bv_refinementt::check_SAT(), and zeros().

§ shift() [1/2]

§ shift() [2/2]

bvt bv_utilst::shift ( const bvt op,
const shiftt  shift,
const bvt distance 
)

Definition at line 459 of file bv_utils.cpp.

References const_literal(), propt::lselect(), prop, and shift().

§ sign_bit()

static literalt bv_utilst::sign_bit ( const bvt op)
inlinestatic

Definition at line 132 of file bv_utils.h.

§ sign_extension()

§ signed_divider()

void bv_utilst::signed_divider ( const bvt op0,
const bvt op1,
bvt res,
bvt rem 
)

Definition at line 819 of file bv_utils.cpp.

References propt::lselect(), propt::lxor(), negate(), prop, and unsigned_divider().

Referenced by divider(), and remainder().

§ signed_less_than()

literalt bv_utilst::signed_less_than ( const bvt bv0,
const bvt bv1 
)

Definition at line 1255 of file bv_utils.cpp.

References lt_or_le(), and SIGNED.

Referenced by is_all_ones(), and float_utilst::round_exponent().

§ signed_multiplier()

bvt bv_utilst::signed_multiplier ( const bvt op0,
const bvt op1 
)

Definition at line 723 of file bv_utils.cpp.

References cond_negate(), propt::lxor(), prop, and unsigned_multiplier().

Referenced by boolbvt::convert_mult(), and multiplier().

§ signed_multiplier_no_overflow()

bvt bv_utilst::signed_multiplier_no_overflow ( const bvt op0,
const bvt op1 
)
protected

§ sub()

§ unsigned_divider()

§ unsigned_less_than()

literalt bv_utilst::unsigned_less_than ( const bvt bv0,
const bvt bv1 
)

Definition at line 1243 of file bv_utils.cpp.

References carry_out(), const_literal(), inverted(), and lt_or_le().

Referenced by is_all_ones(), and float_utilst::relation().

§ unsigned_multiplier()

bvt bv_utilst::unsigned_multiplier ( const bvt op0,
const bvt op1 
)

§ unsigned_multiplier_no_overflow()

bvt bv_utilst::unsigned_multiplier_no_overflow ( const bvt op0,
const bvt op1 
)
protected

§ verilog_bv_has_x_or_z()

literalt bv_utilst::verilog_bv_has_x_or_z ( const bvt src)

Definition at line 1316 of file bv_utils.cpp.

References propt::lor(), and prop.

Referenced by boolbvt::convert_not(), and zeros().

§ verilog_bv_normal_bits()

bvt bv_utilst::verilog_bv_normal_bits ( const bvt src)

Definition at line 1331 of file bv_utils.cpp.

Referenced by boolbvt::convert_not(), and zeros().

§ wallace_tree()

bvt bv_utilst::wallace_tree ( const std::vector< bvt > &  pps)
protected

Definition at line 569 of file bv_utils.cpp.

References add(), carry(), const_literal(), propt::lxor(), and prop.

Referenced by unsigned_multiplier().

§ zero_extension()

§ zeros()

Member Data Documentation

§ prop


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