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 std::string &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 | ~prop_assignmentt () |
Protected Attributes | |
bvt | lcnf_bv |
Additional Inherited Members |
|
strong |
|
inlinevirtual |
Reimplemented in aig_prop_baset.
Definition at line 80 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 |
Implements prop_assignmentt.
Reimplemented in cnf_clause_list_assignmentt.
|
inlinevirtual |
Reimplemented in 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_precosatt, satcheck_picosatt, and satcheck_lingelingt.
Definition at line 106 of file prop.h.
Referenced by bv_refinementt::bv_refinementt(), and prop_conv_solvert::has_is_in_conflict().
|
inlinevirtual |
Reimplemented in 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_precosatt, satcheck_picosatt, and satcheck_lingelingt.
Definition at line 84 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 76 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_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_lingelingt, and satcheck_picosatt.
Definition at line 31 of file prop.cpp.
Referenced by bv_refinementt::is_in_conflict(), and prop_conv_solvert::is_in_conflict().
Implements prop_assignmentt.
Implemented in aig_prop_solvert, cnf_clause_list_assignmentt, prop_wrappert, qbf_bdd_coret, aig_prop_baset, dimacs_cnf_dumpt, dplib_propt, cvc_propt, pbs_dimacs_cnft, smt2_propt, smt1_propt, 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_precosatt, satcheck_smvsatt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, satcheck_limmatt, 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_wrappert::l_get(), prop_conv_solvert::l_get(), aig_prop_solvert::l_get(), and prop_conv_solvert::print_assignment().
|
inlinevirtual |
Reimplemented in aig_prop_constraintt, prop_wrappert, and aig_prop_baset.
Definition at line 42 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(), prop_wrappert::l_set_to(), 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 49 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 47 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 cvc_propt, dplib_propt, smt2_propt, aig_prop_baset, smt1_propt, prop_wrappert, 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(), prop_wrappert::land(), 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 cvc_propt, dplib_propt, smt2_propt, aig_prop_baset, prop_wrappert, smt1_propt, and cnft.
Definition at line 53 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(), prop_wrappert::lcnf(), cnft::lor(), cnft::lselect(), bv_utilst::lt_or_le(), read_dimacs_cnf(), set_equal(), and prop_conv_solvert::set_to().
|
pure virtual |
Implemented in aig_prop_constraintt, satcheck_smvsat_interpolatort, prop_wrappert, qbf_bdd_coret, dimacs_cnf_dumpt, dplib_propt, cvc_propt, smt2_propt, smt1_propt, 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_precosatt, cnf_clause_listt, satcheck_smvsatt, satcheck_lingelingt, satcheck_picosatt, and satcheck_booleforce_baset.
Implemented in prop_wrappert, cvc_propt, dplib_propt, aig_prop_baset, smt2_propt, smt1_propt, 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(), bv_pointerst::convert_rest(), bv_utilst::equal(), bv_utilst::full_adder(), prop_wrappert::lequal(), bv_utilst::lt_or_le(), and bv_utilst::overflow_add().
Implemented in prop_wrappert, cvc_propt, dplib_propt, aig_prop_baset, smt2_propt, smt1_propt, 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(), prop_wrappert::limplies(), and bv_utilst::unsigned_divider().
Implemented in prop_wrappert, cvc_propt, dplib_propt, aig_prop_baset, smt2_propt, smt1_propt, and cnft.
Referenced by boolbvt::convert_bitwise(), and prop_wrappert::lnand().
Implemented in prop_wrappert, cvc_propt, dplib_propt, aig_prop_baset, smt2_propt, smt1_propt, and cnft.
Referenced by boolbvt::convert_bitwise(), and prop_wrappert::lnor().
Implemented in qbf_bdd_coret, cvc_propt, dplib_propt, smt2_propt, aig_prop_baset, smt1_propt, prop_wrappert, 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(), prop_wrappert::lor(), 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, cvc_propt, dplib_propt, prop_wrappert, smt2_propt, aig_prop_baset, smt1_propt, and cnft.
Implemented in prop_wrappert, cvc_propt, dplib_propt, aig_prop_baset, smt2_propt, smt1_propt, 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_update_rec(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), float_utilst::fraction_rounding_decision(), prop_wrappert::lselect(), bv_utilst::overflow_sub(), float_utilst::pack(), float_utilst::relation(), bv_utilst::select(), bv_utilst::shift(), and bv_utilst::signed_divider().
Implemented in cvc_propt, dplib_propt, prop_wrappert, smt2_propt, aig_prop_baset, smt1_propt, 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(), prop_wrappert::lxor(), 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 prop_wrappert, cvc_propt, dplib_propt, aig_prop_baset, smt2_propt, smt1_propt, and cnft.
|
pure virtual |
Implemented in prop_wrappert, qbf_bdd_coret, aig_prop_baset, cvc_propt, dplib_propt, smt2_propt, smt1_propt, 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(), prop_wrappert::new_variable(), 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 prop_wrappert, aig_prop_baset, cvc_propt, dplib_propt, smt2_propt, smt1_propt, and cnft.
Referenced by aig_prop_solvert::convert_aig(), boolbvt::convert_symbol(), prop_wrappert::no_variables(), boolbv_mapt::set_literals(), and bv_refinementt::set_to().
|
pure virtual |
Implemented in aig_prop_solvert, satcheck_minisat1_coret, prop_wrappert, dplib_propt, cvc_propt, qbf_bdd_coret, aig_prop_baset, smt2_propt, smt1_propt, dimacs_cnf_dumpt, pbs_dimacs_cnft, satcheck_smvsat_coret, 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_squolemt, qbf_squolem_coret, qbf_qube_coret, satcheck_minisat1_baset, satcheck_zchaff_baset, satcheck_precosatt, satcheck_smvsatt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, qbf_skizzo_coret, satcheck_limmatt, qbf_quantort, qbf_qubet, and qbf_skizzot.
Referenced by prop_conv_solvert::dec_solve(), bv_refinementt::prop_solve(), prop_wrappert::prop_solve(), and aig_prop_solvert::prop_solve().
|
virtual |
Implements prop_assignmentt.
Reimplemented in smt2_propt, smt1_propt, 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_precosatt, satcheck_zchaff_baset, satcheck_lingelingt, and satcheck_picosatt.
|
inlinevirtual |
Reimplemented in 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_picosatt, and satcheck_lingelingt.
Definition at line 83 of file prop.h.
Referenced by bv_refinementt::prop_solve(), prop_conv_solvert::set_assumptions(), and bv_refinementt::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_glucose_simplifiert, satcheck_minisat_simplifiert, and satcheck_lingelingt.
Definition at line 109 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 |
Definition at line 88 of file prop.h.
Referenced by prop_conv_solvert::get_literal().
|
pure virtual |
Implemented in aig_prop_solvert, satcheck_minisat1_coret, prop_wrappert, satcheck_glucose_simplifiert, satcheck_minisat_simplifiert, satcheck_minisat1_prooft, qbf_bdd_coret, satcheck_glucose_no_simplifiert, satcheck_minisat_no_simplifiert, pbs_dimacs_cnft, aig_prop_baset, dplib_propt, cvc_propt, smt2_propt, smt1_propt, dimacs_cnf_dumpt, cnf_clause_listt, qbf_squolemt, qbf_squolem_coret, qdimacs_cnft, qbf_qube_coret, dimacs_cnft, satcheck_minisat1_baset, satcheck_zchaff_baset, satcheck_precosatt, satcheck_smvsatt, satcheck_lingelingt, satcheck_picosatt, satcheck_booleforce_baset, satcheck_zcoret, qbf_skizzo_coret, satcheck_limmatt, 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(), prop_wrappert::solver_text(), and aig_prop_solvert::solver_text().