CBMC
prop_convt Class Referenceabstract

#include <prop_conv.h>

+ Inheritance diagram for prop_convt:
+ Collaboration diagram for prop_convt:

Public Member Functions

virtual ~prop_convt ()
 
virtual literalt convert (const exprt &expr)=0
 Convert a Boolean expression and return the corresponding literal. More...
 
virtual tvt l_get (literalt l) const =0
 Return value of literal l from satisfying assignment. More...
 
- Public Member Functions inherited from stack_decision_proceduret
virtual void push (const std::vector< exprt > &assumptions)=0
 Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions. More...
 
virtual void push ()=0
 Push a new context on the stack This context becomes a child context nested in the current context. More...
 
virtual void pop ()=0
 Pop whatever is on top of the stack. More...
 
virtual ~stack_decision_proceduret ()=default
 
- Public Member Functions inherited from decision_proceduret
virtual void set_to (const exprt &, bool value)=0
 For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'. More...
 
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...
 
virtual exprt handle (const exprt &)=0
 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...
 
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 exprt get (const exprt &) const =0
 Return expr with variables replaced by values from satisfying assignment if available. More...
 
virtual void print_assignment (std::ostream &out) const =0
 Print satisfying assignment to out. More...
 
virtual std::string decision_procedure_text () const =0
 Return a textual description of the decision procedure. More...
 
virtual std::size_t get_number_of_solver_calls () const =0
 Return the number of incremental solver calls. More...
 
virtual ~decision_proceduret ()
 

Additional Inherited Members

- Public Types inherited from decision_proceduret
enum class  resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
 Result of running the decision procedure. More...
 
- Protected Member Functions inherited from decision_proceduret
virtual resultt dec_solve (const exprt &assumption)=0
 Implementation of the decision procedure. More...
 

Detailed Description

Definition at line 21 of file prop_conv.h.

Constructor & Destructor Documentation

◆ ~prop_convt()

virtual prop_convt::~prop_convt ( )
inlinevirtual

Definition at line 24 of file prop_conv.h.

Member Function Documentation

◆ convert()

virtual literalt prop_convt::convert ( const exprt expr)
pure virtual

Convert a Boolean expression and return the corresponding literal.

Implemented in prop_conv_solvert.

◆ l_get()

virtual tvt prop_convt::l_get ( literalt  l) const
pure virtual

Return value of literal l from satisfying assignment.

Return tvt::UNKNOWN if not available

Implemented in prop_conv_solvert.


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