equalityt Class Reference

#include <equality.h>

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


struct  typestructt

Public Member Functions

 equalityt (propt &_prop, message_handlert &message_handler)
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, message_handlert &message_handler)
virtual ~prop_conv_solvert ()=default
decision_proceduret::resultt dec_solve () override
 Run the decision procedure to solve the problem. More...
void print_assignment (std::ostream &out) const override
 Print satisfying assignment to out. More...
std::string decision_procedure_text () const override
 Return a textual description of the decision procedure. More...
exprt get (const exprt &expr) const override
 Return expr with variables replaced by values from satisfying assignment if available. More...
tvt l_get (literalt a) const override
 Return value of literal l from satisfying assignment. More...
exprt handle (const exprt &expr) override
 Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to. More...
void set_frozen (literalt)
void set_frozen (const bvt &)
void set_all_frozen ()
literalt convert (const exprt &expr) override
 Convert a Boolean expression and return the corresponding literal. More...
bool is_in_conflict (const exprt &expr) const override
 Returns true if an expression is in the final conflict leading to UNSAT. More...
void set_to (const exprt &expr, bool value) override
 For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'. More...
void push () override
 Push a new context on the stack This context becomes a child context nested in the current context. More...
void push (const std::vector< exprt > &assumptions) override
 Push assumptions in form of literal_exprt More...
void pop () override
 Pop whatever is on top of the stack. More...
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
 Set the limit for the solver to time out in seconds. More...
std::size_t get_number_of_solver_calls () const override
 Return the number of incremental solver calls. More...
- Public Member Functions inherited from conflict_providert
virtual ~conflict_providert ()=default
- Public Member Functions inherited from prop_convt
virtual ~prop_convt ()
- Public Member Functions inherited from stack_decision_proceduret
virtual ~stack_decision_proceduret ()=default
- Public Member Functions inherited from decision_proceduret
void set_to_true (const exprt &expr)
 For a Boolean expression expr, add the constraint 'expr'. More...
void set_to_false (const exprt &expr)
 For a Boolean expression expr, add the constraint 'not expr'. More...
resultt operator() ()
 Run the decision procedure to solve the problem. More...
virtual ~decision_proceduret ()
- Public Member Functions inherited from solver_resource_limitst
virtual ~solver_resource_limitst ()=default

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 optionalt< bool > get_bool (const exprt &expr) const
 Get a boolean value from the model if the formula is satisfiable. 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
messaget log
bvt assumption_stack
 Assumptions on the stack. More...
std::size_t context_literal_counter = 0
 To generate unique literal names for contexts. More...
std::vector< size_t > context_size_stack
 assumption_stack is segmented in contexts; Number of assumptions in each context on the stack More...

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 }
 Result of running the decision procedure. More...
- Public Attributes inherited from prop_conv_solvert
bool use_cache = true
bool equality_propagation = true
bool freeze_all = false
- Static Protected Attributes inherited from prop_conv_solvert
static const char * context_prefix = "prop_conv::context$"

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 39 of file equality.h.

◆ elementst

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

Definition at line 37 of file equality.h.

◆ equalitiest

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

Definition at line 38 of file equality.h.

◆ typemapt

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

Definition at line 48 of file equality.h.

Constructor & Destructor Documentation

◆ equalityt()

equalityt::equalityt ( propt _prop,
message_handlert message_handler 

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 29 of file equality.h.

Member Data Documentation

◆ typemap

typemapt equalityt::typemap

Definition at line 50 of file equality.h.

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