cprover
equalityt Class Reference

#include <equality.h>

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

Classes

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

Definition at line 39 of file equality.h.

◆ elementst

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

Definition at line 37 of file equality.h.

◆ equalitiest

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

Definition at line 38 of file equality.h.

◆ typemapt

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

Definition at line 48 of file equality.h.

Constructor & Destructor Documentation

◆ equalityt()

equalityt::equalityt ( propt _prop,
message_handlert message_handler 
)
inline

Definition at line 22 of file equality.h.

Member Function Documentation

◆ add_equality_constraints() [1/2]

void equalityt::add_equality_constraints ( )
protectedvirtual

Definition at line 89 of file equality.cpp.

◆ add_equality_constraints() [2/2]

void equalityt::add_equality_constraints ( const typestructt typestruct)
protectedvirtual

Definition at line 96 of file equality.cpp.

◆ equality()

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

Definition at line 17 of file equality.cpp.

◆ equality2()

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

Definition at line 25 of file equality.cpp.

◆ post_process()

void equalityt::post_process ( )
inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Definition at line 29 of file equality.h.

Member Data Documentation

◆ typemap

typemapt equalityt::typemap
protected

Definition at line 50 of file equality.h.


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