CBMC
prop_conv_solvert Class Reference

#include <prop_conv_solver.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 class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...
 

Public Member Functions

 prop_conv_solvert (propt &_prop, message_handlert &message_handler)
 
virtual ~prop_conv_solvert ()=default
 
virtual void finish_eager_conversion ()
 
decision_proceduret::resultt dec_solve (const exprt &) override
 Implementation of the decision procedure. 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...
 
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...
 
hardness_collectortget_hardness_collector ()
 
- 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 &)
 For a Boolean expression expr, add the constraint 'expr'. More...
 
void set_to_false (const exprt &)
 For a Boolean expression expr, add the constraint 'not expr'. More...
 
resultt operator() ()
 Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat. More...
 
resultt operator() (const exprt &assumption)
 Run the decision procedure to solve the problem under the given assumption. More...
 
virtual ~decision_proceduret ()
 
- Public Member Functions inherited from solver_resource_limitst
virtual ~solver_resource_limitst ()=default
 

Public Attributes

bool use_cache = true
 
bool equality_propagation = true
 
bool freeze_all = false
 

Protected Member Functions

virtual std::optional< 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

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

Static Protected Attributes

static const char * context_prefix = "prop_conv::context$"
 

Private Member Functions

void add_constraints_to_prop (const exprt &expr, bool value)
 Helper method used by set_to for adding the constraints to prop. More...
 

Detailed Description

Definition at line 27 of file prop_conv_solver.h.

Member Typedef Documentation

◆ cachet

typedef std::unordered_map<exprt, literalt, irep_hash> prop_conv_solvert::cachet

Definition at line 84 of file prop_conv_solver.h.

◆ symbolst

Definition at line 83 of file prop_conv_solver.h.

Constructor & Destructor Documentation

◆ prop_conv_solvert()

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

Definition at line 32 of file prop_conv_solver.h.

◆ ~prop_conv_solvert()

virtual prop_conv_solvert::~prop_conv_solvert ( )
virtualdefault

Member Function Documentation

◆ add_constraints_to_prop()

void prop_conv_solvert::add_constraints_to_prop ( const exprt expr,
bool  value 
)
private

Helper method used by set_to for adding the constraints to prop.

This method is private because it must not be used by derived classes.

Definition at line 346 of file prop_conv_solver.cpp.

◆ clear_cache()

virtual void prop_conv_solvert::clear_cache ( )
inlinevirtual

Reimplemented in boolbvt.

Definition at line 78 of file prop_conv_solver.h.

◆ convert()

literalt prop_conv_solvert::convert ( const exprt expr)
overridevirtual

Convert a Boolean expression and return the corresponding literal.

Implements prop_convt.

Definition at line 154 of file prop_conv_solver.cpp.

◆ convert_bool()

literalt prop_conv_solvert::convert_bool ( const exprt expr)
protectedvirtual

Definition at line 190 of file prop_conv_solver.cpp.

◆ convert_rest()

literalt prop_conv_solvert::convert_rest ( const exprt expr)
protectedvirtual

Reimplemented in boolbvt, bv_pointerst, and bv_pointers_widet.

Definition at line 313 of file prop_conv_solver.cpp.

◆ dec_solve()

decision_proceduret::resultt prop_conv_solvert::dec_solve ( const exprt assumption)
overridevirtual

Implementation of the decision procedure.

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 443 of file prop_conv_solver.cpp.

◆ decision_procedure_text()

std::string prop_conv_solvert::decision_procedure_text ( ) const
overridevirtual

Return a textual description of the decision procedure.

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 573 of file prop_conv_solver.cpp.

◆ finish_eager_conversion()

void prop_conv_solvert::finish_eager_conversion ( )
virtual

Reimplemented in equalityt, bv_pointerst, boolbvt, arrayst, and bv_pointers_widet.

Definition at line 438 of file prop_conv_solver.cpp.

◆ get()

exprt prop_conv_solvert::get ( const exprt ) const
overridevirtual

Return expr with variables replaced by values from satisfying assignment if available.

Return nil if not available

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 485 of file prop_conv_solver.cpp.

◆ get_bool()

std::optional< bool > prop_conv_solvert::get_bool ( const exprt expr) const
protectedvirtual

Get a boolean value from the model if the formula is satisfiable.

If the argument is not a boolean expression from the formula, {} is returned.

Definition at line 77 of file prop_conv_solver.cpp.

◆ get_cache()

const cachet& prop_conv_solvert::get_cache ( ) const
inline

Definition at line 86 of file prop_conv_solver.h.

◆ get_hardness_collector()

hardness_collectort* prop_conv_solvert::get_hardness_collector ( )
inline

Definition at line 102 of file prop_conv_solver.h.

◆ get_literal()

literalt prop_conv_solvert::get_literal ( const irep_idt symbol)
protectedvirtual

Definition at line 60 of file prop_conv_solver.cpp.

◆ get_number_of_solver_calls()

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

Return the number of incremental solver calls.

Implements decision_proceduret.

