Line data    Source code

       1             : // Author(s): Muck van Weerdenburg
       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/detail/rewrite/with_prover.h
      10             : /// \brief Rewriting combined with semantic simplification using a prover
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_REWR_PROVER_H
      13             : #define MCRL2_DATA_DETAIL_REWR_PROVER_H
      14             : 
      15             : #include "mcrl2/data/detail/prover/bdd_prover.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace data
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : class RewriterProver: public Rewriter
      25             : {
      26             :   public:
      27             :     BDD_Prover prover_obj;
      28             : 
      29             :     typedef Rewriter::substitution_type substitution_type;
      30             : 
      31             :   public:
      32           0 :     RewriterProver(const data_specification& data_spec, mcrl2::data::rewriter::strategy strat, 
      33             :                    const used_data_equation_selector& equations_selector)
      34           0 :       : Rewriter(data_spec, equations_selector),
      35           0 :         prover_obj(data_spec, equations_selector, strat)
      36             :     {
      37           0 :       thread_initialise();
      38           0 :     }
      39             :     
      40           0 :     virtual ~RewriterProver()
      41           0 :     {}
      42             : 
      43           0 :     rewrite_strategy getStrategy()
      44             :     {
      45           0 :       switch (prover_obj.rewriter_strategy())
      46             :       {
      47           0 :         case jitty:
      48           0 :           return jitty_prover;
      49             : #ifdef MCRL2_ENABLE_JITTYC
      50           0 :         case jitty_compiling:
      51           0 :           return jitty_compiling_prover;
      52             : #endif
      53           0 :         default:
      54           0 :           throw mcrl2::runtime_error("invalid rewrite strategy");
      55             :       }
      56             :     }
      57             : 
      58           0 :     void rewrite(
      59             :          data_expression& result,
      60             :          const data_expression& t,
      61             :          substitution_type& sigma)
      62             :     {
      63             :       // The prover rewriter should also work on terms with other types than Bool. 
      64             :       // Up till 14/5/2020 this was not the case. The old code is left here, to
      65             :       // restore it easily, in case it turns out that the jittyp rewriter cannot
      66             :       // fruitfully be applied on expressions, other than those of type bool. 
      67             :       //
      68             :       // if (mcrl2::data::data_expression(t).sort() == mcrl2::data::sort_bool::bool_())
      69             :       // {
      70           0 :         prover_obj.set_substitution(sigma);
      71           0 :         prover_obj.set_formula(t);
      72           0 :         result=prover_obj.get_bdd();
      73           0 :         return;
      74             :       // }
      75             :       // else
      76             :       //{
      77             :       //  return prover_obj.get_rewriter()->rewrite(t,sigma);
      78             :       //}
      79             :     }
      80             : 
      81           0 :     data_expression rewrite(
      82             :          const data_expression& t,
      83             :          substitution_type& sigma)
      84             :     {
      85           0 :       data_expression result;
      86           0 :       rewrite(result,t,sigma);
      87           0 :       return result;
      88           0 :     }
      89             : 
      90           0 :     void thread_initialise() 
      91             :     {
      92           0 :       Rewriter::thread_initialise();
      93           0 :       prover_obj.thread_initialise();
      94           0 :     }
      95             : 
      96             :   protected:
      97             : 
      98             :     // Protected copy constructor.
      99             :     RewriterProver(const RewriterProver& other) = delete;
     100             : 
     101             :     // Copy constructor intended for cloning. 
     102           0 :     RewriterProver(const RewriterProver& rewr, 
     103             :                    BDD_Prover prover_obj_)
     104           0 :       : Rewriter(rewr),
     105           0 :         prover_obj(prover_obj_)
     106             :     {
     107           0 :       thread_initialise();
     108           0 :     }
     109             :     
     110           0 :     std::shared_ptr<Rewriter> clone()
     111             :     {
     112           0 :       return std::shared_ptr<Rewriter>(new RewriterProver(*this,prover_obj.clone()));
     113             :     }
     114             : };
     115             : 
     116             : }
     117             : }
     118             : }
     119             : 
     120             : #endif