cprover
literal.h File Reference
#include <vector>
#include <iosfwd>
Include dependency graph for literal.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  literalt
 

Macros

#define forall_literals(it, bv)
 
#define Forall_literals(it, bv)
 

Typedefs

typedef std::vector< literaltbvt
 

Functions

std::ostream & operator<< (std::ostream &out, literalt l)
 
literalt const_literal (bool value)
 
literalt neg (literalt a)
 
literalt pos (literalt a)
 
bool is_false (const literalt &l)
 
bool is_true (const literalt &l)
 

Macro Definition Documentation

◆ forall_literals

◆ Forall_literals

#define Forall_literals (   it,
  bv 
)

Typedef Documentation

◆ bvt

typedef std::vector<literalt> bvt

Definition at line 200 of file literal.h.

Function Documentation

◆ const_literal()

literalt const_literal ( bool  value)
inline

Definition at line 187 of file literal.h.

References literalt::const_var_no().

Referenced by float_utilst::abs(), arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), bv_utilst::add_sub(), float_utilst::add_sub(), bv_utilst::adder_no_overflow(), bv_utilst::build_constant(), float_utilst::build_constant(), prop_minimizet::constraint(), smt2_convt::convert(), symex_target_equationt::convert_assertions(), symex_target_equationt::convert_assumptions(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_reduction(), boolbvt::convert_byte_extract(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_constant(), boolbvt::convert_div(), symex_target_equationt::convert_goto_instructions(), symex_target_equationt::convert_guards(), smt2_convt::convert_literal(), boolbvt::convert_not(), boolbvt::convert_onehot(), boolbvt::convert_overflow(), boolbvt::convert_rest(), boolbvt::convert_typecast(), float_utilst::denormalization_shift(), float_utilst::div(), bv_pointerst::encode(), equalityt::equality2(), bv_utilst::extension(), float_utilst::fraction_rounding_decision(), float_utilst::from_unsigned_integer(), bv_utilst::inc(), propt::l_set_to(), cnft::land(), aig_prop_baset::land(), cnft::lor(), aig_prop_baset::lor(), qbf_bdd_coret::lor(), bv_utilst::lt_or_le(), cnft::lxor(), aig_prop_baset::lxor(), bv_utilst::negate(), float_approximationt::normalization_shift(), float_utilst::normalization_shift(), bv_utilst::overflow_add(), bv_utilst::overflow_sub(), float_utilst::pack(), aigt::print(), float_utilst::relation(), float_utilst::rounding_mode_bitst::set(), bv_utilst::shift(), float_utilst::sticky_right_shift(), boolbvt::type_conversion(), bv_utilst::unsigned_divider(), bv_utilst::unsigned_less_than(), bv_utilst::unsigned_multiplier(), bv_utilst::unsigned_multiplier_no_overflow(), bv_utilst::wallace_tree(), and bv_utilst::zeros().

◆ is_false()

bool is_false ( const literalt l)
inline

◆ is_true()

bool is_true ( const literalt l)
inline

◆ neg()

◆ operator<<()

std::ostream& operator<< ( std::ostream &  out,
literalt  l 
)

◆ pos()