Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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 mcrl2/data/rewriter_tool.h
      10             : /// \brief Base class for tools that use a data rewriter.
      11             : 
      12             : #ifndef MCRL2_DATA_REWRITER_TOOL_H
      13             : #define MCRL2_DATA_REWRITER_TOOL_H
      14             : 
      15             : #include "mcrl2/data/detail/enumerator_iteration_limit.h"
      16             : #include "mcrl2/data/rewriter.h"
      17             : #include "mcrl2/utilities/command_line_interface.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace data
      23             : {
      24             : 
      25             : namespace tools
      26             : {
      27             : 
      28             : /// \brief Base class for tools that use a rewriter.
      29             : template <typename Tool>
      30             : class rewriter_tool: public Tool
      31             : {
      32             :   protected:
      33             :     /// The data rewriter strategy
      34             :     data::rewrite_strategy m_rewrite_strategy;
      35             : 
      36             :     /// \brief Add options to an interface description. Also includes
      37             :     /// rewriter options.
      38             :     /// \param desc An interface description.
      39             :     /// \param suppress_jittyp Boolean that if true will prevent showing that jittyp is an option for rewriting. 
      40           0 :     void add_options(utilities::interface_description& desc, bool suppress_jittyp)
      41             :     {
      42           0 :       Tool::add_options(desc);
      43             : 
      44           0 :       utilities::interface_description::enum_argument<data::rewrite_strategy> rewriter_option("NAME");
      45           0 :       rewriter_option.add_value(data::jitty, true);
      46             : #ifdef MCRL2_ENABLE_JITTYC
      47           0 :       rewriter_option.add_value(data::jitty_compiling);
      48             : #endif
      49           0 :       if (!suppress_jittyp)
      50             :       {
      51           0 :         rewriter_option.add_value(data::jitty_prover);
      52             :       }
      53             : 
      54           0 :       desc.add_option(
      55             :         "rewriter", 
      56             :         rewriter_option,
      57             :         "use rewrite strategy NAME:"
      58             :         ,'r'
      59             :       );
      60             : 
      61           0 :       desc.add_option(
      62             :         "qlimit", 
      63             :         utilities::make_mandatory_argument("NUM"),
      64             :         "limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).",
      65             :         'Q'
      66             :       );
      67             : 
      68           0 :     }
      69             : 
      70             :     /// \brief Add options to an interface description. Also includes
      71             :     /// rewriter options.
      72             :     /// \param desc An interface description
      73           0 :     void add_options(utilities::interface_description& desc)
      74             :     {
      75           0 :       add_options(desc,false);
      76           0 :     }
      77             : 
      78             : 
      79             :     /// \brief Parse non-standard options
      80             :     /// \param parser A command line parser
      81           0 :     void parse_options(const utilities::command_line_parser& parser)
      82             :     {
      83           0 :       Tool::parse_options(parser);
      84           0 :       m_rewrite_strategy = parser.option_argument_as< data::rewrite_strategy >("rewriter");
      85             : 
      86           0 :       if(parser.options.count("qlimit"))
      87             :       {
      88             :         //Set enumerator limit for quantifier enumeration
      89           0 :         std::size_t qlimit = parser.option_argument_as< std::size_t >("qlimit");
      90           0 :         data::detail::set_enumerator_iteration_limit(qlimit == 0 ? std::numeric_limits<std::size_t>::max() : qlimit);
      91             :       }
      92           0 :     }
      93             : 
      94             :   public:
      95             : 
      96             :     /// \brief Constructor.
      97           0 :     rewriter_tool(const std::string& name,
      98             :                   const std::string& author,
      99             :                   const std::string& what_is,
     100             :                   const std::string& tool_description,
     101             :                   std::string known_issues = ""
     102             :                  )
     103             :       : Tool(name, author, what_is, tool_description, known_issues),
     104           0 :         m_rewrite_strategy(mcrl2::data::jitty)
     105           0 :     {}
     106             : 
     107             :     /// \brief Returns the rewrite strategy
     108             :     /// \return The rewrite strategy
     109           0 :     data::rewrite_strategy rewrite_strategy() const
     110             :     {
     111           0 :       return m_rewrite_strategy;
     112             :     }
     113             : 
     114             :     /// \brief Creates a data rewriter as specified on the command line.
     115             :     /// \param data_spec A data specification
     116             :     /// \return A data rewriter
     117             :     data::rewriter create_rewriter(const data::data_specification& data_spec = data::data_specification())
     118             :     {
     119             :       return data::rewriter(data_spec, rewrite_strategy());
     120             :     }
     121             : };
     122             : 
     123             : } // namespace tools
     124             : 
     125             : } // namespace data
     126             : 
     127             : } // namespace mcrl2
     128             : 
     129             : #endif // MCRL2_DATA_REWRITER_TOOL_H