cprover
prop_conv_solvert Class Reference

TO_BE_DOCUMENTED. More...

#include <prop_conv.h>

Inheritance diagram for prop_conv_solvert:
[legend]
Collaboration diagram for prop_conv_solvert:
[legend]

Public Types

typedef std::map< irep_idt, literaltsymbolst
 
typedef std::unordered_map< exprt, literalt, irep_hashcachet
 
- Public Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 prop_conv_solvert (const namespacet &_ns, propt &_prop)
 
virtual ~prop_conv_solvert ()=default
 
void set_to (const exprt &expr, bool value) override
 
decision_proceduret::resultt dec_solve () override
 
void print_assignment (std::ostream &out) const override
 
std::string decision_procedure_text () const override
 
exprt get (const exprt &expr) const override
 
virtual tvt l_get (literalt a) const override
 
void set_frozen (literalt a) override
 
void set_assumptions (const bvt &_assumptions) override
 
bool has_set_assumptions () const override
 
void set_all_frozen () override
 
literalt convert (const exprt &expr) override
 
bool is_in_conflict (literalt l) const override
 determine whether a variable is in the final conflict More...
 
bool has_is_in_conflict () const override
 
virtual bool literal (const exprt &expr, literalt &literal) const
 
virtual void clear_cache ()
 
const cachetget_cache () const
 
const symbolstget_symbols () const
 
void set_time_limit_seconds (uint32_t lim) override
 
virtual void set_frozen (literalt a)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from prop_convt
 prop_convt (const namespacet &_ns)
 
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from decision_proceduret
 decision_proceduret (const namespacet &_ns)
 
virtual ~decision_proceduret ()
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
resultt operator() ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Public Attributes

bool use_cache = true
 
bool equality_propagation = true
 
bool freeze_all = false
 

Protected Member Functions

virtual void post_process ()
 
virtual bool get_bool (const exprt &expr, tvt &value) const
 get a boolean value from counter example if not valid More...
 
virtual literalt convert_rest (const exprt &expr)
 
virtual literalt convert_bool (const exprt &expr)
 
virtual bool set_equality_to_true (const equal_exprt &expr)
 
virtual literalt get_literal (const irep_idt &symbol)
 
virtual void ignoring (const exprt &expr)
 

Protected Attributes

bool post_processing_done = false
 
symbolst symbols
 
cachet cache
 
proptprop
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 70 of file prop_conv.h.

Member Typedef Documentation

◆ cachet

typedef std::unordered_map<exprt, literalt, irep_hash> prop_conv_solvert::cachet

Definition at line 118 of file prop_conv.h.

◆ symbolst

Definition at line 117 of file prop_conv.h.

Constructor & Destructor Documentation

◆ prop_conv_solvert()

prop_conv_solvert::prop_conv_solvert ( const namespacet _ns,
propt _prop 
)
inline

Definition at line 73 of file prop_conv.h.

◆ ~prop_conv_solvert()

virtual prop_conv_solvert::~prop_conv_solvert ( )
virtualdefault

Member Function Documentation

◆ clear_cache()

virtual void prop_conv_solvert::clear_cache ( )
inlinevirtual

Reimplemented in boolbvt.

Definition at line 115 of file prop_conv.h.

References cache.

Referenced by boolbvt::clear_cache().

◆ convert()

◆ convert_bool()

◆ convert_rest()

◆ dec_solve()

◆ decision_procedure_text()

std::string prop_conv_solvert::decision_procedure_text ( ) const
inlineoverridevirtual

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 83 of file prop_conv.h.

◆ get()

exprt prop_conv_solvert::get ( const exprt expr) const
overridevirtual

◆ get_bool()

bool prop_conv_solvert::get_bool ( const exprt expr,
tvt value 
) const
protectedvirtual

get a boolean value from counter example if not valid

Definition at line 74 of file prop_conv.cpp.

References cache, forall_operands, irept::id(), tvt::is_false(), exprt::is_false(), tvt::is_true(), exprt::is_true(), propt::l_get(), exprt::op0(), exprt::operands(), prop, messaget::result(), symbols, to_symbol_expr(), and exprt::type().

Referenced by get().

◆ get_cache()

const cachet& prop_conv_solvert::get_cache ( ) const
inline

Definition at line 120 of file prop_conv.h.

References cache.

◆ get_literal()

literalt prop_conv_solvert::get_literal ( const irep_idt symbol)
protectedvirtual

◆ get_symbols()

const symbolst& prop_conv_solvert::get_symbols ( ) const
inline

Definition at line 121 of file prop_conv.h.

References symbols.

Referenced by cbmc_dimacst::write_dimacs().

◆ has_is_in_conflict()

bool prop_conv_solvert::has_is_in_conflict ( ) const
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 105 of file prop_conv.h.

References propt::has_is_in_conflict(), and prop.

◆ has_set_assumptions()

bool prop_conv_solvert::has_set_assumptions ( ) const
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 96 of file prop_conv.h.

References propt::has_set_assumptions(), and prop.

◆ ignoring()

void prop_conv_solvert::ignoring ( const exprt expr)
protectedvirtual

Definition at line 454 of file prop_conv.cpp.

References messaget::eom(), irept::pretty(), and messaget::warning().

Referenced by boolbvt::conversion_failed(), and convert_rest().

◆ is_in_conflict()

