Line data Source code
1 : // Author(s): Ruud Koolen, Thomas Neele 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file solver.h 10 : 11 : #ifndef MCRL2_SMT_SOLVER_H 12 : #define MCRL2_SMT_SOLVER_H 13 : 14 : #include "mcrl2/smt/child_process.h" 15 : #include "mcrl2/smt/native_translation.h" 16 : #include "mcrl2/smt/answer.h" 17 : 18 : namespace mcrl2 19 : { 20 : namespace smt 21 : { 22 : 23 : class smt_solver 24 : { 25 : protected: 26 : native_translations m_native; 27 : std::unordered_map<data::data_expression, std::string> m_cache; 28 : child_process z3; 29 : 30 : protected: 31 : 32 : answer execute_and_check(const std::string& command, const std::chrono::microseconds& timeout) const; 33 : 34 : public: 35 : smt_solver(const data::data_specification& dataspec); 36 : 37 0 : answer solve(const data::variable_list& vars, const data::data_expression& expr, const std::chrono::microseconds& timeout = std::chrono::microseconds::zero()); 38 : }; 39 : 40 : } // namespace smt 41 : } // namespace mcrl2 42 : 43 : #endif // MCRL2_SMT_SOLVER_H