LCOV - code coverage report
Current view: top level - smt/source - cvc4.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 158 0.0 %
Date: 2019-06-26 00:32:26 Functions: 0 34 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 "mcrl2/data/int.h"
      10             : #include "mcrl2/data/real.h"
      11             : #include "mcrl2/smt/cvc4.h"
      12             : #include "mcrl2/smt/recursive_function_definition.h"
      13             : 
      14             : namespace mcrl2
      15             : {
      16             : 
      17             : namespace smt
      18             : {
      19             : 
      20           0 : class cvc4_identifier_generator : public data::set_identifier_generator
      21             : {
      22             :   public:
      23           0 :     virtual core::identifier_string operator()(const std::string& hint, bool add_to_context = true)
      24             :     {
      25           0 :       std::string name = hint;
      26             : 
      27           0 :       if (name == "-") name = "minus";
      28           0 :       if (name == "[]") name = "emptylist";
      29           0 :       if (name == "|>") name = "cons";
      30           0 :       if (name == "<|") name = "snoc";
      31           0 :       if (name == "#") name = "count";
      32           0 :       if (name == "++") name = "concat";
      33           0 :       if (name == ".") name = "at";
      34             : 
      35           0 :       for (std::size_t i = 0; i < name.size(); i++)
      36             :       {
      37           0 :         if (!(
      38           0 :           ('0' <= name[i] && name[i] <= '9') ||
      39           0 :           ('a' <= name[i] && name[i] <= 'z') ||
      40           0 :           ('A' <= name[i] && name[i] <= 'Z')))
      41             :         {
      42           0 :           name[i] = '_';
      43             :         }
      44             :       }
      45             : 
      46           0 :       return data::set_identifier_generator::operator()(name, add_to_context);
      47             :     }
      48             : };
      49             : 
      50           0 : class pos_sort_definition : public sort_definition
      51             : {
      52             :   public:
      53           0 :     pos_sort_definition(data_specification *data_specification):
      54           0 :       sort_definition(data_specification, "Int")
      55           0 :     {}
      56             : 
      57           0 :     std::string generate_variable_declaration(const core::identifier_string& name) const
      58             :     {
      59           0 :       return sort_definition::generate_variable_declaration(name) + "(assert (>= " + (std::string)name + " 1))\n";
      60             :     }
      61             : };
      62             : 
      63           0 : class nat_sort_definition : public sort_definition
      64             : {
      65             :   public:
      66           0 :     nat_sort_definition(data_specification *data_specification):
      67           0 :       sort_definition(data_specification, "Int")
      68           0 :     {}
      69             : 
      70           0 :     std::string generate_variable_declaration(const core::identifier_string& name) const
      71             :     {
      72           0 :       return sort_definition::generate_variable_declaration(name) + "(assert (>= " + (std::string)name + " 0))\n";
      73             :     }
      74             : };
      75             : 
      76           0 : static std::string print_nat(const data::data_expression& number)
      77             : {
      78           0 :   return data::pp(number);
      79             : }
      80             : 
      81           0 : static std::string print_int(const data::data_expression& number)
      82             : {
      83           0 :   assert(data::sort_int::is_cint_application(number) || data::sort_int::is_cneg_application(number));
      84           0 :   if (data::sort_int::is_cneg_application(number))
      85             :   {
      86           0 :     data::application application(number);
      87           0 :     assert(application.size() == 1);
      88           0 :     return "(- " + data::pp(application[0]) + ")";
      89             :   }
      90             :   else
      91             :   {
      92           0 :     return data::pp(number);
      93             :   }
      94             : }
      95             : 
      96           0 : static std::string print_real(const data::data_expression& number)
      97             : {
      98           0 :   assert(data::sort_real::is_creal_application(number));
      99           0 :   data::application application(number);
     100           0 :   std::string numerator = print_int(application[0]);
     101           0 :   std::string denominator = data::pp(application[1]);
     102           0 :   return "(/ " + numerator + " " + denominator + ")";
     103             : }
     104             : 
     105           0 : static std::shared_ptr<function_definition> make_operator(data_specification* data_specification, const std::string& name)
     106             : {
     107           0 :   return std::shared_ptr<function_definition>(new named_function_definition(data_specification, name));
     108             : }
     109             : 
     110           0 : smt4_data_specification::smt4_data_specification(const data::data_specification& data_specification):
     111           0 :   basic_data_specification(data_specification, std::shared_ptr<data::set_identifier_generator>(new cvc4_identifier_generator))
     112             : {
     113           0 :   add_sort_bool(std::shared_ptr<sort_definition>(new sort_definition(this, "Bool")), "true", "false");
     114           0 :   add_sort_pos(std::shared_ptr<sort_definition>(new pos_sort_definition(this)), print_nat);
     115           0 :   add_sort_nat(std::shared_ptr<sort_definition>(new nat_sort_definition(this)), print_nat);
     116           0 :   add_sort_int(std::shared_ptr<sort_definition>(new sort_definition(this, "Int")), print_int);
     117           0 :   add_sort_real(std::shared_ptr<sort_definition>(new sort_definition(this, "Real")), print_real);
     118           0 :   add_constructed_sorts(data_specification);
     119             : 
     120           0 :   add_standard_operators(
     121             :     data_specification,
     122           0 :     make_operator(this, "="),
     123           0 :     make_operator(this, "distinct"),
     124           0 :     make_operator(this, "ite")
     125           0 :   );
     126           0 :   add_boolean_operators(
     127             :     data_specification,
     128           0 :     make_operator(this, "not"),
     129           0 :     make_operator(this, "and"),
     130           0 :     make_operator(this, "or"),
     131           0 :     make_operator(this, "=>")
     132           0 :   );
     133           0 :   add_numerical_operators(
     134             :     data_specification,
     135           0 :     make_operator(this, "<"),
     136           0 :     make_operator(this, "<="),
     137           0 :     make_operator(this, ">"),
     138           0 :     make_operator(this, ">="),
     139           0 :     make_operator(this, "+"),
     140           0 :     make_operator(this, "-"),
     141           0 :     make_operator(this, "*"),
     142           0 :     make_operator(this, "/"),
     143           0 :     make_operator(this, "div"),
     144           0 :     make_operator(this, "mod"),
     145           0 :     make_operator(this, "to_int"),
     146             :     nullptr, // ceil
     147             :     nullptr, // round
     148           0 :     make_operator(this, "-"),
     149             :     nullptr, // maximum
     150             :     nullptr, // minimum
     151           0 :     make_operator(this, "abs")
     152           0 :   );
     153           0 :   add_recursive_functions(data_specification);
     154           0 : }
     155             : 
     156           0 : std::string smt4_data_specification::generate_data_expression(const std::map<data::variable, std::string>& declared_variables, const std::string& function_name, const data::data_expression_vector& arguments) const
     157             : {
     158           0 :   if (arguments.empty())
     159             :   {
     160           0 :     return function_name;
     161             :   }
     162             :   else
     163             :   {
     164           0 :     std::string output;
     165           0 :     output += "(";
     166           0 :     output += function_name;
     167           0 :     for (data::data_expression_vector::const_iterator i = arguments.begin(); i != arguments.end(); i++)
     168             :     {
     169           0 :       output += " ";
     170           0 :       output += generate_data_expression(declared_variables, *i);
     171             :     }
     172           0 :     output += ")";
     173           0 :     return output;
     174             :   }
     175             : }
     176             : 
     177           0 : std::string smt4_data_specification::generate_variable_declaration(const std::string& type_name, const std::string& variable_name) const
     178             : {
     179           0 :   return "(declare-fun " + variable_name + " () " + type_name + ")\n";
     180             : }
     181             : 
     182           0 : std::string smt4_data_specification::generate_assertion(const std::map<data::variable, std::string>& declared_variables, const data::data_expression& assertion) const
     183             : {
     184           0 :   return "(assert " + generate_data_expression(declared_variables, assertion) + ")\n";
     185             : }
     186             : 
     187           0 : std::string smt4_data_specification::generate_distinct_assertion(const std::map<data::variable, std::string>& declared_variables, const data::data_expression_list& distinct_terms) const
     188             : {
     189           0 :   std::string output = "(distinct";
     190           0 :   for (data::data_expression_list::const_iterator i = distinct_terms.begin(); i != distinct_terms.end(); i++)
     191             :   {
     192           0 :     output += " ";
     193           0 :     output += generate_data_expression(declared_variables, *i);
     194             :   }
     195           0 :   output += ")\n";
     196           0 :   return output;
     197             : }
     198             : 
     199           0 : std::string smt4_data_specification::generate_smt_problem(const std::string& variable_declarations, const std::string& assertions) const
     200             : {
     201           0 :   return variable_declarations + assertions + "(check-sat)\n";
     202             : }
     203             : 
     204           0 : class cvc4_constructed_sort_definition : public constructed_sort_definition
     205             : {
     206             :   protected:
     207             :     std::map<data::function_symbol, std::string> m_constructor_names;
     208             :     std::map<data::function_symbol, std::vector<std::string> > m_field_names;
     209             : 
     210             :   public:
     211           0 :     cvc4_constructed_sort_definition(data_specification *data_specification, data::sort_expression sort, const constructors_t &constructors):
     212           0 :       constructed_sort_definition(data_specification, sort, constructors)
     213             :     {
     214           0 :       for (std::size_t i = 0; i < m_constructors.size(); i++)
     215             :       {
     216           0 :         std::string name = data_specification->identifier_generator()(m_constructors[i].constructor.name());
     217           0 :         std::string recogniser_name = "is-" + name;
     218           0 :         data_specification->identifier_generator().add_identifier(recogniser_name);
     219             : 
     220           0 :         m_constructor_names[m_constructors[i].constructor] = name;
     221           0 :         add_constructor_definition(i, new named_function_definition(data_specification, m_constructors[i].constructor.sort(), name));
     222           0 :         add_recogniser_definition(i, new named_function_definition(data_specification, recogniser_name));
     223             : 
     224           0 :         for (std::size_t j = 0; j < m_constructors[i].fields.size(); j++)
     225             :         {
     226           0 :           std::string field_name = data_specification->identifier_generator()(m_constructors[i].fields[j].projections[0].name());
     227           0 :           m_field_names[m_constructors[i].constructor].push_back(field_name);
     228           0 :           add_projection_definition(i, j, new named_function_definition(data_specification, field_name));
     229             :         }
     230             :       }
     231           0 :     }
     232             : 
     233           0 :     std::string generate_definition() const
     234             :     {
     235           0 :       std::string output = "(declare-datatypes () ( (" + m_name + "\n";
     236           0 :       for (std::size_t i = 0; i < m_constructors.size(); i++)
     237             :       {
     238           0 :         output += "  (" + m_constructor_names.at(m_constructors[i].constructor);
     239           0 :         for (std::size_t j = 0; j < m_constructors[i].fields.size(); j++)
     240             :         {
     241           0 :           assert(data::is_function_sort(m_constructors[i].fields[j].projections[0].sort()));
     242           0 :           std::string sort_name = m_data_specification->generate_sort_name(data::function_sort(m_constructors[i].fields[j].projections[0].sort()).codomain());
     243           0 :           output += " (" + m_field_names.at(m_constructors[i].constructor)[j] + " " + sort_name + ")";
     244             :         }
     245           0 :         output += ")\n";
     246             :       }
     247           0 :       output += ")))\n";
     248           0 :       return output;
     249             :     }
     250             : };
     251             : 
     252           0 : constructed_sort_definition *smt4_data_specification::create_constructed_sort(const data::sort_expression& sort, const constructed_sort_definition::constructors_t &constructors)
     253             : {
     254           0 :   return new cvc4_constructed_sort_definition(this, sort, constructors);
     255             : }
     256             : 
     257           0 : class cvc4_recursive_function_definition : public recursive_function_definition
     258             : {
     259             :   protected:
     260             :     data::sort_expression m_codomain;
     261             : 
     262             :   public:
     263           0 :     cvc4_recursive_function_definition(data_specification *data_specification, data::function_symbol function, const data::data_equation_vector& rewrite_rules):
     264           0 :       recursive_function_definition(data_specification, function, rewrite_rules)
     265             :     {
     266           0 :       if (data::is_function_sort(function.sort()))
     267             :       {
     268           0 :         m_codomain = data::function_sort(function.sort()).codomain();
     269             :       }
     270             :       else
     271             :       {
     272           0 :         m_codomain = function.sort();
     273             :       }
     274           0 :     }
     275             : 
     276           0 :     std::string generate_definition() const
     277             :     {
     278           0 :       std::map<data::variable, std::string> parameters;
     279           0 :       for (std::size_t i = 0; i < m_parameters.size(); i++)
     280             :       {
     281           0 :         std::string name = m_data_specification->identifier_generator()(m_parameters[i].name());
     282           0 :         parameters[m_parameters[i]] = name;
     283             :       }
     284           0 :       for (std::size_t i = 0; i < m_parameters.size(); i++)
     285             :       {
     286           0 :         m_data_specification->identifier_generator().remove_identifier(parameters[m_parameters[i]]);
     287             :       }
     288             : 
     289           0 :       std::string output = "(define-fun-rec " + m_name + " (";
     290           0 :       for (std::size_t i = 0; i < m_parameters.size(); i++)
     291             :       {
     292           0 :         output += " (" + parameters[m_parameters[i]] + " " + m_data_specification->generate_sort_name(m_parameters[i].sort()) + ")";
     293             :       }
     294           0 :       output += ") " + m_data_specification->generate_sort_name(m_codomain);
     295           0 :       output += " " + m_data_specification->generate_data_expression(parameters, m_rhs);
     296           0 :       output += ")\n";
     297           0 :       return output;
     298             :     }
     299             : };
     300             : 
     301           0 : function_definition *smt4_data_specification::create_recursive_function_definition(const data::function_symbol& function, const data::data_equation_vector& rewrite_rules)
     302             : {
     303           0 :   return new cvc4_recursive_function_definition(this, function, rewrite_rules);
     304             : }
     305             : 
     306             : } // namespace smt
     307           0 : } // namespace mcrl2

Generated by: LCOV version 1.12