mCRL2
Loading...
Searching...
No Matches
bdd_prover.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_DATA_DETAIL_BDD_PROVER_H
13#define MCRL2_DATA_DETAIL_BDD_PROVER_H
14
17
18namespace mcrl2
19{
20namespace data
21{
22namespace detail
23{
24
78{
82};
83
84
85class BDD_Prover: protected rewriter
86{
87 public:
89
90 private:
91
95 static constexpr bool f_reverse = true;
96
99 static constexpr bool f_full = true;
100
101 protected:
104
107
110
112 bool f_processed = false;
113
116
119
121 const int f_time_limit;
122
125
126 private:
129
131 // const data_specification& f_data_spec;
132
135 std::unordered_map < data_expression, data_expression > f_formula_to_bdd;
136
139 std::unordered_map < data_expression, data_expression > f_smallest;
140
142 std::shared_ptr<BDD_Simplifier> f_bdd_simplifier;
143
146
149 {
150 f_deadline = time(nullptr) + f_time_limit;
151
152 data_expression v_previous_1;
153 data_expression v_previous_2;
154
155 mCRL2log(log::debug) << "Formula: " << f_formula << std::endl;
156
157 data_expression intermediate_bdd = f_formula;
158
159 intermediate_bdd = m_rewriter->rewrite(intermediate_bdd,bdd_sigma);
160 intermediate_bdd = f_manipulator.orient(intermediate_bdd);
161
162 mCRL2log(log::trace) << "Formula rewritten and oriented: " << intermediate_bdd << std::endl;
163
164 while (v_previous_1 != intermediate_bdd && v_previous_2 != intermediate_bdd)
165 {
166 v_previous_2 = v_previous_1;
167 v_previous_1 = intermediate_bdd;
168 intermediate_bdd = bdd_down(intermediate_bdd);
169 mCRL2log(log::trace) << "End of iteration." << std::endl;
170 mCRL2log(log::trace) << "Intermediate BDD: " << intermediate_bdd << std::endl;
171 }
172
173 f_bdd = intermediate_bdd;
174 mCRL2log(log::debug) << "Resulting BDD: " << f_bdd << std::endl;
175
176 }
177
178 // Auxiliary function to deliver an indent of length n.
179 inline std::string indent(size_t n)
180 {
181 return std::string(n, ' ');
182 }
183
185 data_expression bdd_down(const data_expression& formula, const size_t a_indent=0)
186 {
187
188 if (f_time_limit != 0 && (f_deadline - time(nullptr)) <= 0)
189 {
190 mCRL2log(log::debug) << "The time limit has passed." << std::endl;
191 return formula;
192 }
193
194 if (formula==sort_bool::true_())
195 {
196 return formula;
197 }
198 if (formula==sort_bool::false_())
199 {
200 return formula;
201 }
202
203 if (is_abstraction(formula))
204 {
205 const abstraction& a = atermpp::down_cast<abstraction>(formula);
206 return abstraction(a.binding_operator(), a.variables(), bdd_down(a.body(), a_indent));
207 }
208
209 const std::unordered_map < data_expression, data_expression >::const_iterator i = f_formula_to_bdd.find(formula);
210 if (i!=f_formula_to_bdd.end()) // found
211 {
212 return i->second;
213 }
214
215 data_expression v_guard;
216 bool success = smallest(formula, v_guard);
217 if (!success)
218 {
219 return formula;
220 }
221 else
222 {
223 mCRL2log(log::trace) << indent(a_indent) << "Smallest guard: " << v_guard << std::endl;
224 }
225
226 const size_t extra_indent = a_indent + 2;
227
228 data_expression v_term1 = f_manipulator.set_true(formula, v_guard);
229 v_term1 = m_rewriter->rewrite(v_term1,bdd_sigma);
230 v_term1 = f_manipulator.orient(v_term1);
231 mCRL2log(log::trace) << indent(extra_indent) << "True-branch after rewriting and orienting: " << v_term1 << std::endl;
232 v_term1 = bdd_down(v_term1, extra_indent);
233 mCRL2log(log::trace) << indent(extra_indent) << "BDD of the true-branch: " << v_term1 << std::endl;
234
235 data_expression v_term2 = f_manipulator.set_false(formula, v_guard);
236 v_term2 = m_rewriter->rewrite(v_term2,bdd_sigma);
237 v_term2 = f_manipulator.orient(v_term2);
238 mCRL2log(log::trace) << indent(extra_indent) << "False-branch after rewriting and orienting: " << v_term2 << std::endl;
239 v_term2 = bdd_down(v_term2, extra_indent);
240 mCRL2log(log::trace) << indent(extra_indent) << "BDD of the false-branch: " << v_term2 << std::endl;
241
242 data_expression v_bdd = Manipulator::make_reduced_if_then_else(v_guard, v_term1, v_term2);
243 f_formula_to_bdd[formula]=v_bdd;
244
245 return v_bdd;
246 }
247
250 {
251 time_t v_new_time_limit;
252
253 v_new_time_limit = f_deadline - time(nullptr);
254 if (v_new_time_limit > 0 || f_time_limit == 0)
255 {
256 mCRL2log(log::debug) << "Simplifying the BDD:" << std::endl;
257 f_bdd_simplifier->set_time_limit((std::max)(v_new_time_limit, time(nullptr)));
258 f_bdd = f_bdd_simplifier->simplify(f_bdd);
259 mCRL2log(log::debug) << "Resulting BDD: " << f_bdd << std::endl;
260 }
261 }
262
265 {
266 if (!f_processed)
267 {
268 build_bdd();
270 data_expression v_original_formula = f_formula;
271 data_expression v_original_bdd = f_bdd;
273 {
274 f_induction.initialize(v_original_formula);
276 {
277 mCRL2log(log::debug) << "Applying induction." << std::endl;
279 build_bdd();
281 }
283 {
286 }
287 else
288 {
289 v_original_formula = sort_bool::not_(v_original_formula);
290 f_bdd = v_original_bdd;
291 f_induction.initialize(v_original_formula);
293 {
294 mCRL2log(log::debug) << "Applying induction on the negated formula." << std::endl;
296 build_bdd();
298 }
300 {
304 }
305 else
306 {
307 f_bdd = v_original_bdd;
310 }
311 }
312 }
313 else
314 {
316 {
319 }
320 else if (BDD_Info::is_false(f_bdd))
321 {
324 }
325 else
326 {
329 }
330 }
331 f_processed = true;
332 }
333 };
334
336 bool smallest(const data_expression& formula, data_expression& result)
337 {
338 if (is_machine_number(formula))
339 {
340 return false;
341 }
342 if (is_variable(formula))
343 {
344 if (formula.sort()==sort_bool::bool_())
345 {
346 result=formula;
347 return true;
348 }
349 else
350 {
351 return false;
352 }
353 }
354 if (is_function_symbol(formula))
355 {
356 if (formula.sort()==sort_bool::bool_() && !(formula==sort_bool::true_() || formula==sort_bool::false_()))
357 {
358 result=formula;
359 return true;
360 }
361 else
362 {
363 return false;
364 }
365 }
366 if (is_abstraction(formula))
367 {
368 // Guards from within an abstraction may contain
369 // variables that are not bound outside that abstraction.
370 // Therefore, we never return a smallest guard from
371 // within an abstraction.
372 return false;
373 }
374
375 const std::unordered_map < data_expression, data_expression >::const_iterator i = f_smallest.find(formula);
376 if (i!=f_smallest.end()) //found
377 {
378 result=i->second;
379 return true;
380 }
381
382 bool result_is_defined=false;
383 data_expression v_small;
384 for (const data_expression& arg: atermpp::down_cast<application>(formula))
385 {
386 bool success = smallest(arg,v_small);
387 if (success)
388 {
389 if (result_is_defined)
390 {
391 if (f_info.compare_guard(v_small, result) == compare_result_smaller)
392 {
393 result = v_small;
394 }
395 }
396 else
397 {
398 result = v_small;
399 result_is_defined=true;
400 }
401 }
402 }
403 if (!result_is_defined && formula.sort()==sort_bool::bool_())
404 {
405 result = formula;
406 return true;
407 }
408 if (result_is_defined)
409 {
410 f_smallest[formula]=result; // Save the result in the cache
411 return true;
412 }
413
414 return false;
415 }
416
418 bool get_branch(const data_expression& a_bdd, const bool a_polarity, data_expression& result)
419 {
420 if (BDD_Info::is_if_then_else(a_bdd))
421 {
422 const data_expression& v_guard = BDD_Info::get_guard(a_bdd);
423 const data_expression& v_true_branch = BDD_Info::get_true_branch(a_bdd);
424 const data_expression& v_false_branch = BDD_Info::get_false_branch(a_bdd);
425 bool success = get_branch(v_true_branch, a_polarity, result);
426 if (success)
427 {
428 result = lazy::and_(result, v_guard);
429 return true;
430 }
431 else
432 {
433 success = get_branch(v_false_branch, a_polarity, result);
434 if (success)
435 {
436 result = lazy::and_(result, sort_bool::not_(v_guard));
437 return true;
438 }
439 else
440 {
441 return false;
442 }
443 }
444 }
445 else
446 {
447 if ((BDD_Info::is_true(a_bdd) && a_polarity) || (BDD_Info::is_false(a_bdd) && !a_polarity))
448 {
449 result = sort_bool::true_();
450 return true;
451 }
452 return false;
453 }
454 }
455
456 protected:
457
460
463 public:
464
466 const data_specification& data_spec,
467 const used_data_equation_selector& equations_selector,
469 int a_time_limit = 0,
470 bool a_path_eliminator = false,
471 smt_solver_type a_solver_type = solver_type_cvc,
472 bool a_apply_induction = false)
473 : rewriter(data_spec, equations_selector, a_rewrite_strategy),
474 f_time_limit(a_time_limit),
475 f_apply_induction(a_apply_induction),
476 f_bdd_simplifier(a_path_eliminator ? std::shared_ptr<BDD_Simplifier>(new BDD_Path_Eliminator(a_solver_type)) :
477 std::shared_ptr<BDD_Simplifier>(new BDD_Simplifier()))
478 {
480 switch (a_rewrite_strategy)
481 {
482 case(jitty):
483#ifdef MCRL2_ENABLE_JITTYC
484 case(jitty_compiling):
485#endif
486 {
487 /* These provers are ok */
488 break;
489 }
490 case(jitty_prover):
491#ifdef MCRL2_ENABLE_JITTYC
492 case(jitty_compiling_prover):
493#endif
494 {
495 throw mcrl2::runtime_error("The proving rewriters are not supported by the prover (only jitty and jittyc are supported).");
496 }
497 default:
498 {
499 throw mcrl2::runtime_error("Unknown type of rewriter.");
500 break;
501 }
502 }
503
504 mCRL2log(log::debug) << "Flags:" << std::endl
505 << " Reverse: " << std::boolalpha << f_reverse << "," << std::endl
506 << " Full: " << f_full << "," << std::endl;
507 }
508
509 BDD_Prover(const rewriter& r, int time_limit = 0, bool apply_induction = false)
510 : rewriter(r),
511 f_time_limit(time_limit),
512 f_apply_induction(apply_induction),
514 {
516 }
517
520 {
521 // delete f_bdd_simplifier;
522 // f_bdd_simplifier = nullptr;
523 }
524
527 {
529 }
530
533 {
535 }
536
539 {
541 return f_tautology;
542 }
543
546 {
548 return f_contradiction;
549 }
550
553 {
555 return f_bdd;
556 }
557
560 {
563 {
564 mCRL2log(log::debug) << "The formula is a contradiction." << std::endl;
565 return sort_bool::true_();
566 }
567 else if (is_tautology() == answer_yes)
568 {
569 mCRL2log(log::debug) << "The formula is a tautology." << std::endl;
570 return sort_bool::false_();
571 }
572 else
573 {
574 mCRL2log(log::debug) << "The formula is satisfiable, but not a tautology." << std::endl;
575 data_expression result;
576 bool success = get_branch(f_bdd, true, result);
577 if (!success)
578 { throw mcrl2::runtime_error(
579 "Cannot provide witness. This is probably caused by an abrupt stop of the\n"
580 "conversion from expression to EQ-BDD. This typically occurs when a time limit is set.");
581 }
582 return result;
583 }
584 }
585
588 {
591 {
592 mCRL2log(log::debug) << "The formula is a contradiction." << std::endl;
593 return sort_bool::false_();
594 }
595 else if (is_tautology() == answer_yes)
596 {
597 mCRL2log(log::debug) << "The formula is a tautology." << std::endl;
598 return sort_bool::true_();
599 }
600 else
601 {
602 mCRL2log(log::debug) << "The formula is satisfiable, but not a tautology." << std::endl;
603 data_expression result;
604 bool success=get_branch(f_bdd, false,result);
605 if (!success)
606 { throw mcrl2::runtime_error(
607 "Cannot provide counter example. This is probably caused by an abrupt stop of the\n"
608 "conversion from expression to EQ-BDD. This typically occurs when a time limit is set.");
609 }
610 return result;
611 }
612 }
613
615 std::shared_ptr<detail::Rewriter> get_rewriter()
616 {
617 return m_rewriter;
618 }
619
622 {
623 return m_rewriter->getStrategy();
624 }
625
628 void set_formula(const data_expression& formula)
629 {
630 f_formula = formula;
631 f_processed = false;
632 mCRL2log(log::debug) << "The formula has been set." << std::endl;
633 }
634
636 {
637 return BDD_Prover(rewriter::clone());
638 }
639
641 {
643 }
644
645
646};
647} // namespace detail
648} // namespace data
649} // namespace mcrl2
650
651#endif
BDD inconsistent path elimination using external SMT solvers.
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
const binder_type & binding_operator() const
Definition abstraction.h:58
std::shared_ptr< detail::Rewriter > m_rewriter
The wrapped Rewriter.
Definition rewriter.h:36
static const mcrl2::data::data_expression & get_true_branch(const mcrl2::data::data_expression &a_bdd)
Method that returns the true-branch of a BDD.
Definition bdd_info.h:50
static bool is_if_then_else(const data_expression &a_bdd)
Method that indicates wether or not the root of a BDD is a guard node.
Definition bdd_info.h:85
static bool is_false(const data_expression &a_bdd)
Method that indicates whether or not a BDD equals false.
Definition bdd_info.h:76
static const mcrl2::data::data_expression & get_guard(const mcrl2::data::data_expression &a_bdd)
Method that returns the guard of a BDD.
Definition bdd_info.h:42
static const mcrl2::data::data_expression & get_false_branch(const mcrl2::data::data_expression &a_bdd)
Method that returns the false-branch of a BDD.
Definition bdd_info.h:58
static bool is_true(const data_expression &a_bdd)
Method that indicates whether or not a BDD equals true.
Definition bdd_info.h:67
Base class for eliminating inconsistent paths from BDDs.
bool get_branch(const data_expression &a_bdd, const bool a_polarity, data_expression &result)
Returns branch of the BDD a_bdd, depending on the polarity a_polarity.
Definition bdd_prover.h:418
Induction f_induction
Class that creates all statements needed to prove a given property using induction.
Definition bdd_prover.h:145
strategy rewriter_strategy() const
Returns the strategy of the rewriter used inside this proving rewriter.
Definition bdd_prover.h:621
std::shared_ptr< BDD_Simplifier > f_bdd_simplifier
Class that simplifies a BDD.
Definition bdd_prover.h:142
static constexpr bool f_reverse
Flag indicating whether or not the result of the comparison between the first two arguments.
Definition bdd_prover.h:95
void set_substitution(substitution_type &sigma)
Set the substitution to be used to construct the BDD.
Definition bdd_prover.h:526
void set_formula(const data_expression &formula)
Sets Prover::f_formula to formula. precondition: the argument passed as parameter formula is an expre...
Definition bdd_prover.h:628
std::string indent(size_t n)
Definition bdd_prover.h:179
bool smallest(const data_expression &formula, data_expression &result)
Returns the smallest guard in the formula formula.
Definition bdd_prover.h:336
data_expression f_bdd
A binary decision diagram in the internal representation of mCRL2.
Definition bdd_prover.h:462
const Info f_info
A class that provides information about expressions.
Definition bdd_prover.h:106
data_expression bdd_down(const data_expression &formula, const size_t a_indent=0)
Creates the EQ-BDD corresponding to the formula formula.
Definition bdd_prover.h:185
static constexpr bool f_full
Flag indicating whether or not the arguments of equality functions are taken into account.
Definition bdd_prover.h:99
void eliminate_paths()
Removes all inconsistent paths from the BDD BDD_Prover::f_bdd.
Definition bdd_prover.h:249
BDD_Prover(const rewriter &r, int time_limit=0, bool apply_induction=false)
Definition bdd_prover.h:509
data_expression get_counter_example()
Returns all the guards on a path in the BDD that leads to a leaf labelled "false",...
Definition bdd_prover.h:587
rewriter::substitution_type substitution_type
Definition bdd_prover.h:88
substitution_type bdd_sigma
A binary decision diagram in the internal representation of the rewriter.
Definition bdd_prover.h:459
Answer f_tautology
A flag that indicates whether or not the formala Prover::f_formula is a tautology.
Definition bdd_prover.h:115
Answer is_contradiction()
Indicates whether or not the formula Prover::f_formula is a contradiction.
Definition bdd_prover.h:545
data_expression f_formula
An expression of sort Bool.
Definition bdd_prover.h:103
time_t f_deadline
A timestamp representing the moment when the maximal amount of seconds has been spent on processing t...
Definition bdd_prover.h:124
bool f_processed
A flag that indicates whether or not the formala Prover::f_formula has been processed.
Definition bdd_prover.h:112
~BDD_Prover()
Destructor that destroys the BDD simplifier BDD_Prover::f_bdd_simplifier.
Definition bdd_prover.h:519
const int f_time_limit
An integer representing the maximal amount of seconds to be spent on processing a formula.
Definition bdd_prover.h:121
BDD_Prover(const data_specification &data_spec, const used_data_equation_selector &equations_selector, mcrl2::data::rewriter::strategy a_rewrite_strategy=mcrl2::data::jitty, int a_time_limit=0, bool a_path_eliminator=false, smt_solver_type a_solver_type=solver_type_cvc, bool a_apply_induction=false)
Definition bdd_prover.h:465
void update_answers()
Updates the values of Prover::f_tautology and Prover::f_contradiction.
Definition bdd_prover.h:264
std::shared_ptr< detail::Rewriter > get_rewriter()
Returns the rewriter used by this prover (i.e. it returns Prover::f_rewriter).
Definition bdd_prover.h:615
Manipulator f_manipulator
A class that can be used to manipulate expressions.
Definition bdd_prover.h:109
bool f_apply_induction
A flag indicating whether or not induction on lists is applied.
Definition bdd_prover.h:128
void build_bdd()
Constructs the EQ-BDD corresponding to the formula Prover::f_formula.
Definition bdd_prover.h:148
std::unordered_map< data_expression, data_expression > f_smallest
A hashtable that maps formulas to the smallest guard occuring in those formulas.
Definition bdd_prover.h:139
Answer f_contradiction
A flag that indicates whether or not the formala Prover::f_formula is a contradiction.
Definition bdd_prover.h:118
std::unordered_map< data_expression, data_expression > f_formula_to_bdd
A data specification.
Definition bdd_prover.h:135
data_expression get_bdd()
Returns the BDD BDD_Prover::f_bdd.
Definition bdd_prover.h:552
data_expression get_witness()
Returns all the guards on a path in the BDD that leads to a leaf labelled "true", if such a leaf exis...
Definition bdd_prover.h:559
void set_substitution_internal(substitution_type &sigma)
Set the substitution in internal format to be used to construct the BDD.
Definition bdd_prover.h:532
Answer is_tautology()
Indicates whether or not the formula Prover::f_formula is a tautology.
Definition bdd_prover.h:538
A base class for simplifying binary decision diagrams.
The class Induction generates statements corresponding to.
Definition induction.h:29
void initialize(const data_expression &a_formula)
Definition induction.h:167
data_expression apply_induction()
\requires can_apply_induction()
Definition induction.h:180
Base class for classes that provide information about the structure of.
Definition info.h:35
Compare_Result compare_guard(const data_expression &guard1, const data_expression &guard2) const
Compares two guards.
Definition info.h:188
Base class for classes that provide functionality to modify or create terms.
Definition manipulator.h:27
data_expression orient(const data_expression &a_term)
Orients the term a_term such that all equations of the form t1 == t2 are.
data_expression set_true(const data_expression &a_formula, const data_expression &a_guard) const
Initializes the table Manipulator::f_set_true and calls.
data_expression set_false(const data_expression &a_formula, const data_expression &a_guard) const
Initializes the table Manipulator::f_set_false and calls the method.
static data_expression make_reduced_if_then_else(const data_expression &a_expr, const data_expression &a_high, const data_expression &a_low)
Returns an expression in the internal format of the rewriter with the jitty strategy.
A strategy is a list of rules and the number of variables that occur in it.
Rewriter that operates on data expressions.
Definition rewriter.h:81
void thread_initialise()
Initialises this rewriter with thread dependent information.
Definition rewriter.h:150
rewriter clone()
Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared...
Definition rewriter.h:140
basic_rewriter< data_expression >::substitution_type substitution_type
Definition rewriter.h:114
Component for selecting a subset of equations that are actually used in an encompassing specification...
Definition selection.h:37
Standard exception class for reporting runtime errors.
Definition exception.h:27
Proving with induction on lists.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
smt_solver_type
The enumeration type smt_solver_type enumerates all available SMT solvers.
Definition solver_type.h:27
Answer
A prover that uses EQ-BDDs.
Definition bdd_prover.h:78
@ compare_result_smaller
Definition info.h:27
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
rewrite_strategy
The strategy of the rewriter.
@ jitty_prover
JITty.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.