Line data    Source code

       1             : // Author(s): Luc Engelen
       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/prover/bdd_path_eliminator.h
      10             : /// \brief BDD inconsistent path elimination using external SMT solvers
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_PROVER_BDD_PATH_ELIMINATOR_H
      13             : #define MCRL2_DATA_DETAIL_PROVER_BDD_PATH_ELIMINATOR_H
      14             : 
      15             : #include "mcrl2/data/detail/prover/bdd_info.h"
      16             : #include "mcrl2/data/detail/prover/bdd_simplifier.h"
      17             : #include "mcrl2/data/detail/prover/manipulator.h"
      18             : #include "mcrl2/data/detail/prover/smt_lib_solver.h"
      19             : #include "mcrl2/data/detail/prover/solver_type.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : namespace data
      24             : {
      25             : namespace detail
      26             : {
      27             : 
      28             : /** \brief Base class for eliminating inconsistent paths from BDDs.
      29             :  *
      30             :  * \detail
      31             :  * The class BDD_Path_Eliminator is a base class for classes that
      32             :  * eliminate inconsistent paths from BDDs. The class
      33             :  * BDD_Path_Eliminator inherits from the class BDD_Simplifier. It uses
      34             :  * an SMT solver to eliminate inconsistent paths from BDDs. The
      35             :  * parameter a_solver_type of the constructor
      36             :  * BDD_Path_Eliminator::BDD_Path_Eliminator is used to indicate which
      37             :  * SMT solver should be used for this task. A path in a BDD is
      38             :  * constructed by selecting a set of guards as follows: starting at
      39             :  * the root node, one of the two edges at each guard is followed until
      40             :  * a leaf is reached. Each time the true-edge is chosen, the guard is
      41             :  * added to the set. Each time the false-edge is chosen, the negation
      42             :  * of the guard is added to the set. If the conjunction of all
      43             :  * elements in this set is a contradiction, the path
      44             :  * is inconsistent.
      45             : 
      46             :  * The method BDD_Path_Eliminator::simplify receives a BDD as
      47             :  * parameter a_bdd and returns the equivalent BDD from which all
      48             :  * inconsistent paths have been removed.
      49             : */
      50             : class BDD_Path_Eliminator: public BDD_Simplifier
      51             : {
      52             : 
      53             :   private:
      54             : 
      55             :     /// \brief Pointer to an SMT solver used to determine whether or not a path is inconsistent.
      56             :     SMT_Solver* f_smt_solver;
      57             : 
      58             :     /// \brief Class that provides information about the structure of BDDs.
      59             :     BDD_Info f_bdd_info;
      60             : 
      61             :     /// \brief Returns a list representing the conjunction of all guards in a_path and the guard a_guard.
      62             :     /// \param a_path A list of guards and negated guards, representing a path in a BDD.
      63             :     /// \param a_guard A guard or a negated guard.
      64             :     /// \param a_minimal A boolean value indicating whether or not minimal sets of possibly inconsistent guards are constructed.
      65           0 :     data_expression_list create_condition(
      66             :                data_expression_list a_path,
      67             :                const data_expression& a_guard,
      68             :                bool a_minimal)
      69             :     {
      70           0 :       if (!a_minimal)
      71             :       {
      72           0 :         a_path.push_front(a_guard);
      73           0 :         return a_path;
      74             :       }
      75             :       else
      76             :       {
      77           0 :         data_expression_list v_auxiliary_set;
      78           0 :         data_expression_list v_iterate_over_set;
      79           0 :         data_expression_list v_iterate_over_path;
      80           0 :         data_expression v_guard_from_set;
      81           0 :         data_expression v_guard_from_path;
      82             : 
      83           0 :         data_expression_list v_set = { a_guard };
      84           0 :         while (v_set != v_auxiliary_set)
      85             :         {
      86           0 :           v_auxiliary_set = v_set;
      87           0 :           v_iterate_over_set = v_set;
      88           0 :           while (!v_iterate_over_set.empty())
      89             :           {
      90           0 :             v_guard_from_set = v_iterate_over_set.front();
      91           0 :             v_iterate_over_set.pop_front();
      92           0 :             v_iterate_over_path = a_path;
      93           0 :             while (!v_iterate_over_path.empty())
      94             :             {
      95           0 :               v_guard_from_path = v_iterate_over_path.front();
      96           0 :               v_iterate_over_path.pop_front();
      97           0 :               if (variables_overlap(v_guard_from_set, v_guard_from_path))
      98             :               {
      99           0 :                 v_set.push_front(v_guard_from_path);
     100           0 :                 a_path = remove_one_element(a_path, v_guard_from_path);
     101             :               }
     102             :             }
     103             :           }
     104             :         }
     105           0 :         return v_set;
     106           0 :       }
     107             :     }
     108             : 
     109             :     /// \brief Simplifies the BDD a_bdd using path a_path. Paths whose guards in conjunction with the guards in
     110             :     /// \brief a_path are inconsistent are removed.
     111             :     /// \param a_bdd A binary decision diagram.
     112             :     /// \param a_path A list of guards and negated guards, representing a path in a BDD.
     113           0 :     data_expression aux_simplify(
     114             :                         const data_expression& a_bdd,
     115             :                         const data_expression_list& a_path)
     116             :     {
     117           0 :       if (f_deadline != 0 && (f_deadline - time(nullptr)) < 0)
     118             :       {
     119           0 :         mCRL2log(log::debug) << "The time limit has passed." << std::endl;
     120           0 :         return a_bdd;
     121             :       }
     122             : 
     123           0 :       if (f_bdd_info.is_true(a_bdd) || f_bdd_info.is_false(a_bdd))
     124             :       {
     125           0 :         return a_bdd;
     126             :       }
     127             : 
     128           0 :       const data_expression v_guard = f_bdd_info.get_guard(a_bdd);
     129           0 :       const data_expression v_negated_guard = sort_bool::not_(v_guard);
     130           0 :       const data_expression_list v_true_condition = create_condition(a_path, v_guard, true);
     131           0 :       bool v_true_branch_enabled = f_smt_solver->is_satisfiable(v_true_condition);
     132           0 :       if (!v_true_branch_enabled)
     133             :       {
     134           0 :         data_expression_list v_false_path=a_path;
     135           0 :         v_false_path.push_front(v_negated_guard);
     136           0 :         return aux_simplify(f_bdd_info.get_false_branch(a_bdd), v_false_path);
     137           0 :       }
     138             :       else
     139             :       {
     140           0 :         data_expression_list v_false_condition = create_condition(a_path, v_negated_guard, true);
     141           0 :         bool v_false_branch_enabled = f_smt_solver->is_satisfiable(v_false_condition);
     142           0 :         if (!v_false_branch_enabled)
     143             :         {
     144           0 :           data_expression_list v_true_path = a_path;
     145           0 :           v_true_path.push_front(v_guard);
     146           0 :           return aux_simplify(f_bdd_info.get_true_branch(a_bdd), v_true_path);
     147           0 :         }
     148             :         else
     149             :         {
     150           0 :           data_expression_list v_true_path = a_path;
     151           0 :           v_true_path.push_front(v_guard);
     152           0 :           data_expression_list v_false_path = a_path;
     153           0 :           v_false_path.push_front(v_negated_guard);
     154             :           return Manipulator::make_reduced_if_then_else(
     155             :                    v_guard,
     156           0 :                    aux_simplify(f_bdd_info.get_true_branch(a_bdd), v_true_path),
     157           0 :                    aux_simplify(f_bdd_info.get_false_branch(a_bdd), v_false_path)
     158           0 :                  );
     159           0 :         }
     160           0 :       }
     161           0 :     }
     162             : 
     163             :     /// \brief Returns true if the expression a_expression_1 has variables in common with expression a_expression_2.
     164             :     /// \param a_expression_1 An arbitrary expression.
     165             :     /// \param a_expression_2 An arbitrary expression.
     166           0 :     bool variables_overlap(
     167             :                     const data_expression& a_expression_1,
     168             :                     const data_expression& a_expression_2)
     169             :     {
     170           0 :       std::set < variable > set1=find_all_variables(a_expression_1);
     171           0 :       std::set < variable > set2=find_all_variables(a_expression_2);
     172           0 :       std::set < variable > intersection;
     173           0 :       std::set_intersection(set1.begin(),set1.end(),
     174             :                             set2.begin(),set2.end(),
     175             :                             std::insert_iterator<std::set < variable > >(intersection,intersection.begin()));
     176           0 :       return !intersection.empty();
     177           0 :     }
     178             : 
     179             :   public:
     180             : 
     181             :     /// \brief Constructor that initializes the field BDD_Path_Eliminator::f_smt_solver.
     182             :     /// \param a_solver_type A value of an enumerated type, representing an SMT solver.
     183           0 :     BDD_Path_Eliminator(smt_solver_type a_solver_type)
     184           0 :     {
     185             : #if !(defined(_MSC_VER) || defined(__MINGW32__) || defined(__CYGWIN__))
     186           0 :       if (a_solver_type == solver_type_cvc)
     187             :       {
     188           0 :         if (mcrl2::data::detail::prover::cvc_smt_solver::usable())
     189             :         {
     190           0 :           f_smt_solver = new mcrl2::data::detail::prover::cvc_smt_solver();
     191             : 
     192           0 :           return;
     193             :         }
     194             :       }
     195           0 :       else if (a_solver_type == solver_type_z3)
     196             :       {
     197           0 :         if (mcrl2::data::detail::prover::z3_smt_solver::usable())
     198             :         {
     199           0 :           f_smt_solver = new mcrl2::data::detail::prover::z3_smt_solver();
     200             : 
     201           0 :           return;
     202             :         }
     203             :       }
     204             :       else
     205             :       {
     206           0 :         throw mcrl2::runtime_error("An unknown SMT solver type was passed as argument.");
     207             :       }
     208             : #else
     209             :       throw mcrl2::runtime_error("No SMT solvers available on this platform.");
     210             : #endif // _MSC_VER
     211           0 :     }
     212             : 
     213             :     /// \brief Returns a BDD without inconsistent paths, equivalent to a_bdd.
     214             :     /// precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the
     215             :     /// following restrictions: It either represents the constant true or the constant false, or it is an if-then-else
     216             :     /// expression with an expression of sort Bool  as guard, and a then-branch and an else-branch that again follow
     217             :     /// these restrictions
     218             :     /// \param a_bdd A binary decision diagram.
     219           0 :     virtual data_expression simplify(const data_expression& a_bdd)
     220             :     {
     221           0 :       return aux_simplify(a_bdd, data_expression_list());
     222             :     }
     223             : };
     224             : 
     225             : } // namespace detail
     226             : } // namespace data
     227             : } // namespace mcrl2
     228             : 
     229             : #endif