cprover
equalityt Class Reference

#include <equality.h>

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

Classes

struct  typestructt
 

Public Member Functions

 equalityt (const namespacet &_ns, 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 (const namespacet &_ns, propt &_prop)
 
virtual ~prop_conv_solvert ()
 
virtual void set_to (const exprt &expr, bool value) override
 
virtual decision_proceduret::resultt dec_solve () override
 
virtual void print_assignment (std::ostream &out) const override
 
virtual std::string decision_procedure_text () const override
 
virtual exprt get (const exprt &expr) const override
 
virtual tvt l_get (literalt a) const override
 
virtual void set_frozen (literalt a) override
 
virtual void set_assumptions (const bvt &_assumptions) override
 
virtual bool has_set_assumptions () const override
 
virtual void set_all_frozen () override
 
virtual literalt convert (const exprt &expr) override
 
virtual bool is_in_conflict (literalt l) const override
 determine whether a variable is in the final conflict More...
 
virtual 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
 
- 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)
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
resultt operator() ()
 
virtual bool in_core (const exprt &expr)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

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

- 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 {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Public Attributes inherited from prop_conv_solvert
bool use_cache
 
bool equality_propagation
 
bool freeze_all
 

Detailed Description

Definition at line 19 of file equality.h.

Member Typedef Documentation

§ elements_revt

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

Definition at line 38 of file equality.h.

§ elementst

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

Definition at line 36 of file equality.h.

§ equalitiest

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

Definition at line 37 of file equality.h.

§ typemapt

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

Definition at line 47 of file equality.h.

Constructor & Destructor Documentation

§ equalityt()

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

Definition at line 22 of file equality.h.

References equality().

Member Function Documentation

§ add_equality_constraints() [1/2]

void equalityt::add_equality_constraints ( )
protectedvirtual

Definition at line 91 of file equality.cpp.

References typemap.

Referenced by post_process().

§ add_equality_constraints() [2/2]

void equalityt::add_equality_constraints ( const typestructt typestruct)
protectedvirtual

§ equality()

§ equality2()

§ post_process()

void equalityt::post_process ( )
inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Definition at line 28 of file equality.h.

References add_equality_constraints(), prop_conv_solvert::post_process(), and typemap.

Referenced by arrayst::post_process().

Member Data Documentation

§ typemap

typemapt equalityt::typemap
protected

Definition at line 49 of file equality.h.

Referenced by add_equality_constraints(), equality2(), and post_process().


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