decision_proceduret Class Reference

An interface for a decision procedure for satisfiability problems. More...

#include <decision_procedure.h>

Inheritance diagram for decision_proceduret:

Public Types
enum class	resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
	Result of running the decision procedure. More...

Public Member Functions
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 ()

Protected Member Functions
virtual resultt	dec_solve (const exprt &assumption)=0
	Implementation of the decision procedure.

Detailed Description

An interface for a decision procedure for satisfiability problems.

Definition at line 21 of file decision_procedure.h.

Member Enumeration Documentation

resultt

enum class decision_proceduret::resultt

strong

Result of running the decision procedure.

Enumerator
D_SATISFIABLE
D_UNSATISFIABLE
D_ERROR

Definition at line 44 of file decision_procedure.h.

Constructor & Destructor Documentation

~decision_proceduret()

decision_proceduret::~decision_proceduret ( )

virtual

Definition at line 16 of file decision_procedure.cpp.

Member Function Documentation

dec_solve()

virtual resultt decision_proceduret::dec_solve ( const exprt &  assumption )

protectedpure virtual

Implementation of the decision procedure.

Implemented in prop_conv_solvert, bv_refinementt, smt2_convt, smt2_dect, smt2_incremental_decision_proceduret, and string_refinementt.

decision_procedure_text()

virtual std::string decision_proceduret::decision_procedure_text ( ) const

pure virtual

Return a textual description of the decision procedure.

Implemented in prop_conv_solvert, bv_refinementt, smt2_convt, smt2_dect, smt2_incremental_decision_proceduret, and string_refinementt.

get()

virtual exprt decision_proceduret::get ( const exprt &  ) const

pure virtual

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

Return nil if not available

Implemented in boolbvt, prop_conv_solvert, smt2_convt, smt2_incremental_decision_proceduret, and string_refinementt.

get_number_of_solver_calls()

virtual std::size_t decision_proceduret::get_number_of_solver_calls ( ) const

pure virtual

Return the number of incremental solver calls.

Implemented in prop_conv_solvert, smt2_convt, and smt2_incremental_decision_proceduret.

handle()

virtual exprt decision_proceduret::handle ( const exprt &  )

pure virtual

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.

Implemented in boolbvt, prop_conv_solvert, smt2_convt, and smt2_incremental_decision_proceduret.

operator()() [1/2]

decision_proceduret::resultt decision_proceduret::operator()

(

)

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

Definition at line 20 of file decision_procedure.cpp.

operator()() [2/2]

decision_proceduret::resultt decision_proceduret::operator()

(

const exprt &

assumption

)

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

This corresponds to SMT-LIB's check-sat-assuming.

Definition at line 26 of file decision_procedure.cpp.

print_assignment()

virtual void decision_proceduret::print_assignment ( std::ostream &  out ) const

pure virtual

Print satisfying assignment to out.

Implemented in boolbvt, prop_conv_solvert, smt2_convt, and smt2_incremental_decision_proceduret.

set_to()

virtual void decision_proceduret::set_to ( const exprt &  , bool  value  )

pure virtual

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

Implemented in boolbvt, prop_conv_solvert, smt2_convt, smt2_incremental_decision_proceduret, and string_refinementt.

set_to_false()

void decision_proceduret::set_to_false

(

const exprt &

expr

)

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

Definition at line 36 of file decision_procedure.cpp.

set_to_true()

void decision_proceduret::set_to_true

(

const exprt &

expr

)

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

Definition at line 31 of file decision_procedure.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/decision_procedure.h
• /home/runner/work/cbmc/cbmc/src/solvers/decision_procedure.cpp