LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/rewrite - with_prover.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 18 0.0 %
Date: 2020-10-20 00:45:57 Functions: 0 5 0.0 %
Legend: Lines: hit not hit

          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 __REWR_PROVER_H
      13             : #define __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 :     }
      38             :     
      39           0 :     virtual ~RewriterProver()
      40           0 :     {}
      41             : 
      42           0 :     rewrite_strategy getStrategy()
      43             :     {
      44           0 :       switch (prover_obj.get_rewriter()->getStrategy())
      45             :       {
      46           0 :         case jitty:
      47           0 :           return jitty_prover;
      48             : #ifdef MCRL2_JITTYC_AVAILABLE
      49           0 :         case jitty_compiling:
      50           0 :           return jitty_compiling_prover;
      51             : #endif
      52           0 :         default:
      53           0 :           throw mcrl2::runtime_error("invalid rewrite strategy");
      54             :       }
      55             :     }
      56             : 
      57             : 
      58           0 :     data_expression rewrite(
      59             :          const data_expression& t,
      60             :          substitution_type& sigma)
      61             :     {
      62             :       // The prover rewriter should also work on terms with other types than Bool. 
      63             :       // Up till 14/5/2020 this was not the case. The old code is left here, to
      64             :       // restore it easily, in case it turns out that the jittyp rewriter cannot
      65             :       // fruitfully be applied on expressions, other than those of type bool. 
      66             :       //
      67             :       // if (mcrl2::data::data_expression(t).sort() == mcrl2::data::sort_bool::bool_())
      68             :       // {
      69           0 :         prover_obj.set_substitution(sigma);
      70           0 :         prover_obj.set_formula(t);
      71           0 :         return prover_obj.get_bdd();
      72             :       // }
      73             :       // else
      74             :       //{
      75             :       //  return prover_obj.get_rewriter()->rewrite(t,sigma);
      76             :       //}
      77             :     }
      78             : 
      79             : 
      80             : };
      81             : 
      82             : }
      83             : }
      84             : }
      85             : 
      86             : #endif

Generated by: LCOV version 1.13