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/solver.h"
      14             : 
      15             : using namespace mcrl2;
      16             : 
      17           0 : int main(int /*argc*/, char** /*argv*/)
      18             : {
      19             :   // note that the newline characters are significant
      20             :   data::data_specification data_spec = data::parse_data_specification(
      21             :                                    "sort                              \n"
      22             :                                    "  Bit   = struct b0(r:Real) | b1; \n"
      23             :                                    "                                  \n"
      24             :                                    "map                               \n"
      25             :                                    "  invert: Bit -> Bit;             \n"
      26             :                                    "                                  \n"
      27             :                                    "var                               \n"
      28             :                                    "  r1: Real;                       \n"
      29             :                                    "                                  \n"
      30             :                                    "eqn                               \n"
      31             :                                    "  invert(b1)= b0(1);              \n"
      32             :                                    "  invert(b0(r1))= b1;             \n"
      33           0 :                                  );
      34             : 
      35           0 :   smt::smt_solver solv(data_spec);
      36           0 :   data::variable vb1 = data::parse_variable("bit_1: Bit", data_spec);
      37           0 :   data::variable vb2 = data::parse_variable("bit_2: Bit", data_spec);
      38           0 :   data::variable_list bit_vars({vb1});
      39             :   // This may not terminate
      40           0 :   smt::answer result = solv.solve(bit_vars, data::parse_data_expression("invert(invert(bit_1)) != bit_1", bit_vars, data_spec), std::chrono::seconds(5));
      41           0 :   std::cout << "result " << result << std::endl;
      42             : 
      43           0 :   return 0;
      44           0 : }