cprover
|
#include <vector>
#include <iosfwd>
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< literalt > | bvt |
Functions | |
std::ostream & | operator<< (std::ostream &out, literalt l) |
literalt | const_literal (bool value) |
literalt | neg (literalt a) |
literalt | pos (literalt a) |
#define forall_literals | ( | it, | |
bv | |||
) |
Definition at line 199 of file literal.h.
Referenced by prop_minimizet::constraint(), convert(), boolbvt::convert_array(), boolbvt::convert_bv(), boolbvt::convert_complex(), aig_prop_solvert::convert_node(), boolbvt::convert_symbol(), boolbvt::convert_vector(), bv_refinementt::freeze_lazy_constraints(), cnft::is_all(), bv_utilst::is_constant(), smt1_propt::land(), aig_prop_baset::land(), smt2_propt::land(), dplib_propt::land(), cvc_propt::land(), satcheck_picosatt::lcnf(), satcheck_lingelingt::lcnf(), satcheck_precosatt::lcnf(), satcheck_glucose_baset< Glucose::SimpSolver >::lcnf(), satcheck_minisat2_baset< Minisat::Solver >::lcnf(), smt1_propt::lor(), aig_prop_baset::lor(), smt2_propt::lor(), dplib_propt::lor(), cvc_propt::lor(), smt1_propt::lxor(), smt2_propt::lxor(), aig_prop_baset::lxor(), dplib_propt::lxor(), cvc_propt::lxor(), satcheck_picosatt::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::prop_solve(), satcheck_glucose_baset< Glucose::SimpSolver >::prop_solve(), satcheck_lingelingt::set_assumptions(), satcheck_picosatt::set_assumptions(), satcheck_minisat2_baset< Minisat::Solver >::set_assumptions(), satcheck_glucose_baset< Glucose::SimpSolver >::set_assumptions(), boolbv_mapt::set_literals(), boolbvt::type_conversion(), and smt2_convt::write_footer().
#define Forall_literals | ( | it, | |
bv | |||
) |
Definition at line 203 of file literal.h.
Referenced by boolbvt::convert_case(), boolbvt::convert_cond(), bv_pointerst::convert_pointer_type(), boolbv_mapt::get_literals(), bv_utilst::incrementer(), bv_utilst::inverted(), bv_utilst::lt_or_le(), boolbvt::make_free_bv_expr(), and boolbvt::type_conversion().
|
inline |
Definition at line 187 of file literal.h.
References literalt::const_var_no(), and literalt::literalt().
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().
Definition at line 192 of file literal.h.
Referenced by string_refinementt::compute_inverse_function(), aig_prop_solvert::convert_node(), cnft::gate_and(), cnft::gate_nand(), cnft::gate_nor(), cnft::gate_or(), cnft::gate_xor(), integer2binary(), pbs_dimacs_cnft::l_get(), cnft::land(), aig_prop_baset::land(), aig_prop_baset::limplies(), cnft::lor(), aig_prop_baset::lor(), aig_prop_baset::lselect(), aig_prop_baset::lxor(), float_utilst::round_fraction(), aig_prop_baset::set_equal(), and polynomialt::to_expr().
std::ostream& operator<< | ( | std::ostream & | out, |
literalt | l | ||
) |
Definition at line 16 of file literal.cpp.
References literalt::is_constant(), literalt::is_true(), literalt::sign(), and literalt::var_no().
Definition at line 193 of file literal.h.
Referenced by string_constraint_generatort::add_axioms_for_code_point_at(), assembler_name(), shared_bufferst::assignment(), compiler_name(), smt1_convt::convert_constant(), smt2_convt::convert_constant(), java_bytecode_convert_methodt::convert_instructions(), aig_prop_solvert::convert_node(), cnft::gate_and(), cnft::gate_nand(), cnft::gate_nor(), cnft::gate_or(), cnft::gate_xor(), jar_filet::get_manifest(), expr2ct::id_shorthand(), cnft::land(), linker_name(), instrumentert::local(), cnft::lor(), main(), smt1_dect::mathsat_value(), Parser::optAlignas(), Parser::optIntegralTypeOrClassSpec(), remove_asmt::process_instruction(), Parser::rAllocateType(), Parser::rArgDeclListOrInit(), Parser::rCastExpr(), Parser::rClassMember(), Parser::rCondition(), cvc_dect::read_assert(), dplib_dect::read_assert(), read_dimacs_cnf(), smt1_dect::read_result_boolector(), smt1_dect::read_result_cvc3(), smt1_dect::read_result_z3(), cpp_typecheck_resolvet::resolve_scope(), cpp_token_buffert::Restore(), Parser::rExprStatement(), Parser::rMSCuuidof(), Parser::rSizeofExpr(), Parser::rTempArgDeclaration(), Parser::rTemplateArgs(), Parser::rTypeidExpr(), Parser::rTypeNameOrFunctionType(), Parser::rVarNameCore(), configt::set_classpath(), aig_prop_baset::set_equal(), substitute(), goto_symext::symex_gcc_builtin_va_arg_next(), path_symext::symex_va_arg_next(), tdefl_find_match(), and tdefl_flush_block().