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)
 

Macro Definition Documentation

◆ forall_literals

◆ Forall_literals

#define Forall_literals (   it,
  bv 
)

Typedef Documentation

◆ bvt

typedef std::vector<literalt> bvt

Definition at line 197 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(), cvc_convt::convert(), smt1_convt::convert(), smt2_convt::convert(), symex_target_equationt::convert_assertions(), symex_target_equationt::convert_assumptions(), prop_conv_solvert::convert_bool(), string_refinementt::convert_bool_bv(), 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(), cvc_convt::convert_literal(), smt1_convt::convert_literal(), smt2_convt::convert_literal(), boolbvt::convert_not(), boolbvt::convert_onehot(), boolbvt::convert_rest(), boolbvt::convert_typecast(), cvc_propt::cvc_literal(), float_utilst::denormalization_shift(), float_utilst::div(), dplib_propt::dplib_literal(), 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(), smt1_propt::land(), smt2_propt::land(), aig_prop_baset::land(), cvc_propt::land(), dplib_propt::land(), cnft::lor(), smt1_propt::lor(), smt2_propt::lor(), aig_prop_baset::lor(), cvc_propt::lor(), dplib_propt::lor(), qbf_bdd_coret::lor(), smt1_propt::lselect(), smt2_propt::lselect(), cvc_propt::lselect(), dplib_propt::lselect(), bv_utilst::lt_or_le(), cnft::lxor(), smt1_propt::lxor(), smt2_propt::lxor(), aig_prop_baset::lxor(), dplib_propt::lxor(), cvc_propt::lxor(), map_bv(), 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(), smt1_propt::smt1_literal(), smt2_propt::smt2_literal(), 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().

◆ neg()

◆ operator<<()

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

◆ pos()