mcrl2::data::detail::SMT_Solver Class Reference

#include <smt_solver.h>

Inheritance diagram for mcrl2::data::detail::SMT_Solver:

Public Member Functions
virtual	~SMT_Solver ()=default
virtual bool	is_satisfiable (const data_expression_list &a_formula)=0

Detailed Description

Definition at line 20 of file smt_solver.h.

Constructor & Destructor Documentation

~SMT_Solver()

virtual mcrl2::data::detail::SMT_Solver::~SMT_Solver ( )

virtualdefault

Member Function Documentation

is_satisfiable()

virtual bool mcrl2::data::detail::SMT_Solver::is_satisfiable ( const data_expression_list &  a_formula )

pure virtual

Implemented in mcrl2::data::detail::prover::cvc_smt_solver, mcrl2::data::detail::prover::z3_smt_solver, and mcrl2::data::detail::prover::ario_smt_solver.

---

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

• data/include/mcrl2/data/detail/prover/smt_solver.h