cprover
prop_conv_solvert Class Reference

TO_BE_DOCUMENTED. More...

#include <prop_conv.h>

+ Inheritance diagram for prop_conv_solvert:
+ Collaboration diagram for prop_conv_solvert:

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 (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
 
bool literal (const symbol_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
 
std::size_t get_number_of_solver_calls () const override
 Returns the number of incremental solver calls. More...
 
virtual void set_frozen (literalt a)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from prop_convt
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from decision_proceduret
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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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 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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

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 ( propt _prop)
inlineexplicit

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.

◆ convert()

literalt prop_conv_solvert::convert ( const exprt expr)
overridevirtual

Implements prop_convt.

Definition at line 157 of file prop_conv.cpp.

◆ convert_bool()

literalt prop_conv_solvert::convert_bool ( const exprt expr)
protectedvirtual

Definition at line 190 of file prop_conv.cpp.

◆ convert_rest()

literalt prop_conv_solvert::convert_rest ( const exprt expr)
protectedvirtual

Reimplemented in boolbvt, and bv_pointerst.

Definition at line 329 of file prop_conv.cpp.

◆ dec_solve()

decision_proceduret::resultt prop_conv_solvert::dec_solve ( )
overridevirtual

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 464 of file prop_conv.cpp.

◆ 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

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 486 of file prop_conv.cpp.

◆ 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 69 of file prop_conv.cpp.

◆ get_cache()

const cachet& prop_conv_solvert::get_cache ( ) const
inline

Definition at line 120 of file prop_conv.h.

◆ get_literal()

literalt prop_conv_solvert::get_literal ( const irep_idt symbol)
protectedvirtual

Definition at line 51 of file prop_conv.cpp.

◆ get_number_of_solver_calls()

std::size_t prop_conv_solvert::get_number_of_solver_calls ( ) const
overridevirtual

Returns the number of incremental solver calls.

Implements prop_convt.

Definition at line 516 of file prop_conv.cpp.

◆ get_symbols()

const symbolst& prop_conv_solvert::get_symbols ( ) const
inline

Definition at line 121 of file prop_conv.h.

◆ 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.

◆ 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.

◆ ignoring()

void prop_conv_solvert::ignoring ( const exprt expr)
protectedvirtual

Definition at line 453 of file prop_conv.cpp.

◆ 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.

◆ 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.

◆ literal()

bool prop_conv_solvert::literal ( const symbol_exprt expr,
literalt literal 
) const

Definition at line 36 of file prop_conv.cpp.

◆ post_process()

void prop_conv_solvert::post_process ( )
protectedvirtual

Reimplemented in boolbvt, arrayst, equalityt, and bv_pointerst.

Definition at line 460 of file prop_conv.cpp.

◆ print_assignment()

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

Implements decision_proceduret.

Definition at line 510 of file prop_conv.cpp.

◆ set_all_frozen()

void prop_conv_solvert::set_all_frozen ( )
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 98 of file prop_conv.h.

◆ 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.

◆ set_equality_to_true()

bool prop_conv_solvert::set_equality_to_true ( const equal_exprt expr)
protectedvirtual

Definition at line 336 of file prop_conv.cpp.

◆ 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.

◆ 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.

◆ set_to()

void prop_conv_solvert::set_to ( const exprt expr,
bool  value 
)
overridevirtual

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 363 of file prop_conv.cpp.

Member Data Documentation

◆ cache

cachet prop_conv_solvert::cache
protected

Definition at line 149 of file prop_conv.h.

◆ equality_propagation

bool prop_conv_solvert::equality_propagation = true

Definition at line 112 of file prop_conv.h.

◆ freeze_all

bool prop_conv_solvert::freeze_all = false

Definition at line 113 of file prop_conv.h.

◆ post_processing_done

bool prop_conv_solvert::post_processing_done = false
protected

Definition at line 133 of file prop_conv.h.

◆ prop

propt& prop_conv_solvert::prop
protected

Definition at line 154 of file prop_conv.h.

◆ symbols

symbolst prop_conv_solvert::symbols
protected

Definition at line 144 of file prop_conv.h.

◆ use_cache

bool prop_conv_solvert::use_cache = true

Definition at line 111 of file prop_conv.h.


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