#include <solver.h>

Public Member Functions
	smt_solver (const data::data_specification &dataspec)

answer	solve (const data::variable_list &vars, const data::data_expression &expr, const std::chrono::microseconds &timeout=std::chrono::microseconds::zero())

Protected Member Functions
answer	execute_and_check (const std::string &command, const std::chrono::microseconds &timeout) const

Protected Attributes
native_translations	m_native

std::unordered_map< data::data_expression, std::string >	m_cache

child_process	z3

Detailed Description

Definition at line 23 of file solver.h.

Constructor & Destructor Documentation

mcrl2::smt::smt_solver::smt_solver ( const data::data_specification & dataspec )

Definition at line 44 of file solver.cpp.

answer mcrl2::smt::smt_solver::execute_and_check	(	const std::string &	command,
		const std::chrono::microseconds &	timeout
	)		const

protected

Definition at line 21 of file solver.cpp.

answer mcrl2::smt::smt_solver::solve	(	const data::variable_list &	vars,
		const data::data_expression &	expr,
		const std::chrono::microseconds &	timeout = `std::chrono::microseconds::zero()`
	)

Definition at line 53 of file solver.cpp.

std::unordered_map<data::data_expression, std::string> mcrl2::smt::smt_solver::m_cache

protected

Definition at line 27 of file solver.h.

native_translations mcrl2::smt::smt_solver::m_native

protected

Definition at line 26 of file solver.h.

child_process mcrl2::smt::smt_solver::z3

protected

Definition at line 28 of file solver.h.

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