LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/prover - smt_lib_solver.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 502 0.0 %
Date: 2020-09-22 00:46:14 Functions: 0 61 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Luc Engelen
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/data/detail/prover/smt_lib_solver.h
      10             : /// \brief Abstract interface for SMT solvers based on the SMT-LIB format
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_PROVER_SMT_LIB_SOLVER_H
      13             : #define MCRL2_DATA_DETAIL_PROVER_SMT_LIB_SOLVER_H
      14             : 
      15             : #include "mcrl2/core/print.h"
      16             : #include "mcrl2/data/data_specification.h" // Added to make this header compile standalone
      17             : #include "mcrl2/data/detail/prover/smt_solver.h"
      18             : 
      19             : #ifdef HAVE_CVC
      20             : #include "mcrl2/data/detail/prover/smt_solver_cvc_fast.ipp"
      21             : #endif
      22             : 
      23             : #ifndef WIN32
      24             : #include <unistd.h>
      25             : #endif
      26             : 
      27             : namespace mcrl2
      28             : {
      29             : namespace data
      30             : {
      31             : namespace detail
      32             : {
      33             : /// The class SMT_LIB_Solver is a base class for SMT solvers that read the SMT-LIB format
      34             : /// [Silvio Ranise and Cesare Tinelli. The SMT-LIB Standard: Version 1.1. Technical Report, Department of Computer
      35             : /// Science, The University of Iowa, 2005. (Available at http://goedel.cs.uiowa.edu/smtlib)]. It inherits from the class
      36             : /// SMT_Solver.
      37             : ///
      38             : /// The method SMT_LIB_Solver::translate receives an expression of sort Bool in conjunctive normal form as parameter
      39             : /// a_formula and translates it to a benchmark in SMT-LIB format. The result is saved as field std::string f_benchmark.
      40             : 
      41             : class SMT_LIB_Solver: public SMT_Solver
      42             : {
      43             :   private:
      44             :     std::string f_sorts_notes;
      45             :     std::string f_operators_notes;
      46             :     std::string f_predicates_notes;
      47             :     std::string f_extrasorts;
      48             :     std::string f_operators_extrafuns;
      49             :     std::string f_variables_extrafuns;
      50             :     std::string f_extrapreds;
      51             :     std::string f_formula;
      52             :     std::map < sort_expression, std::size_t > f_sorts;
      53             :     std::map < function_symbol, std::size_t > f_operators;
      54             :     std::set < variable > f_variables;
      55             :     std::set < variable > f_nat_variables;
      56             :     std::set < variable > f_pos_variables;
      57             :     bool f_bool2pred;
      58             : 
      59           0 :     const data_expression& left(const data_expression& x) const
      60             :     {
      61           0 :       const application& a = atermpp::down_cast<mcrl2::data::application>(x);
      62           0 :       return binary_left(a);
      63             :     }
      64             : 
      65           0 :     const data_expression& right(const data_expression& x) const
      66             :     {
      67           0 :       const application& a = atermpp::down_cast<mcrl2::data::application>(x);
      68           0 :       return binary_right(a);
      69             :     }
      70             : 
      71           0 :     const data_expression& arg(const data_expression& x) const
      72             :     {
      73           0 :       const application& a = atermpp::down_cast<mcrl2::data::application>(x);
      74           0 :       return unary_operand(a);
      75             :     }
      76             : 
      77           0 :     void declare_sorts()
      78             :     {
      79           0 :       f_extrasorts = "";
      80           0 :       if (!f_sorts.empty())
      81             :       {
      82           0 :         f_extrasorts = "  :extrasorts (";
      83           0 :         sort_expression v_sort;
      84           0 :         for(std::map < sort_expression, std::size_t >::const_iterator i=f_sorts.begin(); i!=f_sorts.end(); ++i)
      85             :         {
      86           0 :           if (v_sort != sort_expression())
      87             :           {
      88           0 :             f_extrasorts = f_extrasorts + " ";
      89             :           }
      90           0 :           v_sort = i->first;
      91           0 :           std::stringstream v_sort_string;
      92           0 :           v_sort_string << "sort" << i->second;
      93           0 :           f_extrasorts = f_extrasorts + v_sort_string.str();
      94             :         }
      95           0 :         f_extrasorts = f_extrasorts + ")\n";
      96             :       }
      97           0 :     }
      98             : 
      99           0 :     void declare_operators()
     100             :     {
     101           0 :       f_operators_extrafuns = "";
     102           0 :       if (!f_operators.empty())
     103             :       {
     104           0 :         f_operators_extrafuns = "  :extrafuns (";
     105           0 :         for(std::map < function_symbol, std::size_t >::const_iterator i=f_operators.begin(); i!=f_operators.end(); ++i)
     106             :         {
     107           0 :           std::stringstream v_operator_string;
     108           0 :           v_operator_string << "op" << i->second;
     109           0 :           f_operators_extrafuns = f_operators_extrafuns + "(" + v_operator_string.str();
     110           0 :           sort_expression v_sort = data_expression(i->first).sort();
     111           0 :           do
     112             :           {
     113           0 :             sort_expression_list v_sort_domain_list;
     114           0 :             if (is_function_sort(v_sort))
     115             :             {
     116           0 :               v_sort_domain_list = function_sort(v_sort).domain();
     117           0 :               v_sort = function_sort(v_sort).codomain();
     118             :             }
     119             :             else
     120             :             {
     121           0 :               v_sort_domain_list = sort_expression_list({v_sort});
     122           0 :               v_sort = sort_expression();
     123             :             }
     124           0 :             for (auto v_sort_domain_elt : v_sort_domain_list)
     125             :             {
     126           0 :               if (is_function_sort(v_sort_domain_elt))
     127             :               {
     128           0 :                 throw mcrl2::runtime_error("Function " + data::pp(i->first) +
     129           0 :                                            " cannot be translated to the SMT-LIB format.");
     130             :               }
     131           0 :               if (sort_int::is_int(v_sort_domain_elt))
     132             :               {
     133           0 :                 f_operators_extrafuns = f_operators_extrafuns + " Int";
     134             :               }
     135           0 :               else if (sort_nat::is_nat(v_sort_domain_elt))
     136             :               {
     137           0 :                 f_operators_extrafuns = f_operators_extrafuns + " Int";
     138             :               }
     139           0 :               else if (sort_pos::is_pos(v_sort_domain_elt))
     140             :               {
     141           0 :                 f_operators_extrafuns = f_operators_extrafuns + " Int";
     142             :               }
     143           0 :               else if (sort_real::is_real(v_sort_domain_elt))
     144             :               {
     145           0 :                 f_operators_extrafuns = f_operators_extrafuns + " Real";
     146             :               }
     147             :               else
     148             :               {
     149           0 :                 std::map < sort_expression, std::size_t >::const_iterator j=f_sorts.find(v_sort_domain_elt);
     150           0 :                 std::size_t v_sort_number=f_sorts.size();
     151           0 :                 if (j==f_sorts.end())  // not found
     152             :                 {
     153           0 :                   f_sorts[v_sort_domain_elt]=v_sort_number; // Assign a new number to v_sort_domain_elt.
     154             :                 }
     155             :                 else
     156             :                 {
     157           0 :                   v_sort_number=j->second; // get the previously assigned number.
     158             :                 }
     159           0 :                 std::stringstream v_sort_string;
     160           0 :                 v_sort_string << "sort" << v_sort_number;
     161           0 :                 f_operators_extrafuns = f_operators_extrafuns + " " + v_sort_string.str();
     162             :               }
     163             :             }
     164             :           }
     165           0 :           while (v_sort != sort_expression());
     166           0 :           f_operators_extrafuns = f_operators_extrafuns + ")";
     167             :         }
     168           0 :         f_operators_extrafuns = f_operators_extrafuns + ")\n";
     169             :       }
     170           0 :     }
     171             : 
     172           0 :     void declare_variables()
     173             :     {
     174           0 :       f_variables_extrafuns = "";
     175           0 :       if (!f_variables.empty())
     176             :       {
     177           0 :         f_variables_extrafuns = "  :extrafuns (";
     178             :       }
     179             : 
     180           0 :       for(auto v_variable : f_variables)
     181             :       {
     182           0 :         std::string v_variable_string = v_variable.name();
     183           0 :         sort_expression v_sort = data_expression(v_variable).sort();
     184           0 :         if (sort_real::is_real(v_sort))
     185             :         {
     186           0 :           f_variables_extrafuns = f_variables_extrafuns + "(" + v_variable_string + " Real)";
     187             :         }
     188           0 :         else if (sort_int::is_int(v_sort))
     189             :         {
     190           0 :           f_variables_extrafuns = f_variables_extrafuns + "(" + v_variable_string + " Int)";
     191             :         }
     192           0 :         else if (sort_nat::is_nat(v_sort))
     193             :         {
     194           0 :           f_variables_extrafuns = f_variables_extrafuns + "(" + v_variable_string + " Int)";
     195             :         }
     196           0 :         else if (sort_pos::is_pos(v_sort))
     197             :         {
     198           0 :           f_variables_extrafuns = f_variables_extrafuns + "(" + v_variable_string + " Int)";
     199             :         }
     200             :         else
     201             :         {
     202           0 :           std::map < sort_expression, std::size_t >::const_iterator j=f_sorts.find(v_sort);
     203           0 :           std::size_t v_sort_number=f_sorts.size();
     204           0 :           if (j==f_sorts.end())  // not found
     205             :           {
     206           0 :             f_sorts[v_sort]=v_sort_number; // Assign a new number to v_sort.
     207             :           }
     208             :           else
     209             :           {
     210           0 :             v_sort_number=j->second; // get the previously assigned number.
     211             :           }
     212             : 
     213           0 :           std::stringstream v_sort_string;
     214           0 :           v_sort_string << "sort" << v_sort_number;
     215           0 :           f_variables_extrafuns = f_variables_extrafuns + "(" + v_variable_string + " " + v_sort_string.str() +")";
     216             :         }
     217             :       }
     218           0 :       if (!f_variables.empty())
     219             :       {
     220           0 :         f_variables_extrafuns = f_variables_extrafuns + ")\n";
     221             :       }
     222           0 :     }
     223             : 
     224           0 :     void declare_predicates()
     225             :     {
     226           0 :       f_extrapreds = "";
     227           0 :       if (f_bool2pred)
     228             :       {
     229           0 :         assert(f_sorts.count(sort_bool::bool_())>0);
     230           0 :         std::size_t v_sort_number = f_sorts[sort_bool::bool_()];
     231           0 :         std::stringstream v_sort_string;
     232           0 :         v_sort_string << "sort" << v_sort_number;
     233           0 :         f_extrapreds = "  :extrapreds ((bool2pred ";
     234           0 :         f_extrapreds = f_extrapreds + v_sort_string.str() + ")";
     235           0 :         f_extrapreds = f_extrapreds + ")\n";
     236             :       }
     237           0 :     }
     238             : 
     239           0 :     void produce_notes_for_sorts()
     240             :     {
     241           0 :       f_sorts_notes = "";
     242           0 :       if (!f_sorts.empty())
     243             :       {
     244           0 :         f_sorts_notes = "  :notes \"";
     245           0 :         for(std::map < sort_expression, std::size_t >::const_iterator i=f_sorts.begin(); i!=f_sorts.end(); ++i)
     246             :         {
     247           0 :           std::stringstream v_sort_string;
     248           0 :           v_sort_string << "sort" << i->second;
     249           0 :           std::string v_sort_original_id = pp(i->first);
     250           0 :           f_sorts_notes = f_sorts_notes + "(" + v_sort_string.str() + " = " + v_sort_original_id + ")";
     251             :         }
     252           0 :         f_sorts_notes = f_sorts_notes + "\"\n";
     253             :       }
     254           0 :     }
     255             : 
     256           0 :     void produce_notes_for_operators()
     257             :     {
     258           0 :       f_operators_notes = "";
     259           0 :       if (!f_operators.empty())
     260             :       {
     261           0 :         f_operators_notes = "  :notes \"";
     262           0 :         for(std::map < function_symbol, std::size_t >::const_iterator i=f_operators.begin(); i!=f_operators.end(); ++i)
     263             :         {
     264           0 :           std::stringstream v_operator_string;
     265           0 :           v_operator_string << "op" << i->second;
     266           0 :           std::string v_operator_original_id = i->first.name();
     267           0 :           f_operators_notes = f_operators_notes + "(" + v_operator_string.str() + " = " + v_operator_original_id + ")";
     268             :         }
     269           0 :         f_operators_notes = f_operators_notes + "\"\n";
     270             :       }
     271           0 :     }
     272             : 
     273           0 :     void produce_notes_for_predicates()
     274             :     {
     275           0 :       f_predicates_notes = "";
     276           0 :       if (f_bool2pred)
     277             :       {
     278           0 :         f_predicates_notes =
     279             :           "  :notes \"bool2pred was introduced, because the smt-lib format cannot deal\"\n"
     280           0 :           "  :notes \"with boolean variables or functions returning boolean values.\"\n";
     281             :       }
     282           0 :     }
     283             : 
     284           0 :     void translate_clause(const data_expression& a_clause, const bool a_expecting_predicate)
     285             :     {
     286           0 :       if (sort_bool::is_not_application(a_clause))
     287             :       {
     288           0 :         translate_not(a_clause);
     289             :       }
     290           0 :       else if (is_equal_to_application(a_clause))
     291             :       {
     292           0 :         translate_equality(a_clause);
     293             :       }
     294           0 :       else if (is_not_equal_to_application(a_clause))
     295             :       {
     296           0 :         translate_inequality(a_clause);
     297             :       }
     298           0 :       else if (is_greater_application(a_clause))
     299             :       {
     300           0 :         translate_greater_than(a_clause);
     301             :       }
     302           0 :       else if (is_greater_equal_application(a_clause))
     303             :       {
     304           0 :         translate_greater_than_or_equal(a_clause);
     305             :       }
     306           0 :       else if (is_less_application(a_clause))
     307             :       {
     308           0 :         translate_less_than(a_clause);
     309             :       }
     310           0 :       else if (is_less_equal_application(a_clause))
     311             :       {
     312           0 :         translate_less_than_or_equal(a_clause);
     313             :       }
     314           0 :       else if (sort_real::is_plus_application(a_clause))
     315             :       {
     316           0 :         translate_plus(a_clause);
     317             :       }
     318           0 :       else if (sort_real::is_negate_application(a_clause))
     319             :       {
     320           0 :         translate_unary_minus(a_clause);
     321             :       }
     322           0 :       else if (sort_real::is_minus_application(a_clause))
     323             :       {
     324           0 :         translate_binary_minus(a_clause);
     325             :       }
     326           0 :       else if (sort_real::is_times_application(a_clause))
     327             :       {
     328           0 :         translate_multiplication(a_clause);
     329             :       }
     330           0 :       else if (sort_real::is_maximum_application(a_clause))
     331             :       {
     332           0 :         translate_max(a_clause);
     333             :       }
     334           0 :       else if (sort_real::is_minimum_application(a_clause))
     335             :       {
     336           0 :         translate_min(a_clause);
     337             :       }
     338           0 :       else if (sort_real::is_abs_application(a_clause))
     339             :       {
     340           0 :         translate_abs(a_clause);
     341             :       }
     342           0 :       else if (sort_real::is_succ_application(a_clause))
     343             :       {
     344           0 :         translate_succ(a_clause);
     345             :       }
     346           0 :       else if (sort_real::is_pred_application(a_clause))
     347             :       {
     348           0 :         translate_pred(a_clause);
     349             :       }
     350           0 :       else if (sort_pos::is_add_with_carry_application(a_clause))
     351             :       {
     352           0 :         translate_add_c(a_clause);
     353             :       }
     354           0 :       else if (sort_nat::is_cnat_application(a_clause))
     355             :       {
     356           0 :         translate_c_nat(a_clause);
     357             :       }
     358           0 :       else if (sort_int::is_cint_application(a_clause))
     359             :       {
     360           0 :         translate_c_int(a_clause);
     361             :       }
     362           0 :       else if (sort_int::is_integer_constant(a_clause))
     363             :       {
     364           0 :         translate_int_constant(a_clause);
     365             :       }
     366           0 :       else if (sort_nat::is_natural_constant(a_clause))
     367             :       {
     368           0 :         translate_nat_constant(a_clause);
     369             :       }
     370           0 :       else if (sort_pos::is_positive_constant(a_clause))
     371             :       {
     372           0 :         translate_pos_constant(a_clause);
     373             :       }
     374           0 :       else if (sort_bool::is_true_function_symbol(a_clause) && a_expecting_predicate)
     375             :       {
     376           0 :         translate_true();
     377             :       }
     378           0 :       else if (sort_bool::is_false_function_symbol(a_clause) && a_expecting_predicate)
     379             :       {
     380           0 :         translate_false();
     381             :       }
     382           0 :       else if (is_variable(a_clause))
     383             :       {
     384           0 :         if (a_expecting_predicate)
     385             :         {
     386           0 :           add_bool2pred_and_translate_clause(a_clause);
     387             :         }
     388           0 :         else if (sort_nat::is_nat(a_clause.sort()))
     389             :         {
     390           0 :           translate_nat_variable(atermpp::down_cast<variable>(a_clause));
     391             :         }
     392           0 :         else if (sort_pos::is_pos(a_clause.sort()))
     393             :         {
     394           0 :           translate_pos_variable(atermpp::down_cast<variable>(a_clause));
     395             :         }
     396             :         else
     397             :         {
     398           0 :           translate_variable(atermpp::down_cast<variable>(a_clause));
     399             :         }
     400             :       }
     401           0 :       else if (is_application(a_clause))
     402             :       {
     403           0 :         if (a_expecting_predicate)
     404             :         {
     405           0 :           add_bool2pred_and_translate_clause(a_clause);
     406             :         }
     407             :         else
     408             :         {
     409           0 :           translate_unknown_operator(a_clause);
     410             :         }
     411             :       }
     412           0 :       else if (data::is_function_symbol(a_clause))
     413             :       {
     414           0 :         translate_function_symbol(a_clause);
     415             :       }
     416             :       else
     417             :       {
     418           0 :         throw mcrl2::runtime_error("Unable to handle the current clause (" +
     419           0 :                                    data::pp(a_clause) + ").");
     420             :       }
     421           0 :     }
     422             : 
     423           0 :     void add_bool2pred_and_translate_clause(const data_expression& a_clause)
     424             :     {
     425           0 :       f_bool2pred = true;
     426           0 :       f_formula = f_formula + "(bool2pred ";
     427           0 :       translate_clause(a_clause, false);
     428           0 :       f_formula = f_formula + ")";
     429           0 :     }
     430             : 
     431           0 :     void translate_not(const data_expression& a_clause)
     432             :     {
     433           0 :       const data_expression v_clause=arg(a_clause);
     434           0 :       f_formula = f_formula + "(not ";
     435           0 :       translate_clause(v_clause, true);
     436           0 :       f_formula = f_formula + ")";
     437           0 :     }
     438             : 
     439           0 :     void translate_equality(const data_expression& a_clause)
     440             :     {
     441           0 :       const data_expression v_clause_1 = left(a_clause);
     442           0 :       const data_expression v_clause_2 = right(a_clause);
     443           0 :       f_formula = f_formula + "(= ";
     444           0 :       translate_clause(v_clause_1, false);
     445           0 :       f_formula = f_formula + " ";
     446           0 :       translate_clause(v_clause_2, false);
     447           0 :       f_formula = f_formula + ")";
     448           0 :     }
     449             : 
     450           0 :     void translate_inequality(const data_expression& a_clause)
     451             :     {
     452           0 :       const data_expression v_clause_1 = left(a_clause);
     453           0 :       const data_expression v_clause_2 = right(a_clause);
     454           0 :       f_formula = f_formula + "(distinct ";
     455           0 :       translate_clause(v_clause_1, false);
     456           0 :       f_formula = f_formula + " ";
     457           0 :       translate_clause(v_clause_2, false);
     458           0 :       f_formula = f_formula + ")";
     459           0 :     }
     460             : 
     461           0 :     void translate_greater_than(const data_expression& a_clause)
     462             :     {
     463           0 :       const data_expression v_clause_1 = left(a_clause);
     464           0 :       const data_expression v_clause_2 = right(a_clause);
     465           0 :       f_formula = f_formula + "(> ";
     466           0 :       translate_clause(v_clause_1, false);
     467           0 :       f_formula = f_formula + " ";
     468           0 :       translate_clause(v_clause_2, false);
     469           0 :       f_formula = f_formula + ")";
     470           0 :     }
     471             : 
     472           0 :     void translate_greater_than_or_equal(const data_expression& a_clause)
     473             :     {
     474           0 :       const data_expression v_clause_1 = left(a_clause);
     475           0 :       const data_expression v_clause_2 = right(a_clause);
     476           0 :       f_formula = f_formula + "(>= ";
     477           0 :       translate_clause(v_clause_1, false);
     478           0 :       f_formula = f_formula + " ";
     479           0 :       translate_clause(v_clause_2, false);
     480           0 :       f_formula = f_formula + ")";
     481           0 :     }
     482             : 
     483           0 :     void translate_less_than(const data_expression& a_clause)
     484             :     {
     485           0 :       const data_expression v_clause_1 = left(a_clause);
     486           0 :       const data_expression v_clause_2 = right(a_clause);
     487           0 :       f_formula = f_formula + "(< ";
     488           0 :       translate_clause(v_clause_1, false);
     489           0 :       f_formula = f_formula + " ";
     490           0 :       translate_clause(v_clause_2, false);
     491           0 :       f_formula = f_formula + ")";
     492           0 :     }
     493             : 
     494           0 :     void translate_less_than_or_equal(const data_expression& a_clause)
     495             :     {
     496           0 :       const data_expression v_clause_1 = left(a_clause);
     497           0 :       const data_expression v_clause_2 = right(a_clause);
     498           0 :       f_formula = f_formula + "(<= ";
     499           0 :       translate_clause(v_clause_1, false);
     500           0 :       f_formula = f_formula + " ";
     501           0 :       translate_clause(v_clause_2, false);
     502           0 :       f_formula = f_formula + ")";
     503           0 :     }
     504             : 
     505           0 :     void translate_plus(const data_expression& a_clause)
     506             :     {
     507           0 :       const data_expression v_clause_1 = left(a_clause);
     508           0 :       const data_expression v_clause_2 = right(a_clause);
     509           0 :       f_formula = f_formula + "(+ ";
     510           0 :       translate_clause(v_clause_1, false);
     511           0 :       f_formula = f_formula + " ";
     512           0 :       translate_clause(v_clause_2, false);
     513           0 :       f_formula = f_formula + ")";
     514           0 :     }
     515             : 
     516           0 :     void translate_unary_minus(const data_expression& a_clause)
     517             :     {
     518           0 :       const data_expression v_clause = arg(a_clause);
     519           0 :       f_formula = f_formula + "(~";
     520           0 :       translate_clause(v_clause, false);
     521           0 :       f_formula = f_formula + ")";
     522           0 :     }
     523             : 
     524           0 :     void translate_binary_minus(const data_expression& a_clause)
     525             :     {
     526           0 :       const data_expression v_clause_1 = left(a_clause);
     527           0 :       const data_expression v_clause_2 = right(a_clause);
     528           0 :       f_formula = f_formula + "(- ";
     529           0 :       translate_clause(v_clause_1, false);
     530           0 :       f_formula = f_formula + " ";
     531           0 :       translate_clause(v_clause_2, false);
     532           0 :       f_formula = f_formula + ")";
     533           0 :     }
     534             : 
     535           0 :     void translate_multiplication(const data_expression& a_clause)
     536             :     {
     537           0 :       const data_expression v_clause_1 = left(a_clause);
     538           0 :       const data_expression v_clause_2 = right(a_clause);
     539           0 :       f_formula = f_formula + "(* ";
     540           0 :       translate_clause(v_clause_1, false);
     541           0 :       f_formula = f_formula + " ";
     542           0 :       translate_clause(v_clause_2, false);
     543           0 :       f_formula = f_formula + ")";
     544           0 :     }
     545             : 
     546           0 :     void translate_max(const data_expression& a_clause)
     547             :     {
     548           0 :       const data_expression v_clause_1 = left(a_clause);
     549           0 :       const data_expression v_clause_2 = right(a_clause);
     550           0 :       f_formula = f_formula + "(ite (>= ";
     551           0 :       translate_clause(v_clause_1, false);
     552           0 :       f_formula = f_formula + " ";
     553           0 :       translate_clause(v_clause_2, false);
     554           0 :       f_formula = f_formula + ") ";
     555           0 :       translate_clause(v_clause_1, false);
     556           0 :       f_formula = f_formula + " ";
     557           0 :       translate_clause(v_clause_2, false);
     558           0 :       f_formula = f_formula + ")";
     559           0 :     }
     560             : 
     561           0 :     void translate_min(const data_expression& a_clause)
     562             :     {
     563           0 :       const data_expression v_clause_1 = left(a_clause);
     564           0 :       const data_expression v_clause_2 = right(a_clause);
     565           0 :       f_formula = f_formula + "(ite (<= ";
     566           0 :       translate_clause(v_clause_1, false);
     567           0 :       f_formula = f_formula + " ";
     568           0 :       translate_clause(v_clause_2, false);
     569           0 :       f_formula = f_formula + ") ";
     570           0 :       translate_clause(v_clause_1, false);
     571           0 :       f_formula = f_formula + " ";
     572           0 :       translate_clause(v_clause_2, false);
     573           0 :       f_formula = f_formula + ")";
     574           0 :     }
     575             : 
     576           0 :     void translate_abs(const data_expression& a_clause)
     577             :     {
     578           0 :       const data_expression v_clause = arg(a_clause);
     579           0 :       f_formula = f_formula + "(ite (< 0 ";
     580           0 :       translate_clause(v_clause, false);
     581           0 :       f_formula = f_formula + ") ~";
     582           0 :       translate_clause(v_clause, false);
     583           0 :       f_formula = f_formula + " ";
     584           0 :       translate_clause(v_clause, false);
     585           0 :       f_formula = f_formula + ")";
     586           0 :     }
     587             : 
     588           0 :     void translate_succ(const data_expression& a_clause)
     589             :     {
     590           0 :       const data_expression v_clause = arg(a_clause);
     591           0 :       f_formula = f_formula + "(+ ";
     592           0 :       translate_clause(v_clause, false);
     593           0 :       f_formula = f_formula + " 1)";
     594           0 :     }
     595             : 
     596           0 :     void translate_pred(const data_expression& a_clause)
     597             :     {
     598           0 :       const data_expression v_clause = arg(a_clause);
     599           0 :       f_formula = f_formula + "(- ";
     600           0 :       translate_clause(v_clause, false);
     601           0 :       f_formula = f_formula + " 1)";
     602           0 :     }
     603             : 
     604           0 :     void translate_add_c(const data_expression& a_clause)
     605             :     {
     606           0 :       const application& v_clause = atermpp::down_cast<application>(a_clause);
     607           0 :       application::const_iterator arg = v_clause.begin();
     608           0 :       const data_expression v_clause_1 = *arg++;
     609           0 :       const data_expression v_clause_2 = *arg++;
     610           0 :       const data_expression v_clause_3 = *arg++;
     611           0 :       f_formula = f_formula + "(ite ";
     612           0 :       translate_clause(v_clause_1, true);
     613           0 :       f_formula = f_formula + " (+ ";
     614           0 :       translate_clause(v_clause_2, false);
     615           0 :       f_formula = f_formula + " ";
     616           0 :       translate_clause(v_clause_3, false);
     617           0 :       f_formula = f_formula + " 1) (+ ";
     618           0 :       translate_clause(v_clause_2, false);
     619           0 :       f_formula = f_formula + " ";
     620           0 :       translate_clause(v_clause_3, false);
     621           0 :       f_formula = f_formula + "))";
     622           0 :     }
     623             : 
     624           0 :     void translate_c_nat(const data_expression& a_clause)
     625             :     {
     626           0 :       const data_expression v_clause = arg(a_clause);
     627           0 :       translate_clause(v_clause, false);
     628           0 :     }
     629             : 
     630           0 :     void translate_c_int(const data_expression& a_clause)
     631             :     {
     632           0 :       const data_expression v_clause = arg(a_clause);
     633           0 :       translate_clause(v_clause, false);
     634           0 :     }
     635             : 
     636           0 :     void translate_unknown_operator(const data_expression& a_clause)
     637             :     {
     638           0 :       data_expression h = atermpp::down_cast<application>(a_clause).head();
     639           0 :       const function_symbol& v_operator = atermpp::down_cast<function_symbol>(h);
     640           0 :       std::map < function_symbol, std::size_t >::const_iterator i=f_operators.find(v_operator);
     641             : 
     642           0 :       std::size_t v_operator_number=f_operators.size(); // This is the value if v_operator does not occur in f_operators.
     643           0 :       if (i==f_operators.end()) // not found.
     644             :       {
     645           0 :         f_operators[v_operator]=v_operator_number;
     646             :       }
     647             :       else
     648             :       {
     649           0 :         v_operator_number=i->second; // this is the number already assigned to v_operator.
     650             :       }
     651           0 :       std::stringstream v_operator_string;
     652           0 :       v_operator_string << "op" << v_operator_number;
     653           0 :       f_formula = f_formula + "(" + v_operator_string.str();
     654             : 
     655           0 :       if (data::is_application(a_clause))
     656             :       {
     657           0 :         const data::application& a = atermpp::down_cast<data::application>(a_clause);
     658           0 :         for (application::const_iterator i = a.begin(); i != a.end(); ++i)
     659             :         {
     660           0 :           f_formula = f_formula + " ";
     661           0 :           translate_clause(*i, false);
     662             :         }
     663             :       }
     664           0 :       f_formula = f_formula + ")";
     665           0 :     }
     666             : 
     667           0 :     void translate_variable(const variable& a_clause)
     668             :     {
     669           0 :       std::string v_string = a_clause.name();
     670           0 :       f_formula = f_formula + v_string;
     671             : 
     672           0 :       f_variables.insert(a_clause);
     673           0 :     }
     674             : 
     675           0 :     void translate_nat_variable(const variable& a_clause)
     676             :     {
     677           0 :       std::string v_string = a_clause.name();
     678           0 :       f_formula = f_formula + v_string;
     679             : 
     680           0 :       f_variables.insert(a_clause);
     681           0 :       f_nat_variables.insert(a_clause);
     682           0 :     }
     683             : 
     684           0 :     void translate_pos_variable(const variable& a_clause)
     685             :     {
     686           0 :       std::string v_string = a_clause.name();
     687           0 :       f_formula = f_formula + v_string;
     688             : 
     689           0 :       f_variables.insert(a_clause);
     690           0 :       f_pos_variables.insert(a_clause);
     691           0 :     }
     692             : 
     693           0 :     void translate_int_constant(const data_expression& a_clause)
     694             :     {
     695           0 :       std::string v_value(data::sort_int::integer_constant_as_string(data::data_expression(a_clause)));
     696           0 :       if (v_value[0] == '-')
     697             :       {
     698           0 :         v_value[0] = '~';
     699           0 :         f_formula = f_formula + "(" + v_value + ")";
     700             :       }
     701             :       else
     702             :       {
     703           0 :         f_formula = f_formula + v_value;
     704             :       }
     705           0 :     }
     706             : 
     707           0 :     void translate_nat_constant(const data_expression& a_clause)
     708             :     {
     709           0 :       std::string v_value(data::sort_nat::natural_constant_as_string(data::data_expression(a_clause)));
     710           0 :       f_formula = f_formula + v_value;
     711           0 :     }
     712             : 
     713           0 :     void translate_pos_constant(const data_expression& a_clause)
     714             :     {
     715           0 :       std::string v_value(data::sort_pos::positive_constant_as_string(data::data_expression(a_clause)));
     716           0 :       f_formula = f_formula + v_value;
     717           0 :     }
     718             : 
     719           0 :     void translate_true()
     720             :     {
     721           0 :       f_formula = f_formula + "true";
     722           0 :     }
     723             : 
     724           0 :     void translate_false()
     725             :     {
     726           0 :       f_formula = f_formula + "false";
     727           0 :     }
     728             : 
     729           0 :     void translate_function_symbol(const data_expression& a_clause)
     730             :     {
     731           0 :       const function_symbol& v_operator = atermpp::down_cast<function_symbol>(a_clause);
     732           0 :       std::map < function_symbol, std::size_t >::const_iterator i=f_operators.find(v_operator);
     733             : 
     734           0 :       std::size_t v_operator_number=f_operators.size(); // This is the value if v_operator does not occur in f_operators.
     735           0 :       if (i==f_operators.end()) // not found.
     736             :       {
     737           0 :         f_operators[v_operator]=v_operator_number;
     738             :       }
     739             :       else
     740             :       {
     741           0 :         v_operator_number=i->second; // this is the number already assigned to v_operator.
     742             :       }
     743             : 
     744           0 :       std::stringstream v_operator_string;
     745           0 :       v_operator_string << "op" << v_operator_number;
     746           0 :       f_formula = f_formula + v_operator_string.str();
     747           0 :     }
     748             : 
     749           0 :     void add_nat_clauses()
     750             :     {
     751           0 :       for(const variable& f_nat_variable : f_nat_variables)
     752             :       {
     753           0 :         std::string v_variable_string = f_nat_variable.name();
     754           0 :         f_formula = f_formula + " (>= " + v_variable_string + " 0)";
     755             :       }
     756           0 :     }
     757             : 
     758           0 :     void add_pos_clauses()
     759             :     {
     760           0 :       for(const variable& f_pos_variable : f_pos_variables)
     761             :       {
     762           0 :         std::string v_variable_string = f_pos_variable.name();
     763           0 :         f_formula = f_formula + " (>= " + v_variable_string + " 1)";
     764             :       }
     765           0 :     }
     766             : 
     767             :   protected:
     768             :     std::string f_benchmark;
     769             : 
     770             :     /// precondition: The argument passed as parameter a_formula is a list of expressions of sort Bool in internal mCRL2
     771             :     /// format. The argument represents a formula in conjunctive normal form, where the elements of the list represent the
     772             :     /// clauses
     773           0 :     void translate(data_expression_list a_formula)
     774             :     {
     775           0 :       data_expression v_clause;
     776             : 
     777           0 :       f_variables.clear();
     778           0 :       f_nat_variables.clear();
     779           0 :       f_pos_variables.clear();
     780           0 :       f_bool2pred = false;
     781             : 
     782           0 :       f_formula = "  :formula (and";
     783           0 :       mCRL2log(log::verbose) << "Formula to be solved: " << a_formula << std::endl;
     784           0 :       while (!a_formula.empty())
     785             :       {
     786           0 :         v_clause = a_formula.front();
     787           0 :         a_formula.pop_front();
     788           0 :         f_formula = f_formula + " ";
     789           0 :         translate_clause(v_clause, true);
     790             :       }
     791           0 :       add_nat_clauses();
     792           0 :       add_pos_clauses();
     793           0 :       f_formula = f_formula + ")\n";
     794           0 :       declare_variables();
     795           0 :       declare_operators();
     796           0 :       declare_predicates();
     797           0 :       declare_sorts();
     798           0 :       produce_notes_for_sorts();
     799           0 :       produce_notes_for_operators();
     800           0 :       produce_notes_for_predicates();
     801           0 :       f_benchmark =
     802           0 :         "(benchmark nameless\n" + f_sorts_notes + f_operators_notes + f_predicates_notes +
     803           0 :         f_extrasorts + f_operators_extrafuns + f_variables_extrafuns + f_extrapreds + f_formula +
     804           0 :         ")\n";
     805           0 :       mCRL2log(log::verbose) << "Corresponding benchmark:" << std::endl << f_benchmark;;
     806           0 :     }
     807             : 
     808             : 
     809             :   public:
     810           0 :     SMT_LIB_Solver()
     811           0 :     {
     812           0 :     }
     813             : 
     814           0 :     virtual ~SMT_LIB_Solver()
     815           0 :     {
     816           0 :     }
     817             : };
     818             : 
     819             : namespace prover
     820             : {
     821             : 
     822             : /**
     823             :  * Template class for SMT provers that come as an external binary and use the
     824             :  * SMT-lib format. Input to the tool is specified on standard input,
     825             :  * output is read from standard output and matches one of the strings:
     826             :  * "sat", "unsat", "unknown".
     827             :  *
     828             :  * Parameter T follows the curiously recurring template pattern (CRTP). Type T
     829             :  * is required to have the name and exec methods as in the example below.
     830             :  *
     831             :  *  \code
     832             :  *  class cvc_smt_solver : public binary_smt_solver< cvc_smt_solver > {
     833             :  *    inline static char* name() {
     834             :  *      return "CVC3";
     835             :  *    }
     836             :  *
     837             :  *    inline static void exec() {
     838             :  *      ::execlp("cvc", "cvc3", "-lang smt-lib", 0);
     839             :  *    }
     840             :  *  };
     841             :  *  \endcode
     842             :  **/
     843             : template < typename T >
     844             : class binary_smt_solver
     845             : {
     846             : 
     847             :   protected:
     848             : 
     849             :     // \brief Calls one of the exec functions
     850             :     static bool execute(std::string const& benchmark);
     851             : 
     852             :   public:
     853             : 
     854             :     // \brief Checks the availability/usability of the prover
     855             :     static bool usable();
     856             : };
     857             : #if !(defined(_MSC_VER) || defined(__MINGW32__) || defined(__CYGWIN__))
     858             : /// The class inherits from the class SMT_LIB_Solver. It uses the SMT solver
     859             : /// CVC / (http://www.cs.nyu.edu/acsys/cvcl/) to determine the satisfiability
     860             : /// of propositional formulas. To use the solver CVC / the directory containing
     861             : /// the corresponding executable must be in the path.
     862             : ///
     863             : /// The static method usable can be used to check checks if CVC's executable is indeed available.
     864             : ///
     865             : /// The method SMT_Solver_CVC::is_satisfiable receives a formula in conjunctive normal form as parameter a_formula and
     866             : /// indicates whether or not this formula is satisfiable.
     867           0 : class cvc_smt_solver : public SMT_LIB_Solver, public binary_smt_solver< cvc_smt_solver >
     868             : {
     869             :     friend class binary_smt_solver< cvc_smt_solver >;
     870             : 
     871             :   private:
     872             : 
     873           0 :     inline static char const* name()
     874             :     {
     875           0 :       return "CVC3";
     876             :     }
     877             : 
     878           0 :     inline static void exec()
     879             :     {
     880           0 :       ::execlp("cvc3", "cvc3", "-lang", "smt", (char*)nullptr);
     881           0 :     }
     882             : 
     883             :   public:
     884             : 
     885             :     /// precondition: The argument passed as parameter a_formula is a list of expressions of sort Bool in internal mCRL2
     886             :     /// format. The argument represents a formula in conjunctive normal form, where the elements of the list represent the
     887             :     /// clauses
     888           0 :     bool is_satisfiable(const data_expression_list& a_formula)
     889             :     {
     890           0 :       translate(a_formula);
     891             : 
     892           0 :       return execute(f_benchmark);
     893             :     }
     894             : };
     895             : 
     896             : /// The class inherits from the class SMT_LIB_Solver. It uses the SMT solver
     897             : /// Z3 / (https://github.com/Z3Prover/z3) to determine the satisfiability
     898             : /// of propositional formulas. To use the solver Z3 / the directory containing
     899             : /// the corresponding executable must be in the path.
     900             : ///
     901             : /// The static method usable can be used to check checks if Z3's executable is indeed available.
     902             : ///
     903             : /// The method z3_smt_solver::is_satisfiable receives a formula in conjunctive normal form as parameter a_formula and
     904             : /// indicates whether or not this formula is satisfiable.
     905           0 : class z3_smt_solver : public SMT_LIB_Solver, public binary_smt_solver< z3_smt_solver >
     906             : {
     907             :     friend class binary_smt_solver< z3_smt_solver >;
     908             : 
     909             :   private:
     910             : 
     911           0 :     inline static char const* name()
     912             :     {
     913           0 :       return "Z3";
     914             :     }
     915             : 
     916           0 :     inline static void exec()
     917             :     {
     918           0 :       ::execlp("z3", "z3", "-smt", "-in", (char*)nullptr);
     919           0 :     }
     920             : 
     921             :   public:
     922             : 
     923             :     /// precondition: The argument passed as parameter a_formula is a list of expressions of sort Bool in internal mCRL2
     924             :     /// format. The argument represents a formula in conjunctive normal form, where the elements of the list represent the
     925             :     /// clauses
     926           0 :     bool is_satisfiable(const data_expression_list& a_formula)
     927             :     {
     928           0 :       translate(a_formula);
     929             : 
     930           0 :       return execute(f_benchmark);
     931             :     }
     932             : };
     933             : 
     934             : /// The class inherits from the class SMT_LIB_Solver. It uses the SMT solver Ario 1.1
     935             : /// (http://www.eecs.umich.edu/~ario/) to determine the satisfiability of propositional formulas. To use the solver Ario
     936             : /// 1.1, the directory containing the corresponding executable must be in the path.
     937             : ///
     938             : /// The static method usable can be used to check checks if CVC's executable is indeed available.
     939             : ///
     940             : /// The method is_satisfiable receives a formula in conjunctive normal form as parameter a_formula and
     941             : /// indicates whether or not this formula is satisfiable.
     942             : class ario_smt_solver : public SMT_LIB_Solver, public binary_smt_solver< ario_smt_solver >
     943             : {
     944             :     friend class binary_smt_solver< ario_smt_solver >;
     945             : 
     946             :   private:
     947             : 
     948           0 :     inline static char const* name()
     949             :     {
     950           0 :       return "Ario";
     951             :     }
     952             : 
     953           0 :     inline static void exec()
     954             :     {
     955           0 :       ::execlp("ario", "ario", (char*)nullptr);
     956           0 :     }
     957             : 
     958             :   public:
     959             : 
     960             :     /// precondition: The argument passed as parameter a_formula is a list of expressions of sort Bool in internal mCRL2
     961             :     /// format. The argument represents a formula in conjunctive normal form, where the elements of the list represent the
     962             :     /// clauses
     963             :     bool is_satisfiable(const data_expression_list& a_formula)
     964             :     {
     965             :       translate(a_formula);
     966             : 
     967             :       return execute(f_benchmark);
     968             :     }
     969             : };
     970             : #endif
     971             : } // namespace prover
     972             : 
     973             : } // namespace detail
     974             : } // namespace data
     975             : } // namespace mcrl2
     976             : 
     977             : #endif

Generated by: LCOV version 1.13