bool prop_conv_solvert::is_in_conflict ( literalt  l) const
inlineoverridevirtual

determine whether a variable is in the final conflict

Reimplemented from prop_convt.

Definition at line 103 of file prop_conv.h.

References propt::is_in_conflict(), and prop.

◆ l_get()

virtual tvt prop_conv_solvert::l_get ( literalt  a) const
inlineoverridevirtual

Implements prop_convt.

Definition at line 89 of file prop_conv.h.

References propt::l_get(), and prop.

◆ literal()

bool prop_conv_solvert::literal ( const exprt expr,
literalt literal 
) const
virtual

◆ post_process()

void prop_conv_solvert::post_process ( )
protectedvirtual

Reimplemented in boolbvt, arrayst, equalityt, and bv_pointerst.

Definition at line 461 of file prop_conv.cpp.

Referenced by dec_solve(), and equalityt::post_process().

◆ print_assignment()

void prop_conv_solvert::print_assignment ( std::ostream &  out) const
overridevirtual

Implements decision_proceduret.

Definition at line 509 of file prop_conv.cpp.

References propt::l_get(), prop, and symbols.

Referenced by boolbvt::print_assignment().

◆ set_all_frozen()

void prop_conv_solvert::set_all_frozen ( )
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 98 of file prop_conv.h.

References freeze_all.

◆ set_assumptions()

void prop_conv_solvert::set_assumptions ( const bvt _assumptions)
inlineoverridevirtual

Reimplemented from prop_convt.

Reimplemented in bv_refinementt.

Definition at line 94 of file prop_conv.h.

References prop, and propt::set_assumptions().

◆ set_equality_to_true()

bool prop_conv_solvert::set_equality_to_true ( const equal_exprt expr)
protectedvirtual

◆ set_frozen() [1/3]

void prop_convt::set_frozen

Definition at line 24 of file prop_conv.cpp.

◆ set_frozen() [2/3]

void prop_convt::set_frozen

Definition at line 29 of file prop_conv.cpp.

◆ set_frozen() [3/3]

void prop_conv_solvert::set_frozen ( literalt  a)
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 90 of file prop_conv.h.

References prop, and propt::set_frozen().

Referenced by bv_refinementt::add_approximation(), and boolbvt::boolbv_set_equality_to_true().

◆ set_time_limit_seconds()

void prop_conv_solvert::set_time_limit_seconds ( uint32_t  lim)
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 123 of file prop_conv.h.

References prop, and propt::set_time_limit_seconds().

◆ set_to()

Member Data Documentation

◆ cache

cachet prop_conv_solvert::cache
protected

Definition at line 147 of file prop_conv.h.

Referenced by clear_cache(), convert(), get_bool(), and get_cache().

◆ equality_propagation

bool prop_conv_solvert::equality_propagation = true

◆ freeze_all

bool prop_conv_solvert::freeze_all = false

◆ post_processing_done

bool prop_conv_solvert::post_processing_done = false
protected

Definition at line 131 of file prop_conv.h.

Referenced by dec_solve().

◆ prop

propt& prop_conv_solvert::prop
protected

Definition at line 152 of file prop_conv.h.

Referenced by bv_refinementt::add_approximation(), arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraint(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_if(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), equalityt::add_equality_constraints(), string_refinementt::add_lemma(), bv_refinementt::arrays_overapproximated(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), bv_refinementt::bv_refinementt(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), arrayst::collect_arrays(), bv_refinementt::conflicts_with(), boolbvt::conversion_failed(), convert(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), convert_bool(), boolbvt::convert_bv(), boolbvt::convert_bv_reduction(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), boolbvt::convert_case(), boolbvt::convert_cond(), boolbvt::convert_constraint_select_one(), boolbvt::convert_equality(), boolbvt::convert_extractbit(), boolbvt::convert_floatbv_op(), boolbvt::convert_floatbv_typecast(), boolbvt::convert_function_application(), boolbvt::convert_ieee_float_rel(), boolbvt::convert_index(), bv_refinementt::convert_mult(), boolbvt::convert_not(), boolbvt::convert_onehot(), boolbvt::convert_overflow(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), boolbvt::convert_quantifier(), boolbvt::convert_reduction(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), convert_rest(), boolbvt::convert_symbol(), boolbvt::convert_typecast(), boolbvt::convert_unary_minus(), boolbvt::convert_union(), boolbvt::convert_update_rec(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), bv_refinementt::dec_solve(), dec_solve(), bv_refinementt::decision_procedure_text(), string_refinementt::decision_procedure_text(), bv_pointerst::do_postponed(), equalityt::equality2(), bv_refinementt::freeze_lazy_constraints(), get_bool(), get_literal(), boolbvt::get_value(), has_is_in_conflict(), has_set_assumptions(), is_in_conflict(), l_get(), boolbvt::make_free_bv_expr(), boolbvt::post_process_quantifiers(), boolbvt::print_assignment(), print_assignment(), bv_refinementt::prop_solve(), arrayst::record_array_equality(), bv_refinementt::set_assumptions(), set_assumptions(), set_frozen(), set_time_limit_seconds(), set_to(), boolbvt::type_conversion(), and cbmc_dimacst::write_dimacs().

◆ symbols

◆ use_cache

bool prop_conv_solvert::use_cache = true

Definition at line 111 of file prop_conv.h.

Referenced by convert().


The documentation for this class was generated from the following files: