LCOV - code coverage report
Current view: top level - smt/source - basic_data_specification.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 469 0.0 %
Date: 2019-06-19 00:50:04 Functions: 0 20 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Ruud Koolen
       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             : #include <queue>
      10             : #include <vector>
      11             : 
      12             : #include "mcrl2/data/join.h"
      13             : #include "mcrl2/data/list.h"
      14             : #include "mcrl2/data/standard.h"
      15             : #include "mcrl2/data/rewriter.h"
      16             : #include "mcrl2/smt/basic_data_specification.h"
      17             : #include "mcrl2/smt/identity_function_definition.h"
      18             : #include "mcrl2/smt/recursive_function_definition.h"
      19             : #include "mcrl2/smt/translation_error.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace smt
      25             : {
      26             : 
      27           0 : template<class T> std::vector<T> topological_sort(std::map<T, std::set<T> > dependencies)
      28             : {
      29           0 :   std::queue<T> vertices_without_dependencies;
      30           0 :   std::map<T, std::set<T> > reverse_dependencies;
      31           0 :   for (typename std::map<T, std::set<T> >::const_iterator i = dependencies.begin(); i != dependencies.end(); i++)
      32             :   {
      33           0 :     for (typename std::set<T>::const_iterator j = i->second.begin(); j != i->second.end(); j++)
      34             :     {
      35           0 :       reverse_dependencies[*j].insert(i->first);
      36             :     }
      37             : 
      38           0 :     if (i->second.empty())
      39             :     {
      40           0 :       vertices_without_dependencies.push(i->first);
      41             :     }
      42             :   }
      43             : 
      44           0 :   std::vector<T> output;
      45           0 :   output.reserve(dependencies.size());
      46             : 
      47           0 :   while (!vertices_without_dependencies.empty())
      48             :   {
      49           0 :     T vertex = vertices_without_dependencies.front();
      50           0 :     vertices_without_dependencies.pop();
      51           0 :     output.push_back(vertex);
      52             : 
      53           0 :     const std::set<T> &edges = reverse_dependencies[vertex];
      54           0 :     for (typename std::set<T>::const_iterator i = edges.begin(); i != edges.end(); i++)
      55             :     {
      56           0 :       dependencies[*i].erase(vertex);
      57           0 :       if (dependencies[*i].empty())
      58             :       {
      59           0 :         vertices_without_dependencies.push(*i);
      60             :       }
      61             :     }
      62             :   }
      63             : 
      64           0 :   if (output.size() != dependencies.size())
      65             :   {
      66           0 :     for (typename std::vector<T>::const_iterator i = output.begin(); i != output.end(); i++)
      67             :     {
      68           0 :       dependencies.erase(*i);
      69             :     }
      70           0 :     assert(!dependencies.empty());
      71             :     //TODO: SMT2.5 format supports mutually recursive functions
      72           0 :     throw translation_error("Dependency loop trying to resolve dependencies for " + data::pp(dependencies.begin()->first));
      73             :   }
      74             :   else
      75             :   {
      76           0 :     return output;
      77             :   }
      78             : }
      79             : 
      80           0 : basic_data_specification::basic_data_specification(const data::data_specification& data_specification, std::shared_ptr<data::set_identifier_generator> identifier_generator):
      81             :   m_data_specification(data_specification),
      82             :   m_identifier_generator(identifier_generator),
      83           0 :   m_representative_generator(data_specification)
      84             : {
      85           0 :   find_rewrite_rules(data_specification);
      86           0 : }
      87             : 
      88           0 : std::string basic_data_specification::generate_data_expression(const std::map<data::variable, std::string>& declared_variables, const data::data_expression& expression) const
      89             : {
      90           0 :   if (data::is_variable(expression))
      91             :   {
      92           0 :     data::variable variable(expression);
      93           0 :     if (!declared_variables.count(variable))
      94             :     {
      95           0 :       throw translation_error("Undeclared variable: " + data::pp(expression));
      96             :     }
      97           0 :     return declared_variables.at(variable);
      98             :   }
      99           0 :   else if (data::is_application(expression) || data::is_function_symbol(expression))
     100             :   {
     101           0 :     data::function_symbol function;
     102           0 :     data::data_expression_vector arguments;
     103             : 
     104           0 :     if (data::is_application(expression))
     105             :     {
     106           0 :       data::application application(expression);
     107           0 :       if (data::is_function_symbol(application.head()))
     108             :       {
     109           0 :         function = data::function_symbol(application.head());
     110             :       }
     111             :       else
     112             :       {
     113           0 :         throw translation_error("Application " + data::pp(expression) + " does not have a function symbol as its head");
     114             :       }
     115           0 :       arguments.insert(arguments.end(), application.begin(), application.end());
     116             :     }
     117             :     else
     118             :     {
     119           0 :       function = data::function_symbol(expression);
     120             :     }
     121             : 
     122           0 :     if (!m_functions.count(function))
     123             :     {
     124           0 :       throw translation_error("Untranslatable function symbol " + data::pp(function));
     125             :     }
     126           0 :     return m_functions.at(function)->generate_data_expression(declared_variables, arguments);
     127             :   }
     128             :   else
     129             :   {
     130           0 :     throw translation_error("Unsupported expression " + data::pp(expression));
     131             :   }
     132             : }
     133             : 
     134           0 : std::string basic_data_specification::generate_data_specification() const
     135             : {
     136           0 :   std::queue<data::function_symbol> function_queue;
     137           0 :   for (const std::pair<data::function_symbol, std::shared_ptr<function_definition>>& function: m_functions)
     138             :   {
     139             :     // Check whether the function symbol is actually present in the data specification
     140           0 :     if(std::find(m_data_specification.mappings().begin(), m_data_specification.mappings().end(), function.first) != m_data_specification.mappings().end())
     141             :     {
     142           0 :       function_queue.push(function.first);
     143             :     }
     144             :   }
     145           0 :   for (const data::function_symbol& function: m_data_specification.user_defined_mappings())
     146             :   {
     147           0 :     function_queue.push(function);
     148             :   }
     149           0 :   std::map<data::function_symbol, std::set<data::function_symbol> > function_dependencies;
     150           0 :   while (!function_queue.empty())
     151             :   {
     152           0 :     data::function_symbol function = function_queue.front();
     153           0 :     function_queue.pop();
     154           0 :     if (!m_functions.count(function))
     155             :     {
     156           0 :       throw translation_error("Untranslated function " + atermpp::pp(function));
     157             :     }
     158             : 
     159           0 :     const std::set<data::function_symbol>& dependencies = m_functions.at(function)->function_dependencies();
     160           0 :     function_dependencies[function] = dependencies;
     161           0 :     function_dependencies[function].erase(function);
     162             : 
     163           0 :     for (std::set<data::function_symbol>::const_iterator i = dependencies.begin(); i != dependencies.end(); i++)
     164             :     {
     165           0 :       if (!function_dependencies.count(*i))
     166             :       {
     167           0 :         function_queue.push(*i);
     168             :       }
     169             :     }
     170             :   }
     171             : 
     172           0 :   std::queue<data::sort_expression> sort_queue;
     173           0 :   for (const std::pair<data::sort_expression, std::shared_ptr<sort_definition>>& sort: m_sorts)
     174             :   {
     175             :     // Check whether the sort is actually present in the data specification
     176           0 :     if(std::find(m_data_specification.sorts().begin(), m_data_specification.sorts().end(), sort.first) != m_data_specification.sorts().end())
     177             :     {
     178           0 :       sort_queue.push(sort.first);
     179             :     }
     180             :   }
     181           0 :   for (const data::sort_expression& sort: m_data_specification.user_defined_sorts())
     182             :   {
     183           0 :     sort_queue.push(sort);
     184             :   }
     185           0 :   std::map<data::sort_expression, std::set<data::sort_expression> > sort_dependencies;
     186           0 :   while (!sort_queue.empty())
     187             :   {
     188           0 :     data::sort_expression sort = sort_queue.front();
     189           0 :     sort_queue.pop();
     190           0 :     if (!m_sorts.count(sort))
     191             :     {
     192           0 :       throw translation_error("Untranslated sort " + data::pp(sort));
     193             :     }
     194             : 
     195           0 :     const std::set<data::sort_expression>& dependencies = m_sorts.at(sort)->sort_dependencies();
     196           0 :     sort_dependencies[sort] = dependencies;
     197           0 :     sort_dependencies[sort].erase(sort);
     198           0 :     for (std::set<data::sort_expression>::const_iterator i = dependencies.begin(); i != dependencies.end(); i++)
     199             :     {
     200           0 :       if (!sort_dependencies.count(*i))
     201             :       {
     202           0 :         sort_queue.push(*i);
     203             :       }
     204             :     }
     205             :   }
     206             : 
     207           0 :   std::vector<data::sort_expression> sort_order = topological_sort(sort_dependencies);
     208           0 :   std::vector<data::function_symbol> function_order = topological_sort(function_dependencies);
     209             : 
     210           0 :   std::string output;
     211           0 :   for (std::vector<data::sort_expression>::const_iterator i = sort_order.begin(); i != sort_order.end(); i++)
     212             :   {
     213           0 :     assert(m_sorts.count(*i));
     214           0 :     output += m_sorts.at(*i)->generate_definition();
     215             :   }
     216           0 :   for (std::vector<data::function_symbol>::const_iterator i = function_order.begin(); i != function_order.end(); i++)
     217             :   {
     218           0 :     assert(m_functions.count(*i));
     219           0 :     output += m_functions.at(*i)->generate_definition();
     220             :   }
     221           0 :   return output;
     222             : }
     223             : 
     224           0 : std::string basic_data_specification::generate_smt_problem(const smt_problem& problem)
     225             : {
     226           0 :   std::string variable_declarations;
     227           0 :   std::string assertions;
     228             : 
     229             :   class identifier_storage: public std::set<core::identifier_string>
     230             :   {
     231             :     public:
     232             :       data::set_identifier_generator& m_generator;
     233           0 :       identifier_storage(data::set_identifier_generator& generator):
     234           0 :         m_generator(generator)
     235           0 :       {}
     236             : 
     237           0 :       ~identifier_storage()
     238           0 :       {
     239           0 :         m_generator.remove_identifiers(*this);
     240           0 :       }
     241             :   };
     242           0 :   identifier_storage variable_identifiers(identifier_generator());
     243           0 :   std::map<data::variable, std::string> declared_variables;
     244             : 
     245           0 :   for (std::set<data::variable>::const_iterator i = problem.variables().begin(); i != problem.variables().end(); i++)
     246             :   {
     247           0 :     core::identifier_string name = identifier_generator()(i->name());
     248           0 :     variable_identifiers.insert(name);
     249           0 :     declared_variables[*i] = name;
     250             : 
     251           0 :     if (!m_sorts.count(i->sort()))
     252             :     {
     253           0 :       throw translation_error("Untranslated sort " + data::pp(*i));
     254             :     }
     255           0 :     variable_declarations += m_sorts.at(i->sort())->generate_variable_declaration(name);
     256             :   }
     257             : 
     258           0 :   for (std::set<data::data_expression>::const_iterator i = problem.assertions().begin(); i != problem.assertions().end(); i++)
     259             :   {
     260           0 :     assertions += generate_assertion(declared_variables, *i);
     261             :   }
     262             : 
     263           0 :   for (std::set<data::data_expression_list>::const_iterator i = problem.distinct_assertions().begin(); i != problem.distinct_assertions().end(); i++)
     264             :   {
     265           0 :     if (i->size() == 0 || i->size() == 1)
     266             :     {
     267           0 :       continue;
     268             :     }
     269             : 
     270           0 :     assertions += generate_distinct_assertion(declared_variables, *i);
     271             :   }
     272             : 
     273           0 :   return generate_smt_problem(variable_declarations, assertions);
     274             : }
     275             : 
     276           0 : std::string basic_data_specification::generate_distinct_assertion(const std::map<data::variable, std::string>& declared_variables, const data::data_expression_list& distinct_terms) const
     277             : {
     278           0 :   std::string output;
     279           0 :   for (data::data_expression_list::const_iterator i = distinct_terms.begin(); i != distinct_terms.end(); i++)
     280             :   {
     281           0 :     data::data_expression_list::const_iterator j = i;
     282           0 :     j++;
     283           0 :     for (; j != distinct_terms.end(); j++)
     284             :     {
     285           0 :       output += generate_assertion(declared_variables, data::not_equal_to(*i, *j));
     286             :     }
     287             :   }
     288           0 :   return output;
     289             : }
     290             : 
     291           0 : void basic_data_specification::find_rewrite_rules(const data::data_specification& data_specification)
     292             : {
     293           0 :   for (data::data_equation_vector::const_iterator i = data_specification.equations().begin(); i != data_specification.equations().end(); i++)
     294             :   {
     295           0 :     data::data_expression lhs = i->lhs();
     296           0 :     data::function_symbol function;
     297           0 :     if (data::is_application(lhs))
     298             :     {
     299           0 :       data::application application(lhs);
     300           0 :       if (data::is_function_symbol(application.head()))
     301             :       {
     302           0 :         function = data::function_symbol(application.head());
     303             :       }
     304             :       else
     305             :       {
     306           0 :         continue;
     307             :       }
     308             :     }
     309           0 :     else if (data::is_function_symbol(lhs))
     310             :     {
     311           0 :       function = data::function_symbol(lhs);
     312             :     }
     313             :     else
     314             :     {
     315           0 :       continue;
     316             :     }
     317             : 
     318           0 :     m_rewrite_rules[function].push_back(*i);
     319             :   }
     320             : 
     321             :   /*
     322             :    * For each mapping, find out whether it is a recogniser or projection function.
     323             :    */
     324           0 :   for (std::map<data::function_symbol, data::data_equation_vector>::const_iterator i = m_rewrite_rules.begin(); i != m_rewrite_rules.end(); i++)
     325             :   {
     326           0 :     if (!data::is_function_sort(i->first.sort()))
     327             :     {
     328           0 :       continue;
     329             :     }
     330           0 :     data::function_sort sort(i->first.sort());
     331           0 :     if (sort.domain().size() != 1)
     332             :     {
     333           0 :       continue;
     334             :     }
     335           0 :     data::sort_expression domain = sort.domain().front();
     336           0 :     data::function_symbol_vector constructor_vector = data_specification.constructors(domain);
     337           0 :     if (constructor_vector.empty())
     338             :     {
     339           0 :       continue;
     340             :     }
     341           0 :     std::set<data::function_symbol> constructors;
     342           0 :     constructors.insert(constructor_vector.begin(), constructor_vector.end());
     343             : 
     344             :     /*
     345             :      * Check for recognisers.
     346             :      */
     347           0 :     if (data::sort_bool::is_bool(sort.codomain()))
     348             :     {
     349           0 :       std::set<data::function_symbol> positive_recogniser_equation_seen;
     350           0 :       std::set<data::function_symbol> negative_recogniser_equation_seen;
     351           0 :       bool invalid_equations_seen = false;
     352           0 :       for (data::data_equation_vector::const_iterator j = i->second.begin(); j != i->second.end(); j++)
     353             :       {
     354           0 :         if (j->condition() != data::sort_bool::true_())
     355             :         {
     356           0 :           invalid_equations_seen = true;
     357           0 :           break;
     358             :         }
     359           0 :         if (!data::is_application(j->lhs()))
     360             :         {
     361           0 :           invalid_equations_seen = true;
     362           0 :           break;
     363             :         }
     364           0 :         data::application application(j->lhs());
     365           0 :         assert(application.head() == i->first);
     366           0 :         assert(application.size() == 1);
     367           0 :         data::data_expression argument(application[0]);
     368           0 :         data::function_symbol constructor;
     369           0 :         if (data::is_application(argument))
     370             :         {
     371           0 :           data::application constructor_application(argument);
     372           0 :           if (data::is_function_symbol(constructor_application.head()))
     373             :           {
     374           0 :             constructor = data::function_symbol(constructor_application.head());
     375             :           }
     376             :           else
     377             :           {
     378           0 :             invalid_equations_seen = true;
     379           0 :             break;
     380             :           }
     381           0 :           std::set<data::variable> arguments;
     382           0 :           for (data::application::const_iterator k = constructor_application.begin(); k != constructor_application.end(); k++)
     383             :           {
     384           0 :             if (data::is_variable(*k))
     385             :             {
     386           0 :               arguments.insert(data::variable(*k));
     387             :             }
     388             :             else
     389             :             {
     390           0 :               invalid_equations_seen = true;
     391           0 :               break;
     392             :             }
     393             :           }
     394           0 :           if (invalid_equations_seen)
     395             :           {
     396           0 :             break;
     397             :           }
     398           0 :           if (arguments.size() != constructor_application.size())
     399             :           {
     400           0 :             invalid_equations_seen = true;
     401           0 :             break;
     402             :           }
     403             :         }
     404           0 :         else if (data::is_function_symbol(argument))
     405             :         {
     406           0 :           constructor = data::function_symbol(argument);
     407             :         }
     408             :         else
     409             :         {
     410           0 :           invalid_equations_seen = true;
     411           0 :           break;
     412             :         }
     413           0 :         if (constructors.count(constructor) == 0)
     414             :         {
     415           0 :           invalid_equations_seen = true;
     416           0 :           break;
     417             :         }
     418             : 
     419           0 :         if (j->rhs() == data::sort_bool::true_())
     420             :         {
     421           0 :           positive_recogniser_equation_seen.insert(constructor);
     422           0 :           if (negative_recogniser_equation_seen.count(constructor) != 0)
     423             :           {
     424           0 :             invalid_equations_seen = true;
     425           0 :             break;
     426             :           }
     427             :         }
     428           0 :         else if (j->rhs() == data::sort_bool::false_())
     429             :         {
     430           0 :           negative_recogniser_equation_seen.insert(constructor);
     431           0 :           if (negative_recogniser_equation_seen.count(constructor) != 0)
     432             :           {
     433           0 :             invalid_equations_seen = true;
     434           0 :             break;
     435             :           }
     436             :         }
     437             :         else
     438             :         {
     439           0 :           invalid_equations_seen = true;
     440           0 :           break;
     441             :         }
     442             :       }
     443           0 :       if (!invalid_equations_seen &&
     444           0 :           positive_recogniser_equation_seen.size() == 1 &&
     445           0 :           positive_recogniser_equation_seen.size() + negative_recogniser_equation_seen.size() == constructors.size())
     446             :       {
     447           0 :         data::function_symbol constructor = *positive_recogniser_equation_seen.begin();
     448           0 :         m_all_recognisers[constructor].push_back(i->first);
     449             :       }
     450             :     }
     451             : 
     452             :     /*
     453             :      * Check for projections.
     454             :      */
     455           0 :     if (i->second.size() == 1)
     456             :     {
     457           0 :       data::data_equation equation = i->second[0];
     458           0 :       if (equation.condition() == data::sort_bool::true_() &&
     459           0 :           data::is_variable(equation.rhs()) &&
     460           0 :           data::is_application(equation.lhs()))
     461             :       {
     462           0 :         data::application application(equation.lhs());
     463           0 :         assert(application.head() == i->first);
     464           0 :         assert(application.size() == 1);
     465           0 :         data::data_expression argument(application[0]);
     466           0 :         if (data::is_application(argument) &&
     467           0 :             data::is_function_symbol(data::application(argument).head()) &&
     468           0 :             constructors.count(data::function_symbol(data::application(argument).head())) == 1)
     469             :         {
     470           0 :           data::application constructor_application(argument);
     471           0 :           data::function_symbol constructor(constructor_application.head());
     472           0 :           std::size_t index = 0;
     473           0 :           bool found = false;
     474           0 :           std::set<data::variable> arguments;
     475           0 :           for (data::application::const_iterator j = constructor_application.begin(); j != constructor_application.end(); j++)
     476             :           {
     477           0 :             if (!data::is_variable(*j))
     478             :             {
     479           0 :               break;
     480             :             }
     481           0 :             data::variable variable(*j);
     482           0 :             arguments.insert(variable);
     483           0 :             if (variable == equation.rhs())
     484             :             {
     485           0 :               found = true;
     486             :             }
     487           0 :             if (!found)
     488             :             {
     489           0 :               index++;
     490             :             }
     491             :           }
     492           0 :           if (found && arguments.size() == constructor_application.size())
     493             :           {
     494           0 :             m_all_projections[constructor][index].push_back(i->first);
     495             :           }
     496             :         }
     497             :       }
     498             :     }
     499             :   }
     500           0 : }
     501             : 
     502           0 : void basic_data_specification::add_constructed_sort(const data::data_specification& data_specification, const data::sort_expression& sort)
     503             : {
     504           0 :   m_constructed_sort_constructors[sort].insert(data_specification.constructors(sort).begin(), data_specification.constructors(sort).end());
     505             : 
     506           0 :   constructed_sort_definition::constructors_t constructor_specification;
     507           0 :   for (std::set<data::function_symbol>::const_iterator i = m_constructed_sort_constructors[sort].begin(); i != m_constructed_sort_constructors[sort].end(); i++)
     508             :   {
     509           0 :     constructor_specification.push_back(constructed_sort_definition::constructor_t());
     510           0 :     constructed_sort_definition::constructor_t& constructor = constructor_specification.back();
     511             : 
     512           0 :     constructor.constructor = *i;
     513           0 :     if (m_all_recognisers[*i].empty())
     514             :     {
     515           0 :       std::string name = std::string("recognise-") + std::string(i->name());
     516           0 :       m_all_recognisers[*i].push_back(data::function_symbol(identifier_generator()(name), data::make_function_sort(sort, data::sort_bool::bool_())));
     517             :     }
     518           0 :     constructor.recognisers = m_all_recognisers[*i];
     519           0 :     m_recognisers[*i] = constructor.recognisers[0];
     520             : 
     521           0 :     if (data::is_function_sort(i->sort()))
     522             :     {
     523           0 :       data::function_sort constructor_sort(i->sort());
     524           0 :       std::size_t index = 0;
     525           0 :       for (data::sort_expression_list::const_iterator j = constructor_sort.domain().begin(); j != constructor_sort.domain().end(); j++)
     526             :       {
     527           0 :         constructor.fields.push_back(constructed_sort_definition::field_t());
     528           0 :         constructed_sort_definition::field_t& field = constructor.fields.back();
     529             : 
     530           0 :         if (m_all_projections[*i][index].empty())
     531             :         {
     532           0 :           std::string name = std::string(i->name()) + "-field-" + std::to_string(index);
     533           0 :           m_all_projections[*i][index].push_back(data::function_symbol(identifier_generator()(name), data::make_function_sort(sort, *j)));
     534             :         }
     535           0 :         field.projections = m_all_projections[*i][index];
     536           0 :         m_projections[*i][index] = field.projections[0];
     537             : 
     538           0 :         index++;
     539             :       }
     540             :     }
     541             :   }
     542             : 
     543           0 :   constructed_sort_definition *definition = create_constructed_sort(sort, constructor_specification);
     544           0 :   add_sort_definition(sort, std::shared_ptr<sort_definition>(definition));
     545           0 : }
     546             : 
     547             : /*
     548             :  * TODO: This should be moved to the data library.
     549             :  */
     550           0 : static bool is_constructed_sort(const data::data_specification& data_specification, const data::sort_expression& sort)
     551             : {
     552           0 :   data::function_symbol_vector constructors = data_specification.constructors(sort);
     553           0 :   if (constructors.empty())
     554             :   {
     555           0 :     return false;
     556             :   }
     557             : 
     558           0 :   data::rewriter r(data_specification);
     559             : 
     560           0 :   for (data::function_symbol_vector::const_iterator i = constructors.begin(); i != constructors.end(); i++)
     561             :   {
     562           0 :     for (data::function_symbol_vector::const_iterator j = constructors.begin(); j != constructors.end(); j++)
     563             :     {
     564           0 :       std::size_t index = 1;
     565             : 
     566           0 :       data::variable_vector variables_i;
     567           0 :       data::data_expression term_i;
     568           0 :       if (data::is_function_sort(i->sort()))
     569             :       {
     570           0 :         data::function_sort sort(i->sort());
     571           0 :         for (data::sort_expression_list::const_iterator k = sort.domain().begin(); k != sort.domain().end(); k++)
     572             :         {
     573           0 :           variables_i.push_back(data::variable("v" + std::to_string(index++), *k));
     574             :         }
     575           0 :         term_i = data::application(*i, variables_i);
     576             :       }
     577             :       else
     578             :       {
     579           0 :         term_i = *i;
     580             :       }
     581             : 
     582           0 :       data::variable_vector variables_j;
     583           0 :       data::data_expression term_j;
     584           0 :       if (data::is_function_sort(j->sort()))
     585             :       {
     586           0 :         data::function_sort sort(j->sort());
     587           0 :         for (data::sort_expression_list::const_iterator k = sort.domain().begin(); k != sort.domain().end(); k++)
     588             :         {
     589           0 :           variables_j.push_back(data::variable("v" + std::to_string(index++), *k));
     590             :         }
     591           0 :         term_j = data::application(*j, variables_j);
     592             :       }
     593             :       else
     594             :       {
     595           0 :         term_j = *j;
     596             :       }
     597             : 
     598           0 :       data::data_expression equality = data::equal_to(term_i, term_j);
     599           0 :       data::data_expression result = r(equality);
     600             : 
     601           0 :       if (*i == *j)
     602             :       {
     603           0 :         std::set<data::data_expression> conjuncts = data::split_and(result);
     604           0 :         if (conjuncts.count(data::sort_bool::true_()))
     605             :         {
     606           0 :           conjuncts.erase(data::sort_bool::true_());
     607             :         }
     608             : 
     609           0 :         assert(variables_i.size() == variables_j.size());
     610           0 :         for (std::size_t k = 0; k < variables_i.size(); k++)
     611             :         {
     612           0 :           bool found = false;
     613           0 :           if (conjuncts.count(data::equal_to(variables_i[k], variables_j[k])))
     614             :           {
     615           0 :             conjuncts.erase(data::equal_to(variables_i[k], variables_j[k]));
     616           0 :             found = true;
     617             :           }
     618           0 :           if (conjuncts.count(data::equal_to(variables_j[k], variables_i[k])))
     619             :           {
     620           0 :             conjuncts.erase(data::equal_to(variables_j[k], variables_i[k]));
     621           0 :             found = true;
     622             :           }
     623           0 :           if (!found)
     624             :           {
     625           0 :             return false;
     626             :           }
     627             :         }
     628           0 :         if (!conjuncts.empty())
     629             :         {
     630           0 :           return false;
     631             :         }
     632             :       }
     633             :       else
     634             :       {
     635           0 :         if (result != data::sort_bool::false_())
     636             :         {
     637           0 :           return false;
     638             :         }
     639             :       }
     640             :     }
     641             :   }
     642             : 
     643           0 :   return true;
     644             : }
     645             : 
     646           0 : void basic_data_specification::add_constructed_sorts(const data::data_specification& data_specification)
     647             : {
     648           0 :   for (std::set<data::sort_expression>::const_iterator i = data_specification.sorts().begin(); i != data_specification.sorts().end(); i++)
     649             :   {
     650             :     /*
     651             :      * bool, pos, nat, and int are constructed sorts, but they are not translated as constructed sorts
     652             :      * but are instead mapped to solver-specific builtin sorts.
     653             :      */
     654           0 :     if (data::sort_bool::is_bool(*i) ||
     655           0 :         data::sort_pos::is_pos(*i) ||
     656           0 :         data::sort_nat::is_nat(*i) ||
     657           0 :         data::sort_int::is_int(*i))
     658             :     {
     659           0 :       continue;
     660             :     }
     661             : 
     662           0 :     if (m_sorts.count(*i))
     663             :     {
     664           0 :       continue;
     665             :     }
     666             : 
     667           0 :     if (smt::is_constructed_sort(data_specification, *i))
     668             :     {
     669           0 :       add_constructed_sort(data_specification, *i);
     670             :     }
     671             :   }
     672           0 : }
     673             : 
     674           0 : void basic_data_specification::add_standard_operators(
     675             :   const data::data_specification& data_specification,
     676             :   const std::shared_ptr<function_definition>& equal_to,
     677             :   const std::shared_ptr<function_definition>& not_equal_to,
     678             :   const std::shared_ptr<function_definition>& if_)
     679             : {
     680           0 :   for (std::set<data::sort_expression>::const_iterator i = data_specification.sorts().begin(); i != data_specification.sorts().end(); i++)
     681             :   {
     682           0 :     add_function_definition(data::equal_to(*i), equal_to);
     683           0 :     add_function_definition(data::not_equal_to(*i), not_equal_to);
     684           0 :     add_function_definition(data::if_(*i), if_);
     685             :   }
     686           0 : }
     687             : 
     688           0 : void basic_data_specification::add_boolean_operators(
     689             :   const data::data_specification& /* data_specification */,
     690             :   const std::shared_ptr<function_definition>& not_,
     691             :   const std::shared_ptr<function_definition>& and_,
     692             :   const std::shared_ptr<function_definition>& or_,
     693             :   const std::shared_ptr<function_definition>& implies)
     694             : {
     695           0 :   add_function_definition(data::sort_bool::not_(), not_);
     696           0 :   add_function_definition(data::sort_bool::and_(), and_);
     697           0 :   add_function_definition(data::sort_bool::or_(), or_);
     698           0 :   add_function_definition(data::sort_bool::implies(), implies);
     699           0 : }
     700             : 
     701           0 : void basic_data_specification::add_numerical_operators(
     702             :   const data::data_specification& /* data_specification */,
     703             :   const std::shared_ptr<function_definition>& less,
     704             :   const std::shared_ptr<function_definition>& less_equal,
     705             :   const std::shared_ptr<function_definition>& greater,
     706             :   const std::shared_ptr<function_definition>& greater_equal,
     707             :   const std::shared_ptr<function_definition>& plus,
     708             :   const std::shared_ptr<function_definition>& minus,
     709             :   const std::shared_ptr<function_definition>& times,
     710             :   const std::shared_ptr<function_definition>& divides,
     711             :   const std::shared_ptr<function_definition>& div,
     712             :   const std::shared_ptr<function_definition>& mod,
     713             :   const std::shared_ptr<function_definition>& floor,
     714             :   const std::shared_ptr<function_definition>& ceil,
     715             :   const std::shared_ptr<function_definition>& round,
     716             :   const std::shared_ptr<function_definition>& unary_minus,
     717             :   const std::shared_ptr<function_definition>& maximum,
     718             :   const std::shared_ptr<function_definition>& minimum,
     719             :   const std::shared_ptr<function_definition>& abs)
     720             : {
     721             :   /*
     722             :    * Missing functions:
     723             :    * - exp
     724             :    * - sqrt
     725             :    */
     726             : 
     727           0 :   const data::basic_sort& pos = data::sort_pos::pos();
     728           0 :   const data::basic_sort& nat = data::sort_nat::nat();
     729           0 :   const data::basic_sort& int_ = data::sort_int::int_();
     730           0 :   const data::basic_sort& real = data::sort_real::real_();
     731             : 
     732           0 :   data::variable b1("b1", data::sort_bool::bool_());
     733           0 :   data::variable p1("p1", pos);
     734           0 :   data::variable p2("p2", pos);
     735           0 :   data::variable n1("n1", nat);
     736           0 :   data::variable n2("n2", nat);
     737           0 :   data::variable i1("i1", int_);
     738           0 :   data::variable i2("i2", int_);
     739           0 :   data::variable r1("r1", real);
     740           0 :   data::variable r2("r2", real);
     741             : 
     742           0 :   const data::data_expression& pos_one = data::sort_pos::c1();
     743           0 :   data::data_expression pos_two = data::sort_pos::cdub(data::sort_bool::false_(), pos_one);
     744           0 :   const data::data_expression& nat_zero = data::sort_nat::c0();
     745           0 :   data::data_expression nat_one = data::sort_nat::cnat(pos_one);
     746           0 :   data::data_expression int_zero = data::sort_int::cint(nat_zero);
     747           0 :   data::data_expression int_one = data::sort_int::cint(nat_one);
     748           0 :   data::data_expression real_zero = data::sort_real::creal(int_zero, pos_one);
     749           0 :   data::data_expression real_one = data::sort_real::creal(int_one, pos_one);
     750           0 :   data::data_expression real_half = data::sort_real::divides(pos_one, pos_two);
     751             : 
     752           0 :   std::shared_ptr<function_definition> identity(new identity_function_definition(this));
     753             : 
     754           0 :   add_function_definition(data::less(pos), less);
     755           0 :   add_function_definition(data::less_equal(pos), less_equal);
     756           0 :   add_function_definition(data::greater(pos), greater);
     757           0 :   add_function_definition(data::greater_equal(pos), greater_equal);
     758           0 :   add_function_definition(data::sort_pos::plus(), plus);
     759           0 :   add_function_definition(data::sort_pos::add_with_carry(), data::variable_vector({b1,p1,p2}), data::if_(b1, data::sort_pos::plus(data::sort_pos::c1(), data::sort_pos::plus(p1,p2)), data::sort_pos::plus(p1,p2)));
     760           0 :   add_function_definition(data::sort_pos::times(), times);
     761           0 :   add_function_definition(data::sort_pos::maximum(), maximum, data::variable_vector({p1, p2}), data::if_(data::greater(p1, p2), p1, p2));
     762           0 :   add_function_definition(data::sort_pos::minimum(), minimum, data::variable_vector({p1, p2}), data::if_(data::less(p1, p2), p1, p2));
     763           0 :   add_function_definition(data::sort_pos::succ(), data::variable_vector({p1}), data::sort_pos::plus(p1, pos_one));
     764             : 
     765           0 :   add_function_definition(data::less(nat), less);
     766           0 :   add_function_definition(data::less_equal(nat), less_equal);
     767           0 :   add_function_definition(data::greater(nat), greater);
     768           0 :   add_function_definition(data::greater_equal(nat), greater_equal);
     769           0 :   add_function_definition(data::sort_nat::plus(pos, nat), plus);
     770           0 :   add_function_definition(data::sort_nat::plus(nat, pos), plus);
     771           0 :   add_function_definition(data::sort_nat::plus(nat, nat), plus);
     772           0 :   add_function_definition(data::sort_nat::times(nat, nat), times);
     773           0 :   add_function_definition(data::sort_nat::div(), div);
     774           0 :   add_function_definition(data::sort_nat::mod(), mod);
     775           0 :   add_function_definition(data::sort_nat::maximum(pos, nat), maximum, data::variable_vector({p1, n1}), data::sort_nat::nat2pos(data::if_(data::greater(data::sort_nat::pos2nat(p1), n1), data::sort_nat::pos2nat(p1), n1)));
     776           0 :   add_function_definition(data::sort_nat::maximum(nat, pos), maximum, data::variable_vector({n1, p1}), data::sort_nat::nat2pos(data::if_(data::greater(data::sort_nat::pos2nat(p1), n1), data::sort_nat::pos2nat(p1), n1)));
     777           0 :   add_function_definition(data::sort_nat::maximum(nat, nat), maximum, data::variable_vector({n1, n2}), data::if_(data::greater(n1, n2), n1, n2));
     778           0 :   add_function_definition(data::sort_nat::minimum(nat, nat), minimum, data::variable_vector({n1, n2}), data::if_(data::less(n1, n2), n1, n2));
     779           0 :   add_function_definition(data::sort_nat::pos2nat(), identity);
     780           0 :   add_function_definition(data::sort_nat::nat2pos(), identity);
     781           0 :   add_function_definition(data::sort_nat::succ(nat), data::variable_vector({n1}), data::sort_nat::plus(n1, pos_one));
     782           0 :   add_function_definition(data::sort_nat::pred(), data::variable_vector({p1}), data::sort_int::int2nat(data::sort_int::minus(p1, pos_one)));
     783             : 
     784           0 :   add_function_definition(data::less(int_), less);
     785           0 :   add_function_definition(data::less_equal(int_), less_equal);
     786           0 :   add_function_definition(data::greater(int_), greater);
     787           0 :   add_function_definition(data::greater_equal(int_), greater_equal);
     788           0 :   add_function_definition(data::sort_int::plus(int_, int_), plus);
     789           0 :   add_function_definition(data::sort_int::minus(pos, pos), minus);
     790           0 :   add_function_definition(data::sort_int::minus(nat, nat), minus);
     791           0 :   add_function_definition(data::sort_int::minus(int_, int_), minus);
     792           0 :   add_function_definition(data::sort_int::times(int_, int_), times);
     793           0 :   add_function_definition(data::sort_int::div(int_, pos), div);
     794           0 :   add_function_definition(data::sort_int::mod(int_, pos), mod);
     795           0 :   add_function_definition(data::sort_int::negate(pos), unary_minus, data::variable_vector({p1}), data::sort_int::minus(int_zero, data::sort_int::pos2int(p1)));
     796           0 :   add_function_definition(data::sort_int::negate(nat), unary_minus, data::variable_vector({n1}), data::sort_int::minus(int_zero, data::sort_int::nat2int(n1)));
     797           0 :   add_function_definition(data::sort_int::negate(int_), unary_minus, data::variable_vector({i1}), data::sort_int::minus(int_zero, i1));
     798           0 :   add_function_definition(data::sort_int::maximum(pos, int_), maximum, data::variable_vector({p1, i1}), data::sort_int::int2pos(data::if_(data::greater(data::sort_int::pos2int(p1), i1), data::sort_int::pos2int(p1), i1)));
     799           0 :   add_function_definition(data::sort_int::maximum(int_, pos), maximum, data::variable_vector({i1, p1}), data::sort_int::int2pos(data::if_(data::greater(data::sort_int::pos2int(p1), i1), data::sort_int::pos2int(p1), i1)));
     800           0 :   add_function_definition(data::sort_int::maximum(nat, int_), maximum, data::variable_vector({n1, i1}), data::sort_int::int2nat(data::if_(data::greater(data::sort_int::nat2int(n1), i1), data::sort_int::nat2int(n1), i1)));
     801           0 :   add_function_definition(data::sort_int::maximum(int_, nat), maximum, data::variable_vector({i1, n1}), data::sort_int::int2nat(data::if_(data::greater(data::sort_int::nat2int(n1), i1), data::sort_int::nat2int(n1), i1)));
     802           0 :   add_function_definition(data::sort_int::maximum(int_, int_), maximum, data::variable_vector({i1, i2}), data::if_(data::greater(i1, i2), i1, i2));
     803           0 :   add_function_definition(data::sort_int::minimum(int_, int_), minimum, data::variable_vector({i1, i2}), data::if_(data::less(i1, i2), i1, i2));
     804           0 :   add_function_definition(data::sort_int::abs(), abs, data::variable_vector({i1}), data::if_(data::less(i1, int_zero), data::sort_int::negate(i1), i1));
     805           0 :   add_function_definition(data::sort_int::pos2int(), identity);
     806           0 :   add_function_definition(data::sort_int::int2pos(), identity);
     807           0 :   add_function_definition(data::sort_int::nat2int(), identity);
     808           0 :   add_function_definition(data::sort_int::int2nat(), identity);
     809           0 :   add_function_definition(data::sort_int::succ(int_), data::variable_vector({i1}), data::sort_int::plus(i1, int_one));
     810           0 :   add_function_definition(data::sort_int::pred(nat), data::variable_vector({n1}), data::sort_int::minus(n1, nat_one));
     811           0 :   add_function_definition(data::sort_int::pred(int_), data::variable_vector({i1}), data::sort_int::minus(i1, int_one));
     812             : 
     813           0 :   add_function_definition(data::less(real), less);
     814           0 :   add_function_definition(data::less_equal(real), less_equal);
     815           0 :   add_function_definition(data::greater(real), greater);
     816           0 :   add_function_definition(data::greater_equal(real), greater_equal);
     817           0 :   add_function_definition(data::sort_real::plus(real, real), plus);
     818           0 :   add_function_definition(data::sort_real::minus(real, real), minus);
     819           0 :   add_function_definition(data::sort_real::times(real, real), times);
     820           0 :   add_function_definition(data::sort_real::divides(pos, pos), divides);
     821           0 :   add_function_definition(data::sort_real::divides(nat, nat), divides);
     822           0 :   add_function_definition(data::sort_real::divides(int_, int_), divides);
     823           0 :   add_function_definition(data::sort_real::divides(real, real), divides);
     824           0 :   add_function_definition(data::sort_real::floor(), floor);
     825           0 :   add_function_definition(data::sort_real::ceil(), ceil, data::variable_vector({r1}), data::sort_real::negate(data::sort_real::floor(data::sort_real::negate(r1))));
     826           0 :   add_function_definition(data::sort_real::round(), round, data::variable_vector({r1}), data::sort_real::floor(data::sort_real::plus(r1, real_half)));
     827           0 :   add_function_definition(data::sort_real::negate(real), unary_minus, data::variable_vector({r1}), data::sort_real::minus(real_zero, r1));
     828           0 :   add_function_definition(data::sort_real::maximum(real, real), maximum, data::variable_vector({r1, r2}), data::if_(data::greater(r1, r2), r1, r2));
     829           0 :   add_function_definition(data::sort_real::minimum(real, real), minimum, data::variable_vector({r1, r2}), data::if_(data::less(r1, r2), r1, r2));
     830           0 :   add_function_definition(data::sort_real::abs(real), abs, data::variable_vector({r1}), data::if_(data::less(r1, real_zero), data::sort_real::negate(r1), r1));
     831           0 :   add_function_definition(data::sort_real::pos2real(), identity);
     832           0 :   add_function_definition(data::sort_real::real2pos(), identity);
     833           0 :   add_function_definition(data::sort_real::nat2real(), identity);
     834           0 :   add_function_definition(data::sort_real::real2nat(), identity);
     835           0 :   add_function_definition(data::sort_real::int2real(), identity);
     836           0 :   add_function_definition(data::sort_real::real2int(), identity);
     837           0 :   add_function_definition(data::sort_real::succ(real), data::variable_vector({r1}), data::sort_real::plus(r1, real_one));
     838           0 :   add_function_definition(data::sort_real::pred(real), data::variable_vector({r1}), data::sort_real::minus(r1, real_one));
     839           0 : }
     840             : 
     841           0 : void basic_data_specification::add_recursive_function(const data::function_symbol& function)
     842             : {
     843           0 :   if (!m_rewrite_rules.count(function))
     844             :   {
     845           0 :     return;
     846             :   }
     847             : 
     848           0 :   data::data_equation_vector pattern_matching_rules;
     849           0 :   for (data::data_equation_vector::const_iterator i = m_rewrite_rules.at(function).begin(); i != m_rewrite_rules.at(function).end(); i++)
     850             :   {
     851           0 :     if (recursive_function_definition::is_pattern_matching_rule(this, *i))
     852             :     {
     853           0 :       pattern_matching_rules.push_back(*i);
     854             :     }
     855             :   }
     856           0 :   if (pattern_matching_rules.empty())
     857             :   {
     858           0 :     return;
     859             :   }
     860             : 
     861           0 :   function_definition *definition = create_recursive_function_definition(function, pattern_matching_rules);
     862           0 :   add_function_definition(function, std::shared_ptr<function_definition>(definition));
     863             : }
     864             : 
     865           0 : void basic_data_specification::add_recursive_functions(const data::data_specification& data_specification)
     866             : {
     867           0 :   data::function_symbol_vector candidate_functions = data_specification.user_defined_mappings();
     868           0 :   for (std::set<data::sort_expression>::const_iterator i = data_specification.sorts().begin(); i != data_specification.sorts().end(); i++)
     869             :   {
     870           0 :     if (data_specification.sorts().count(data::sort_list::list(*i)))
     871             :     {
     872           0 :       data::function_symbol_vector list_functions = data::sort_list::list_generate_functions_code(*i);
     873           0 :       candidate_functions.insert(candidate_functions.end(), list_functions.begin(), list_functions.end());
     874             : 
     875             :       // Add the element_at function.
     876           0 :       data::variable n("n", data::sort_nat::nat());
     877           0 :       data::variable l("l", data::sort_list::list(*i));
     878           0 :       add_function_definition(data::sort_list::element_at(*i), {l, n}, data::if_(data::equal_to(n, data::sort_nat::c0()), data::sort_list::head(*i)(l), data::sort_list::element_at(*i)(data::sort_list::tail(*i)(l), data::sort_nat::pred(n))));
     879             :     }
     880             :   }
     881             : 
     882           0 :   for (data::function_symbol_vector::const_iterator i = candidate_functions.begin(); i != candidate_functions.end(); i++)
     883             :   {
     884           0 :     add_recursive_function(*i);
     885             :   }
     886           0 : }
     887             : 
     888             : } // namespace smt
     889           0 : } // namespace mcrl2

Generated by: LCOV version 1.12