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) |
bool | is_false (const literalt &l) |
bool | is_true (const literalt &l) |
#define forall_literals | ( | it, | |
bv | |||
) |
Definition at line 202 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(), aig_prop_baset::land(), satcheck_lingelingt::lcnf(), satcheck_picosatt::lcnf(), satcheck_glucose_baset< Glucose::SimpSolver >::lcnf(), satcheck_minisat2_baset< Minisat::Solver >::lcnf(), aig_prop_baset::lor(), aig_prop_baset::lxor(), satcheck_picosatt::prop_solve(), satcheck_lingelingt::prop_solve(), satcheck_glucose_baset< Glucose::SimpSolver >::prop_solve(), satcheck_minisat2_baset< Minisat::Solver >::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 206 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(), and boolbvt::type_conversion().
|
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().
|
inline |
Definition at line 196 of file literal.h.
References literalt::is_false().
Referenced by linker_script_merget::linker_data_is_malformed(), and simplify_exprt::simplify_boolean().
|
inline |
Definition at line 197 of file literal.h.
References literalt::is_true().
Referenced by linkingt::adjust_object_type_rec(), symex_slice_by_tracet::compute_ts_back(), and simplify_exprt::simplify_boolean().
Definition at line 192 of file literal.h.
Referenced by 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(), smt2_convt::convert_constant(), aig_prop_solvert::convert_node(), java_bytecode_convert_methodt::do_exception_handling(), cnft::gate_and(), cnft::gate_nand(), cnft::gate_nor(), cnft::gate_or(), cnft::gate_xor(), expr2ct::id_shorthand(), cnft::land(), linker_name(), instrumentert::local(), cnft::lor(), main(), Parser::optAlignas(), Parser::optIntegralTypeOrClassSpec(), remove_asmt::process_instruction(), Parser::rAllocateType(), Parser::rArgDeclListOrInit(), Parser::rCastExpr(), Parser::rClassMember(), Parser::rCondition(), 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(), aig_prop_baset::set_equal(), goto_symext::symex_gcc_builtin_va_arg_next(), and tdefl_find_match().