LCOV - code coverage report
Current view: top level - data/test - quantifier_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 88 93 94.6 %
Date: 2024-03-08 02:52:28 Functions: 9 9 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Frank Stappers
       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 quantifier_test.cpp
      10             : /// \brief Basic regression test for quantifier expressions.
      11             : 
      12             : #define BOOST_TEST_MODULE quantifier_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/detail/rewrite_strategies.h"
      16             : #include "mcrl2/data/list.h"
      17             : #include "mcrl2/data/parse.h"
      18             : #include "mcrl2/data/rewriter.h"
      19             : #include "mcrl2/data/rewriters/quantifiers_inside_rewriter.h"
      20             : #include "mcrl2/data/set.h"
      21             : 
      22             : using namespace mcrl2;
      23             : using namespace mcrl2::data;
      24             : using namespace mcrl2::data::sort_list;
      25             : 
      26          34 : void quantifier_expression_test(const std::string& expr1_text, const std::string& expr2_text, const data_specification& dataspec, const rewriter& r)
      27             : {
      28          34 :   data_expression expr1 = parse_data_expression(expr1_text, dataspec);
      29          34 :   data_expression expr2 = parse_data_expression(expr2_text, dataspec);
      30          34 :   std::cout << "Testing " << expr1_text << " <-> " << expr2_text << std::endl;
      31          34 :   if (r(expr1) != expr2)
      32             :   {
      33           0 :     std::cout << "--- ERROR ---\n";
      34           0 :     std::cout << " expr1    = " << expr1 << std::endl;
      35           0 :     std::cout << " r(expr1) = " << r(expr1) << std::endl;
      36           0 :     std::cout << " expr2    = " << expr2 << std::endl;
      37           0 :     BOOST_CHECK(r(expr1) == expr2);
      38             :   }
      39          34 : }
      40             : 
      41           1 : void quantifier_expression_test(mcrl2::data::rewrite_strategy s)
      42             : {
      43           1 :   data_specification dataspec;
      44           1 :   rewriter r(dataspec, s);
      45             : 
      46             :   // tests for Bool
      47           1 :   quantifier_expression_test("exists x: Bool. x == false", "true", dataspec, r);
      48           1 :   quantifier_expression_test("forall x: Bool. x == false", "false", dataspec, r);
      49           1 :   quantifier_expression_test("exists x: Bool. x == true", "true", dataspec, r);
      50           1 :   quantifier_expression_test("forall x: Bool. x == true", "false", dataspec, r);
      51           1 :   quantifier_expression_test("forall x: Bool. x == true && x==false", "false", dataspec, r);
      52           1 :   quantifier_expression_test("exists x: Bool. x == true && x==false", "false", dataspec, r);
      53           1 :   quantifier_expression_test("forall x: Bool. x == true || x==false", "true", dataspec, r);
      54           1 :   quantifier_expression_test("exists x: Bool. x == true || x==false", "true", dataspec, r);
      55           1 :   quantifier_expression_test("forall x:Bool.exists y: Bool. x == y", "true", dataspec, r);
      56           1 :   quantifier_expression_test("exists x: Bool.forall y:Bool.x == y", "false", dataspec, r);
      57           1 :   quantifier_expression_test("forall b: Bool. b", "false", dataspec, r);
      58             : 
      59             :   // tests for Pos / Nat
      60           1 :   dataspec.add_context_sort(sort_nat::nat());
      61           1 :   dataspec.add_context_sort(sort_set::set_(sort_nat::nat()));
      62           1 :   r = rewriter(dataspec, s);
      63           1 :   quantifier_expression_test("1<2", "true",dataspec, r);
      64           1 :   quantifier_expression_test("exists x: Nat. (  x in {1,2,25,600} && 25 == x )", "true", dataspec, r);
      65             : 
      66             :   // Rewriter only enumerates up to some bound, check whether it can find small solutions
      67           1 :   quantifier_expression_test("exists n:Nat . n div 2 == 1", "true", dataspec, r);
      68           1 :   quantifier_expression_test("forall n:Nat . n div 2 == 1", "false", dataspec, r);
      69             : 
      70             : 
      71           1 :   quantifier_expression_test("forall x: Nat. x == 3", "false", dataspec, r);
      72           1 :   quantifier_expression_test("exists x: Nat. x == 3", "true", dataspec, r);
      73           1 :   quantifier_expression_test("forall x: Pos. exists y: Pos.x == y+1", "false", dataspec, r);
      74           1 :   quantifier_expression_test("forall x: Pos. exists y1,y2:Pos.x==y1+y2", "false", dataspec, r);
      75             :   // The rewriter cannot deal with this
      76             :   // quantifier_expression_test("forall x: Nat. exists y1,y2:Nat.x==y1+y2", "true", dataspec, r);
      77             : 
      78             :   /* Test 15. Test whether elimination of quantifiers also happens inside a term. */
      79           1 :   quantifier_expression_test("(exists x_0: Bool. false) && (forall x_0: Nat. true)", "false", dataspec, r);
      80           1 :   quantifier_expression_test("(forall x_0: Pos. true) || (exists x_0: Bool. false)", "true", dataspec, r);
      81             : 
      82             :   // The four tests below may need to be changed when the implementation of the
      83             :   // rewriter/enumerator is improved to deal with them
      84             :   // The test below is too complex for the enumerator to solve.
      85             :   // It is included to verify that at least no wrong result is produced
      86             :   // quantifier_expression_test("forall x: Pos. exists y: Nat.x == y+1", "forall x: Pos. exists y: Nat.x == y+1", dataspec, r);
      87             :   // This test depends on the naming of variables in the enumerator
      88             :   // quantifier_expression_test("forall x: Nat. exists y: Nat. y == x", "true", dataspec, r);
      89             : 
      90             :   // Tests with Real numbers, which will in general not be rewritten
      91           1 :   dataspec.add_context_sort(sort_real::real_());
      92           1 :   quantifier_expression_test("forall r:Real . r < 5", "forall r:Real . r < 5", dataspec, r);
      93           1 :   quantifier_expression_test("exists r:Real . r >= 10", "exists r:Real . r >= 10", dataspec, r);
      94             : 
      95             :   // tests for struct / List
      96           2 :   dataspec = parse_data_specification("sort S = struct s1?is_s1 | s2?is_s2;"
      97             :                                       "sort T = struct t;"
      98           1 :                                       "sort L = List(T);");
      99           1 :   r = rewriter(dataspec, s);
     100             : 
     101           1 :   quantifier_expression_test("exists s: S.( is_s1(s) && is_s2(s) )", "false", dataspec, r);
     102           1 :   quantifier_expression_test("exists s: S.( s == s2 && is_s2(s) )", "true", dataspec, r);
     103           1 :   quantifier_expression_test("forall y: T. y in [t]", "true", dataspec, r);
     104             : 
     105             : /* Should work but takes too much time.
     106             :   dataspec = parse_data_specification(
     107             :   " sort A = struct ac( first: Bool, args: List(Bool));"
     108             :   " "
     109             :   " map COMM: List(Bool)#Bool#List(A) -> List(A);"
     110             :   "     COMM: List(Bool)#Bool#List(A)#(List(Bool)->FBag(Bool))#FBag(Bool) -> List(A);"
     111             :   "     MAC: List(Bool) -> FBag(Bool);"
     112             :   "     PART: List(A)#(List(Bool) -> FBag(Bool)) -> (List(Bool) -> FBag(Bool));"
     113             :   "     ELM: List(Bool)#Bool#List(A)#List(Bool)#List(Bool) -> List(A);"
     114             :   "     RM: A#List(A)->List(A);"
     115             :   " var func: List(Bool)->FBag(Bool);"
     116             :   "     as: List(A);"
     117             :   "     ca: Bool;"
     118             :   "     cal: List(Bool);"
     119             :   "     cal_const: List(Bool);"
     120             :   "     al: Bool;"
     121             :   "     lsa: List(A);"
     122             :   "     m: FBag(Bool);"
     123             :   "     args: List(Bool);"
     124             :   "     a, b: A;"
     125             :   " eqn PART( [] , func ) = func;"
     126             :   "     PART( a |> as , func ) = PART( as, func[ args(a) -> func(args(a)) + {first(a):1}]  );"
     127             :   "     MAC( [] ) = {:};"
     128             :   "     MAC( ca |> cal ) = {ca:1} + MAC(cal);"
     129             :   " "
     130             :   "     COMM( cal, al, lsa ) = COMM( cal, al, lsa,  PART( lsa, lambda x: List(Bool). {:} ), MAC(cal) );"
     131             :   "     COMM( cal, al, [] , func, m ) = [];"
     132             :   "     COMM( cal, al, a |> lsa, func, m ) = if( m <= func(args(a)), "
     133             :   "                                                      ELM( cal, al, a |> lsa, args(a) , cal ) , "
     134             :   "                                                      a |> COMM( cal, al, lsa, func, m)"
     135             :   "                                                    );"
     136             :   "     ELM( [] , al, lsa, args, cal_const ) = [ac(al, args)] ++ COMM( cal_const, al, lsa );"
     137             :   "     ELM( ca |> cal, al, lsa, args, cal_const ) = ELM( cal, al , RM( ac( ca ,args), lsa), args, cal_const );"
     138             :   "     RM( a, [] ) = [];"
     139             :   "     RM( a, b |> lsa ) = if(a == b , lsa,  b |> RM( a, lsa)) ;"
     140             :   );
     141             :   r = rewriter(dataspec, s);
     142             : 
     143             :   quantifier_expression_test("exists x_0: List(A). x_0 == [ac( false, []), ac(true, []), ac(false, [])] && [ac(true, []), ac(true, [])] == COMM([false, false], true, x_0, PART(x_0, lambda x: List(Bool). {:}), {false: 2}) ", "true", dataspec, r);
     144             :   quantifier_expression_test("exists x_0: List(A). [ac(true, []), ac(true, [])] == "
     145             :        "        COMM([false, false], true, x_0, PART(x_0, lambda x: List(Bool). {:}), {false: 2}) &&  "
     146             :        "        x_0 == [ac( false, []), ac(true, []), ac(false, [])]", "true", dataspec, r);
     147             : */
     148             : 
     149             :   // tests for Set
     150           1 :   dataspec = parse_data_specification( "sort A = Set(Bool);");
     151           1 :   r = rewriter(dataspec, s);
     152             : 
     153             :   /* Test that exists and forall over a non enumerable sort (situation winter 2012)
     154             :      with a trivial predicate can still be reduced, by removing the variable. */
     155           1 :   quantifier_expression_test("exists x:Set(Bool). x==x", "true", dataspec, r);
     156           1 :   quantifier_expression_test("forall x:Set(Bool). x==x", "true", dataspec, r);
     157           1 :   quantifier_expression_test("exists x:Set(Bool). x!=x", "false", dataspec, r);
     158           1 :   quantifier_expression_test("forall x:Set(Bool). x!=x", "false", dataspec, r);
     159           1 : }
     160             : 
     161           1 : void quantifier_in_rewrite_rules_test(mcrl2::data::rewrite_strategy s)
     162             : {
     163             :   // The test below checks whether bound variables in rewrite rules are properly renamed
     164             :   // when substituting variables. In concreto, if the y in the eqn for f is substituted in
     165             :   // the body of g(x), then if y is substituted for x, the rhs of g(x) reduces to y!=y, or false.
     166             :   // The correct answer however is true, as f states taht for every boolean y there is an y' that
     167             :   // is not equal to it.
     168             :   data_specification dataspec = parse_data_specification(
     169             :                     "map f:Bool;\n"
     170             :                     "    g:Bool->Bool;\n"
     171             :                     "var x:Bool;\n"
     172             :                     "eqn f=forall y:Bool.g(y);\n"
     173           2 :                     "    g(x)=exists y:Bool.x!=y;\n");
     174             : 
     175           1 :   rewriter r(dataspec, s);
     176           1 :   quantifier_expression_test("f", "true", dataspec, r);
     177           1 : }
     178             : 
     179           1 : void test_mixed_enumeration()
     180             : {
     181           1 :   quantifier_expression_test("exists x:Real, p:Pos . p == 1 && x > 4", "exists x:Real . x > 4", data_specification(), data::rewriter(data_specification()));
     182           1 :   quantifier_expression_test("exists x:Real, p:Pos . p == 1", "true", data_specification(), data::rewriter(data_specification()));
     183           1 :   quantifier_expression_test("exists x:Real, p:Pos . x > 4", "exists x:Real . x > 4", data_specification(), data::rewriter(data_specification()));
     184           1 : }
     185             : 
     186          12 : void quantifier_inside_test(const std::string& expr1_text, const std::string& expr2_text, const std::vector<variable>& vars, const data_specification& dataspec)
     187             : {
     188          12 :   data_expression expr1 = parse_data_expression(expr1_text, vars, dataspec);
     189          12 :   data_expression expr2 = parse_data_expression(expr2_text, vars, dataspec);
     190          12 :   BOOST_CHECK_EQUAL(quantifiers_inside_rewrite(expr1), expr2);
     191          12 : }
     192             : 
     193           2 : BOOST_AUTO_TEST_CASE(test_quantifier_inside)
     194             : {
     195           1 :   data_specification dataspec;
     196           4 :   std::vector<variable> vars{variable("m", sort_nat::nat())};
     197             : 
     198           1 :   quantifier_inside_test("forall n:Nat. (m == 2 || m == 3)", "m == 2 || m == 3", vars, dataspec);
     199           1 :   quantifier_inside_test("forall n:Nat. (n == 2 || n == 3)", "forall n:Nat. (n == 2 || n == 3)", vars, dataspec);
     200           1 :   quantifier_inside_test("forall n:Nat. (n == m || m == 3)", "m == 3 || (forall n: Nat. n == m)", vars, dataspec);
     201           1 :   quantifier_inside_test("forall n:Nat. (n == m || n == 3)", "forall n: Nat. n == m || n == 3", vars, dataspec);
     202           1 :   quantifier_inside_test("forall n:Nat. false", "false", vars, dataspec);
     203           1 :   quantifier_inside_test("forall n:Nat. true", "true", vars, dataspec);
     204             : 
     205           1 :   quantifier_inside_test("exists n:Nat. (m == 2 && m == 3)", "m == 2 && m == 3", vars, dataspec);
     206           1 :   quantifier_inside_test("exists n:Nat. (n == 2 && n == 3)", "exists n:Nat. (n == 2 && n == 3)", vars, dataspec);
     207           1 :   quantifier_inside_test("exists n:Nat. (n == m && m == 3)", "m == 3 && (exists n: Nat. n == m)", vars, dataspec);
     208           1 :   quantifier_inside_test("exists n:Nat. (n == m && n == 3)", "exists n: Nat. n == m && n == 3", vars, dataspec);
     209           1 :   quantifier_inside_test("exists n:Nat. false", "false", vars, dataspec);
     210           1 :   quantifier_inside_test("exists n:Nat. true", "true", vars, dataspec);
     211           1 : }
     212             : 
     213           2 : BOOST_AUTO_TEST_CASE(test_main)
     214             : {
     215           1 :   auto strategies = data::detail::get_test_rewrite_strategies(false);
     216           2 :   for (const auto& strategy: strategies)
     217             :   {
     218           1 :     std::clog << "  Strategy: " << strategy << std::endl;
     219           1 :     quantifier_expression_test(strategy);
     220           1 :     quantifier_in_rewrite_rules_test(strategy);
     221             :   }
     222             : 
     223           1 :   test_mixed_enumeration();
     224           1 : }

Generated by: LCOV version 1.14