equalityt Class Reference

#include <equality.h>

+ Inheritance diagram for equalityt:
+ Collaboration diagram for equalityt:


struct  typestructt

Public Member Functions

 equalityt (propt &_prop)
virtual literalt equality (const exprt &e1, const exprt &e2)
void post_process () override
- Public Member Functions inherited from prop_conv_solvert
 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...

Protected Types

typedef std::unordered_map< const exprt, unsigned, irep_hashelementst
typedef std::map< std::pair< unsigned, unsigned >, literaltequalitiest
typedef std::map< unsigned, exprtelements_revt
typedef std::unordered_map< const typet, typestructt, irep_hashtypemapt

Protected Member Functions

virtual literalt equality2 (const exprt &e1, const exprt &e2)
virtual void add_equality_constraints ()
virtual void add_equality_constraints (const typestructt &typestruct)
- Protected Member Functions inherited from prop_conv_solvert
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

typemapt typemap
- Protected Attributes inherited from prop_conv_solvert
bool post_processing_done = false
symbolst symbols
cachet cache
- Protected Attributes inherited from messaget
mstreamt mstream

Additional Inherited Members

- Public Types inherited from prop_conv_solvert
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 {
- 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...
- Public Attributes inherited from prop_conv_solvert
bool use_cache = true
bool equality_propagation = true
bool freeze_all = false
- 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

Definition at line 19 of file equality.h.

Member Typedef Documentation

◆ elements_revt

typedef std::map<unsigned, exprt> equalityt::elements_revt

Definition at line 38 of file equality.h.

◆ elementst

typedef std::unordered_map<const exprt, unsigned, irep_hash> equalityt::elementst

Definition at line 36 of file equality.h.

◆ equalitiest

typedef std::map<std::pair<unsigned, unsigned>, literalt> equalityt::equalitiest

Definition at line 37 of file equality.h.

◆ typemapt

typedef std::unordered_map<const typet, typestructt, irep_hash> equalityt::typemapt

Definition at line 47 of file equality.h.

Constructor & Destructor Documentation

◆ equalityt()

equalityt::equalityt ( propt _prop)

Definition at line 22 of file equality.h.

Member Function Documentation

◆ add_equality_constraints() [1/2]

void equalityt::add_equality_constraints ( )

Definition at line 89 of file equality.cpp.

◆ add_equality_constraints() [2/2]

void equalityt::add_equality_constraints ( const typestructt typestruct)

Definition at line 96 of file equality.cpp.

◆ equality()

literalt equalityt::equality ( const exprt e1,
const exprt e2 

Definition at line 17 of file equality.cpp.

◆ equality2()

literalt equalityt::equality2 ( const exprt e1,
const exprt e2 

Definition at line 25 of file equality.cpp.

◆ post_process()

void equalityt::post_process ( )

Reimplemented from prop_conv_solvert.

Definition at line 28 of file equality.h.

Member Data Documentation

◆ typemap

typemapt equalityt::typemap

Definition at line 49 of file equality.h.

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