Line data Source code
1 : // Author(s): Jeroen van der Wulp
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 : #define BOOST_TEST_MODULE print_test
10 :
11 : #include <boost/test/included/unit_test.hpp>
12 :
13 : #include "mcrl2/data/parse.h"
14 : #include "mcrl2/data/print.h"
15 :
16 : using namespace mcrl2;
17 : using namespace mcrl2::data;
18 : using namespace mcrl2::data::sort_bool;
19 : using namespace mcrl2::data::sort_nat;
20 :
21 : template <typename T>
22 0 : void test_term(const std::string& , const T& x)
23 : {
24 0 : std::cout << data::pp(x) << std::endl;
25 0 : }
26 :
27 0 : void test_term(const std::string& s)
28 : {
29 0 : atermpp::aterm a = atermpp::read_term_from_string(s);
30 0 : if (s.find("DataEqn") == 0)
31 : {
32 0 : data_equation x (a);
33 0 : test_term(s, x);
34 0 : }
35 0 : else if (s.find("SortCons") == 0)
36 : {
37 0 : sort_expression x (a);
38 0 : test_term(s, x);
39 0 : }
40 0 : else if (s.find("OpId") == 0)
41 : {
42 0 : data::function_symbol x (a);
43 0 : test_term(s, x);
44 0 : }
45 : else
46 : {
47 0 : const data_expression& x = atermpp::down_cast<data_expression>(a);
48 0 : test_term(s, x);
49 : }
50 0 : }
51 :
52 2 : BOOST_AUTO_TEST_CASE(problem_cases)
53 : {
54 : /*
55 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Pos\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Pos\"))],SortCons(SortSet,SortId(\"Pos\")))),OpId(\"@false_\",SortArrow([SortId(\"Pos\")],SortId(\"Bool\"))),DataAppl(OpId(\"@fset_cons\",SortArrow([SortId(\"Pos\"),SortCons(SortFSet,SortId(\"Pos\"))],SortCons(SortFSet,SortId(\"Pos\")))),OpId(\"@c1\",SortId(\"Pos\")),OpId(\"@fset_empty\",SortCons(SortFSet,SortId(\"Pos\")))))");
56 :
57 : test_term("DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"ActionLabel\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"ActionLabel\"))],SortCons(SortBag,SortId(\"ActionLabel\")))),OpId(\"@zero_\",SortArrow([SortId(\"ActionLabel\")],SortId(\"Nat\"))),DataAppl(OpId(\"@fbag_cons\",SortArrow([SortId(\"ActionLabel\"),SortId(\"Pos\"),SortCons(SortFBag,SortId(\"ActionLabel\"))],SortCons(SortFBag,SortId(\"ActionLabel\")))),OpId(\"a1\",SortId(\"ActionLabel\")),OpId(\"@c1\",SortId(\"Pos\")),OpId(\"@fbag_empty\",SortCons(SortFBag,SortId(\"ActionLabel\")))))");
58 :
59 : test_term("DataEqn([DataVarId(\"X0\",SortCons(SortSet,SortId(\"Bool\"))),DataVarId(\"X1\",SortCons(SortSet,SortId(\"Bool\")))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"LiftGenerated_not\",SortArrow([SortCons(SortSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"X0\",SortCons(SortSet,SortId(\"Bool\")))),DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataAppl(OpId(\"lambda@1\",SortArrow([SortCons(SortSet,SortId(\"Bool\"))],SortArrow([SortId(\"Bool\")],SortId(\"Bool\")))),DataVarId(\"X0\",SortCons(SortSet,SortId(\"Bool\")))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\")))))");
60 :
61 : test_term("DataAppl(OpId(\"==\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Bool\"))),DataAppl(OpId(\"*\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Int\"))),DataVarId(\"x\",SortId(\"Int\")),DataAppl(OpId(\"@cInt\",SortArrow([SortId(\"Nat\")],SortId(\"Int\"))),DataAppl(OpId(\"@cNat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"q\",SortId(\"Pos\"))))),DataAppl(OpId(\"*\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Int\"))),DataVarId(\"y\",SortId(\"Int\")),DataAppl(OpId(\"@cInt\",SortArrow([SortId(\"Nat\")],SortId(\"Int\"))),DataAppl(OpId(\"@cNat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"p\",SortId(\"Pos\"))))))");
62 :
63 : test_term("DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortBag,SortId(\"Bool\")))),DataAppl(OpId(\"@add_\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))],SortArrow([SortId(\"Bool\")],SortId(\"Nat\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))),DataVarId(\"g\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\")))),DataAppl(OpId(\"@fbag_join\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Bool\")),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortFBag,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))),DataVarId(\"g\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))),DataVarId(\"b\",SortCons(SortFBag,SortId(\"Bool\"))),DataVarId(\"c\",SortCons(SortFBag,SortId(\"Bool\")))))");
64 :
65 : test_term("DataAppl(OpId(\"@bagcomp\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))],SortCons(SortBag,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))))");
66 : test_term("DataAppl(OpId(\"==\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataVarId(\"b\",SortId(\"Bool\")),DataVarId(\"b\",SortId(\"Bool\")))");
67 : test_term("OpId(\"e1\",SortId(\"Enum\"))");
68 :
69 : test_term("DataAppl(OpId(\"div\",SortArrow([SortId(\"Pos\"),SortId(\"Pos\")],SortId(\"Nat\"))),OpId(\"@c1\",SortId(\"Pos\")),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),DataVarId(\"b\",SortId(\"Bool\")),DataVarId(\"p\",SortId(\"Pos\"))))");
70 : test_term("DataAppl(OpId(\"@cNeg\",SortArrow([SortId(\"Pos\")],SortId(\"Int\"))),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"false\",SortId(\"Bool\")),DataVarId(\"p\",SortId(\"Pos\"))))");
71 : test_term("DataAppl(OpId(\"-\",SortArrow([SortId(\"Real\")],SortId(\"Real\"))),DataAppl(OpId(\"@cReal\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Real\"))),DataVarId(\"x\",SortId(\"Int\")),DataVarId(\"p\",SortId(\"Pos\"))))");
72 : test_term("DataAppl(OpId(\"@cReal\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Real\"))),DataAppl(OpId(\"-\",SortArrow([SortId(\"Int\")],SortId(\"Int\"))),DataVarId(\"x\",SortId(\"Int\"))),DataVarId(\"p\",SortId(\"Pos\")))");
73 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),OpId(\"@false_\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\"))))");
74 : test_term("OpId(\"@c0\",SortId(\"Nat\"))");
75 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),OpId(\"@false_\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\"))))");
76 :
77 : test_term("variable_list()", variable_list());
78 :
79 : test_term("DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortBag,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))),OpId(\"@fbag_empty\",SortCons(SortFBag,SortId(\"Bool\"))))");
80 :
81 : test_term("DataAppl(OpId(\"mod\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"y\",SortId(\"Int\")),DataVarId(\"q\",SortId(\"Pos\")))");
82 :
83 : test_term("SortCons(SortFSet,SortId(\"Bool\"))");
84 : test_term("SortCons(SortFBag,SortId(\"Bool\"))");
85 :
86 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),OpId(\"@false_\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))),DataVarId(\"s\",SortCons(SortFSet,SortId(\"Bool\"))))");
87 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\"))))");
88 : test_term("OpId(\"@c0\",SortId(\"Nat\"))");
89 : test_term("DataEqn([DataVarId(\"n\",SortId(\"Nat\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"exp\",SortArrow([SortId(\"Nat\"),SortId(\"Nat\")],SortId(\"Nat\"))),DataVarId(\"n\",SortId(\"Nat\")),OpId(\"@c0\",SortId(\"Nat\"))),DataAppl(OpId(\"@cNat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),OpId(\"@c1\",SortId(\"Pos\"))))");
90 : test_term("DataEqn([DataVarId(\"p\",SortId(\"Pos\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"@dub\",SortArrow([SortId(\"Bool\"),SortId(\"Int\")],SortId(\"Int\"))),OpId(\"false\",SortId(\"Bool\")),DataAppl(OpId(\"@cNeg\",SortArrow([SortId(\"Pos\")],SortId(\"Int\"))),DataVarId(\"p\",SortId(\"Pos\")))),DataAppl(OpId(\"@cNeg\",SortArrow([SortId(\"Pos\")],SortId(\"Int\"))),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"false\",SortId(\"Bool\")),DataVarId(\"p\",SortId(\"Pos\")))))");
91 : test_term("DataEqn([DataVarId(\"p\",SortId(\"Pos\")),DataVarId(\"x\",SortId(\"Int\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"-\",SortArrow([SortId(\"Real\")],SortId(\"Real\"))),DataAppl(OpId(\"@cReal\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Real\"))),DataVarId(\"x\",SortId(\"Int\")),DataVarId(\"p\",SortId(\"Pos\")))),DataAppl(OpId(\"@cReal\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Real\"))),DataAppl(OpId(\"-\",SortArrow([SortId(\"Int\")],SortId(\"Int\"))),DataVarId(\"x\",SortId(\"Int\"))),DataVarId(\"p\",SortId(\"Pos\"))))");
92 :
93 : test_term("DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortBag,SortId(\"Bool\")))),OpId(\"@zero_\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))),DataVarId(\"b\",SortCons(SortFBag,SortId(\"Bool\"))))");
94 :
95 : // <pp> @bagfbag(b) = @bagfbag(b)
96 : // <print>b = {b}
97 : // <aterm>DataEqn([DataVarId("b",SortCons(SortFBag,SortId("Bool")))],OpId("true",SortId("Bool")),DataAppl(OpId("@bagfbag",SortArrow([SortCons(SortFBag,SortId("Bool"))],SortCons(SortBag,SortId("Bool")))),[DataVarId("b",SortCons(SortFBag,SortId("Bool")))]),DataAppl(OpId("@bag",SortArrow([SortArrow([SortId("Bool")],SortId("Nat")),SortCons(SortFBag,SortId("Bool"))],SortCons(SortBag,SortId("Bool")))),[OpId("@zero_",SortArrow([SortId("Bool")],SortId("Nat"))),DataVarId("b",SortCons(SortFBag,SortId("Bool")))]))
98 : test_term("DataEqn([DataVarId(\"b\",SortCons(SortFBag,SortId(\"Bool\")))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"@bagfbag\",SortArrow([SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortBag,SortId(\"Bool\")))),DataVarId(\"b\",SortCons(SortFBag,SortId(\"Bool\")))),DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortBag,SortId(\"Bool\")))),OpId(\"@zero_\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))),DataVarId(\"b\",SortCons(SortFBag,SortId(\"Bool\")))))");
99 :
100 : test_term("DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"Nat\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Nat\"))],SortCons(SortBag,SortId(\"Nat\")))),Binder(Lambda,[DataVarId(\"x\",SortId(\"Nat\"))],DataVarId(\"x\",SortId(\"Nat\"))),OpId(\"@fbag_empty\",SortCons(SortFBag,SortId(\"Nat\"))))");
101 : // <pp> { b: Bool | b }
102 : // <print>{ [b: Bool] | b }
103 : // <aterm>DataAppl(OpId("@set",SortArrow([SortArrow([SortId("Bool")],SortId("Bool")),SortCons(SortFSet,SortId("Bool"))],SortCons(SortSet,SortId("Bool")))),[Binder(Lambda,[DataVarId("b",SortId("Bool"))],DataVarId("b",SortId("Bool"))),OpId("@sort_fset::empty",SortCons(SortFSet,SortId("Bool")))])
104 :
105 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),Binder(Lambda,[DataVarId(\"b\",SortId(\"Bool\"))],DataVarId(\"b\",SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\"))))");
106 :
107 : // <pp> { b: Bool | if(b, 2, 3) }
108 : // <print>{ [b: Bool] | if(b, 2, 3) }
109 : // <aterm>DataAppl(OpId("@bag",SortArrow([SortArrow([SortId("Bool")],SortId("Nat")),SortCons(SortFBag,SortId("Bool"))],SortCons(SortBag,SortId("Bool")))),[Binder(Lambda,[DataVarId("b",SortId("Bool"))],DataAppl(OpId("if",SortArrow([SortId("Bool"),SortId("Nat"),SortId("Nat")],SortId("Nat"))),[DataVarId("b",SortId("Bool")),DataAppl(OpId("Pos2Nat",SortArrow([SortId("Pos")],SortId("Nat"))),[DataAppl(OpId("@cDub",SortArrow([SortId("Bool"),SortId("Pos")],SortId("Pos"))),[OpId("false",SortId("Bool")),OpId("@c1",SortId("Pos"))])]),DataAppl(OpId("Pos2Nat",SortArrow([SortId("Pos")],SortId("Nat"))),[DataAppl(OpId("@cDub",SortArrow([SortId("Bool"),SortId("Pos")],SortId("Pos"))),[OpId("true",SortId("Bool")),OpId("@c1",SortId("Pos"))])])])),OpId("@fbag_empty",SortCons(SortFBag,SortId("Bool")))])
110 : test_term("DataAppl(OpId(\"@bag\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\")),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortBag,SortId(\"Bool\")))),Binder(Lambda,[DataVarId(\"b\",SortId(\"Bool\"))],DataAppl(OpId(\"if\",SortArrow([SortId(\"Bool\"),SortId(\"Nat\"),SortId(\"Nat\")],SortId(\"Nat\"))),DataVarId(\"b\",SortId(\"Bool\")),DataAppl(OpId(\"Pos2Nat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"false\",SortId(\"Bool\")),OpId(\"@c1\",SortId(\"Pos\")))),DataAppl(OpId(\"Pos2Nat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"true\",SortId(\"Bool\")),OpId(\"@c1\",SortId(\"Pos\")))))),OpId(\"@fbag_empty\",SortCons(SortFBag,SortId(\"Bool\"))))");
111 :
112 : // <pp> !true = false, !false = true, !!b = b, b && true = b, b && false = false, true && b = b, false && b = false, b || true = true, b || false = b, true || b = true, false || b = b, b => true = true, b => false = !b, true => b = b, false => b = true, true == b = b, false == b = !b, b == true = b, b == false = !b, false < b = b, true < b = false, b < false = false, b < true = !b, false <= b = true, true <= b = b, b <= false = !b, b <= true = true
113 : // <print>!true = false!false = true!!b = bb && true = bb && false = falsetrue && b = bfalse && b = falseb || true = trueb || false = btrue || b = truefalse || b = bb => true = trueb => false = !btrue => b = bfalse => b = truetrue == b = bfalse == b = !bb == true = bb == false = !bfalse < b = btrue < b = falseb < false = falseb < true = !bfalse <= b = truetrue <= b = bb <= false = !bb <= true = true
114 : // <aterm>unknown
115 :
116 : // <pp> 1 == 2 * p + 2 * if(b, 1, 0) = false
117 : // <print>1 == @cDub(b, p) = false
118 : // <aterm>DataEqn([DataVarId("b",SortId("Bool")),DataVarId("p",SortId("Pos"))],OpId("true",SortId("Bool")),DataAppl(OpId("==",SortArrow([SortId("Pos"),SortId("Pos")],SortId("Bool"))),[OpId("@c1",SortId("Pos")),DataAppl(OpId("@cDub",SortArrow([SortId("Bool"),SortId("Pos")],SortId("Pos"))),[DataVarId("b",SortId("Bool")),DataVarId("p",SortId("Pos"))])]),OpId("false",SortId("Bool")))
119 : test_term("DataEqn([DataVarId(\"b\",SortId(\"Bool\")),DataVarId(\"p\",SortId(\"Pos\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"==\",SortArrow([SortId(\"Pos\"),SortId(\"Pos\")],SortId(\"Bool\"))),OpId(\"@c1\",SortId(\"Pos\")),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),DataVarId(\"b\",SortId(\"Bool\")),DataVarId(\"p\",SortId(\"Pos\")))),OpId(\"false\",SortId(\"Bool\")))");
120 :
121 : test_term("DataAppl(OpId(\"mod\",SortArrow([SortId(\"Nat\"),SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"n\",SortId(\"Nat\")),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"false\",SortId(\"Bool\")),OpId(\"@c1\",SortId(\"Pos\"))))");
122 :
123 : // <pp> succ(succ(n)) = 2 * succ(n div 2) + 2 * if(n mod 2 == 1, 1, 0)
124 : // <print>succ(succ(n)) = @cDub(n mod 2 == 1, succ(n / 2))
125 : // <aterm>DataEqn([DataVarId("n",SortId("Nat"))],OpId("true",SortId("Bool")),DataAppl(OpId("succ",SortArrow([SortId("Pos")],SortId("Pos"))),[DataAppl(OpId("succ",SortArrow([SortId("Nat")],SortId("Pos"))),[DataVarId("n",SortId("Nat"))])]),DataAppl(OpId("@cDub",SortArrow([SortId("Bool"),SortId("Pos")],SortId("Pos"))),[DataAppl(OpId("==",SortArrow([SortId("Nat"),SortId("Nat")],SortId("Bool"))),[DataAppl(OpId("mod",SortArrow([SortId("Nat"),SortId("Pos")],SortId("Nat"))),[DataVarId("n",SortId("Nat")),DataAppl(OpId("@cDub",SortArrow([SortId("Bool"),SortId("Pos")],SortId("Pos"))),[OpId("false",SortId("Bool")),OpId("@c1",SortId("Pos"))])]),DataAppl(OpId("@cNat",SortArrow([SortId("Pos")],SortId("Nat"))),[OpId("@c1",SortId("Pos"))])]),DataAppl(OpId("succ",SortArrow([SortId("Nat")],SortId("Pos"))),[DataAppl(OpId("div",SortArrow([SortId("Nat"),SortId("Pos")],SortId("Nat"))),[DataVarId("n",SortId("Nat")),DataAppl(OpId("@cDub",SortArrow([SortId("Bool"),SortId("Pos")],SortId("Pos"))),[OpId("false",SortId("Bool")),OpId("@c1",SortId("Pos"))])])])]))
126 : test_term("DataEqn([DataVarId(\"n\",SortId(\"Nat\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"succ\",SortArrow([SortId(\"Pos\")],SortId(\"Pos\"))),DataAppl(OpId(\"succ\",SortArrow([SortId(\"Nat\")],SortId(\"Pos\"))),DataVarId(\"n\",SortId(\"Nat\")))),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),DataAppl(OpId(\"==\",SortArrow([SortId(\"Nat\"),SortId(\"Nat\")],SortId(\"Bool\"))),DataAppl(OpId(\"mod\",SortArrow([SortId(\"Nat\"),SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"n\",SortId(\"Nat\")),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"false\",SortId(\"Bool\")),OpId(\"@c1\",SortId(\"Pos\")))),DataAppl(OpId(\"@cNat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),OpId(\"@c1\",SortId(\"Pos\")))),DataAppl(OpId(\"succ\",SortArrow([SortId(\"Nat\")],SortId(\"Pos\"))),DataAppl(OpId(\"div\",SortArrow([SortId(\"Nat\"),SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"n\",SortId(\"Nat\")),DataAppl(OpId(\"@cDub\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\")],SortId(\"Pos\"))),OpId(\"false\",SortId(\"Bool\")),OpId(\"@c1\",SortId(\"Pos\")))))))");
127 :
128 : // <pp> n == -p = false
129 : // <print>n == @cNeg(p) = false
130 : // <aterm>DataEqn([DataVarId("n",SortId("Nat")),DataVarId("p",SortId("Pos"))],OpId("true",SortId("Bool")),DataAppl(OpId("==",SortArrow([SortId("Int"),SortId("Int")],SortId("Bool"))),[DataAppl(OpId("@cInt",SortArrow([SortId("Nat")],SortId("Int"))),[DataVarId("n",SortId("Nat"))]),DataAppl(OpId("@cNeg",SortArrow([SortId("Pos")],SortId("Int"))),[DataVarId("p",SortId("Pos"))])]),OpId("false",SortId("Bool")))
131 : test_term("DataEqn([DataVarId(\"n\",SortId(\"Nat\")),DataVarId(\"p\",SortId(\"Pos\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"==\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Bool\"))),DataAppl(OpId(\"@cInt\",SortArrow([SortId(\"Nat\")],SortId(\"Int\"))),DataVarId(\"n\",SortId(\"Nat\"))),DataAppl(OpId(\"@cNeg\",SortArrow([SortId(\"Pos\")],SortId(\"Int\"))),DataVarId(\"p\",SortId(\"Pos\")))),OpId(\"false\",SortId(\"Bool\")))");
132 :
133 : // <pp> x / p == y / q = x * q == y * p
134 : // <print>x == y = x * q == y * p
135 : // <aterm>DataEqn([DataVarId("p",SortId("Pos")),DataVarId("q",SortId("Pos")),DataVarId("x",SortId("Int")),DataVarId("y",SortId("Int"))],OpId("true",SortId("Bool")),DataAppl(OpId("==",SortArrow([SortId("Real"),SortId("Real")],SortId("Bool"))),[DataAppl(OpId("@cReal",SortArrow([SortId("Int"),SortId("Pos")],SortId("Real"))),[DataVarId("x",SortId("Int")),DataVarId("p",SortId("Pos"))]),DataAppl(OpId("@cReal",SortArrow([SortId("Int"),SortId("Pos")],SortId("Real"))),[DataVarId("y",SortId("Int")),DataVarId("q",SortId("Pos"))])]),DataAppl(OpId("==",SortArrow([SortId("Int"),SortId("Int")],SortId("Bool"))),[DataAppl(OpId("*",SortArrow([SortId("Int"),SortId("Int")],SortId("Int"))),[DataVarId("x",SortId("Int")),DataAppl(OpId("@cInt",SortArrow([SortId("Nat")],SortId("Int"))),[DataAppl(OpId("@cNat",SortArrow([SortId("Pos")],SortId("Nat"))),[DataVarId("q",SortId("Pos"))])])]),DataAppl(OpId("*",SortArrow([SortId("Int"),SortId("Int")],SortId("Int"))),[DataVarId("y",SortId("Int")),DataAppl(OpId("@cInt",SortArrow([SortId("Nat")],SortId("Int"))),[DataAppl(OpId("@cNat",SortArrow([SortId("Pos")],SortId("Nat"))),[DataVarId("p",SortId("Pos"))])])])]))
136 : test_term("DataEqn([DataVarId(\"p\",SortId(\"Pos\")),DataVarId(\"q\",SortId(\"Pos\")),DataVarId(\"x\",SortId(\"Int\")),DataVarId(\"y\",SortId(\"Int\"))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"==\",SortArrow([SortId(\"Real\"),SortId(\"Real\")],SortId(\"Bool\"))),DataAppl(OpId(\"@cReal\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Real\"))),DataVarId(\"x\",SortId(\"Int\")),DataVarId(\"p\",SortId(\"Pos\"))),DataAppl(OpId(\"@cReal\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Real\"))),DataVarId(\"y\",SortId(\"Int\")),DataVarId(\"q\",SortId(\"Pos\")))),DataAppl(OpId(\"==\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Bool\"))),DataAppl(OpId(\"*\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Int\"))),DataVarId(\"x\",SortId(\"Int\")),DataAppl(OpId(\"@cInt\",SortArrow([SortId(\"Nat\")],SortId(\"Int\"))),DataAppl(OpId(\"@cNat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"q\",SortId(\"Pos\"))))),DataAppl(OpId(\"*\",SortArrow([SortId(\"Int\"),SortId(\"Int\")],SortId(\"Int\"))),DataVarId(\"y\",SortId(\"Int\")),DataAppl(OpId(\"@cInt\",SortArrow([SortId(\"Nat\")],SortId(\"Int\"))),DataAppl(OpId(\"@cNat\",SortArrow([SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"p\",SortId(\"Pos\")))))))");
137 :
138 : test_term("OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\")))");
139 :
140 : // <pp> {} == {} = true
141 : // <print>@sort_fset::empty == @sort_fset::empty = true
142 : // <aterm>DataEqn([],OpId("true",SortId("Bool")),DataAppl(OpId("==",SortArrow([SortCons(SortFSet,SortId("Bool")),SortCons(SortFSet,SortId("Bool"))],SortId("Bool"))),[OpId("@sort_fset::empty",SortCons(SortFSet,SortId("Bool"))),OpId("@sort_fset::empty",SortCons(SortFSet,SortId("Bool")))]),OpId("true",SortId("Bool")))
143 : test_term("DataEqn([],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"==\",SortArrow([SortCons(SortFSet,SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\")))),OpId(\"true\",SortId(\"Bool\")))");
144 :
145 : test_term("DataAppl(OpId(\"@sort_set::set_fset\",SortArrow([SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"s\",SortCons(SortFSet,SortId(\"Bool\"))))");
146 :
147 : // <pp> @sort_set::set_fset(s) = @sort_set::set_fset(s)
148 : // <print>s = { x: Bool | @false_(x) != x in s }
149 : // <aterm>DataEqn([DataVarId("s",SortCons(SortFSet,SortId("Bool")))],OpId("true",SortId("Bool")),DataAppl(OpId("@sort_set::set_fset",SortArrow([SortCons(SortFSet,SortId("Bool"))],SortCons(SortSet,SortId("Bool")))),[DataVarId("s",SortCons(SortFSet,SortId("Bool")))]),DataAppl(OpId("@set",SortArrow([SortArrow([SortId("Bool")],SortId("Bool")),SortCons(SortFSet,SortId("Bool"))],SortCons(SortSet,SortId("Bool")))),[OpId("@false_",SortArrow([SortId("Bool")],SortId("Bool"))),DataVarId("s",SortCons(SortFSet,SortId("Bool")))]))
150 : test_term("DataEqn([DataVarId(\"s\",SortCons(SortFSet,SortId(\"Bool\")))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"@sort_set::set_fset\",SortArrow([SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"s\",SortCons(SortFSet,SortId(\"Bool\")))),DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),OpId(\"@false_\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))),DataVarId(\"s\",SortCons(SortFSet,SortId(\"Bool\")))))");
151 :
152 : // <pp> @fbag_cons(v0, v1, v2) < @fbag_cons(v3, v4, v5) = v0 < v3 || v0 == v3 && v1 < v4 || v1 == v4 && v2 < v5
153 : // <print>@fbag_cons(v0, v1, v2) < @fbag_cons(v3, v4, v5) = v0 < v3 || (v0 == v3 && (v1 < v4 || (v1 == v4 && v2 < v5)))
154 : // <aterm>DataEqn([DataVarId("v0",SortId("Bool")),DataVarId("v1",SortId("Pos")),DataVarId("v2",SortCons(SortFBag,SortId("Bool"))),DataVarId("v3",SortId("Bool")),DataVarId("v4",SortId("Pos")),DataVarId("v5",SortCons(SortFBag,SortId("Bool")))],OpId("true",SortId("Bool")),DataAppl(OpId("<",SortArrow([SortCons(SortFBag,SortId("Bool")),SortCons(SortFBag,SortId("Bool"))],SortId("Bool"))),[DataAppl(OpId("@fbag_cons",SortArrow([SortId("Bool"),SortId("Pos"),SortCons(SortFBag,SortId("Bool"))],SortCons(SortFBag,SortId("Bool")))),[DataVarId("v0",SortId("Bool")),DataVarId("v1",SortId("Pos")),DataVarId("v2",SortCons(SortFBag,SortId("Bool")))]),DataAppl(OpId("@fbag_cons",SortArrow([SortId("Bool"),SortId("Pos"),SortCons(SortFBag,SortId("Bool"))],SortCons(SortFBag,SortId("Bool")))),[DataVarId("v3",SortId("Bool")),DataVarId("v4",SortId("Pos")),DataVarId("v5",SortCons(SortFBag,SortId("Bool")))])]),DataAppl(OpId("||",SortArrow([SortId("Bool"),SortId("Bool")],SortId("Bool"))),[DataAppl(OpId("<",SortArrow([SortId("Bool"),SortId("Bool")],SortId("Bool"))),[DataVarId("v0",SortId("Bool")),DataVarId("v3",SortId("Bool"))]),DataAppl(OpId("&&",SortArrow([SortId("Bool"),SortId("Bool")],SortId("Bool"))),[DataAppl(OpId("==",SortArrow([SortId("Bool"),SortId("Bool")],SortId("Bool"))),[DataVarId("v0",SortId("Bool")),DataVarId("v3",SortId("Bool"))]),DataAppl(OpId("||",SortArrow([SortId("Bool"),SortId("Bool")],SortId("Bool"))),[DataAppl(OpId("<",SortArrow([SortId("Pos"),SortId("Pos")],SortId("Bool"))),[DataVarId("v1",SortId("Pos")),DataVarId("v4",SortId("Pos"))]),DataAppl(OpId("&&",SortArrow([SortId("Bool"),SortId("Bool")],SortId("Bool"))),[DataAppl(OpId("==",SortArrow([SortId("Pos"),SortId("Pos")],SortId("Bool"))),[DataVarId("v1",SortId("Pos")),DataVarId("v4",SortId("Pos"))]),DataAppl(OpId("<",SortArrow([SortCons(SortFBag,SortId("Bool")),SortCons(SortFBag,SortId("Bool"))],SortId("Bool"))),[DataVarId("v2",SortCons(SortFBag,SortId("Bool"))),DataVarId("v5",SortCons(SortFBag,SortId("Bool")))])])])])]))
155 : test_term("DataEqn([DataVarId(\"v0\",SortId(\"Bool\")),DataVarId(\"v1\",SortId(\"Pos\")),DataVarId(\"v2\",SortCons(SortFBag,SortId(\"Bool\"))),DataVarId(\"v3\",SortId(\"Bool\")),DataVarId(\"v4\",SortId(\"Pos\")),DataVarId(\"v5\",SortCons(SortFBag,SortId(\"Bool\")))],OpId(\"true\",SortId(\"Bool\")),DataAppl(OpId(\"<\",SortArrow([SortCons(SortFBag,SortId(\"Bool\")),SortCons(SortFBag,SortId(\"Bool\"))],SortId(\"Bool\"))),DataAppl(OpId(\"@fbag_cons\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\"),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortFBag,SortId(\"Bool\")))),DataVarId(\"v0\",SortId(\"Bool\")),DataVarId(\"v1\",SortId(\"Pos\")),DataVarId(\"v2\",SortCons(SortFBag,SortId(\"Bool\")))),DataAppl(OpId(\"@fbag_cons\",SortArrow([SortId(\"Bool\"),SortId(\"Pos\"),SortCons(SortFBag,SortId(\"Bool\"))],SortCons(SortFBag,SortId(\"Bool\")))),DataVarId(\"v3\",SortId(\"Bool\")),DataVarId(\"v4\",SortId(\"Pos\")),DataVarId(\"v5\",SortCons(SortFBag,SortId(\"Bool\"))))),DataAppl(OpId(\"||\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataAppl(OpId(\"<\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataVarId(\"v0\",SortId(\"Bool\")),DataVarId(\"v3\",SortId(\"Bool\"))),DataAppl(OpId(\"&&\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataAppl(OpId(\"==\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataVarId(\"v0\",SortId(\"Bool\")),DataVarId(\"v3\",SortId(\"Bool\"))),DataAppl(OpId(\"||\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataAppl(OpId(\"<\",SortArrow([SortId(\"Pos\"),SortId(\"Pos\")],SortId(\"Bool\"))),DataVarId(\"v1\",SortId(\"Pos\")),DataVarId(\"v4\",SortId(\"Pos\"))),DataAppl(OpId(\"&&\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataAppl(OpId(\"==\",SortArrow([SortId(\"Pos\"),SortId(\"Pos\")],SortId(\"Bool\"))),DataVarId(\"v1\",SortId(\"Pos\")),DataVarId(\"v4\",SortId(\"Pos\"))),DataAppl(OpId(\"<\",SortArrow([SortCons(SortFBag,SortId(\"Bool\")),SortCons(SortFBag,SortId(\"Bool\"))],SortId(\"Bool\"))),DataVarId(\"v2\",SortCons(SortFBag,SortId(\"Bool\"))),DataVarId(\"v5\",SortCons(SortFBag,SortId(\"Bool\")))))))))");
156 :
157 : test_term("DataAppl(OpId(\"@setcomp\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))))");
158 : test_term("DataAppl(OpId(\"@set\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\")),SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))),OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\"))))");
159 : */
160 1 : }
161 :
162 : template <typename ExpressionType>
163 79 : bool print_check(ExpressionType const& left, std::string const& right)
164 : {
165 79 : std::clog << "Checking printing of " << data::pp(left) << " with " << right << std::endl;
166 79 : if (pp(left) != right)
167 : {
168 0 : std::clog << "pp(" << left << ") != " << right << std::endl;
169 0 : std::clog << left << " != " << right << std::endl;
170 :
171 0 : return false;
172 : }
173 :
174 79 : return true;
175 : }
176 :
177 : template <typename Container>
178 9 : bool print_container_check(Container const& c)
179 : {
180 9 : std::string r = data::pp(c);
181 9 : if (r == "")
182 : {
183 0 : std::clog << "error printing container" << std::endl;
184 0 : return false;
185 : }
186 :
187 9 : return true;
188 9 : }
189 :
190 : #define PRINT_CHECK(x,y) BOOST_CHECK(print_check(x,y))
191 :
192 2 : BOOST_AUTO_TEST_CASE(test_function_symbol_print)
193 : {
194 2 : data::function_symbol f("f", sort_bool::bool_());
195 :
196 1 : PRINT_CHECK(f, "f");
197 1 : }
198 :
199 2 : BOOST_AUTO_TEST_CASE(test_application_print)
200 : {
201 2 : data::function_symbol f("f", make_function_sort_(bool_(), bool_()));
202 2 : data::function_symbol g("g", make_function_sort_(bool_(), nat(), bool_()));
203 :
204 1 : PRINT_CHECK(f(true_()), "f(true)");
205 1 : PRINT_CHECK(g(false_(), sort_nat::nat(10)), "g(false, 10)");
206 1 : PRINT_CHECK(g(f(true_()), sort_nat::nat(10)), "g(f(true), 10)");
207 1 : }
208 :
209 2 : BOOST_AUTO_TEST_CASE(test_abstraction_print)
210 : {
211 : using namespace sort_pos;
212 : using namespace sort_nat;
213 :
214 4 : variable_vector x {variable("x", sort_nat::nat())};
215 4 : variable_vector y {variable("y", sort_pos::pos())};
216 5 : variable_vector xy {x[0], y[0]};
217 :
218 1 : PRINT_CHECK(lambda(x, equal_to(x[0], nat(10))), "lambda x: Nat. x == 10");
219 1 : PRINT_CHECK(lambda(xy, equal_to(xy[0], pos2nat(xy[1]))), "lambda x: Nat, y: Pos. x == y");
220 1 : PRINT_CHECK(exists(x, equal_to(x[0], nat(10))), "exists x: Nat. x == 10");
221 1 : PRINT_CHECK(exists(xy, equal_to(xy[0], pos2nat(xy[1]))), "exists x: Nat, y: Pos. x == y");
222 1 : PRINT_CHECK(forall(x, equal_to(x[0], nat(10))), "forall x: Nat. x == 10");
223 1 : PRINT_CHECK(forall(xy, equal_to(xy[0], pos2nat(xy[1]))), "forall x: Nat, y: Pos. x == y");
224 1 : PRINT_CHECK(forall(x, exists(y, not_equal_to(xy[0], pos2nat(xy[1])))), "forall x: Nat. exists y: Pos. x != y");
225 1 : }
226 :
227 2 : BOOST_AUTO_TEST_CASE(test_list_print)
228 : {
229 : using namespace sort_bool;
230 : using namespace sort_list;
231 :
232 2 : data_expression empty_(empty(bool_()));
233 :
234 : // Using all operations
235 1 : BOOST_CHECK(print_check(empty(bool_()), "[]"));
236 1 : BOOST_CHECK(print_check(cons_(bool_(), true_(), empty_), "[true]"));
237 1 : BOOST_CHECK(print_check(cons_(bool_(), false_(), cons_(bool_(), true_(), empty_)), "[false, true]"));
238 : //BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), true_(), empty), false_()), "[true, false]"));
239 1 : BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), true_(), empty_), false_()), "[true] <| false"));
240 1 : BOOST_CHECK(print_check(snoc(bool_(), snoc(bool_(), empty_, true_()), false_()), "[true, false]"));
241 1 : BOOST_CHECK(print_check(cons_(bool_(), in(bool_(), false_(), cons_(bool_(), true_(), empty_)), empty_), "[false in [true]]"));
242 : //BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_())), true_()), "[false, true, true]"));
243 1 : BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_())), true_()), "(false |> [true]) <| true"));
244 : //BOOST_CHECK(print_check(in(bool_(), true_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_()))), "true in [false, true]"));
245 1 : BOOST_CHECK(print_check(in(bool_(), true_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_()))), "true in false |> [true]"));
246 : //BOOST_CHECK(print_check(count(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_()))), "#[false, true]"));
247 1 : BOOST_CHECK(print_check(count(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_()))), "#(false |> [true])"));
248 : //BOOST_CHECK(print_check(concat(bool_(), cons_(bool_(), true_(), empty), cons_(bool_(), false_(), snoc(bool_(), empty, true_()))), "[true] ++ [false, true]"));
249 1 : BOOST_CHECK(print_check(concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), snoc(bool_(), empty_, true_()))), "[true] ++ (false |> [true])"));
250 : //BOOST_CHECK(print_check(element_at(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_())), sort_nat::nat(1)), "[false, true].1"));
251 1 : BOOST_CHECK(print_check(element_at(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_())), sort_nat::nat(1)), "(false |> [true]) . 1"));
252 1 : BOOST_CHECK(print_check(head(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "head([false, true])"));
253 1 : BOOST_CHECK(print_check(tail(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "tail([false, true])"));
254 1 : BOOST_CHECK(print_check(rhead(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "rhead([false, true])"));
255 1 : BOOST_CHECK(print_check(rtail(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "rtail([false, true])"));
256 1 : BOOST_CHECK(print_check(cons_(bool_(), true_(), concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), empty_))), "true |> [true] ++ [false]"));
257 1 : BOOST_CHECK(print_check(snoc(bool_(), concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), empty_)), true_()), "[true] ++ [false] <| true"));
258 1 : BOOST_CHECK(print_check(cons_(bool_(), false_(), snoc(bool_(), concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), empty_)), true_())), "false |> [true] ++ [false] <| true"));
259 :
260 : // lists of lists
261 2 : data_expression list_empty = empty(list(bool_()));
262 1 : data_expression list_true = cons_(bool_(), true_(), empty_);
263 2 : data_expression list_false_true = cons_(bool_(), false_(), cons_(bool_(), true_(), empty_));
264 :
265 1 : BOOST_CHECK(print_check(empty(list(bool_())), "[]"));
266 1 : BOOST_CHECK(print_check(list_true, "[true]"));
267 1 : BOOST_CHECK(print_check(cons_(list(bool_()), list_true, list_empty), "[[true]]"));
268 1 : BOOST_CHECK(print_check(cons_(list(bool_()), list_true, cons_(list(bool_()), list_false_true, list_empty)), "[[true], [false, true]]"));
269 1 : BOOST_CHECK(print_check(snoc(list(bool_()), cons_(list(bool_()), list_false_true, list_empty), list_true), "[[false, true]] <| [true]"));
270 1 : BOOST_CHECK(print_check(in(list(bool_()), list_true, cons_(list(bool_()), list_true, list_empty)), "[true] in [[true]]"));
271 1 : BOOST_CHECK(print_check(in(list(bool_()), list_true, cons_(list(bool_()), list_true, list_empty)), "[true] in [[true]]"));
272 :
273 : // List enumeration
274 1 : data_expression_vector v;
275 1 : v.push_back(sort_bool::true_());
276 1 : v.push_back(sort_bool::false_());
277 1 : v.push_back(sort_bool::true_());
278 1 : v.push_back(sort_bool::true_());
279 2 : data_expression l1(list_enumeration(list(sort_bool::bool_()), v));
280 1 : BOOST_CHECK(print_check(l1, "[true, false, true, true]"));
281 :
282 2 : data_expression l2(sort_list::list(sort_bool::bool_(), v));
283 1 : BOOST_CHECK(print_check(l2, "[true, false, true, true]"));
284 :
285 : // Sort expression
286 1 : BOOST_CHECK(print_check(list(bool_()), "List(Bool)"));
287 :
288 :
289 1 : }
290 :
291 2 : BOOST_AUTO_TEST_CASE(test_set_print)
292 : {
293 : using namespace sort_bool;
294 :
295 1 : data_expression set_empty = sort_fset::empty(bool_());
296 2 : data_expression set_false = sort_set::set_fset(bool_(), sort_fset::cons_(bool_(), false_(), sort_fset::empty(bool_())));
297 2 : data_expression set_true = sort_set::set_fset(bool_(), sort_fset::cons_(bool_(), true_(), sort_fset::empty(bool_())));
298 :
299 : // Using all operations
300 1 : BOOST_CHECK(print_check(sort_fset::empty(bool_()), "{}"));
301 1 : BOOST_CHECK(print_check(sort_set::set_fset(bool_(), sort_fset::empty(bool_())), "{}"));
302 1 : BOOST_CHECK(print_check(sort_set::constructor(bool_(), sort_set::false_function(bool_()), sort_fset::empty(bool_())), "{}"));
303 1 : BOOST_CHECK(print_check(sort_set::in(bool_(), false_(), set_empty), "false in {}"));
304 1 : BOOST_CHECK(print_check(sort_set::union_(bool_(), set_false, set_true), "{false} + {true}"));
305 1 : BOOST_CHECK(print_check(sort_set::intersection(bool_(), set_false, set_true), "{false} * {true}"));
306 1 : BOOST_CHECK(print_check(sort_set::difference(bool_(), set_false, set_true), "{false} - {true}"));
307 1 : BOOST_CHECK(print_check(sort_set::complement(bool_(), set_false), "!{false}"));
308 :
309 : // Some parsed expressions
310 1 : BOOST_CHECK(print_check(parse_data_expression("{true}"), "{true}"));
311 1 : BOOST_CHECK(print_check(parse_data_expression("{true, false}"), "{true, false}"));
312 1 : BOOST_CHECK(print_check(parse_data_expression("{ b: Bool | b }"), "{ b: Bool | b }"));
313 1 : BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | x == 0 }"), "{ x: Nat | x == 0 }"));
314 1 : BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | (lambda y: Nat. y == 0)(x) }"), "{ x: Nat | (lambda y: Nat. y == 0)(x) }"));
315 :
316 : // Some types
317 1 : BOOST_CHECK(print_check(sort_fset::fset(bool_()), "FSet(Bool)"));
318 1 : BOOST_CHECK(print_check(parse_sort_expression("Set(Nat)"), "Set(Nat)"));
319 1 : }
320 :
321 2 : BOOST_AUTO_TEST_CASE(test_bag_print)
322 : {
323 : using namespace sort_bool;
324 : using namespace sort_nat;
325 :
326 1 : data_expression bag_empty(sort_fbag::empty(bool_()));
327 1 : data_expression fbag_empty_(sort_fbag::empty(bool_()));
328 2 : data_expression bag_false = sort_bag::bag_fbag(bool_(), sort_fbag::cons_(bool_(), false_(), number(sort_pos::pos(), "1"), fbag_empty_));
329 2 : data_expression bag_true = sort_bag::bag_fbag(bool_(), sort_fbag::cons_(bool_(), true_(), number(sort_pos::pos(), "1"), fbag_empty_));
330 :
331 : // Using all operations
332 1 : BOOST_CHECK(print_check(bag_empty, "{:}"));
333 1 : BOOST_CHECK(print_check(sort_bag::bag_fbag(bool_(), sort_fbag::empty(bool_())), "{:}"));
334 1 : BOOST_CHECK(print_check(sort_bag::constructor(bool_(), sort_bag::zero_function(bool_()), fbag_empty_), "{:}"));
335 1 : BOOST_CHECK(print_check(sort_bag::in(bool_(), false_(), bag_empty), "false in {:}"));
336 1 : BOOST_CHECK(print_check(sort_bag::in(bool_(), false_(), bag_false), "false in {false: 1}"));
337 1 : BOOST_CHECK(print_check(sort_bag::count(bool_(), false_(), bag_true), "count(false, {true: 1})"));
338 1 : BOOST_CHECK(print_check(sort_bag::union_(bool_(), bag_false, bag_true), "{false: 1} + {true: 1}"));
339 1 : BOOST_CHECK(print_check(sort_bag::intersection(bool_(), bag_false, bag_true), "{false: 1} * {true: 1}"));
340 1 : BOOST_CHECK(print_check(sort_bag::difference(bool_(), bag_false, bag_true), "{false: 1} - {true: 1}"));
341 :
342 : // Some parsed expressions
343 1 : BOOST_CHECK(print_check(parse_data_expression("{true: 2}"), "{true: 2}"));
344 1 : BOOST_CHECK(print_check(parse_data_expression("{false: 3, true: 1}"), "{false: 3, true: 1}"));
345 1 : BOOST_CHECK(print_check(parse_data_expression("{ b: Bool | if(b, Pos2Nat(2), Pos2Nat(3)) }"), "{ b: Bool | if(b, 2, 3) }"));
346 1 : BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | x * x }"), "{ x: Nat | x * x }"));
347 1 : BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | (lambda y: Nat. y * y)(x) }"), "{ x: Nat | (lambda y: Nat. y * y)(x) }"));
348 :
349 : // Some types
350 1 : BOOST_CHECK(print_check(sort_fbag::fbag(bool_()), "FBag(Bool)"));
351 1 : BOOST_CHECK(print_check(parse_sort_expression("Bag(Nat)"), "Bag(Nat)"));
352 1 : }
353 :
354 2 : BOOST_AUTO_TEST_CASE(test_function_update_print)
355 : {
356 1 : PRINT_CHECK(function_update(sort_nat::nat(), sort_bool::bool_()), "@func_update");
357 1 : PRINT_CHECK(parse_data_expression("(lambda x: Bool. x)[true -> false]"), "(lambda x: Bool. x)[true -> false]");
358 1 : PRINT_CHECK(parse_data_expression("(lambda x: Bool. x)[true -> false][false -> true]"), "(lambda x: Bool. x)[true -> false][false -> true]");
359 1 : PRINT_CHECK(parse_data_expression("(lambda n: Nat. n mod 2 == 0)[0 -> false]"), "(lambda n: Nat. n mod 2 == 0)[0 -> false]");
360 1 : }
361 :
362 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_bool_print)
363 : {
364 1 : BOOST_CHECK(print_container_check(sort_bool::bool_generate_equations_code()));
365 1 : }
366 :
367 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_pos_print)
368 : {
369 1 : BOOST_CHECK(print_container_check(sort_pos::pos_generate_equations_code()));
370 1 : }
371 :
372 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_nat_print)
373 : {
374 1 : BOOST_CHECK(print_container_check(sort_nat::nat_generate_equations_code()));
375 1 : }
376 :
377 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_int_print)
378 : {
379 1 : BOOST_CHECK(print_container_check(sort_int::int_generate_equations_code()));
380 1 : }
381 :
382 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_real_print)
383 : {
384 1 : BOOST_CHECK(print_container_check(sort_real::real_generate_equations_code()));
385 1 : }
386 :
387 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_fset_print)
388 : {
389 1 : BOOST_CHECK(print_container_check(sort_fset::fset_generate_equations_code(sort_bool::bool_())));
390 1 : }
391 :
392 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_set_print)
393 : {
394 1 : BOOST_CHECK(print_container_check(sort_set::set_generate_equations_code(sort_bool::bool_())));
395 1 : }
396 :
397 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_fbag_print)
398 : {
399 1 : BOOST_CHECK(print_container_check(sort_fbag::fbag_generate_equations_code(sort_bool::bool_())));
400 1 : }
401 :
402 2 : BOOST_AUTO_TEST_CASE(test_rewrite_rule_bag_print)
403 : {
404 1 : BOOST_CHECK(print_container_check(sort_bag::bag_generate_equations_code(sort_bool::bool_())));
405 1 : }
406 :
407 2 : BOOST_AUTO_TEST_CASE(test_standard_sort_expressions)
408 : {
409 1 : BOOST_CHECK(print_check(sort_bool::bool_(), "Bool"));
410 1 : BOOST_CHECK(print_check(sort_pos::pos(), "Pos"));
411 1 : BOOST_CHECK(print_check(sort_nat::nat(), "Nat"));
412 1 : BOOST_CHECK(print_check(sort_int::int_(), "Int"));
413 1 : BOOST_CHECK(print_check(sort_real::real_(), "Real"));
414 1 : }
415 :
416 2 : BOOST_AUTO_TEST_CASE(test_mod)
417 : {
418 2 : data::data_expression x = parse_data_expression("(1 + 2) mod 3");
419 1 : BOOST_CHECK(sort_nat::is_mod_application(x));
420 :
421 1 : application left = atermpp::down_cast<application>(sort_nat::left(x));
422 1 : std::cout << "left = " << left << " " << data::pp(left) << std::endl;
423 1 : BOOST_CHECK(data::detail::is_plus(left));
424 :
425 1 : BOOST_CHECK(data::pp(x) == "(1 + 2) mod 3");
426 1 : std::cout << "x = " << x << " " << data::pp(x) << std::endl;
427 :
428 1 : x = parse_data_expression("(2 - 1) mod 3");
429 1 : left = atermpp::down_cast<application>(sort_int::left(x));
430 1 : std::cout << "left = " << left << " " << data::pp(left) << std::endl;
431 1 : BOOST_CHECK(data::detail::is_minus(left));
432 1 : std::cout << "precedence(left) = " << precedence(left) << std::endl;
433 :
434 1 : BOOST_CHECK(data::sort_nat::is_nat(x.sort()));
435 1 : BOOST_CHECK(data::sort_int::is_mod_application(x));
436 :
437 1 : BOOST_CHECK(data::pp(x) == "(2 - 1) mod 3");
438 1 : std::cout << "x = " << x << " " << data::pp(x) << std::endl;
439 1 : }
440 :
441 2 : BOOST_AUTO_TEST_CASE(test_sort_expressions)
442 : {
443 2 : data::sort_expression x = parse_sort_expression("Bool # Nat -> (Pos -> Real)");
444 1 : std::string xtext = data::pp(x);
445 1 : data::sort_expression y = parse_sort_expression(xtext);
446 1 : std::string ytext = data::pp(y);
447 1 : std::cout << "original = " << "Bool # Nat -> (Pos -> Real)" << std::endl;
448 1 : std::cout << "xtext = " << xtext << std::endl;
449 1 : std::cout << "ytext = " << ytext << std::endl;
450 1 : BOOST_CHECK(x == y);
451 1 : BOOST_CHECK(xtext == ytext);
452 1 : BOOST_CHECK(data::pp(data::untyped_sort()) == "untyped_sort");
453 1 : }
454 :
455 2 : BOOST_AUTO_TEST_CASE(test_set_print2)
456 : {
457 : using namespace sort_bool;
458 :
459 2 : data_expression one = parse_data_expression("1");
460 2 : data_expression x = sort_fset::insert(sort_nat::nat(), one, sort_fset::empty(sort_nat::nat()));
461 1 : const sort_expression& s = sort_nat::nat();
462 :
463 1 : data_expression true_ = sort_set::false_function(s);
464 1 : data_expression false_ = sort_set::true_function(s);
465 2 : data_expression f = parse_function_symbol("f: Pos -> Bool");
466 :
467 1 : data_expression x1 = sort_set::constructor(s, true_, x);
468 1 : data_expression x2 = sort_set::constructor(s, false_, x);
469 2 : data_expression x3 = sort_set::constructor(s, f, x);
470 :
471 1 : BOOST_CHECK_EQUAL(data::pp(x1), "{1}");
472 1 : BOOST_CHECK_EQUAL(data::pp(x2), "!{1}");
473 1 : BOOST_CHECK_EQUAL(data::pp(x3), "{ x: Pos | f(x) != x in {1} }");
474 1 : }
475 :
476 2 : BOOST_AUTO_TEST_CASE(test_fset_print)
477 : {
478 : using namespace sort_bool;
479 :
480 2 : data_expression one = parse_data_expression("1");
481 2 : data_expression x = parse_data_expression("{1, 2}");
482 2 : data_expression y = parse_data_expression("{3}");
483 1 : const sort_expression& s = sort_pos::pos();
484 2 : data_expression f = parse_function_symbol("f: Pos -> Bool");
485 2 : data_expression g = parse_function_symbol("g: Pos -> Bool");
486 1 : data_expression false_ = sort_set::false_function(s);
487 1 : data_expression true_ = sort_set::true_function(s);
488 :
489 1 : data_expression xy_union = sort_set::fset_union(s, false_, false_, x, y);
490 1 : data_expression xy_intersection = sort_set::fset_intersection(s, false_, false_, x, y);
491 1 : data_expression xy_difference = sort_fset::difference(s, x, y);
492 2 : data_expression xy_in = sort_fset::in(s, one, x);
493 :
494 1 : BOOST_CHECK_EQUAL(data::pp(xy_union) , "{1, 2} + {3}");
495 1 : BOOST_CHECK_EQUAL(data::pp(xy_intersection), "{1, 2} * {3}");
496 1 : BOOST_CHECK_EQUAL(data::pp(xy_difference) , "{1, 2} - {3}");
497 1 : BOOST_CHECK_EQUAL(data::pp(xy_in) , "1 in {1, 2}");
498 :
499 1 : xy_union = sort_set::fset_union(s, f, false_, x, y);
500 1 : xy_intersection = sort_set::fset_intersection(s, f, false_, x, y);
501 1 : BOOST_CHECK_EQUAL(data::pp(xy_union) , "{1, 2} + { x: Pos | !f(x) && x in {3} }");
502 1 : BOOST_CHECK_EQUAL(data::pp(xy_intersection), "{1, 2} * { x: Pos | !f(x) && x in {3} }");
503 :
504 1 : xy_union = sort_set::fset_union(s, f, g, x, y);
505 1 : xy_intersection = sort_set::fset_intersection(s, f, g, x, y);
506 1 : BOOST_CHECK_EQUAL(data::pp(xy_union) , "{ x: Pos | !g(x) && x in {1, 2} } + { x: Pos | !f(x) && x in {3} }");
507 1 : BOOST_CHECK_EQUAL(data::pp(xy_intersection), "{ x: Pos | !g(x) && x in {1, 2} } * { x: Pos | !f(x) && x in {3} }");
508 1 : }
509 :
510 2 : BOOST_AUTO_TEST_CASE(test_precedence)
511 : {
512 2 : data::data_expression x = parse_data_expression("exists b:Bool. true");
513 1 : BOOST_CHECK(is_exists(x));
514 1 : BOOST_CHECK(precedence(x) == 1);
515 :
516 2 : data::variable a("a", sort_real::real_());
517 2 : data::variable b("b", sort_real::real_());
518 4 : std::vector<data::variable> variables = { a, b };
519 2 : data::data_expression y = parse_data_expression("-(a + b)", variables);
520 1 : std::string py = data::pp(y);
521 1 : BOOST_CHECK(py == "-(a + b)");
522 1 : }
523 :
524 : // The test case below tests whether an excessive amount of
525 : // memory is required when printing terms.
526 2 : BOOST_AUTO_TEST_CASE(printing_terms_takes_a_lot_of_memory)
527 : {
528 : const std::string text(
529 : "sort S;\n"
530 : "cons d0:S;\n"
531 : " f:S -> S;\n"
532 1 : );
533 :
534 1 : data::data_specification spec(data::parse_data_specification(text));
535 :
536 2 : data_expression f = parse_function_symbol("f: S -> S",text);
537 1 : std::cerr << f << "\n";
538 2 : data_expression t = parse_data_expression("d0",spec);
539 1 : std::cerr << t << "\n";
540 :
541 41 : for(size_t i=0; i<40; ++i)
542 : // for(size_t i=0; i<40000000; ++i)
543 : {
544 40 : t=application(f,t);
545 40 : std::cerr << t << "\n";
546 : }
547 1 : std::cerr << "Print term " << data::pp(t) << "\n";;
548 1 : }
549 :
|
