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.

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.

bool is_in_conflict (const exprt &expr) const override

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

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

void push () override

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

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

Push assumptions in form of literal_exprt

void pop () override

Pop whatever is on top of the stack.

virtual void clear_cache ()

const cachet & get_cache () const

const symbolst & get_symbols () const

void set_time_limit_seconds (uint32_t lim) override

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

std::size_t get_number_of_solver_calls () const override

Return the number of incremental solver calls.

hardness_collectort * get_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'.

void set_to_false (const exprt &)

For a Boolean expression expr, add the constraint 'not expr'.

resultt operator() ()

Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt operator() (const exprt &assumption)

Run the decision procedure to solve the problem under the given assumption.

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.

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

propt & prop

messaget log

bvt assumption_stack

Assumptions on the stack.

std::size_t context_literal_counter = 0

To generate unique literal names for contexts.

std::vector< size_t > context_size_stack

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

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.

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

typedef std::map<irep_idt, literalt> prop_conv_solvert::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 347 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 bv_pointers_widet, bv_pointerst, and boolbvt.

Definition at line 314 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.

Definition at line 444 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.

Definition at line 586 of file prop_conv_solver.cpp.

◆ finish_eager_conversion()

void prop_conv_solvert::finish_eager_conversion ( )

virtual

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

Definition at line 439 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 498 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 528 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 432 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 574 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 522 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 564 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 550 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 321 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 535 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:

/home/runner/work/cbmc/cbmc/src/solvers/prop/prop_conv_solver.h
/home/runner/work/cbmc/cbmc/src/solvers/prop/prop_conv_solver.cpp