CBMC
Public Types | Public Member Functions | Protected Member Functions | List of all members
decision_proceduret Class Referenceabstract

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

Protected Member Functions

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

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 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 string_refinementt, smt2_incremental_decision_proceduret, smt2_dect, smt2_convt, bv_refinementt, and prop_conv_solvert.

◆ decision_procedure_text()

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

Return a textual description of the decision procedure.

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

◆ 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 string_refinementt, smt2_incremental_decision_proceduret, smt2_convt, prop_conv_solvert, and boolbvt.

◆ 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 smt2_incremental_decision_proceduret, smt2_convt, and prop_conv_solvert.

◆ 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 smt2_incremental_decision_proceduret, smt2_convt, prop_conv_solvert, and boolbvt.

◆ operator()() [1/2]

decision_proceduret::resultt decision_proceduret::operator() ( void  )

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 smt2_incremental_decision_proceduret, smt2_convt, prop_conv_solvert, and boolbvt.

◆ 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 string_refinementt, smt2_incremental_decision_proceduret, smt2_convt, prop_conv_solvert, and boolbvt.

◆ 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: