Line data    Source code

       1             : // Author(s): Thomas Neele
       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 run_solver.cpp
      10             : 
      11             : #include "mcrl2/data/data.h"
      12             : #include "mcrl2/data/parse.h"
      13             : #include "mcrl2/smt/translate_specification.h"
      14             : #include "mcrl2/smt/solver.h"
      15             : 
      16             : using namespace mcrl2;
      17             : 
      18           0 : int main(int /*argc*/, char** /*argv*/)
      19             : {
      20             :   // note that the newline characters are significant
      21             :   data::data_specification data_spec = data::parse_data_specification(
      22             :                                    "sort                                                              \n"
      23             :                                    "  Bit   = struct b0 | b1;                                         \n"
      24             :                                    "                                                                  \n"
      25             :                                    "map                                                               \n"
      26             :                                    "  invert: Bit -> Bit;                                             \n"
      27             :                                    "                                                                  \n"
      28             :                                    "eqn                                                               \n"
      29             :                                    "  invert(b1)= b0;                                                 \n"
      30             :                                    "  invert(b0)= b1;                                                 \n"
      31             :                                    "                                                                  \n"
      32             :                                    "map                                                               \n"
      33             :                                    "  insertB: Bool # Nat # List(Bool) -> List(Bool);                 \n"
      34             :                                    "var                                                               \n"
      35             :                                    "  d,d': Bool; i: Nat; q: List(Bool);                              \n"
      36             :                                    "eqn                                                               \n"
      37             :                                    "  i == 0 -> insertB(d,i,q)     = d  |> tail(q);                   \n"
      38             :                                    "  i > 0  -> insertB(d,i,d'|>q) = d' |> insertB(d,Int2Nat(i-1),q); \n"
      39             :                                    "                                                                  \n"
      40           0 :                                  );
      41           0 :   smt::native_translations ntm = smt::initialise_native_translation(data_spec);
      42             : 
      43           0 :   std::ostringstream out;
      44           0 :   std::unordered_map<data::data_expression, std::string> cache;
      45           0 :   smt::translate_data_specification(data_spec, out, cache, ntm);
      46           0 :   std::cout << out.str() << std::endl;
      47             : 
      48           0 :   smt::smt_solver solv(data_spec);
      49             : 
      50             :   smt::answer result;
      51           0 :   data::variable vp1("p1", data::sort_pos::pos());
      52           0 :   data::variable vp2("p2", data::sort_pos::pos());
      53           0 :   data::variable_list pos_vars({vp1, vp2});
      54           0 :   result = solv.solve(pos_vars, data::parse_data_expression("(p1 == p2 + 2) && (p1 == p2 * 2)", pos_vars, data_spec));
      55           0 :   std::cout << "result " << result << std::endl;
      56             : 
      57           0 :   data::variable vb1 = data::parse_variable("bit1: Bit", data_spec);
      58           0 :   data::variable vb2 = data::parse_variable("bit2: Bit", data_spec);
      59           0 :   data::variable_list bit_vars({vb1, vb2});
      60           0 :   result = solv.solve(data::variable_list(), data::parse_data_expression("forall bit1: Bit. invert(invert(bit1)) == bit1", data::variable_list(), data_spec));
      61           0 :   std::cout << "result " << result << std::endl;
      62             : 
      63           0 :   return 0;
      64           0 : }