Definition at line 515 of file prop_conv_solver.cpp.

◆ get_symbols()

const symbolst& prop_conv_solvert::get_symbols ( ) const
inline

Definition at line 90 of file prop_conv_solver.h.

◆ handle()

exprt prop_conv_solvert::handle ( const exprt )
overridevirtual

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.

The returned expression may be the expression itself or a more compact but solver-specific representation.

Implements decision_proceduret.

Definition at line 38 of file prop_conv_solver.cpp.

◆ ignoring()

void prop_conv_solvert::ignoring ( const exprt expr)
protectedvirtual

Definition at line 431 of file prop_conv_solver.cpp.

◆ is_in_conflict()

bool prop_conv_solvert::is_in_conflict ( const exprt ) const
overridevirtual

Returns true if an expression is in the final conflict leading to UNSAT.

The argument can be a Boolean expression or something more solver-specific, e.g. a literal_exprt.

Implements conflict_providert.

Definition at line 16 of file prop_conv_solver.cpp.

◆ l_get()

tvt prop_conv_solvert::l_get ( literalt  l) const
inlineoverridevirtual

Return value of literal l from satisfying assignment.

Return tvt::UNKNOWN if not available

Implements prop_convt.

Definition at line 48 of file prop_conv_solver.h.

◆ pop()

void prop_conv_solvert::pop ( )
overridevirtual

Pop whatever is on top of the stack.

Popping from the empty stack results in an invariant violation.

Implements stack_decision_proceduret.

Definition at line 561 of file prop_conv_solver.cpp.

◆ print_assignment()

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

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 509 of file prop_conv_solver.cpp.

◆ push() [1/2]

void prop_conv_solvert::push ( )
overridevirtual

Push a new context on the stack This context becomes a child context nested in the current context.

Implements stack_decision_proceduret.

Definition at line 551 of file prop_conv_solver.cpp.

◆ push() [2/2]

void prop_conv_solvert::push ( const std::vector< exprt > &  assumptions)
overridevirtual

Push assumptions in form of literal_exprt

Implements stack_decision_proceduret.

Definition at line 537 of file prop_conv_solver.cpp.

◆ set_all_frozen()

void prop_conv_solvert::set_all_frozen ( )

Definition at line 33 of file prop_conv_solver.cpp.

◆ set_equality_to_true()

bool prop_conv_solvert::set_equality_to_true ( const equal_exprt expr)
protectedvirtual

Definition at line 320 of file prop_conv_solver.cpp.

◆ set_frozen() [1/2]

void prop_conv_solvert::set_frozen ( const bvt bv)

Definition at line 21 of file prop_conv_solver.cpp.

◆ set_frozen() [2/2]

void prop_conv_solvert::set_frozen ( literalt  a)

Definition at line 28 of file prop_conv_solver.cpp.

◆ set_time_limit_seconds()

void prop_conv_solvert::set_time_limit_seconds ( uint32_t  )
inlineoverridevirtual

Set the limit for the solver to time out in seconds.

Implements solver_resource_limitst.

Definition at line 95 of file prop_conv_solver.h.

◆ set_to()

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

For a Boolean expression expr, add the constraint 'current_context => expr' if value is true, otherwise add 'current_context => not expr'.

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 522 of file prop_conv_solver.cpp.

Member Data Documentation

◆ assumption_stack

bvt prop_conv_solvert::assumption_stack
protected

Assumptions on the stack.

Definition at line 137 of file prop_conv_solver.h.

◆ cache

cachet prop_conv_solvert::cache
protected

Definition at line 126 of file prop_conv_solver.h.

◆ context_literal_counter

std::size_t prop_conv_solvert::context_literal_counter = 0
protected

To generate unique literal names for contexts.

Definition at line 140 of file prop_conv_solver.h.

◆ context_prefix

const char * prop_conv_solvert::context_prefix = "prop_conv::context$"
staticprotected

Definition at line 134 of file prop_conv_solver.h.

◆ context_size_stack

std::vector<size_t> prop_conv_solvert::context_size_stack
protected

assumption_stack is segmented in contexts; Number of assumptions in each context on the stack

Definition at line 144 of file prop_conv_solver.h.

◆ equality_propagation

bool prop_conv_solvert::equality_propagation = true

Definition at line 75 of file prop_conv_solver.h.

◆ freeze_all

bool prop_conv_solvert::freeze_all = false

Definition at line 76 of file prop_conv_solver.h.

◆ log

messaget prop_conv_solvert::log
protected

Definition at line 132 of file prop_conv_solver.h.

◆ post_processing_done

bool prop_conv_solvert::post_processing_done = false
protected

Definition at line 108 of file prop_conv_solver.h.

◆ prop

propt& prop_conv_solvert::prop
protected

Definition at line 130 of file prop_conv_solver.h.

◆ symbols

symbolst prop_conv_solvert::symbols
protected

Definition at line 121 of file prop_conv_solver.h.

◆ use_cache

bool prop_conv_solvert::use_cache = true

Definition at line 74 of file prop_conv_solver.h.


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