cprover
|
TO_BE_DOCUMENTED. More...
#include <prop.h>
Public Types | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
Public Member Functions | |
propt () | |
virtual | ~propt () |
virtual literalt | land (literalt a, literalt b)=0 |
virtual literalt | lor (literalt a, literalt b)=0 |
virtual literalt | land (const bvt &bv)=0 |
virtual literalt | lor (const bvt &bv)=0 |
virtual literalt | lxor (literalt a, literalt b)=0 |
virtual literalt | lxor (const bvt &bv)=0 |
virtual literalt | lnand (literalt a, literalt b)=0 |
virtual literalt | lnor (literalt a, literalt b)=0 |
virtual literalt | lequal (literalt a, literalt b)=0 |
virtual literalt | limplies (literalt a, literalt b)=0 |
virtual literalt | lselect (literalt a, literalt b, literalt c)=0 |
virtual void | set_equal (literalt a, literalt b) |
asserts a==b in the propositional formula More... | |
virtual void | l_set_to (literalt a, bool value) |
void | l_set_to_true (literalt a) |
void | l_set_to_false (literalt a) |
void | lcnf (literalt l0, literalt l1) |
void | lcnf (literalt l0, literalt l1, literalt l2) |
void | lcnf (literalt l0, literalt l1, literalt l2, literalt l3) |
virtual void | lcnf (const bvt &bv)=0 |
virtual bool | has_set_to () const |
virtual bool | cnf_handled_well () const |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual literalt | new_variable ()=0 |
virtual void | set_variable_name (literalt a, const irep_idt &name) |
virtual size_t | no_variables () const =0 |
bvt | new_variables (std::size_t width) |
generates a bitvector of given width with new variables More... | |
virtual const std::string | solver_text ()=0 |
virtual resultt | prop_solve ()=0 |
virtual tvt | l_get (literalt a) const =0 |
virtual void | set_assignment (literalt a, bool value) |
virtual void | copy_assignment_from (const propt &prop) |
virtual bool | is_in_conflict (literalt l) const |
virtual bool | has_is_in_conflict () const |
virtual void | set_frozen (literalt a) |
virtual void | set_time_limit_seconds (uint32_t lim) |
Protected Attributes | |
bvt | lcnf_bv |
Additional Inherited Members |
|
strong |
|
inlinevirtual |
Reimplemented in aig_prop_baset.
Definition at line 82 of file prop.h.
Referenced by bv_utilst::carry(), bv_utilst::cond_implies_equal(), bv_utilst::full_adder(), and bv_utilst::lt_or_le().
|
virtual |
Reimplemented in cnf_clause_list_assignmentt.
|
inlinevirtual |
Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat1_baset, satcheck_cadicalt, satcheck_picosatt, and satcheck_lingelingt.
Definition at line 108 of file prop.h.
Referenced by bv_refinementt::bv_refinementt(), and prop_conv_solvert::has_is_in_conflict().
|
inlinevirtual |
Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat1_baset, satcheck_cadicalt, satcheck_picosatt, and satcheck_lingelingt.
Definition at line 86 of file prop.h.
Referenced by bv_refinementt::bv_refinementt(), and prop_conv_solvert::has_set_assumptions().
|
inlinevirtual |
Reimplemented in aig_prop_constraintt, and aig_prop_baset.
Definition at line 78 of file prop.h.
Referenced by bv_refinementt::bv_refinementt(), bv_utilst::carry(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_cond(), boolbvt::convert_constraint_select_one(), boolbvt::convert_extractbit(), boolbvt::convert_index(), bv_utilst::divider(), bv_utilst::full_adder(), and bv_utilst::lt_or_le().
|
virtual |
Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat1_baset, satcheck_cadicalt, satcheck_lingelingt, and satcheck_picosatt.
Definition at line 31 of file prop.cpp.
Referenced by bv_refinementt::conflicts_with(), and prop_conv_solvert::is_in_conflict().
Implemented in aig_prop_solvert, cnf_clause_list_assignmentt, qbf_bdd_coret, aig_prop_baset, dimacs_cnf_dumpt, pbs_dimacs_cnft, satcheck_ipasirt, qbf_bdd_certificatet, cnf_clause_listt, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, qbf_qube_coret, qbf_squolem_coret, qbf_squolemt, satcheck_minisat1_baset, satcheck_zchaff_baset, satcheck_cadicalt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, qbf_quantort, qbf_qubet, qbf_skizzot, and qdimacs_coret.
Referenced by bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), cnf_clause_list_assignmentt::copy_assignment_from(), float_utilst::get(), prop_conv_solvert::get_bool(), boolbv_mapt::map_entryt::get_value(), boolbvt::get_value(), prop_conv_solvert::l_get(), aig_prop_solvert::l_get(), and prop_conv_solvert::print_assignment().
|
inlinevirtual |
Reimplemented in aig_prop_constraintt, and aig_prop_baset.
Definition at line 44 of file prop.h.
References const_literal(), and set_equal().
Referenced by bv_utilst::adder_no_overflow(), bv_utilst::cond_negate_no_overflow(), aig_prop_solvert::convert_aig(), boolbvt::convert_unary_minus(), bv_pointerst::do_postponed(), l_set_to_false(), l_set_to_true(), bv_utilst::negate_no_overflow(), prop_conv_solvert::set_to(), and bv_utilst::signed_multiplier_no_overflow().
|
inline |
Definition at line 51 of file prop.h.
References l_set_to().
Referenced by bv_utilst::adder_no_overflow(), and bv_utilst::unsigned_multiplier_no_overflow().
|
inline |
Definition at line 49 of file prop.h.
References l_set_to().
Referenced by arrayst::add_array_constraint(), string_refinementt::add_lemma(), bv_refinementt::arrays_overapproximated(), bv_refinementt::check_SAT(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_extractbit(), boolbvt::convert_index(), bv_refinementt::convert_mult(), aig_prop_constraintt::lcnf(), bv_utilst::lt_or_le(), aig_prop_baset::set_equal(), and bv_utilst::unsigned_divider().
Implemented in aig_prop_baset, and cnft.
Referenced by float_utilst::add_sub(), bv_utilst::adder_no_overflow(), float_utilst::bias(), bv_utilst::carry(), bv_refinementt::check_SAT(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_reduction(), boolbvt::convert_byte_extract(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_index(), boolbvt::convert_onehot(), boolbvt::convert_overflow(), boolbvt::convert_reduction(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), float_utilst::denormalization_shift(), float_utilst::div(), bv_utilst::equal(), float_utilst::fraction_rounding_decision(), bv_utilst::full_adder(), bv_utilst::incrementer(), bv_utilst::is_all_ones(), float_utilst::is_infinity(), float_utilst::is_minus_inf(), float_utilst::is_NaN(), float_utilst::is_normal(), bv_utilst::is_one(), float_utilst::is_plus_inf(), float_utilst::mul(), float_approximationt::normalization_shift(), float_utilst::normalization_shift(), bv_utilst::overflow_add(), bv_utilst::overflow_negate(), float_utilst::pack(), float_utilst::relation(), float_utilst::round_exponent(), float_utilst::round_fraction(), float_utilst::sticky_right_shift(), float_utilst::to_integer(), boolbvt::type_conversion(), bv_utilst::unsigned_multiplier(), and bv_utilst::unsigned_multiplier_no_overflow().
Implemented in aig_prop_baset, and cnft.
Definition at line 55 of file prop.h.
References lcnf_bv.
Referenced by arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_if(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), bv_utilst::carry(), bv_utilst::cond_implies_equal(), boolbvt::convert_constraint_select_one(), aig_prop_solvert::convert_node(), cnf_clause_listt::copy_to(), bv_utilst::full_adder(), cnft::gate_and(), cnft::gate_nand(), cnft::gate_nor(), cnft::gate_or(), cnft::gate_xor(), cnft::land(), lcnf(), cnft::lor(), cnft::lselect(), bv_utilst::lt_or_le(), set_equal(), and prop_conv_solvert::set_to().
|
pure virtual |
Implemented in aig_prop_constraintt, qbf_bdd_coret, dimacs_cnf_dumpt, satcheck_ipasirt, qbf_squolem_coret, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, aig_prop_baset, qbf_squolemt, satcheck_minisat1_baset, satcheck_cadicalt, cnf_clause_listt, satcheck_lingelingt, satcheck_picosatt, and satcheck_booleforce_baset.
Implemented in aig_prop_baset, and cnft.
Referenced by bv_utilst::adder_no_overflow(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), boolbvt::convert_byte_extract(), boolbvt::convert_extractbit(), boolbvt::convert_index(), boolbvt::convert_overflow(), bv_pointerst::convert_rest(), bv_utilst::equal(), bv_utilst::full_adder(), bv_utilst::lt_or_le(), and bv_utilst::overflow_add().
Implemented in aig_prop_baset, and cnft.
Referenced by bv_refinementt::check_SAT(), bv_utilst::cond_implies_equal(), bv_utilst::cond_negate_no_overflow(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_extractbit(), boolbvt::convert_index(), bv_refinementt::convert_mult(), bv_pointerst::do_postponed(), and bv_utilst::unsigned_divider().
Implemented in aig_prop_baset, and cnft.
Referenced by boolbvt::convert_bitwise().
Implemented in aig_prop_baset, and cnft.
Referenced by boolbvt::convert_bitwise().
Implemented in qbf_bdd_coret, aig_prop_baset, and cnft.
Referenced by float_utilst::add_sub(), bv_utilst::carry(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_reduction(), boolbvt::convert_case(), boolbvt::convert_cond(), bv_refinementt::convert_mult(), boolbvt::convert_onehot(), boolbvt::convert_overflow(), boolbvt::convert_reduction(), bv_pointerst::convert_rest(), boolbvt::convert_typecast(), float_utilst::denormalization_shift(), float_utilst::div(), float_utilst::fraction_rounding_decision(), bv_utilst::full_adder(), bv_utilst::is_not_zero(), bv_utilst::is_zero(), float_utilst::limit_distance(), bv_utilst::lt_or_le(), float_utilst::mul(), bv_utilst::overflow_negate(), float_utilst::pack(), float_utilst::relation(), float_utilst::round_exponent(), float_utilst::round_fraction(), float_utilst::sticky_right_shift(), boolbvt::type_conversion(), bv_utilst::unsigned_divider(), and bv_utilst::verilog_bv_has_x_or_z().
Implemented in qbf_bdd_coret, aig_prop_baset, and cnft.
Implemented in aig_prop_baset, and cnft.
Referenced by float_utilst::add_sub(), bv_utilst::cond_negate(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_reduction(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), boolbvt::convert_cond(), boolbvt::convert_constraint_select_one(), boolbvt::convert_extractbit(), boolbvt::convert_index(), boolbvt::convert_not(), boolbvt::convert_overflow(), boolbvt::convert_update_rec(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), float_utilst::fraction_rounding_decision(), bv_utilst::overflow_sub(), float_utilst::pack(), float_utilst::relation(), bv_utilst::select(), bv_utilst::shift(), and bv_utilst::signed_divider().
Implemented in aig_prop_baset, and cnft.
Referenced by float_utilst::add_sub(), bv_utilst::adder_no_overflow(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_reduction(), boolbvt::convert_overflow(), boolbvt::convert_reduction(), float_utilst::div(), bv_utilst::full_adder(), bv_utilst::incrementer(), bv_utilst::lt_or_le(), float_utilst::mul(), bv_utilst::overflow_add(), float_utilst::relation(), bv_utilst::signed_divider(), bv_utilst::signed_multiplier(), bv_utilst::signed_multiplier_no_overflow(), and bv_utilst::wallace_tree().
Implemented in aig_prop_baset, and cnft.
|
pure virtual |
Implemented in qbf_bdd_coret, aig_prop_baset, cnft, and qbf_bdd_certificatet.
Referenced by equalityt::add_equality_constraints(), bv_utilst::carry(), aig_prop_solvert::convert_aig(), bv_pointerst::convert_bitvector(), prop_conv_solvert::convert_bool(), boolbvt::convert_byte_extract(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_constraint_select_one(), boolbvt::convert_equality(), boolbvt::convert_extractbit(), boolbvt::convert_index(), bv_pointerst::convert_pointer_type(), boolbvt::convert_quantifier(), bv_pointerst::convert_rest(), prop_conv_solvert::convert_rest(), boolbvt::convert_union(), equalityt::equality2(), float_utilst::fraction_rounding_decision(), bv_utilst::full_adder(), prop_conv_solvert::get_literal(), boolbv_mapt::get_literals(), bv_utilst::lt_or_le(), boolbvt::make_free_bv_expr(), new_variables(), float_approximationt::overapproximating_left_shift(), boolbvt::type_conversion(), and bv_utilst::unsigned_divider().
bvt propt::new_variables | ( | std::size_t | width | ) |
generates a bitvector of given width with new variables
Definition at line 39 of file prop.cpp.
References new_variable(), and messaget::result().
Referenced by bv_refinementt::add_approximation(), boolbvt::conversion_failed(), boolbvt::convert_constraint_select_one(), boolbvt::convert_function_application(), boolbvt::convert_power(), float_approximationt::normalization_shift(), and float_utilst::normalization_shift().
|
pure virtual |
Implemented in aig_prop_baset, and cnft.
Referenced by aig_prop_solvert::convert_aig(), boolbvt::convert_symbol(), and boolbv_mapt::set_literals().
|
pure virtual |
Implemented in aig_prop_solvert, satcheck_minisat1_coret, qbf_bdd_coret, aig_prop_baset, dimacs_cnf_dumpt, pbs_dimacs_cnft, cnf_clause_listt, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, qbf_squolemt, qbf_squolem_coret, qbf_qube_coret, satcheck_minisat1_baset, satcheck_zchaff_baset, satcheck_cadicalt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, qbf_skizzo_coret, qbf_quantort, qbf_qubet, and qbf_skizzot.
Referenced by prop_conv_solvert::dec_solve(), bv_refinementt::prop_solve(), and aig_prop_solvert::prop_solve().
|
virtual |
Reimplemented in satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_minisat1_baset, satcheck_cadicalt, satcheck_zchaff_baset, satcheck_lingelingt, and satcheck_picosatt.
|
inlinevirtual |
Reimplemented in satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_minisat2_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_minisat1_baset, satcheck_cadicalt, satcheck_picosatt, and satcheck_lingelingt.
Definition at line 85 of file prop.h.
Referenced by bv_refinementt::prop_solve(), bv_refinementt::set_assumptions(), and prop_conv_solvert::set_assumptions().
asserts a==b in the propositional formula
Reimplemented in aig_prop_baset.
Definition at line 14 of file prop.cpp.
References lcnf().
Referenced by equalityt::add_equality_constraints(), l_set_to(), boolbvt::post_process_quantifiers(), bv_utilst::set_equal(), and boolbv_mapt::set_literals().
|
inlinevirtual |
Reimplemented in satcheck_minisat_simplifiert, satcheck_glucose_simplifiert, and satcheck_lingelingt.
Definition at line 111 of file prop.h.
Referenced by prop_conv_solvert::convert(), boolbvt::convert_bv(), equalityt::equality2(), bv_refinementt::freeze_lazy_constraints(), and prop_conv_solvert::set_frozen().
|
inlinevirtual |
Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, and satcheck_minisat2_baset< Minisat::Solver >.
Definition at line 114 of file prop.h.
References messaget::eom(), and messaget::warning().
Referenced by prop_conv_solvert::set_time_limit_seconds().
Definition at line 90 of file prop.h.
Referenced by prop_conv_solvert::get_literal().
|
pure virtual |
Implemented in aig_prop_solvert, satcheck_minisat_simplifiert, satcheck_minisat1_coret, satcheck_minisat_no_simplifiert, satcheck_glucose_simplifiert, satcheck_minisat1_prooft, qbf_bdd_coret, satcheck_glucose_no_simplifiert, pbs_dimacs_cnft, aig_prop_baset, dimacs_cnf_dumpt, satcheck_ipasirt, cnf_clause_listt, qbf_squolemt, qbf_squolem_coret, qdimacs_cnft, qbf_qube_coret, dimacs_cnft, satcheck_minisat1_baset, satcheck_zchaff_baset, satcheck_cadicalt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, qbf_skizzo_coret, qbf_quantort, qbf_qubet, and qbf_skizzot.
Referenced by bv_refinementt::dec_solve(), prop_conv_solvert::dec_solve(), bv_refinementt::decision_procedure_text(), string_refinementt::decision_procedure_text(), and aig_prop_solvert::solver_text().