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: 128 208 61.5 %
Date: 2020-09-22 00:46:14 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::debug) << "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::debug) << "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 formula.
     186         424 :     data_expression bdd_down(const data_expression& 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::debug) << "The time limit has passed." << std::endl;
     192           0 :         return formula;
     193             :       }
     194             : 
     195         424 :       if (formula==sort_bool::true_())
     196             :       {
     197         178 :         return formula;
     198             :       }
     199         246 :       if (formula==sort_bool::false_())
     200             :       {
     201          72 :         return formula;
     202             :       }
     203             : 
     204         174 :       if (is_abstraction(formula))
     205             :       {
     206           0 :         const abstraction& a = atermpp::down_cast<abstraction>(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(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;
     217         145 :       bool success  = smallest(formula, v_guard);
     218         145 :       if (!success)
     219             :       {
     220           0 :         return formula;
     221             :       }
     222             :       else
     223             :       {
     224         145 :         mCRL2log(log::debug1) << indent(a_indent) << "Smallest guard: " << v_guard << std::endl;
     225             :       }
     226             : 
     227         145 :       const size_t extra_indent = a_indent + 2;
     228             : 
     229         290 :       data_expression v_term1 = f_manipulator.set_true(formula, v_guard);
     230         145 :       v_term1 = m_rewriter->rewrite(v_term1,bdd_sigma);
     231         145 :       v_term1 = f_manipulator.orient(v_term1);
     232         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "True-branch after rewriting and orienting: " << v_term1 << std::endl;
     233         145 :       v_term1 = bdd_down(v_term1, extra_indent);
     234         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "BDD of the true-branch: " << v_term1 << std::endl;
     235             : 
     236         290 :       data_expression v_term2 = f_manipulator.set_false(formula, v_guard);
     237         145 :       v_term2 = m_rewriter->rewrite(v_term2,bdd_sigma);
     238         145 :       v_term2 = f_manipulator.orient(v_term2);
     239         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "False-branch after rewriting and orienting: " << v_term2 << std::endl;
     240         145 :       v_term2 = bdd_down(v_term2, extra_indent);
     241         145 :       mCRL2log(log::debug1) << indent(extra_indent) << "BDD of the false-branch: " << v_term2 << std::endl;
     242             : 
     243         290 :       data_expression v_bdd = Manipulator::make_reduced_if_then_else(v_guard, v_term1, v_term2);
     244         145 :       f_formula_to_bdd[formula]=v_bdd;
     245             : 
     246         145 :       return v_bdd;
     247             :     }
     248             : 
     249             :     /// \brief Removes all inconsistent paths from the BDD BDD_Prover::f_bdd.
     250          81 :     void eliminate_paths()
     251             :     {
     252             :       time_t v_new_time_limit;
     253             : 
     254          81 :       v_new_time_limit = f_deadline - time(nullptr);
     255          81 :       if (v_new_time_limit > 0 || f_time_limit == 0)
     256             :       {
     257          81 :         mCRL2log(log::debug) << "Simplifying the BDD:" << std::endl;
     258          81 :         f_bdd_simplifier->set_time_limit((std::max)(v_new_time_limit, time(nullptr)));
     259          81 :         f_bdd = f_bdd_simplifier->simplify(f_bdd);
     260          81 :         mCRL2log(log::debug) << "Resulting BDD: " << f_bdd << std::endl;
     261             :       }
     262          81 :     }
     263             : 
     264             :     /// \brief Updates the values of Prover::f_tautology and Prover::f_contradiction.
     265          81 :     void update_answers()
     266             :     {
     267          81 :       if (!f_processed)
     268             :       {
     269          81 :         build_bdd();
     270          81 :         eliminate_paths();
     271         162 :         data_expression v_original_formula = f_formula;
     272         162 :         data_expression v_original_bdd = f_bdd;
     273          81 :         if (f_apply_induction && !(BDD_Info::is_true(f_bdd) || BDD_Info::is_false(f_bdd)))
     274             :         {
     275           0 :           f_induction.initialize(v_original_formula);
     276           0 :           while (f_induction.can_apply_induction() && !BDD_Info::is_true(f_bdd))
     277             :           {
     278           0 :             mCRL2log(log::debug) << "Applying induction." << std::endl;
     279           0 :             f_formula = f_induction.apply_induction();
     280           0 :             build_bdd();
     281           0 :             eliminate_paths();
     282             :           }
     283           0 :           if (BDD_Info::is_true(f_bdd))
     284             :           {
     285           0 :             f_tautology = answer_yes;
     286           0 :             f_contradiction = answer_no;
     287             :           }
     288             :           else
     289             :           {
     290           0 :             v_original_formula = sort_bool::not_(v_original_formula);
     291           0 :             f_bdd = v_original_bdd;
     292           0 :             f_induction.initialize(v_original_formula);
     293           0 :             while (f_induction.can_apply_induction() && !BDD_Info::is_true(f_bdd))
     294             :             {
     295           0 :               mCRL2log(log::debug) << "Applying induction on the negated formula." << std::endl;
     296           0 :               f_formula = f_induction.apply_induction();
     297           0 :               build_bdd();
     298           0 :               eliminate_paths();
     299             :             }
     300           0 :             if (BDD_Info::is_true(f_bdd))
     301             :             {
     302           0 :               f_bdd = sort_bool::false_();
     303           0 :               f_tautology = answer_no;
     304           0 :               f_contradiction = answer_yes;
     305             :             }
     306             :             else
     307             :             {
     308           0 :               f_bdd = v_original_bdd;
     309           0 :               f_tautology = answer_undefined;
     310           0 :               f_contradiction = answer_undefined;
     311             :             }
     312             :           }
     313             :         }
     314             :         else
     315             :         {
     316          81 :           if (BDD_Info::is_true(f_bdd))
     317             :           {
     318          59 :             f_tautology = answer_yes;
     319          59 :             f_contradiction = answer_no;
     320             :           }
     321          22 :           else if (BDD_Info::is_false(f_bdd))
     322             :           {
     323           2 :             f_tautology = answer_no;
     324           2 :             f_contradiction = answer_yes;
     325             :           }
     326             :           else
     327             :           {
     328          20 :             f_tautology = answer_undefined;
     329          20 :             f_contradiction = answer_undefined;
     330             :           }
     331             :         }
     332          81 :         f_processed = true;
     333             :       }
     334          81 :     };
     335             : 
     336             :     /// \brief Returns the smallest guard in the formula formula.
     337         989 :     bool smallest(const data_expression& formula, data_expression& result)
     338             :     {
     339         989 :       if (is_variable(formula))
     340             :       {
     341         195 :         if (formula.sort()==sort_bool::bool_())
     342             :         {
     343          82 :           result=formula;
     344          82 :           return true;
     345             :         }
     346             :         else
     347             :         {
     348         113 :           return false;
     349             :         }
     350             :       }
     351         794 :       if (is_function_symbol(formula))
     352             :       { 
     353         235 :         if (formula.sort()==sort_bool::bool_() && !(formula==sort_bool::true_() || formula==sort_bool::false_()))
     354             :         {
     355           0 :           result=formula;
     356           0 :           return true;
     357             :         }
     358             :         else
     359             :         { 
     360         235 :           return false;
     361             :         }
     362             :       }
     363         559 :       if (is_abstraction(formula))
     364             :       {
     365             :         // Guards from within an abstraction may contain
     366             :         // variables that are not bound outside that abstraction.
     367             :         // Therefore, we never return a smallest guard from
     368             :         // within an abstraction.
     369           0 :         return false;
     370             :       }
     371             : 
     372         559 :       const std::unordered_map < data_expression, data_expression >::const_iterator i = f_smallest.find(formula);
     373         559 :       if (i!=f_smallest.end()) //found
     374             :       {
     375         122 :         result=i->second;
     376         122 :         return true;
     377             :       }
     378             : 
     379         437 :       bool result_is_defined=false;
     380         874 :       data_expression v_small;
     381        1281 :       for (const data_expression& arg: atermpp::down_cast<application>(formula))
     382             :       {
     383         844 :         bool success = smallest(arg,v_small);
     384         844 :         if (success)
     385             :         {
     386         427 :           if (result_is_defined)
     387             :           {
     388         171 :             if (f_info.compare_guard(v_small, result) == compare_result_smaller)
     389             :             {
     390          29 :               result = v_small;
     391             :             }
     392             :           }
     393             :           else
     394             :           {
     395         256 :             result = v_small;
     396         256 :             result_is_defined=true;
     397             :           }
     398             :         }
     399             :       }
     400         437 :       if (!result_is_defined && formula.sort()==sort_bool::bool_())
     401             :       {
     402         112 :         result = formula;
     403         112 :         return true;
     404             :       }
     405         325 :       if (result_is_defined)
     406             :       {
     407         256 :         f_smallest[formula]=result;  // Save the result in the cache
     408         256 :         return true;
     409             :       }
     410             : 
     411          69 :       return false;
     412             :     }
     413             : 
     414             :     /// \brief Returns branch of the BDD a_bdd, depending on the polarity a_polarity.
     415           0 :     bool get_branch(const data_expression& a_bdd, const bool a_polarity, data_expression& result)
     416             :     {
     417           0 :       if (BDD_Info::is_if_then_else(a_bdd))
     418             :       {
     419           0 :         const data_expression& v_guard = BDD_Info::get_guard(a_bdd);
     420           0 :         const data_expression& v_true_branch = BDD_Info::get_true_branch(a_bdd);
     421           0 :         const data_expression& v_false_branch = BDD_Info::get_false_branch(a_bdd);
     422           0 :         bool success = get_branch(v_true_branch, a_polarity, result);
     423           0 :         if (success)
     424             :         {
     425           0 :           result = lazy::and_(result, v_guard);
     426           0 :           return true;
     427             :         }
     428             :         else
     429             :         {
     430           0 :           success = get_branch(v_false_branch, a_polarity, result);
     431           0 :           if (success)
     432             :           {
     433           0 :             result = lazy::and_(result, sort_bool::not_(v_guard));
     434           0 :             return true;
     435             :           }
     436             :           else
     437             :           {
     438           0 :             return false;
     439             :           }
     440             :         }
     441             :       }
     442             :       else
     443             :       {
     444           0 :         if ((BDD_Info::is_true(a_bdd) && a_polarity) || (BDD_Info::is_false(a_bdd) && !a_polarity))
     445             :         {
     446           0 :           result = sort_bool::true_();
     447           0 :           return true;
     448             :         }
     449           0 :         return false;
     450             :       }
     451             :     }
     452             : 
     453             :   protected:
     454             : 
     455             :     /// \brief A binary decision diagram in the internal representation of the rewriter.
     456             :     substitution_type bdd_sigma;
     457             : 
     458             :     /// \brief A binary decision diagram in the internal representation of mCRL2.
     459             :     data_expression f_bdd;
     460             :   public:
     461             : 
     462          18 :     BDD_Prover(
     463             :       const data_specification& data_spec,
     464             :       const used_data_equation_selector& equations_selector,
     465             :       mcrl2::data::rewriter::strategy a_rewrite_strategy = mcrl2::data::jitty,
     466             :       int a_time_limit = 0,
     467             :       bool a_path_eliminator = false,
     468             :       smt_solver_type a_solver_type = solver_type_cvc,
     469             :       bool a_apply_induction = false)
     470          18 :     : rewriter(data_spec, equations_selector, a_rewrite_strategy)
     471             :     , f_time_limit(a_time_limit)
     472             :     , f_apply_induction(a_apply_induction)
     473          18 :     , f_bdd_simplifier(a_path_eliminator ? new BDD_Path_Eliminator(a_solver_type) : new BDD_Simplifier())
     474             :     {
     475          18 :       switch (a_rewrite_strategy)
     476             :       {
     477          18 :         case(jitty):
     478             : #ifdef MCRL2_JITTYC_AVAILABLE
     479             :         case(jitty_compiling):
     480             : #endif
     481             :         {
     482             :           /* These provers are ok */
     483          18 :           break;
     484             :         }
     485           0 :         case(jitty_prover):
     486             : #ifdef MCRL2_JITTYC_AVAILABLE
     487             :         case(jitty_compiling_prover):
     488             : #endif
     489             :         {
     490           0 :           throw mcrl2::runtime_error("The proving rewriters are not supported by the prover (only jitty and jittyc are supported).");
     491             :         }
     492           0 :         default:
     493             :         {
     494           0 :           throw mcrl2::runtime_error("Unknown type of rewriter.");
     495             :           break;
     496             :         }
     497             :       }
     498             : 
     499          18 :       mCRL2log(log::debug) << "Flags:" << std::endl
     500           0 :                       << "  Reverse: " << std::boolalpha << f_reverse << "," << std::endl
     501           0 :                       << "  Full: " << f_full << "," << std::endl;
     502          18 :     }
     503             : 
     504             :     BDD_Prover(const rewriter& r, int time_limit = 0, bool apply_induction = false)
     505             :     : rewriter(r)
     506             :     , f_time_limit(time_limit)
     507             :     , f_apply_induction(apply_induction)
     508             :     , f_bdd_simplifier(new BDD_Simplifier())
     509             :     {}
     510             : 
     511             :     /// \brief Destructor that destroys the BDD simplifier BDD_Prover::f_bdd_simplifier.
     512          18 :     ~BDD_Prover()
     513          18 :     {
     514          18 :       delete f_bdd_simplifier;
     515          18 :       f_bdd_simplifier = nullptr;
     516          18 :     }
     517             : 
     518             :     /// \brief Set the substitution to be used to construct the BDD
     519           0 :     void set_substitution(substitution_type& sigma)
     520             :     {
     521           0 :       bdd_sigma = sigma;
     522           0 :     }
     523             : 
     524             :     /// \brief Set the substitution in internal format to be used to construct the BDD
     525             :     void set_substitution_internal(substitution_type& sigma)
     526             :     {
     527             :       bdd_sigma = sigma;
     528             :     }
     529             : 
     530             :     /// \brief Indicates whether or not the formula Prover::f_formula is a tautology.
     531          60 :     Answer is_tautology()
     532             :     {
     533          60 :       update_answers();
     534          60 :       return f_tautology;
     535             :     }
     536             : 
     537             :     /// \brief Indicates whether or not the formula Prover::f_formula is a contradiction.
     538           0 :     Answer is_contradiction()
     539             :     {
     540           0 :       update_answers();
     541           0 :       return f_contradiction;
     542             :     }
     543             : 
     544             :     /// \brief Returns the BDD BDD_Prover::f_bdd.
     545          21 :     data_expression get_bdd()
     546             :     {
     547          21 :       update_answers();
     548          21 :       return f_bdd;
     549             :     }
     550             : 
     551             :     /// \brief Returns all the guards on a path in the BDD that leads to a leaf labelled "true", if such a leaf exists.
     552             :     data_expression get_witness()
     553             :     {
     554             :       update_answers();
     555             :       if (is_contradiction() == answer_yes)
     556             :       {
     557             :         mCRL2log(log::debug) << "The formula is a contradiction." << std::endl;
     558             :         return sort_bool::true_();
     559             :       }
     560             :       else if (is_tautology() == answer_yes)
     561             :       {
     562             :         mCRL2log(log::debug) << "The formula is a tautology." << std::endl;
     563             :         return sort_bool::false_();
     564             :       }
     565             :       else
     566             :       {
     567             :         mCRL2log(log::debug) << "The formula is satisfiable, but not a tautology." << std::endl;
     568             :         data_expression result;
     569             :         bool success = get_branch(f_bdd, true, result);
     570             :         if (!success)
     571             :         { throw mcrl2::runtime_error(
     572             :             "Cannot provide witness. This is probably caused by an abrupt stop of the\n"
     573             :             "conversion from expression to EQ-BDD. This typically occurs when a time limit is set.");
     574             :         }
     575             :         return result;
     576             :       }
     577             :     }
     578             : 
     579             :     /// \brief Returns all the guards on a path in the BDD that leads to a leaf labelled "false", if such a leaf exists.
     580           0 :     data_expression get_counter_example()
     581             :     {
     582           0 :       update_answers();
     583           0 :       if (is_contradiction() == answer_yes)
     584             :       {
     585           0 :         mCRL2log(log::debug) << "The formula is a contradiction." << std::endl;
     586           0 :         return sort_bool::false_();
     587             :       }
     588           0 :       else if (is_tautology() == answer_yes)
     589             :       {
     590           0 :         mCRL2log(log::debug) << "The formula is a tautology." << std::endl;
     591           0 :         return sort_bool::true_();
     592             :       }
     593             :       else
     594             :       {
     595           0 :         mCRL2log(log::debug) << "The formula is satisfiable, but not a tautology." << std::endl;
     596           0 :         data_expression result;
     597           0 :         bool success=get_branch(f_bdd, false,result);
     598           0 :         if (!success)
     599             :         { throw mcrl2::runtime_error(
     600             :             "Cannot provide counter example. This is probably caused by an abrupt stop of the\n"
     601           0 :             "conversion from expression to EQ-BDD. This typically occurs when a time limit is set.");
     602             :         }
     603           0 :         return result;
     604             :       }
     605             :     }
     606             : 
     607             :     /// \brief Returns the rewriter used by this prover (i.e. it returns Prover::f_rewriter).
     608           0 :     std::shared_ptr<detail::Rewriter> get_rewriter()
     609             :     {
     610           0 :       return m_rewriter;
     611             :     }
     612             : 
     613             :     /// \brief Sets Prover::f_formula to formula.
     614             :     /// precondition: the argument passed as parameter formula is an expression of sort Bool
     615          81 :     void set_formula(const data_expression& formula)
     616             :     {
     617          81 :       f_formula = formula;
     618          81 :       f_processed = false;
     619          81 :       mCRL2log(log::debug) << "The formula has been set." << std::endl;
     620          81 :     }
     621             : 
     622             : 
     623             : };
     624             : } // namespace detail
     625             : } // namespace data
     626             : } // namespace mcrl2
     627             : 
     628             : #endif

Generated by: LCOV version 1.13