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 : }
|