cprover
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  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::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
 
void set_to (const exprt &expr, bool value) override
 For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'. More...
 
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...
 
void set_frozen (literalt a) override
 
void set_assumptions (const bvt &_assumptions) override
 
bool has_set_assumptions () const override
 
void set_all_frozen () override
 
literalt convert (const exprt &expr) override
 Convert a Boolean expression and return the corresponding literal. More...
 
bool is_in_conflict (literalt l) const override
 determine whether a variable is in the final conflict More...
 
bool has_is_in_conflict () const override
 
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...
 
virtual void set_frozen (literalt a)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from prop_convt
virtual ~prop_convt ()
 
exprt handle (const exprt &expr) override
 returns a 'handle', which is an expression that has the same value as the argument in any model that is generated. More...
 
virtual void set_frozen (const bvt &)
 
- 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
 

Public Attributes

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

Protected Member Functions

virtual void post_process ()
 
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

bool post_processing_done = false
 
symbolst symbols
 
cachet cache
 
proptprop
 
messaget log
 

Detailed Description

Definition at line 25 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 90 of file prop_conv_solver.h.

◆ symbolst

Definition at line 89 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 28 of file prop_conv_solver.h.

◆ ~prop_conv_solvert()

virtual prop_conv_solvert::~prop_conv_solvert ( )
virtualdefault

Member Function Documentation

◆ clear_cache()

virtual void prop_conv_solvert::clear_cache ( )
inlinevirtual

Reimplemented in boolbvt.

Definition at line 84 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 122 of file prop_conv_solver.cpp.

◆ convert_bool()

literalt prop_conv_solvert::convert_bool ( const exprt expr)
protectedvirtual

Definition at line 153 of file prop_conv_solver.cpp.

◆ convert_rest()

literalt prop_conv_solvert::convert_rest ( const exprt expr)
protectedvirtual

Reimplemented in boolbvt, and bv_pointerst.

Definition at line 291 of file prop_conv_solver.cpp.

◆ dec_solve()

decision_proceduret::resultt prop_conv_solvert::dec_solve ( )
overridevirtual

Run the decision procedure to solve the problem.

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 425 of file prop_conv_solver.cpp.

◆ decision_procedure_text()

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

Return a textual description of the decision procedure.

Implements decision_proceduret.

Reimplemented in string_refinementt, and bv_refinementt.

Definition at line 39 of file prop_conv_solver.h.

◆ get()

exprt prop_conv_solvert::get ( const exprt expr) 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 450 of file prop_conv_solver.cpp.

◆ get_bool()

optionalt< 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 45 of file prop_conv_solver.cpp.

◆ get_cache()

const cachet& prop_conv_solvert::get_cache ( ) const
inline

Definition at line 92 of file prop_conv_solver.h.

◆ get_literal()

literalt prop_conv_solvert::get_literal ( const irep_idt symbol)
protectedvirtual

Definition at line 28 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 480 of file prop_conv_solver.cpp.

◆ get_symbols()

const symbolst& prop_conv_solvert::get_symbols ( ) const
inline

Definition at line 96 of file prop_conv_solver.h.

◆ has_is_in_conflict()

bool prop_conv_solvert::has_is_in_conflict ( ) const
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 72 of file prop_conv_solver.h.

◆ has_set_assumptions()

bool prop_conv_solvert::has_set_assumptions ( ) const
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 59 of file prop_conv_solver.h.

◆ ignoring()

void prop_conv_solvert::ignoring ( const exprt expr)
protectedvirtual

Definition at line 414 of file prop_conv_solver.cpp.

◆ is_in_conflict()

bool prop_conv_solvert::is_in_conflict ( literalt  l) const
inlineoverridevirtual

determine whether a variable is in the final conflict

Reimplemented from prop_convt.

Definition at line 68 of file prop_conv_solver.h.

◆ 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 47 of file prop_conv_solver.h.

◆ literal()

bool prop_conv_solvert::literal ( const symbol_exprt expr,
literalt literal 
) const

Definition at line 13 of file prop_conv_solver.cpp.

◆ post_process()

void prop_conv_solvert::post_process ( )
protectedvirtual

Reimplemented in boolbvt, arrayst, equalityt, and bv_pointerst.

Definition at line 421 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 474 of file prop_conv_solver.cpp.

◆ set_all_frozen()

void prop_conv_solvert::set_all_frozen ( )
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 63 of file prop_conv_solver.h.

◆ set_assumptions()

void prop_conv_solvert::set_assumptions ( const bvt _assumptions)
inlineoverridevirtual

Reimplemented from prop_convt.

Reimplemented in bv_refinementt.

Definition at line 55 of file prop_conv_solver.h.

◆ set_equality_to_true()

bool prop_conv_solvert::set_equality_to_true ( const equal_exprt expr)
protectedvirtual

Definition at line 298 of file prop_conv_solver.cpp.

◆ set_frozen() [1/3]

void prop_convt::set_frozen

Definition at line 51 of file prop_conv.cpp.

◆ set_frozen() [2/3]

void prop_convt::set_frozen

Definition at line 56 of file prop_conv.cpp.

◆ set_frozen() [3/3]

void prop_conv_solvert::set_frozen ( literalt  a)
inlineoverridevirtual

Reimplemented from prop_convt.

Definition at line 51 of file prop_conv_solver.h.

◆ 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 101 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 'expr' if value is true, otherwise add 'not expr'.

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 324 of file prop_conv_solver.cpp.

Member Data Documentation

◆ cache

cachet prop_conv_solvert::cache
protected

Definition at line 129 of file prop_conv_solver.h.

◆ equality_propagation

bool prop_conv_solvert::equality_propagation = true

Definition at line 81 of file prop_conv_solver.h.

◆ freeze_all

bool prop_conv_solvert::freeze_all = false

Definition at line 82 of file prop_conv_solver.h.

◆ log

messaget prop_conv_solvert::log
protected

Definition at line 136 of file prop_conv_solver.h.

◆ post_processing_done

bool prop_conv_solvert::post_processing_done = false
protected

Definition at line 111 of file prop_conv_solver.h.

◆ prop

propt& prop_conv_solvert::prop
protected

Definition at line 134 of file prop_conv_solver.h.

◆ symbols

symbolst prop_conv_solvert::symbols
protected

Definition at line 124 of file prop_conv_solver.h.

◆ use_cache

bool prop_conv_solvert::use_cache = true

Definition at line 80 of file prop_conv_solver.h.


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