LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/prover - bdd_prover.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 121 198 61.1 %
Date: 2020-02-13 00:44:47 Functions: 10 16 62.5 %
Legend: Lines: hit not hit

          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/bdd_prover.h
      10             : /// \brief EQ-BDD based prover for mCRL2 boolean data expressions
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_BDD_PROVER_H
      13             : #define MCRL2_DATA_DETAIL_BDD_PROVER_H
      14             : 
      15             : #include "mcrl2/data/detail/prover/bdd_path_eliminator.h"
      16             : #include "mcrl2/data/detail/prover/induction.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : namespace data
      21             : {
      22             : namespace detail
      23             : {
      24             : 
      25             : /** \brief A prover that uses EQ-BDDs.
      26             :  *
      27             :  * \detail
      28             :  * A class based on the Prover class that takes an expression of sort
      29             :  * Bool in internal mCRL2 format and creates the corresponding EQ-BDD.
      30             :  * Using this EQ-BDD, the class can determine if the original
      31             :  * formula is a tautology or a contradiction. The term "formula" in
      32             :  * the following text denotes arbitrary expressions of sort Bool in
      33             :  * the mCRL2 format.
      34             :  *
      35             :  * A prover uses a rewriter to rewrite parts of the formulas it
      36             :  * manipulates. The constructor BDD_Prover::BDD_Prover initializes the
      37             :  * prover's rewriter with the data equations in internal mCRL2 format
      38             :  * contained in the LPS passed as parameter a_lps and the rewrite
      39             :  * strategy passed as parameter a_rewrite_strategy. The parameter
      40             :  * a_rewrite_strategy can be set to either
      41             :  * GS_REWR_data::jitty or GS_REWR_data::jittyC. To limit the
      42             :  * number of seconds spent on proving a single formula, a time limit
      43             :  * can be set. If the time limit is set to 0, no time limit will be
      44             :  * enforced. The parameter a_apply_induction indicates whether or
      45             :  * induction on lists is applied. The constructor
      46             :  * BDD_Prover::BDD_Prover has two additional parameters,
      47             :  * a_path_eliminator and a_solver_type. The parameter
      48             :  * a_path_eliminator can be used to enable the use of an instance of
      49             :  * the class BDD_Path_Eliminator. Instances of this class use an SMT
      50             :  * solver to eliminate inconsistent paths from BDDs. The parameter
      51             :  * a_solver_type can be used to indicate which SMT solver should be
      52             :  * used for this task. Either the SMT solver ario
      53             :  * (http://www.eecs.umich.edu/~ario/) or cvc-lite
      54             :  * (http://www.cs.nyu.edu/acsys/cvcl/) can be used. To use one of
      55             :  * these solvers, the directory containing the corresponding
      56             :  * executable must be in the path. If the parameter a_path_eliminator
      57             :  * is set to false, the parameter a_solver_type is ignored and no
      58             :  * instance of the class BDD_Path_Eliminator is initialized.
      59             :  *
      60             :  * The formula to be handled is set using the method
      61             :  * Prover::set_formula inherited from the class Prover. An entity of
      62             :  * the class BDD_Prover uses binary decision diagrams to determine if
      63             :  * a given formula is a tautology or a contradiction. The resulting
      64             :  * BDD can be retreived using the method BDD_Prover::get_bdd.
      65             :  *
      66             :  * The methods BDD_Prover::is_tautology and
      67             :  * BDD_Prover::is_contradiction indicate whether or not a formula is a
      68             :  * tautology or a contradiction. These methods will return answer_yes,
      69             :  * answer_no or answer_undefined. If a formula is neither a tautology
      70             :  * nor a contradiction according to the prover, a so called witness or
      71             :  * counter example can be returned by the methods
      72             :  * BDD_Prover::get_witness and BDD_Prover::get_counter_example. A
      73             :  * witness is a valuation for which the formula holds, a counter
      74             :  * example is a valuation for which it does not hold.
      75             : */
      76             : 
      77             : enum Answer
      78             : {
      79             :   answer_yes,
      80             :   answer_no,
      81             :   answer_undefined
      82             : };
      83             : 
      84             : 
      85             : // class BDD_Prover: public Prover
      86             : class BDD_Prover: protected rewriter
      87             : {
      88             :   public:
      89             :     typedef rewriter::substitution_type substitution_type;
      90             : 
      91             :   private:
      92             : 
      93             :     /// \brief Flag indicating whether or not the result of the comparison between the first two arguments
      94             :     /// \brief weighs stronger than the result of the comparison between the second pair of arguments of an
      95             :     /// \brief equation, when determining the order of expressions.
      96             :     static constexpr bool f_reverse = true;
      97             : 
      98             :     /// \brief Flag indicating whether or not the arguments of equality functions are taken into account
      99             :     /// \brief when determining the order of expressions.
     100             :     static constexpr bool f_full = true;
     101             : 
     102             :   protected:
     103             :     /// \brief An expression of sort Bool.
     104             :     data_expression f_formula;
     105             : 
     106             :     /// \brief A class that provides information about expressions.
     107             :     const Info f_info = Info(f_full, f_reverse);
     108             : 
     109             :     /// \brief A class that can be used to manipulate expressions.
     110             :     Manipulator f_manipulator = Manipulator(f_info);
     111             : 
     112             :     /// \brief A flag that indicates whether or not the formala Prover::f_formula has been processed.
     113             :     bool f_processed = false;
     114             : 
     115             :     /// \brief A flag that indicates whether or not the formala Prover::f_formula is a tautology.
     116             :     Answer f_tautology;
     117             : 
     118             :     /// \brief A flag that indicates whether or not the formala Prover::f_formula is a contradiction.
     119             :     Answer f_contradiction;
     120             : 
     121             :     /// \brief An integer representing the maximal amount of seconds to be spent on processing a formula.
     122             :     const int f_time_limit;
     123             : 
     124             :     /// \brief A timestamp representing the moment when the maximal amount of seconds has been spent on processing the current formula.
     125             :     time_t f_deadline;
     126             : 
     127             :   private:
     128             :     /// \brief A flag indicating whether or not induction on lists is applied.
     129             :     bool f_apply_induction;
     130             : 
     131             :     /// \brief A data specification.
     132             :     // const data_specification& f_data_spec;
     133             : 
     134             :     /// \brief A hashtable that maps formulas to BDDs.
     135             :     /// \brief If the BDD of a formula is unknown, it maps this formula to 0.
     136             :     std::unordered_map < data_expression, data_expression > f_formula_to_bdd;
     137             : 
     138             :     /// \brief A hashtable that maps formulas to the smallest guard occuring in those formulas.
     139             :     /// \brief If the smallest guard of a formula is unknown, it maps this formula to 0.
     140             :     std::unordered_map < data_expression, data_expression > f_smallest;
     141             : 
     142             :     /// \brief Class that simplifies a BDD.
     143             :     BDD_Simplifier* f_bdd_simplifier;
     144             : 
     145             :     /// \brief Class that creates all statements needed to prove a given property using induction.
     146             :     Induction f_induction;
     147             : 
     148             :     /// \brief Constructs the EQ-BDD corresponding to the formula Prover::f_formula.
     149          81 :     void build_bdd()
     150             :     {
     151          81 :       f_deadline = time(nullptr) + f_time_limit;
     152             : 
     153         162 :       data_expression v_previous_1;
     154         162 :       data_expression v_previous_2;
     155             : 
     156          81 :       mCRL2log(log::debug1) << "Formula: " << f_formula << std::endl;
     157             : 
     158         162 :       data_expression intermediate_bdd = f_formula;
     159             : 
     160          81 :       intermediate_bdd = m_rewriter->rewrite(intermediate_bdd,bdd_sigma);
     161          81 :       intermediate_bdd = f_manipulator.orient(intermediate_bdd);
     162             : 
     163          81 :       mCRL2log(log::debug1) << "Formula rewritten and oriented: " << intermediate_bdd << std::endl;
     164             : 
     165         349 :       while (v_previous_1 != intermediate_bdd && v_previous_2 != intermediate_bdd)
     166             :       {
     167         134 :         v_previous_2 = v_previous_1;
     168         134 :         v_previous_1 = intermediate_bdd;
     169         134 :         intermediate_bdd = bdd_down(intermediate_bdd);
     170         134 :         mCRL2log(log::debug1) << "End of iteration." << std::endl;
     171         134 :         mCRL2log(log::debug1) << "Intermediate BDD: " << intermediate_bdd << std::endl;
     172             :       }
     173             : 
     174          81 :       f_bdd = intermediate_bdd;
     175          81 :       mCRL2log(log::debug1) << "Resulting BDD: " << f_bdd << std::endl;
     176             : 
     177          81 :     }
     178             : 
     179             :     // Auxiliary function to deliver an indent of length n.
     180           0 :     inline std::string indent(size_t n)
     181             :     {
     182           0 :       return std::string(n, ' ');
     183             :     }
     184             : 
     185             :     /// \brief Creates the EQ-BDD corresponding to the formula a_formula.
     186         424 :     data_expression bdd_down(const data_expression& a_formula, const size_t a_indent=0)
     187             :     {
     188             : 
     189         424 :       if (f_time_limit != 0 && (f_deadline - time(nullptr)) <= 0)
     190             :       {
     191           0 :         mCRL2log(log::debug1) << "The time limit has passed." << std::endl;
     192           0 :         return a_formula;
     193             :       }
     194             : 
     195         424 :       if (a_formula==sort_bool::true_())
     196             :       {
     197         178 :         return a_formula;
     198             :       }
     199         246 :       if (a_formula==sort_bool::false_())
     200             :       {
     201          72 :         return a_formula;
     202             :       }
     203             : 
     204         174 :       if (is_abstraction(a_formula))
     205             :       {
     206           0 :         const abstraction& a = atermpp::down_cast<abstraction>(a_formula);
     207           0 :         return abstraction(a.binding_operator(), a.variables(), bdd_down(a.body(), a_indent));
     208             :       }
     209             : 
     210         174 :       const std::unordered_map < data_expression, data_expression >::const_iterator i = f_formula_to_bdd.find(a_formula);
     211         174 :       if (i!=f_formula_to_bdd.end()) // found
     212             :       {
     213          29 :         return i->second;
     214             :       }
     215             : 
     216         290 :       data_expression v_guard = smallest(a_formula);
     217         145 :       if (v_guard==data_expression())
     218             :       {
     219           0 :         return a_formula;
     220             :       }
     221             :       else
     222             :       {
     223         145 :         mCRL2log(log::debug1) << indent(a_indent) << "Smallest guard: " << v_guard << std::endl;
     224             :       }
     225             : 
     226         145 :       const size_t extra_indent = a_indent + 2;
     227             : 
     228         290 :       data_expression v_term1 = f_manipulator.set_true(a_formula, v_guard);
     229         145 :       v_term1 = m_rewriter->rewrite(v_term1,bdd_sigma);
     230         145 :       v_term1 = f_manipulator.orient(v_term1);
     231         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "True-branch after rewriting and orienting: " << v_term1 << std::endl;
     232         145 :       v_term1 = bdd_down(v_term1, extra_indent);
     233         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "BDD of the true-branch: " << v_term1 << std::endl;
     234             : 
     235         290 :       data_expression v_term2 = f_manipulator.set_false(a_formula, v_guard);
     236         145 :       v_term2 = m_rewriter->rewrite(v_term2,bdd_sigma);
     237         145 :       v_term2 = f_manipulator.orient(v_term2);
     238         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "False-branch after rewriting and orienting: " << v_term2 << std::endl;
     239         145 :       v_term2 = bdd_down(v_term2, extra_indent);
     240         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "BDD of the false-branch: " << v_term2 << std::endl;
     241             : 
     242         290 :       data_expression v_bdd = Manipulator::make_reduced_if_then_else(v_guard, v_term1, v_term2);
     243         145 :       f_formula_to_bdd[a_formula]=v_bdd;
     244             : 
     245         145 :       return v_bdd;
     246             :     }
     247             : 
     248             :     /// \brief Removes all inconsistent paths from the BDD BDD_Prover::f_bdd.
     249          81 :     void eliminate_paths()
     250             :     {
     251             :       time_t v_new_time_limit;
     252             : 
     253          81 :       v_new_time_limit = f_deadline - time(nullptr);
     254          81 :       if (v_new_time_limit > 0 || f_time_limit == 0)
     255             :       {
     256          81 :         mCRL2log(log::debug1) << "Simplifying the BDD:" << std::endl;
     257          81 :         f_bdd_simplifier->set_time_limit((std::max)(v_new_time_limit, time(nullptr)));
     258          81 :         f_bdd = f_bdd_simplifier->simplify(f_bdd);
     259          81 :         mCRL2log(log::debug1) << "Resulting BDD: " << f_bdd << std::endl;
     260             :       }
     261          81 :     }
     262             : 
     263             :     /// \brief Updates the values of Prover::f_tautology and Prover::f_contradiction.
     264          81 :     void update_answers()
     265             :     {
     266          81 :       if (!f_processed)
     267             :       {
     268          81 :         build_bdd();
     269          81 :         eliminate_paths();
     270         162 :         data_expression v_original_formula = f_formula;
     271         162 :         data_expression v_original_bdd = f_bdd;
     272          81 :         if (f_apply_induction && !(BDD_Info::is_true(f_bdd) || BDD_Info::is_false(f_bdd)))
     273             :         {
     274           0 :           f_induction.initialize(v_original_formula);
     275           0 :           while (f_induction.can_apply_induction() && !BDD_Info::is_true(f_bdd))
     276             :           {
     277           0 :             mCRL2log(log::debug1) << "Applying induction." << std::endl;
     278           0 :             f_formula = f_induction.apply_induction();
     279           0 :             build_bdd();
     280           0 :             eliminate_paths();
     281             :           }
     282           0 :           if (BDD_Info::is_true(f_bdd))
     283             :           {
     284           0 :             f_tautology = answer_yes;
     285           0 :             f_contradiction = answer_no;
     286             :           }
     287             :           else
     288             :           {
     289           0 :             v_original_formula = sort_bool::not_(v_original_formula);
     290           0 :             f_bdd = v_original_bdd;
     291           0 :             f_induction.initialize(v_original_formula);
     292           0 :             while (f_induction.can_apply_induction() && !BDD_Info::is_true(f_bdd))
     293             :             {
     294           0 :               mCRL2log(log::debug1) << "Applying induction on the negated formula." << std::endl;
     295           0 :               f_formula = f_induction.apply_induction();
     296           0 :               build_bdd();
     297           0 :               eliminate_paths();
     298             :             }
     299           0 :             if (BDD_Info::is_true(f_bdd))
     300             :             {
     301           0 :               f_bdd = sort_bool::false_();
     302           0 :               f_tautology = answer_no;
     303           0 :               f_contradiction = answer_yes;
     304             :             }
     305             :             else
     306             :             {
     307           0 :               f_bdd = v_original_bdd;
     308           0 :               f_tautology = answer_undefined;
     309           0 :               f_contradiction = answer_undefined;
     310             :             }
     311             :           }
     312             :         }
     313             :         else
     314             :         {
     315          81 :           if (BDD_Info::is_true(f_bdd))
     316             :           {
     317          59 :             f_tautology = answer_yes;
     318          59 :             f_contradiction = answer_no;
     319             :           }
     320          22 :           else if (BDD_Info::is_false(f_bdd))
     321             :           {
     322           2 :             f_tautology = answer_no;
     323           2 :             f_contradiction = answer_yes;
     324             :           }
     325             :           else
     326             :           {
     327          20 :             f_tautology = answer_undefined;
     328          20 :             f_contradiction = answer_undefined;
     329             :           }
     330             :         }
     331          81 :         f_processed = true;
     332             :       }
     333          81 :     };
     334             : 
     335             :     /// \brief Returns the smallest guard in the formula a_formula.
     336         789 :     data_expression smallest(data_expression a_formula)
     337             :     {
     338         789 :       if (is_variable(a_formula))
     339             :       {
     340         124 :         if (a_formula.sort()==sort_bool::bool_())
     341             :         {
     342          82 :           return a_formula;
     343             :         }
     344             :         else
     345             :         {
     346          42 :           return data_expression();
     347             :         }
     348             :       }
     349         665 :       if (a_formula==sort_bool::true_() || a_formula==sort_bool::false_())
     350             :       {
     351          88 :         return data_expression();
     352             :       }
     353         577 :       if (is_abstraction(a_formula))
     354             :       {
     355             :         // Guards from within an abstraction may contain
     356             :         // variables that are not bound outside that abstraction.
     357             :         // Therefore, we never return a smallest guard from
     358             :         // within an abstraction.
     359           0 :         return data_expression();
     360             :       }
     361             : 
     362         577 :       const std::unordered_map < data_expression, data_expression >::const_iterator i = f_smallest.find(a_formula);
     363         577 :       if (i!=f_smallest.end()) //found
     364             :       {
     365         193 :         return i->second;
     366             :       }
     367             : 
     368         768 :       data_expression v_result;
     369             : 
     370         384 :       std::size_t v_length = f_info.get_number_of_arguments(a_formula);
     371             : 
     372        1028 :       for (std::size_t s = 0; s < v_length; s++)
     373             :       {
     374        1288 :         const data_expression v_small = smallest(f_info.get_argument(a_formula, s));
     375         644 :         if (v_small!=data_expression())
     376             :         {
     377         427 :           if (v_result!=data_expression())
     378             :           {
     379         171 :             if (f_info.compare_guard(v_small, v_result) == compare_result_smaller)
     380             :             {
     381          29 :               v_result = v_small;
     382             :             }
     383             :           }
     384             :           else
     385             :           {
     386         256 :             v_result = v_small;
     387             :           }
     388             :         }
     389             :       }
     390         384 :       if (v_result==data_expression() && a_formula.sort()==sort_bool::bool_())
     391             :       {
     392          41 :         v_result = a_formula;
     393             :       }
     394         384 :       if (v_result!=data_expression())
     395             :       {
     396         297 :         f_smallest[a_formula]=v_result;
     397             :       }
     398             : 
     399         384 :       return v_result;
     400             :     }
     401             : 
     402             :     /// \brief Returns branch of the BDD a_bdd, depending on the polarity a_polarity.
     403           0 :     data_expression get_branch(const data_expression& a_bdd, const bool a_polarity)
     404             :     {
     405           0 :       data_expression v_result;
     406             : 
     407           0 :       if (BDD_Info::is_if_then_else(a_bdd))
     408             :       {
     409           0 :         data_expression v_guard = BDD_Info::get_guard(a_bdd);
     410           0 :         data_expression v_true_branch = BDD_Info::get_true_branch(a_bdd);
     411           0 :         data_expression v_false_branch = BDD_Info::get_false_branch(a_bdd);
     412           0 :         data_expression v_branch = get_branch(v_true_branch, a_polarity);
     413           0 :         if (v_branch==data_expression())
     414             :         {
     415           0 :           v_branch = get_branch(v_false_branch, a_polarity);
     416           0 :           if (v_branch==data_expression())
     417             :           {
     418           0 :             v_result = data_expression();
     419             :           }
     420             :           else
     421             :           {
     422           0 :             data_expression v_term = sort_bool::not_(v_guard);
     423           0 :             v_result = lazy::and_(v_branch, v_term);
     424             :           }
     425             :         }
     426             :         else
     427             :         {
     428           0 :           v_result = lazy::and_(v_branch, v_guard);
     429             :         }
     430             :       }
     431             :       else
     432             :       {
     433           0 :         if ((BDD_Info::is_true(a_bdd) && a_polarity) || (BDD_Info::is_false(a_bdd) && !a_polarity))
     434             :         {
     435           0 :           v_result = sort_bool::true_();
     436             :         }
     437             :         else
     438             :         {
     439           0 :           v_result = data_expression();
     440             :         }
     441             :       }
     442           0 :       return v_result;
     443             :     }
     444             : 
     445             :   protected:
     446             : 
     447             :     /// \brief A binary decision diagram in the internal representation of the rewriter.
     448             :     substitution_type bdd_sigma;
     449             : 
     450             :     /// \brief A binary decision diagram in the internal representation of mCRL2.
     451             :     data_expression f_bdd;
     452             :   public:
     453             : 
     454          18 :     BDD_Prover(
     455             :       const data_specification& data_spec,
     456             :       const used_data_equation_selector& equations_selector,
     457             :       mcrl2::data::rewriter::strategy a_rewrite_strategy = mcrl2::data::jitty,
     458             :       int a_time_limit = 0,
     459             :       bool a_path_eliminator = false,
     460             :       smt_solver_type a_solver_type = solver_type_cvc,
     461             :       bool a_apply_induction = false)
     462          18 :     : rewriter(data_spec, equations_selector, a_rewrite_strategy)
     463             :     , f_time_limit(a_time_limit)
     464             :     , f_apply_induction(a_apply_induction)
     465          18 :     , f_bdd_simplifier(a_path_eliminator ? new BDD_Path_Eliminator(a_solver_type) : new BDD_Simplifier())
     466             :     {
     467          18 :       switch (a_rewrite_strategy)
     468             :       {
     469          18 :         case(jitty):
     470             : #ifdef MCRL2_JITTYC_AVAILABLE
     471             :         case(jitty_compiling):
     472             : #endif
     473             :         {
     474             :           /* These provers are ok */
     475          18 :           break;
     476             :         }
     477           0 :         case(jitty_prover):
     478             : #ifdef MCRL2_JITTYC_AVAILABLE
     479             :         case(jitty_compiling_prover):
     480             : #endif
     481             :         {
     482           0 :           throw mcrl2::runtime_error("The proving rewriters are not supported by the prover (only jitty and jittyc are supported).");
     483             :         }
     484           0 :         default:
     485             :         {
     486           0 :           throw mcrl2::runtime_error("Unknown type of rewriter.");
     487             :           break;
     488             :         }
     489             :       }
     490             : 
     491          18 :       mCRL2log(log::debug1) << "Flags:" << std::endl
     492           0 :                       << "  Reverse: " << std::boolalpha << f_reverse << "," << std::endl
     493           0 :                       << "  Full: " << f_full << "," << std::endl;
     494          18 :     }
     495             : 
     496             :     BDD_Prover(const rewriter& r, int time_limit = 0, bool apply_induction = false)
     497             :     : rewriter(r)
     498             :     , f_time_limit(time_limit)
     499             :     , f_apply_induction(apply_induction)
     500             :     , f_bdd_simplifier(new BDD_Simplifier())
     501             :     {}
     502             : 
     503             :     /// \brief Destructor that destroys the BDD simplifier BDD_Prover::f_bdd_simplifier.
     504          18 :     ~BDD_Prover()
     505          18 :     {
     506          18 :       delete f_bdd_simplifier;
     507          18 :       f_bdd_simplifier = nullptr;
     508          18 :     }
     509             : 
     510             :     /// \brief Set the substitution to be used to construct the BDD
     511           0 :     void set_substitution(substitution_type& sigma)
     512             :     {
     513           0 :       bdd_sigma = sigma;
     514           0 :     }
     515             : 
     516             :     /// \brief Set the substitution in internal format to be used to construct the BDD
     517             :     void set_substitution_internal(substitution_type& sigma)
     518             :     {
     519             :       bdd_sigma = sigma;
     520             :     }
     521             : 
     522             :     /// \brief Indicates whether or not the formula Prover::f_formula is a tautology.
     523          60 :     Answer is_tautology()
     524             :     {
     525          60 :       update_answers();
     526          60 :       return f_tautology;
     527             :     }
     528             : 
     529             :     /// \brief Indicates whether or not the formula Prover::f_formula is a contradiction.
     530           0 :     Answer is_contradiction()
     531             :     {
     532           0 :       update_answers();
     533           0 :       return f_contradiction;
     534             :     }
     535             : 
     536             :     /// \brief Returns the BDD BDD_Prover::f_bdd.
     537          21 :     data_expression get_bdd()
     538             :     {
     539          21 :       update_answers();
     540          21 :       return f_bdd;
     541             :     }
     542             : 
     543             :     /// \brief Returns all the guards on a path in the BDD that leads to a leaf labelled "true", if such a leaf exists.
     544             :     data_expression get_witness()
     545             :     {
     546             :       update_answers();
     547             :       if (is_contradiction() == answer_yes)
     548             :       {
     549             :         mCRL2log(log::debug1) << "The formula is a contradiction." << std::endl;
     550             :         return sort_bool::true_();
     551             :       }
     552             :       else if (is_tautology() == answer_yes)
     553             :       {
     554             :         mCRL2log(log::debug1) << "The formula is a tautology." << std::endl;
     555             :         return sort_bool::false_();
     556             :       }
     557             :       else
     558             :       {
     559             :         mCRL2log(log::debug1) << "The formula is satisfiable, but not a tautology." << std::endl;
     560             :         data_expression t=get_branch(f_bdd, true);
     561             :         if (t==data_expression())
     562             :         { throw mcrl2::runtime_error(
     563             :             "Cannot provide witness. This is probably caused by an abrupt stop of the\n"
     564             :             "conversion from expression to EQ-BDD. This typically occurs when a time limit is set.");
     565             :         }
     566             :         return t;
     567             :       }
     568             :     }
     569             : 
     570             :     /// \brief Returns all the guards on a path in the BDD that leads to a leaf labelled "false", if such a leaf exists.
     571           0 :     data_expression get_counter_example()
     572             :     {
     573           0 :       update_answers();
     574           0 :       if (is_contradiction() == answer_yes)
     575             :       {
     576           0 :         mCRL2log(log::debug1) << "The formula is a contradiction." << std::endl;
     577           0 :         return sort_bool::false_();
     578             :       }
     579           0 :       else if (is_tautology() == answer_yes)
     580             :       {
     581           0 :         mCRL2log(log::debug1) << "The formula is a tautology." << std::endl;
     582           0 :         return sort_bool::true_();
     583             :       }
     584             :       else
     585             :       {
     586           0 :         mCRL2log(log::debug1) << "The formula is satisfiable, but not a tautology." << std::endl;
     587           0 :         data_expression t=get_branch(f_bdd, false);
     588           0 :         if (t==data_expression())
     589             :         { throw mcrl2::runtime_error(
     590             :             "Cannot provide counter example. This is probably caused by an abrupt stop of the\n"
     591           0 :             "conversion from expression to EQ-BDD. This typically occurs when a time limit is set.");
     592             :         }
     593           0 :         return t;
     594             :       }
     595             :     }
     596             : 
     597             :     /// \brief Returns the rewriter used by this prover (i.e. it returns Prover::f_rewriter).
     598           0 :     std::shared_ptr<detail::Rewriter> get_rewriter()
     599             :     {
     600           0 :       return m_rewriter;
     601             :     }
     602             : 
     603             :     /// \brief Sets Prover::f_formula to a_formula.
     604             :     /// precondition: the argument passed as parameter a_formula is an expression of sort Bool
     605          81 :     void set_formula(const data_expression& a_formula)
     606             :     {
     607          81 :       f_formula = a_formula;
     608          81 :       f_processed = false;
     609          81 :       mCRL2log(log::debug1) << "The formula has been set." << std::endl;
     610          81 :     }
     611             : 
     612             : 
     613             : };
     614             : } // namespace detail
     615             : } // namespace data
     616             : } // namespace mcrl2
     617             : 
     618             : #endif

Generated by: LCOV version 1.13