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

virtual tvt	l_get (literalt l) const =0
	Return value of literal `l` from satisfying assignment.

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

virtual void	push ()=0
	Push a new context on the stack This context becomes a child context nested in the current context.

virtual void	pop ()=0
	Pop whatever is on top of the stack.

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

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

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.

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 exprt	get (const exprt &) const =0
	Return `expr` with variables replaced by values from satisfying assignment if available.

virtual void	print_assignment (std::ostream &out) const =0
	Print satisfying assignment to `out`.

virtual std::string	decision_procedure_text () const =0
	Return a textual description of the decision procedure.

virtual std::size_t	get_number_of_solver_calls () const =0
	Return the number of incremental solver calls.

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.

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