12#ifndef MCRL2_DATA_DETAIL_BDD_PROVER_H
13#define MCRL2_DATA_DETAIL_BDD_PROVER_H
139 std::unordered_map < data_expression, data_expression >
f_smallest;
162 mCRL2log(
log::trace) <<
"Formula rewritten and oriented: " << intermediate_bdd << std::endl;
164 while (v_previous_1 != intermediate_bdd && v_previous_2 != intermediate_bdd)
166 v_previous_2 = v_previous_1;
167 v_previous_1 = intermediate_bdd;
168 intermediate_bdd =
bdd_down(intermediate_bdd);
173 f_bdd = intermediate_bdd;
181 return std::string(n,
' ');
205 const abstraction& a = atermpp::down_cast<abstraction>(formula);
209 const std::unordered_map < data_expression, data_expression >::const_iterator i =
f_formula_to_bdd.find(formula);
216 bool success =
smallest(formula, v_guard);
226 const size_t extra_indent = a_indent + 2;
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);
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);
251 time_t v_new_time_limit;
253 v_new_time_limit =
f_deadline - time(
nullptr);
257 f_bdd_simplifier->set_time_limit((std::max)(v_new_time_limit, time(
nullptr)));
290 f_bdd = v_original_bdd;
307 f_bdd = v_original_bdd;
375 const std::unordered_map < data_expression, data_expression >::const_iterator i =
f_smallest.find(formula);
382 bool result_is_defined=
false;
384 for (
const data_expression& arg: atermpp::down_cast<application>(formula))
386 bool success =
smallest(arg,v_small);
389 if (result_is_defined)
399 result_is_defined=
true;
408 if (result_is_defined)
425 bool success =
get_branch(v_true_branch, a_polarity, result);
433 success =
get_branch(v_false_branch, a_polarity, result);
469 int a_time_limit = 0,
470 bool a_path_eliminator =
false,
472 bool a_apply_induction =
false)
473 :
rewriter(data_spec, equations_selector, a_rewrite_strategy),
480 switch (a_rewrite_strategy)
483#ifdef MCRL2_ENABLE_JITTYC
484 case(jitty_compiling):
491#ifdef MCRL2_ENABLE_JITTYC
492 case(jitty_compiling_prover):
495 throw mcrl2::runtime_error(
"The proving rewriters are not supported by the prover (only jitty and jittyc are supported).");
505 <<
" Reverse: " << std::boolalpha <<
f_reverse <<
"," << std::endl
506 <<
" Full: " <<
f_full <<
"," << std::endl;
574 mCRL2log(
log::debug) <<
"The formula is satisfiable, but not a tautology." << std::endl;
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.");
602 mCRL2log(
log::debug) <<
"The formula is satisfiable, but not a tautology." << std::endl;
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.");
BDD inconsistent path elimination using external SMT solvers.
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
const binder_type & binding_operator() const
std::shared_ptr< detail::Rewriter > m_rewriter
The wrapped Rewriter.
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.
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.
static bool is_false(const data_expression &a_bdd)
Method that indicates whether or not a BDD equals false.
static const mcrl2::data::data_expression & get_guard(const mcrl2::data::data_expression &a_bdd)
Method that returns the guard of a BDD.
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.
static bool is_true(const data_expression &a_bdd)
Method that indicates whether or not a BDD equals true.
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.
Induction f_induction
Class that creates all statements needed to prove a given property using induction.
strategy rewriter_strategy() const
Returns the strategy of the rewriter used inside this proving rewriter.
std::shared_ptr< BDD_Simplifier > f_bdd_simplifier
Class that simplifies a BDD.
static constexpr bool f_reverse
Flag indicating whether or not the result of the comparison between the first two arguments.
void set_substitution(substitution_type &sigma)
Set the substitution to be used to construct the BDD.
void set_formula(const data_expression &formula)
Sets Prover::f_formula to formula. precondition: the argument passed as parameter formula is an expre...
std::string indent(size_t n)
bool smallest(const data_expression &formula, data_expression &result)
Returns the smallest guard in the formula formula.
data_expression f_bdd
A binary decision diagram in the internal representation of mCRL2.
const Info f_info
A class that provides information about expressions.
data_expression bdd_down(const data_expression &formula, const size_t a_indent=0)
Creates the EQ-BDD corresponding to the formula formula.
static constexpr bool f_full
Flag indicating whether or not the arguments of equality functions are taken into account.
void eliminate_paths()
Removes all inconsistent paths from the BDD BDD_Prover::f_bdd.
BDD_Prover(const rewriter &r, int time_limit=0, bool apply_induction=false)
data_expression get_counter_example()
Returns all the guards on a path in the BDD that leads to a leaf labelled "false",...
rewriter::substitution_type substitution_type
substitution_type bdd_sigma
A binary decision diagram in the internal representation of the rewriter.
Answer f_tautology
A flag that indicates whether or not the formala Prover::f_formula is a tautology.
Answer is_contradiction()
Indicates whether or not the formula Prover::f_formula is a contradiction.
data_expression f_formula
An expression of sort Bool.
time_t f_deadline
A timestamp representing the moment when the maximal amount of seconds has been spent on processing t...
bool f_processed
A flag that indicates whether or not the formala Prover::f_formula has been processed.
~BDD_Prover()
Destructor that destroys the BDD simplifier BDD_Prover::f_bdd_simplifier.
const int f_time_limit
An integer representing the maximal amount of seconds to be spent on processing a formula.
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)
void update_answers()
Updates the values of Prover::f_tautology and Prover::f_contradiction.
std::shared_ptr< detail::Rewriter > get_rewriter()
Returns the rewriter used by this prover (i.e. it returns Prover::f_rewriter).
Manipulator f_manipulator
A class that can be used to manipulate expressions.
bool f_apply_induction
A flag indicating whether or not induction on lists is applied.
void build_bdd()
Constructs the EQ-BDD corresponding to the formula Prover::f_formula.
std::unordered_map< data_expression, data_expression > f_smallest
A hashtable that maps formulas to the smallest guard occuring in those formulas.
Answer f_contradiction
A flag that indicates whether or not the formala Prover::f_formula is a contradiction.
std::unordered_map< data_expression, data_expression > f_formula_to_bdd
A data specification.
data_expression get_bdd()
Returns the BDD BDD_Prover::f_bdd.
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...
void set_substitution_internal(substitution_type &sigma)
Set the substitution in internal format to be used to construct the BDD.
Answer is_tautology()
Indicates whether or not the formula Prover::f_formula is a tautology.
A base class for simplifying binary decision diagrams.
The class Induction generates statements corresponding to.
bool can_apply_induction() const
void initialize(const data_expression &a_formula)
data_expression apply_induction()
\requires can_apply_induction()
Base class for classes that provide information about the structure of.
Compare_Result compare_guard(const data_expression &guard1, const data_expression &guard2) const
Compares two guards.
Base class for classes that provide functionality to modify or create terms.
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.
void thread_initialise()
Initialises this rewriter with thread dependent information.
rewriter clone()
Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared...
basic_rewriter< data_expression >::substitution_type substitution_type
Component for selecting a subset of equations that are actually used in an encompassing specification...
Standard exception class for reporting runtime errors.
Proving with induction on lists.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
smt_solver_type
The enumeration type smt_solver_type enumerates all available SMT solvers.
Answer
A prover that uses EQ-BDDs.
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.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & not_()
Constructor for function symbol !.
const function_symbol & true_()
Constructor for function symbol true.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
rewrite_strategy
The strategy of the rewriter.
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...