text:
// Author(s): Jeroen van der Wulp
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)

#define BOOST_TEST_MODULE print_test

#include <boost/test/included/unit_test_framework.hpp>

#include "mcrl2/data/parse.h"
#include "mcrl2/data/print.h"

using namespace mcrl2;
using namespace mcrl2::data;
using namespace mcrl2::data::sort_bool;
using namespace mcrl2::data::sort_nat;

template <typename T>
void test_term(const std::string& s, const T& x)
{
  std::cout << data::pp(x) << std::endl;
}

void test_term(const std::string& s)
{
  atermpp::aterm a = atermpp::read_term_from_string(s);
  if (s.find("DataEqn") == 0)
  {
    data_equation x (a);
    test_term(s, x);
  }
  else if (s.find("SortCons") == 0)
  {
    sort_expression x (a);
    test_term(s, x);
  }
  else if (s.find("OpId") == 0)
  {
    data::function_symbol x (a);
    test_term(s, x);
  }
  else
  {
    const data_expression& x = atermpp::down_cast<data_expression>(a);
    test_term(s, x);
  }
}

BOOST_AUTO_TEST_CASE(problem_cases)
{
/*
  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\")))))");

  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\")))))");

  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\")))))");

  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\"))))))");

  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\")))))");

  test_term("DataAppl(OpId(\"@bagcomp\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))],SortCons(SortBag,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Nat\"))))");
  test_term("DataAppl(OpId(\"==\",SortArrow([SortId(\"Bool\"),SortId(\"Bool\")],SortId(\"Bool\"))),DataVarId(\"b\",SortId(\"Bool\")),DataVarId(\"b\",SortId(\"Bool\")))");
  test_term("OpId(\"e1\",SortId(\"Enum\"))");

  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\"))))");
  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\"))))");
  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\"))))");
  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\")))");
  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\"))))");
  test_term("OpId(\"@c0\",SortId(\"Nat\"))");
  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\"))))");

  test_term("variable_list()", variable_list());

  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\"))))");

  test_term("DataAppl(OpId(\"mod\",SortArrow([SortId(\"Int\"),SortId(\"Pos\")],SortId(\"Nat\"))),DataVarId(\"y\",SortId(\"Int\")),DataVarId(\"q\",SortId(\"Pos\")))");

  test_term("SortCons(SortFSet,SortId(\"Bool\"))");
  test_term("SortCons(SortFBag,SortId(\"Bool\"))");

  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\"))))");
  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\"))))");
  test_term("OpId(\"@c0\",SortId(\"Nat\"))");
  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\"))))");
  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\")))))");
  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\"))))");

  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\"))))");

  // <pp>   @bagfbag(b)  =  @bagfbag(b)
  // <print>b  =  {b}
  // <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")))]))
  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\")))))");

  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\"))))");
  // <pp>   { b: Bool | b }
  // <print>{ [b: Bool] | b }
  // <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")))])

  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\"))))");

  // <pp>   { b: Bool | if(b, 2, 3) }
  // <print>{ [b: Bool] | if(b, 2, 3) }
  // <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")))])
  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\"))))");

  // <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
  // <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
  // <aterm>unknown

  // <pp>   1 == 2 * p + 2 * if(b, 1, 0)  =  false
  // <print>1 == @cDub(b, p)  =  false
  // <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")))
  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\")))");

  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\"))))");

  // <pp>   succ(succ(n))  =  2 * succ(n div 2) + 2 * if(n mod 2 == 1, 1, 0)
  // <print>succ(succ(n))  =  @cDub(n mod 2 == 1, succ(n / 2))
  // <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"))])])])]))
  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\")))))))");

  // <pp>   n == -p  =  false
  // <print>n == @cNeg(p)  =  false
  // <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")))
  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\")))");

  // <pp>   x / p == y / q  =  x * q == y * p
  // <print>x == y  =  x * q == y * p
  // <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"))])])])]))
  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\")))))))");

  test_term("OpId(\"@sort_fset::empty\",SortCons(SortFSet,SortId(\"Bool\")))");

  // <pp>   {} == {}  =  true
  // <print>@sort_fset::empty == @sort_fset::empty  =  true
  // <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")))
  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\")))");

  test_term("DataAppl(OpId(\"@sort_set::set_fset\",SortArrow([SortCons(SortFSet,SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"s\",SortCons(SortFSet,SortId(\"Bool\"))))");

  // <pp>   @sort_set::set_fset(s)  =  @sort_set::set_fset(s)
  // <print>s  =  { x: Bool | @false_(x) != x in s }
  // <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")))]))
  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\")))))");

  // <pp>   @fbag_cons(v0, v1, v2) < @fbag_cons(v3, v4, v5)  =  v0 < v3 || v0 == v3 && v1 < v4 || v1 == v4 && v2 < v5
  // <print>@fbag_cons(v0, v1, v2) < @fbag_cons(v3, v4, v5)  =  v0 < v3 || (v0 == v3 && (v1 < v4 || (v1 == v4 && v2 < v5)))
  // <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")))])])])])]))
  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\")))))))))");

  test_term("DataAppl(OpId(\"@setcomp\",SortArrow([SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))],SortCons(SortSet,SortId(\"Bool\")))),DataVarId(\"f\",SortArrow([SortId(\"Bool\")],SortId(\"Bool\"))))");
  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\"))))");
*/
}

template <typename ExpressionType>
bool print_check(ExpressionType const& left, std::string const& right)
{
  std::clog << "Checking printing of " << data::pp(left) << " with " << right << std::endl;
  if (pp(left) != right)
  {
    std::clog << "pp(" << left << ") != " << right << std::endl;
    std::clog << left << " != " << right << std::endl;

    return false;
  }

  return true;
}

template <typename Container>
bool print_container_check(Container const& c)
{
  std::string r = data::pp(c);
  if (r == "")
  {
    std::clog << "error printing container" << std::endl;
    return false;
  }

  return true;
}

#define PRINT_CHECK(x,y) BOOST_CHECK(print_check(x,y))

BOOST_AUTO_TEST_CASE(test_function_symbol_print)
{
  data::function_symbol f("f", sort_bool::bool_());

  PRINT_CHECK(f, "f");
}

BOOST_AUTO_TEST_CASE(test_application_print)
{
  data::function_symbol f("f", make_function_sort(bool_(), bool_()));
  data::function_symbol g("g", make_function_sort(bool_(), nat(), bool_()));

  PRINT_CHECK(f(true_()), "f(true)");
  PRINT_CHECK(g(false_(), sort_nat::nat(10)), "g(false, 10)");
  PRINT_CHECK(g(f(true_()), sort_nat::nat(10)), "g(f(true), 10)");
}

BOOST_AUTO_TEST_CASE(test_abstraction_print)
{
  using namespace sort_pos;
  using namespace sort_nat;

  variable_vector x {variable("x", sort_nat::nat())};
  variable_vector y {variable("y", sort_pos::pos())};
  variable_vector xy {x[0], y[0]};

  PRINT_CHECK(lambda(x, equal_to(x[0], nat(10))), "lambda x: Nat. x == 10");
  PRINT_CHECK(lambda(xy, equal_to(xy[0], pos2nat(xy[1]))), "lambda x: Nat, y: Pos. x == y");
  PRINT_CHECK(exists(x, equal_to(x[0], nat(10))), "exists x: Nat. x == 10");
  PRINT_CHECK(exists(xy, equal_to(xy[0], pos2nat(xy[1]))), "exists x: Nat, y: Pos. x == y");
  PRINT_CHECK(forall(x, equal_to(x[0], nat(10))), "forall x: Nat. x == 10");
  PRINT_CHECK(forall(xy, equal_to(xy[0], pos2nat(xy[1]))), "forall x: Nat, y: Pos. x == y");
  PRINT_CHECK(forall(x, exists(y, not_equal_to(xy[0], pos2nat(xy[1])))), "forall x: Nat. exists y: Pos. x != y");
}

BOOST_AUTO_TEST_CASE(test_list_print)
{
  using namespace sort_bool;
  using namespace sort_list;

  data_expression empty_(empty(bool_()));

  // Using all operations
  BOOST_CHECK(print_check(empty(bool_()), "[]"));
  BOOST_CHECK(print_check(cons_(bool_(), true_(), empty_), "[true]"));
  BOOST_CHECK(print_check(cons_(bool_(), false_(), cons_(bool_(), true_(), empty_)), "[false, true]"));
  //BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), true_(), empty), false_()), "[true, false]"));
  BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), true_(), empty_), false_()), "[true] <| false"));
  BOOST_CHECK(print_check(snoc(bool_(), snoc(bool_(), empty_, true_()), false_()), "[true, false]"));
  BOOST_CHECK(print_check(cons_(bool_(), in(bool_(), false_(), cons_(bool_(), true_(), empty_)), empty_), "[false in [true]]"));
  //BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_())), true_()), "[false, true, true]"));
  BOOST_CHECK(print_check(snoc(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_())), true_()), "(false |> [true]) <| true"));
  //BOOST_CHECK(print_check(in(bool_(), true_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_()))), "true in [false, true]"));
  BOOST_CHECK(print_check(in(bool_(), true_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_()))), "true in false |> [true]"));
  //BOOST_CHECK(print_check(count(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_()))), "#[false, true]"));
  BOOST_CHECK(print_check(count(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_()))), "#(false |> [true])"));
  //BOOST_CHECK(print_check(concat(bool_(), cons_(bool_(), true_(), empty), cons_(bool_(), false_(), snoc(bool_(), empty, true_()))), "[true] ++ [false, true]"));
  BOOST_CHECK(print_check(concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), snoc(bool_(), empty_, true_()))), "[true] ++ (false |> [true])"));
  //BOOST_CHECK(print_check(element_at(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty, true_())), sort_nat::nat(1)), "[false, true].1"));
  BOOST_CHECK(print_check(element_at(bool_(), cons_(bool_(), false_(), snoc(bool_(), empty_, true_())), sort_nat::nat(1)), "(false |> [true]) . 1"));
  BOOST_CHECK(print_check(head(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "head([false, true])"));
  BOOST_CHECK(print_check(tail(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "tail([false, true])"));
  BOOST_CHECK(print_check(rhead(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "rhead([false, true])"));
  BOOST_CHECK(print_check(rtail(bool_(), cons_(bool_(), false_(), cons_(bool_(), true_(), empty_))), "rtail([false, true])"));
  BOOST_CHECK(print_check(cons_(bool_(), true_(), concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), empty_))), "true |> [true] ++ [false]"));
  BOOST_CHECK(print_check(snoc(bool_(), concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), empty_)), true_()), "[true] ++ [false] <| true"));
  BOOST_CHECK(print_check(cons_(bool_(), false_(), snoc(bool_(), concat(bool_(), cons_(bool_(), true_(), empty_), cons_(bool_(), false_(), empty_)), true_())), "false |> [true] ++ [false] <| true"));

  // lists of lists
  data_expression list_empty = empty(list(bool_()));
  data_expression list_true = cons_(bool_(), true_(), empty_);
  data_expression list_false_true = cons_(bool_(), false_(), cons_(bool_(), true_(), empty_));

  BOOST_CHECK(print_check(empty(list(bool_())), "[]"));
  BOOST_CHECK(print_check(list_true, "[true]"));
  BOOST_CHECK(print_check(cons_(list(bool_()), list_true, list_empty), "[[true]]"));
  BOOST_CHECK(print_check(cons_(list(bool_()), list_true, cons_(list(bool_()), list_false_true, list_empty)), "[[true], [false, true]]"));
  BOOST_CHECK(print_check(snoc(list(bool_()), cons_(list(bool_()), list_false_true, list_empty), list_true), "[[false, true]] <| [true]"));
  BOOST_CHECK(print_check(in(list(bool_()), list_true, cons_(list(bool_()), list_true, list_empty)), "[true] in [[true]]"));
  BOOST_CHECK(print_check(in(list(bool_()), list_true, cons_(list(bool_()), list_true, list_empty)), "[true] in [[true]]"));

  // List enumeration
  data_expression_vector v;
  v.push_back(sort_bool::true_());
  v.push_back(sort_bool::false_());
  v.push_back(sort_bool::true_());
  v.push_back(sort_bool::true_());
  data_expression l1(list_enumeration(list(sort_bool::bool_()), v));
  BOOST_CHECK(print_check(l1, "[true, false, true, true]"));

  data_expression l2(sort_list::list(sort_bool::bool_(), v));
  BOOST_CHECK(print_check(l2, "[true, false, true, true]"));

  // Sort expression
  BOOST_CHECK(print_check(list(bool_()), "List(Bool)"));

}

BOOST_AUTO_TEST_CASE(test_set_print)
{
  using namespace sort_bool;

  data_expression set_empty = sort_fset::empty(bool_());
  data_expression set_false = sort_set::set_fset(bool_(), sort_fset::cons_(bool_(), false_(), sort_fset::empty(bool_())));
  data_expression set_true = sort_set::set_fset(bool_(), sort_fset::cons_(bool_(), true_(), sort_fset::empty(bool_())));

  // Using all operations
  BOOST_CHECK(print_check(sort_fset::empty(bool_()), "{}"));
  BOOST_CHECK(print_check(sort_set::set_fset(bool_(), sort_fset::empty(bool_())), "{}"));
  BOOST_CHECK(print_check(sort_set::constructor(bool_(), sort_set::false_function(bool_()), sort_fset::empty(bool_())), "{}"));
  BOOST_CHECK(print_check(sort_set::in(bool_(), false_(), set_empty), "false in {}"));
  BOOST_CHECK(print_check(sort_set::union_(bool_(), set_false, set_true), "{false} + {true}"));
  BOOST_CHECK(print_check(sort_set::intersection(bool_(), set_false, set_true), "{false} * {true}"));
  BOOST_CHECK(print_check(sort_set::difference(bool_(), set_false, set_true), "{false} - {true}"));
  BOOST_CHECK(print_check(sort_set::complement(bool_(), set_false), "!{false}"));

  // Some parsed expressions
  BOOST_CHECK(print_check(parse_data_expression("{true}"), "{true}"));
  BOOST_CHECK(print_check(parse_data_expression("{true, false}"), "{true, false}"));
  BOOST_CHECK(print_check(parse_data_expression("{ b: Bool | b }"), "{ b: Bool | b }"));
  BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | x == 0 }"), "{ x: Nat | x == 0 }"));
  BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | (lambda y: Nat. y == 0)(x) }"), "{ x: Nat | (lambda y: Nat. y == 0)(x) }"));

  // Some types
  BOOST_CHECK(print_check(sort_fset::fset(bool_()), "FSet(Bool)"));
  BOOST_CHECK(print_check(parse_sort_expression("Set(Nat)"), "Set(Nat)"));
}

BOOST_AUTO_TEST_CASE(test_bag_print)
{
  using namespace sort_bool;
  using namespace sort_nat;

  data_expression bag_empty(sort_fbag::empty(bool_()));
  data_expression fbag_empty_(sort_fbag::empty(bool_()));
  data_expression bag_false = sort_bag::bag_fbag(bool_(), sort_fbag::cons_(bool_(), false_(), number(sort_pos::pos(), "1"), fbag_empty_));
  data_expression bag_true = sort_bag::bag_fbag(bool_(), sort_fbag::cons_(bool_(), true_(), number(sort_pos::pos(), "1"), fbag_empty_));

  // Using all operations
  BOOST_CHECK(print_check(bag_empty, "{:}"));
  BOOST_CHECK(print_check(sort_bag::bag_fbag(bool_(), sort_fbag::empty(bool_())), "{:}"));
  BOOST_CHECK(print_check(sort_bag::constructor(bool_(), sort_bag::zero_function(bool_()), fbag_empty_), "{:}"));
  BOOST_CHECK(print_check(sort_bag::in(bool_(), false_(), bag_empty), "false in {:}"));
  BOOST_CHECK(print_check(sort_bag::in(bool_(), false_(), bag_false), "false in {false: 1}"));
  BOOST_CHECK(print_check(sort_bag::count(bool_(), false_(), bag_true), "count(false, {true: 1})"));
  BOOST_CHECK(print_check(sort_bag::union_(bool_(), bag_false, bag_true), "{false: 1} + {true: 1}"));
  BOOST_CHECK(print_check(sort_bag::intersection(bool_(), bag_false, bag_true), "{false: 1} * {true: 1}"));
  BOOST_CHECK(print_check(sort_bag::difference(bool_(), bag_false, bag_true), "{false: 1} - {true: 1}"));

  // Some parsed expressions
  BOOST_CHECK(print_check(parse_data_expression("{true: 2}"), "{true: 2}"));
  BOOST_CHECK(print_check(parse_data_expression("{false: 3, true: 1}"), "{false: 3, true: 1}"));
  BOOST_CHECK(print_check(parse_data_expression("{ b: Bool | if(b, Pos2Nat(2), Pos2Nat(3)) }"), "{ b: Bool | if(b, 2, 3) }"));
  BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | x * x }"), "{ x: Nat | x * x }"));
  BOOST_CHECK(print_check(parse_data_expression("{ x: Nat | (lambda y: Nat. y * y)(x) }"), "{ x: Nat | (lambda y: Nat. y * y)(x) }"));

  // Some types
  BOOST_CHECK(print_check(sort_fbag::fbag(bool_()), "FBag(Bool)"));
  BOOST_CHECK(print_check(parse_sort_expression("Bag(Nat)"), "Bag(Nat)"));
}

BOOST_AUTO_TEST_CASE(test_function_update_print)
{
  PRINT_CHECK(function_update(sort_nat::nat(), sort_bool::bool_()), "@func_update");
  PRINT_CHECK(parse_data_expression("(lambda x: Bool. x)[true -> false]"), "(lambda x: Bool. x)[true -> false]");
  PRINT_CHECK(parse_data_expression("(lambda x: Bool. x)[true -> false][false -> true]"), "(lambda x: Bool. x)[true -> false][false -> true]");
  PRINT_CHECK(parse_data_expression("(lambda n: Nat. n mod 2 == 0)[0 -> false]"), "(lambda n: Nat. n mod 2 == 0)[0 -> false]");
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_bool_print)
{
  BOOST_CHECK(print_container_check(sort_bool::bool_generate_equations_code()));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_pos_print)
{
  BOOST_CHECK(print_container_check(sort_pos::pos_generate_equations_code()));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_nat_print)
{
  BOOST_CHECK(print_container_check(sort_nat::nat_generate_equations_code()));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_int_print)
{
  BOOST_CHECK(print_container_check(sort_int::int_generate_equations_code()));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_real_print)
{
  BOOST_CHECK(print_container_check(sort_real::real_generate_equations_code()));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_fset_print)
{
  BOOST_CHECK(print_container_check(sort_fset::fset_generate_equations_code(sort_bool::bool_())));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_set_print)
{
  BOOST_CHECK(print_container_check(sort_set::set_generate_equations_code(sort_bool::bool_())));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_fbag_print)
{
  BOOST_CHECK(print_container_check(sort_fbag::fbag_generate_equations_code(sort_bool::bool_())));
}

BOOST_AUTO_TEST_CASE(test_rewrite_rule_bag_print)
{
  BOOST_CHECK(print_container_check(sort_bag::bag_generate_equations_code(sort_bool::bool_())));
}

BOOST_AUTO_TEST_CASE(test_standard_sort_expressions)
{
  BOOST_CHECK(print_check(sort_bool::bool_(), "Bool"));
  BOOST_CHECK(print_check(sort_pos::pos(), "Pos"));
  BOOST_CHECK(print_check(sort_nat::nat(), "Nat"));
  BOOST_CHECK(print_check(sort_int::int_(), "Int"));
  BOOST_CHECK(print_check(sort_real::real_(), "Real"));
}

BOOST_AUTO_TEST_CASE(test_mod)
{
  data::data_expression x = parse_data_expression("(1 + 2) mod 3");
  BOOST_CHECK(sort_nat::is_mod_application(x));

  application left = atermpp::down_cast<application>(sort_nat::left(x));
  std::cout << "left = " << left << " " << data::pp(left) << std::endl;
  BOOST_CHECK(data::detail::is_plus(left));

  application left1 = atermpp::down_cast<application>(detail::remove_numeric_casts(left));
  std::cout << "left1 = " << left1 << " " << data::pp(left1) << std::endl;
  BOOST_CHECK(data::detail::is_plus(left1));

  BOOST_CHECK(data::pp(x) == "(1 + 2) mod 3");
  std::cout << "x = " << x << " " << data::pp(x) << std::endl;

  x = parse_data_expression("(2 - 1) mod 3");
  left = atermpp::down_cast<application>(sort_int::left(x));
  std::cout << "left = " << left << " " << data::pp(left) << std::endl;
  BOOST_CHECK(data::detail::is_minus(left));
  std::cout << "precedence(left) = " << precedence(left) << std::endl;

  BOOST_CHECK(data::sort_nat::is_nat(x.sort()));
  BOOST_CHECK(data::sort_int::is_mod_application(x));

  left1 = atermpp::down_cast<application>(detail::remove_numeric_casts(left));
  std::cout << "left1 = " << left1 << " " << data::pp(left1) << std::endl;
  BOOST_CHECK(data::detail::is_minus(left1));
  std::cout << "precedence(left1) = " << precedence(left1) << std::endl;

  BOOST_CHECK(data::pp(x) == "(2 - 1) mod 3");
  std::cout << "x = " << x << " " << data::pp(x) << std::endl;
}

BOOST_AUTO_TEST_CASE(test_sort_expressions)
{
  data::sort_expression x = parse_sort_expression("Bool # Nat -> (Pos -> Real)");
  std::string xtext = data::pp(x);
  data::sort_expression y = parse_sort_expression(xtext);
  std::string ytext = data::pp(y);
  std::cout << "original = " << "Bool # Nat -> (Pos -> Real)" << std::endl;
  std::cout << "xtext    = " << xtext << std::endl;
  std::cout << "ytext    = " << ytext << std::endl;
  BOOST_CHECK(x == y);
  BOOST_CHECK(xtext == ytext);
  BOOST_CHECK(data::pp(data::untyped_sort()) == "untyped_sort");
}

BOOST_AUTO_TEST_CASE(test_set_print2)
{
  using namespace sort_bool;

  data_expression one = parse_data_expression("1");
  data_expression x = sort_fset::insert(sort_nat::nat(), one, sort_fset::empty(sort_nat::nat()));
  const sort_expression& s = sort_nat::nat();

  data_expression true_  = sort_set::false_function(s);
  data_expression false_ = sort_set::true_function(s);
  data_expression f      = parse_function_symbol("f: Pos -> Bool");

  data_expression x1 = sort_set::constructor(s, true_, x);
  data_expression x2 = sort_set::constructor(s, false_, x);
  data_expression x3 = sort_set::constructor(s, f, x);

  BOOST_CHECK_EQUAL(data::pp(x1), "{1}");
  BOOST_CHECK_EQUAL(data::pp(x2), "!{1}");
  BOOST_CHECK_EQUAL(data::pp(x3), "{ x: Pos | f(x) != x in {1} }");
}

BOOST_AUTO_TEST_CASE(test_fset_print)
{
  using namespace sort_bool;

  data_expression one = parse_data_expression("1");
  data_expression x = parse_data_expression("{1, 2}");
  data_expression y = parse_data_expression("{3}");
  const sort_expression& s = sort_pos::pos();
  data_expression f = parse_function_symbol("f: Pos -> Bool");
  data_expression g = parse_function_symbol("g: Pos -> Bool");
  data_expression false_ = sort_set::false_function(s);
  data_expression true_ = sort_set::true_function(s);

  data_expression xy_union = sort_set::fset_union(s, false_, false_, x, y);
  data_expression xy_intersection = sort_set::fset_intersection(s, false_, false_, x, y);
  data_expression xy_difference = sort_fset::difference(s, x, y);
  data_expression xy_in = sort_fset::in(s, one, x);

  BOOST_CHECK_EQUAL(data::pp(xy_union)       , "{1, 2} + {3}");
  BOOST_CHECK_EQUAL(data::pp(xy_intersection), "{1, 2} * {3}");
  BOOST_CHECK_EQUAL(data::pp(xy_difference)  , "{1, 2} - {3}");
  BOOST_CHECK_EQUAL(data::pp(xy_in)          , "1 in {1, 2}");

  xy_union = sort_set::fset_union(s, f, false_, x, y);
  xy_intersection = sort_set::fset_intersection(s, f, false_, x, y);
  BOOST_CHECK_EQUAL(data::pp(xy_union)       , "{1, 2} + { x: Pos | !f(x) && x in {3} }");
  BOOST_CHECK_EQUAL(data::pp(xy_intersection), "{1, 2} * { x: Pos | !f(x) && x in {3} }");

  xy_union = sort_set::fset_union(s, f, g, x, y);
  xy_intersection = sort_set::fset_intersection(s, f, g, x, y);
  BOOST_CHECK_EQUAL(data::pp(xy_union)       , "{ x: Pos | !g(x) && x in {1, 2} } + { x: Pos | !f(x) && x in {3} }");
  BOOST_CHECK_EQUAL(data::pp(xy_intersection), "{ x: Pos | !g(x) && x in {1, 2} } * { x: Pos | !f(x) && x in {3} }");
}

BOOST_AUTO_TEST_CASE(test_precedence)
{
  data::data_expression x = parse_data_expression("exists b:Bool. true");
  BOOST_CHECK(is_exists(x));
  BOOST_CHECK(precedence(x) == 1);

  data::variable a("a", sort_real::real_());
  data::variable b("b", sort_real::real_());
  std::vector<data::variable> variables = { a, b };
  data::data_expression y = parse_data_expression("-(a + b)", variables);
  std::string py = data::pp(y);
  BOOST_CHECK(py == "-(a + b)");
}

// The test case below tests whether an excessive amount of
// memory is required when printing terms.
BOOST_AUTO_TEST_CASE(printing_terms_takes_a_lot_of_memory)
{
   const std::string text(
    "sort S;\n"
    "cons d0:S;\n"
    "     f:S -> S;\n"
  );

  data::data_specification spec(data::parse_data_specification(text));

  data_expression f = parse_function_symbol("f: S -> S",text);
  std::cerr << f << "\n";
  data_expression t = parse_data_expression("d0",spec);
  std::cerr << t << "\n";

  for(size_t i=0; i<40; ++i)
  // for(size_t i=0; i<40000000; ++i)
  {
    t=application(f,t);
    std::cerr << t << "\n";
  }
  std::cerr << "Print term " << data::pp(t) << "\n";;
}


text:
#pragma once
/*
**  Copyright (C) 2013 Aldebaran Robotics
**  See COPYING for the license
*/

#ifndef _QITYPE_DETAIL_PROPERTY_HXX_
#define _QITYPE_DETAIL_PROPERTY_HXX_

#include <boost/thread/locks.hpp>
#include <qi/future.hpp>

namespace qi
{
  inline FutureSync<void> GenericProperty::set(const AnyValue& v)
  {
    std::pair<AnyReference, bool> conv = v.convert(_type);
    if (!conv.first.type())
      throw std::runtime_error(std::string("Failed converting ") + v.type()->infoString() + " to " + _type->infoString());

    Property<AnyValue>::set(AnyValue(conv.first, false, conv.second));

    return FutureSync<void>(0);
  }

  template<typename T>
  PropertyImpl<T>::PropertyImpl(Getter getter, Setter setter,
    SignalBase::OnSubscribers onsubscribe)
  : SignalF<void(const T&)>(std::move(onsubscribe))
  , _getter(std::move(getter))
  , _setter(std::move(setter))
  {
  }

  template<typename T>
  PropertyImpl<T>::PropertyImpl(AutoAnyReference defaultValue,
    Getter getter, Setter setter,
    SignalBase::OnSubscribers onsubscribe)
  : SignalF<void(const T&)>(std::move(onsubscribe))
  , _getter(std::move(getter))
  , _setter(std::move(setter))
  , _value(defaultValue.to<T>())
  {
  }

  template<typename T>
  T PropertyImpl<T>::getImpl() const
  {
    if (_getter)
      return _getter(_value);
    else
      return _value;
  }
  template<typename T>
  void PropertyImpl<T>::setImpl(const T& v)
  {
    qiLogDebug("qitype.property") << "set " << this << " " << (!!_setter);
    if (_setter)
    {
      const bool ok = _setter(_value, v);
      if (ok)
        (*this)(_value);
    }
    else
    {
      _value = v;
      (*this)(_value);
    }
  }

  template<typename T>
  FutureSync<T> UnsafeProperty<T>::get() const
  {
    return FutureSync<T>(this->getImpl());
  }

  template<typename T>
  FutureSync<void> UnsafeProperty<T>::set(const T& v)
  {
    this->setImpl(v);
    return FutureSync<void>(0);
  }

  template<typename T>
  FutureSync<AnyValue> UnsafeProperty<T>::value() const
  {
    return FutureSync<AnyValue>(AnyValue::from(this->getImpl()));
  }

  template<typename T>
  FutureSync<void> UnsafeProperty<T>::setValue(AutoAnyReference value)
  {
    this->setImpl(value.to<T>());
    return FutureSync<void>(0);
  }

  template<typename T>
  FutureSync<T> Property<T>::get() const
  {
    boost::mutex::scoped_lock lock(_mutex);
    return FutureSync<T>(this->getImpl());
  }

  template<typename T>
  FutureSync<void> Property<T>::set(const T& v)
  {
    boost::mutex::scoped_lock lock(_mutex);
    this->setImpl(v);
    return FutureSync<void>(0);
  }

  template<typename T>
  FutureSync<AnyValue> Property<T>::value() const
  {
    boost::mutex::scoped_lock lock(_mutex);
    return FutureSync<AnyValue>(AnyValue::from(this->getImpl()));
  }

  template<typename T>
  FutureSync<void> Property<T>::setValue(AutoAnyReference value)
  {
    boost::mutex::scoped_lock lock(_mutex);
    this->setImpl(value.to<T>());
    return FutureSync<void>(0);
  }

  template<class T>
  typename Property<T>::ScopedLockReadWrite
    Property<T>::getLockedReadWrite()
  {
    return ScopedLockReadWrite(*this);
  }

  template<class T>
  typename Property<T>::ScopedLockReadOnly
    Property<T>::getLockedReadOnly() const
  {
    return ScopedLockReadOnly(*this);
  }
}

#endif  // _QITYPE_DETAIL_PROPERTY_HXX_

ext: hxx


text:
// Software License for MTL
//
// Copyright (c) 2007 The Trustees of Indiana University.
//               2008 Dresden University of Technology and the Trustees of Indiana University.
//               2010 SimuNova UG (haftungsbeschränkt), www.simunova.com.
// All rights reserved.
// Authors: Peter Gottschling and Andrew Lumsdaine
//
// This file is part of the Matrix Template Library
//
// See also license.mtl.txt in the distribution.

#ifndef MTL_STRIDED_VECTOR_REF_INCLUDE
#define MTL_STRIDED_VECTOR_REF_INCLUDE

#include <iostream>
#include <cassert>
#include <vector>
#include <algorithm>
#include <boost/static_assert.hpp>
#include <boost/utility/enable_if.hpp>

#include <boost/numeric/mtl/mtl_fwd.hpp>
#include <boost/numeric/mtl/utility/exception.hpp>
#include <boost/numeric/mtl/utility/ashape.hpp>
#include <boost/numeric/mtl/utility/common_include.hpp>
#include <boost/numeric/mtl/vector/all_vec_expr.hpp>
#include <boost/numeric/mtl/vector/parameter.hpp>
#include <boost/numeric/mtl/vector/crtp_base_vector.hpp>
#include <boost/numeric/mtl/utility/dense_el_cursor.hpp>
#include <boost/numeric/mtl/utility/range_generator.hpp>
#include <boost/numeric/mtl/utility/property_map.hpp>
#include <boost/numeric/mtl/utility/irange.hpp>
#include <boost/numeric/mtl/utility/is_row_major.hpp>
#include <boost/numeric/mtl/utility/strided_dense_el_iterator.hpp>
#include <boost/numeric/mtl/utility/strided_dense_el_cursor.hpp>
#include <boost/numeric/mtl/operation/is_negative.hpp>

namespace mtl { namespace vec {

/// Class for referring vectors stored in strides, e.g. columns in a row-major matrix
template <class Value, typename Parameters = parameters<> >
class strided_vector_ref
  : public vec_expr<strided_vector_ref<Value, Parameters> >,
    public crtp_base_vector< strided_vector_ref<Value, Parameters>, Value, std::size_t >
{
    typedef strided_vector_ref                                                       self;
    typedef crtp_base_vector< self, Value, std::size_t >                             crtp_base;
    typedef crtp_vector_assign< self, Value, std::size_t >                           assign_base;
    typedef vec_expr<strided_vector_ref<Value, Parameters> >                         expr_base;
  public:
    typedef typename boost::remove_const<Value>::type                                value_type ;
    typedef std::size_t                                                              size_type ;
    typedef Value&                                                                   reference ;
    typedef Value const&                                                             const_reference ;
    typedef Value*                                                                   pointer ;
    typedef Value const*                                                             const_pointer ;
    typedef const_pointer                                                            key_type;
    typedef mtl::strided_dense_el_cursor<Value>                                      cursor_type;
    typedef mtl::strided_dense_el_const_iterator<Value>                              const_iterator;
    typedef mtl::strided_dense_el_iterator<Value>                                    iterator;
    typedef typename Parameters::orientation                                         orientation;

    void check_index( size_type MTL_DEBUG_ARG(i) ) const
    {
	MTL_DEBUG_THROW_IF( is_negative(i) || i >= size(*this), index_out_of_range());
    }

    void check_dim( size_type MTL_DEBUG_ARG(s) ) const
    {
	MTL_DEBUG_THROW_IF( size(*this) != 0 && size(*this) != s, incompatible_size());
    }

    template <class E>
    void check_consistent_shape( vec_expr<E> const& ) const
    {
	MTL_DEBUG_THROW_IF((!boost::is_same<
			        typename ashape::ashape<self>::type
			      , typename ashape::ashape<E>::type
			    >::value),
			   incompatible_shape());
    }

  private:
    /// Make default constructor invisible
    strided_vector_ref();

  public:

    /// Constructor take address, length and stride
    strided_vector_ref( size_type length, pointer start_address, size_type stride= 1)
      : data(start_address), my_size(length), my_stride(stride), cloned(false) {}

    /// Clone constructor
    strided_vector_ref(const strided_vector_ref& other, clone_ctor)
      : data(new Value[other.my_size]), my_size(other.my_size), my_stride(1), cloned(true)
    {
	*this= other;
    }

    // Default copy constructor refers to same vector which is okay

    ~strided_vector_ref() { if (cloned && data) delete[] data; }

    //  friend size_type inline size(const self& v) { return v.my_size; } // impedes explicit namespace qualification

    template <typename V2, typename P2>
    friend std::size_t size(const strided_vector_ref<V2, P2>& v);

    size_type stride() const { return my_stride ; }

    reference operator()( size_type i ) { check_index(i); return data[i * my_stride]; }
    const_reference operator()( size_type i ) const { check_index(i); return data[i * my_stride]; }

    reference operator[]( size_type i ) { return (*this)( i ) ; }
    const_reference operator[]( size_type i ) const { return (*this)( i ) ;  }

    self operator[]( irange r ) { return sub_vector(*this, r.start(), r.finish()); }
    const self  operator[]( irange r ) const { return sub_vector(*this, r.start(), r.finish());  }

    void delay_assign() const {}

    const_iterator begin() const { return const_iterator(data, my_stride); }
    const_iterator end() const { return const_iterator(data + my_size * my_stride, my_stride); }

    iterator begin() { return iterator(data, my_stride); }
    iterator end() { return iterator(data + my_size * my_stride, my_stride); }

    /// Address of first data entry; to be used with care.
    pointer address_data() { return data; }
    const_pointer address_data() const { return data; }

    // from pointer to index
    size_type offset(const_pointer p) const
    {
	size_type o= p - data, i= o / my_stride;
	MTL_DEBUG_THROW_IF(o % my_stride, logic_error("Address not consistent with stride."));
	check_index(i);
	return i;
    }

    friend size_type inline num_rows(const self& v) { return mtl::traits::is_row_major<self>::value ? 1 : size(v); }
    friend size_type inline num_cols(const self& v) { return mtl::traits::is_row_major<self>::value ? size(v) : 1; }

    vec_vec_asgn_expr<self, self> operator=( self const& e )
    {
	return vec_vec_asgn_expr<self, self>( *this, e );
    }

    // self& operator=(self src) Cannot move!

    using assign_base::operator=;

    template <typename Value2> friend void fill(self& vector, const Value2& value)
    {
	std::fill(vector.begin(), vector.end(), value);
    }

    /// Swapping not efficient since elements have to be swapped for not owning the data
    friend void swap(self& vector1, self& vector2)
    {
	vector1.check_dim(vector2.size()); // size(vector2) doesn't compiled with ICC 10.1
	for (size_type i= 0; i < vector1.size(); ++i)
	    swap(vector1[i], vector2[i]);
    }

    void change_dim(size_type MTL_DEBUG_ARG(n)) { MTL_DEBUG_THROW_IF(my_size != n, incompatible_size()); }
    void crop() {} // Only dummy here

  private:
    pointer     data;
    size_type   my_size, my_stride;
    bool        cloned;
} ; // strided_vector_ref

template <typename Value, typename Parameters>
inline std::size_t size(const strided_vector_ref<Value, Parameters>& v)
{
    return v.my_size;
}

template <typename Value, typename Parameters>
strided_vector_ref<Value, Parameters>
inline sub_vector(strided_vector_ref<Value, Parameters>& v,
		  typename strided_vector_ref<Value, Parameters>::size_type start,
		  typename strided_vector_ref<Value, Parameters>::size_type finish)
{
    using std::min;
    typedef strided_vector_ref<Value, Parameters>    Vector;
    typedef typename Vector::size_type               size_type;

    MTL_DEBUG_THROW_IF( is_negative(start) || is_negative(finish), index_out_of_range());
    finish= min(finish, size(v));
    start= min(start, finish); // implies min(start, size(v))
    return Vector(start <= finish ? finish - start : size_type(0), &v[start], v.stride());
}

template <typename Value, typename Parameters>
const strided_vector_ref<Value, Parameters>
inline sub_vector(const strided_vector_ref<Value, Parameters>& v,
		  typename strided_vector_ref<Value, Parameters>::size_type start,
		  typename strided_vector_ref<Value, Parameters>::size_type finish)
{
    typedef strided_vector_ref<Value, Parameters>    Vector;
    return sub_vector(const_cast<Vector&>(v), start, finish);
}

}} // namespace mtl::vector

namespace mtl {

    // Enable cloning of strided_vector_ref
    template <typename Value, typename Parameters>
    struct is_clonable< vec::strided_vector_ref<Value, Parameters> > : boost::mpl::true_ {};

} // namespace mtl

namespace mtl { namespace traits {

// ================
// Range generators
// For cursors
// ================

    template <typename Value, class Parameters>
    struct range_generator<tag::all, vec::strided_vector_ref<Value, Parameters> >
      : public detail::strided_element_range_generator<
	  vec::strided_vector_ref<Value, Parameters>,
	  const vec::strided_vector_ref<Value, Parameters>,
	  mtl::strided_dense_el_cursor<Value>
	> {};

    template <typename Value, class Parameters>
    struct range_generator<tag::nz, vec::strided_vector_ref<Value, Parameters> >
      : public range_generator<tag::all, vec::strided_vector_ref<Value, Parameters> > {};

    template <typename Value, class Parameters>
    struct range_generator<tag::iter::all, vec::strided_vector_ref<Value, Parameters> >
      : public detail::strided_element_range_generator<
	  vec::strided_vector_ref<Value, Parameters>,
	  vec::strided_vector_ref<Value, Parameters>,
	  mtl::strided_dense_el_iterator<Value>
	> {};

    template <typename Value, class Parameters>
    struct range_generator<tag::iter::nz, vec::strided_vector_ref<Value, Parameters> >
      : public range_generator<tag::iter::all, vec::strided_vector_ref<Value, Parameters> > {};

    template <typename Value, class Parameters>
    struct range_generator<tag::const_iter::all, vec::strided_vector_ref<Value, Parameters> >
      : public detail::strided_element_range_generator<
	  vec::strided_vector_ref<Value, Parameters>,
	  const vec::strided_vector_ref<Value, Parameters>,
	  mtl::strided_dense_el_const_iterator<Value>
	> {};

    template <typename Value, class Parameters>
    struct range_generator<tag::const_iter::nz, vec::strided_vector_ref<Value, Parameters> >
	: public range_generator<tag::const_iter::all, vec::strided_vector_ref<Value, Parameters> >
    {};

}} // namespace mtl::traits

#endif // MTL_STRIDED_VECTOR_REF_INCLUDE

ext: hpp


text:
/*
Copyright 2019 Glen Joseph Fernandes
(glenjofe@gmail.com)

Distributed under the Boost Software License, Version 1.0.
(http://www.boost.org/LICENSE_1_0.txt)
*/
#include <boost/span/span.hpp>
#include <boost/core/lightweight_test_trait.hpp>

template<class T>
struct range {
    T* data() {
        return 0;
    }

    const T* data() const {
        return 0;
    }

    std::size_t size() const {
        return 0;
    }
};

struct base { };

struct derived
    : base { };

void test_default()
{
    BOOST_TEST_TRAIT_TRUE((std::is_default_constructible<
        boost::spans::span<int> >));
    BOOST_TEST_TRAIT_TRUE((std::is_default_constructible<
        boost::spans::span<int, 0> >));
    BOOST_TEST_TRAIT_FALSE((std::is_default_constructible<
        boost::spans::span<int, 2> >));
}

void test_data_size()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        int*, std::size_t>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        int*, std::size_t>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        int, std::size_t>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        const int*, std::size_t>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base>,
        derived*, std::size_t>));
}

void test_first_last()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        int*, int*>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        int*, const int*>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        int*, int*>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        int, int*>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        const int*, int*>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base>,
        derived*, derived*>));
}

void test_array()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        int(&)[4]>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int, 4>,
        int(&)[4]>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 2>,
        int(&)[4]>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 4>,
        int(&)[2]>));
}

void test_std_array()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        std::array<int, 4>&>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        std::array<int, 4>&>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int, 4>,
        std::array<int, 4>&>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int,
        4>, std::array<int, 4>&>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        std::array<const int, 4>&>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base>,
        std::array<derived, 4>&>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 2>,
        std::array<int, 4>&>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 4>,
        std::array<const int, 4>&>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base, 4>,
        std::array<derived, 4>&>));
}

void test_const_std_array()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        const std::array<int, 4> >));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int,
        4>, const std::array<int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        const std::array<int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<const
        base>, const std::array<derived, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<const int,
        2>, const std::array<int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 4>,
        const std::array<int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<const
        base, 4>, const std::array<derived, 4> >));
}

void test_range()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        range<int>&>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        range<int>&>));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        range<int> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        int*>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        range<int> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        const range<int>&>));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base>,
        range<derived>&>));
}

void test_span()
{
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int>,
        boost::spans::span<int> >));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int>,
        boost::spans::span<int, 4> >));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<int, 4>,
        boost::spans::span<int> >));
    BOOST_TEST_TRAIT_TRUE((std::is_constructible<boost::spans::span<const int,
        4>, boost::spans::span<int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int>,
        boost::spans::span<const int> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base>,
        boost::spans::span<derived> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 2>,
        boost::spans::span<int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<int, 4>,
        boost::spans::span<const int, 4> >));
    BOOST_TEST_TRAIT_FALSE((std::is_constructible<boost::spans::span<base, 4>,
        boost::spans::span<derived, 4> >));
}

void test_copy()
{
    BOOST_TEST_TRAIT_TRUE((std::is_copy_constructible<
        boost::spans::span<int> >));
    BOOST_TEST_TRAIT_TRUE((std::is_copy_constructible<
        boost::spans::span<int, 4> >));
}

void test_assign()
{
    BOOST_TEST_TRAIT_TRUE((std::is_copy_assignable<
        boost::spans::span<int> >));
    BOOST_TEST_TRAIT_TRUE((std::is_copy_assignable<
        boost::spans::span<int, 4> >));
}

int main()
{
    test_default();
    test_data_size();
    test_first_last();
    test_array();
    test_std_array();
    test_const_std_array();
    test_range();
    test_span();
    test_copy();
    test_assign();
    return boost::report_errors();
}

ext: cpp

max_stars_repo_name: glenfe/span

max_issues_repo_name: glenfe/span

max_forks_repo_name: glenfe/span


text:
#include <cstdlib>
#include <iostream>
#include <set>
#include <climits>
#include <algorithm>

#include <boost/property_map/property_map.hpp>
#include <boost/graph/adjacency_list.hpp>
#include <boost/graph/random.hpp>
#include <boost/random/mersenne_twister.hpp>
#include <boost/graph/graphviz.hpp>

#include <vector>
#include <utility>
#include <queue>
#include <ctime>

#include "naive.hh"

//using namespace std;

//Treewidth is always positive, so we can use this in place of -Inf
const int NO_WIDTH = -1;

int naiveTW(std::set<Vertex> S, Graph G)
{
    if (S.empty())
    {
        return NO_WIDTH;
    }
    else
    {
        int minSoFar = INT_MAX;

        for (auto iter = S.begin(); iter != S.end(); iter++)
        {
            Vertex v = *iter;
            std::set<Vertex> S2(S);

            S2.erase(v);

            int subTW = naiveTW(S2, G);
            int qVal = sizeQ(S2, v, G);

            //std::cout << "S2 is " << showSet(S2) << std::endl;
            //std::cout << "subTW " << subTW << std::endl;
            //std::cout << "qVal " << qVal << std::endl;

            minSoFar = std::min(minSoFar, std::max(subTW, qVal ) );
        }
        return minSoFar;

    }
}

int naiveMain()
{

    Graph g;
    boost::mt19937 rng(time (NULL));
    boost::generate_random_graph(g, 8, 20, rng, true, true);

    boost::write_graphviz(std::cout, g);

    auto iterInfo = boost::vertices(g);
    std::set<Vertex> S;
    for (auto iter = iterInfo.first; iter != iterInfo.second; iter++ )
    {
        S.insert(*iter);
    }

    std::cout << "Treewidth: " << naiveTW(S, g) << std::endl;

    return EXIT_SUCCESS;

}

ext: cc

max_stars_repo_name: JoeyEremondi/treewidth-memoization

max_issues_repo_name: JoeyEremondi/treewidth-memoization

max_forks_repo_name: JoeyEremondi/treewidth-memoization


text:
// (C) Copyright 2007 Matthias Troyer

// Use, modification and distribution is subject to the Boost Software
// License, Version 1.0. (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)

//  Authors: Matthias Troyer

/** @file is_bitwise_serializable.hpp
 *
 *  This header provides a traits class for determining whether a class
 * can be serialized (in a non-portable way) just by copying the bits.
 */

#ifndef BOOST_SERIALIZATION_IS_BITWISE_SERIALIZABLE_HPP
#define BOOST_SERIALIZATION_IS_BITWISE_SERIALIZABLE_HPP

// MS compatible compilers support #pragma once
#if defined(_MSC_VER)
#pragma once
#endif

#include <boost/mpl/bool_fwd.hpp>
#include <boost/type_traits/is_arithmetic.hpp>

namespace boost {
namespace serialization {
template <class T> struct is_bitwise_serializable : public is_arithmetic<T> {};
} // namespace serialization
} // namespace boost

// define a macro to make explicit designation of this more transparent
#define BOOST_IS_BITWISE_SERIALIZABLE(T)                                       \
  namespace boost {                                                            \
  namespace serialization {                                                    \
  template <> struct is_bitwise_serializable<T> : mpl::true_ {};               \
  }                                                                            \
  }                                                                            \
  /**/

#endif // BOOST_SERIALIZATION_IS_BITWISE_SERIALIZABLE_HPP

max_stars_repo_name: henrywarhurst/matrix

max_issues_repo_name: henrywarhurst/matrix

max_forks_repo_name: henrywarhurst/matrix


text:
//
// $Id: InterpolatorTest.cpp 8434 2012-03-29 16:09:22Z chambm $
//
// Original author: Matt Chambers <matt.chambers .@. vanderbilt.edu>
// Copyright 2011 Vanderbilt University
//
// Licensed under the Code Project Open License, Version 1.02 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.codeproject.com/info/cpol10.aspx
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
//

#include "pwiz/utility/misc/unit.hpp"
#include "pwiz/utility/misc/Std.hpp"
#include "Interpolator.hpp"
#include <boost/assign.hpp>

using namespace pwiz::util;
using namespace freicore;
using namespace boost::assign;

int main()
{
    try
    {
        {
            vector<double> x; x += 1, 2, 3,  4,  6,  7,  8, 9;
            vector<double> y; y += 1, 8, 27, 64, 64, 27, 8, 1;
            Interpolator test(x, y);

            unit_assert_equal(1, test.interpolate(x, y, 1), 1e-6);
            unit_assert_equal(8, test.interpolate(x, y, 2), 1e-6);
            unit_assert_equal(27, test.interpolate(x, y, 3), 1e-6);
            unit_assert_equal(64, test.interpolate(x, y, 4), 1e-6);
            //unit_assert_equal(64, test.interpolate(x, y, 5), 1e-6);
            unit_assert_equal(64, test.interpolate(x, y, 6), 1e-6);
            unit_assert_equal(27, test.interpolate(x, y, 7), 1e-6);
            unit_assert_equal(1, test.interpolate(x, y, 9), 1e-6);

            test.resample(x, y);
            unit_assert_operator_equal(18, x.size() + y.size());
            unit_assert_equal(1, x[0], 1e-6);
            unit_assert_equal(2, x[1], 1e-6);
            unit_assert_equal(8, x[7], 1e-6);
            unit_assert_equal(9, x[8], 1e-6);

            unit_assert_equal(1, y[0], 1e-6);
            unit_assert_equal(8, y[1], 1e-6);
            unit_assert_equal(27, y[2], 1e-6);
            unit_assert_equal(64, y[3], 1e-6);
            //unit_assert_equal(64, y[4], 1e-6);
            unit_assert_equal(64, y[5], 1e-6);
            unit_assert_equal(27, y[6], 1e-6);
            //unit_assert_equal(8, y[7], 1e-6);
            unit_assert_equal(1, y[8], 1e-6);
        }

        {
            vector<double> x; x += 1, 3,  4,  5,  6,  7,  9;
            vector<double> y; y += 1, 27, 64, 64, 64, 27, 1;
            Interpolator test(x, y);

            unit_assert_operator_equal(1, test.interpolate(x, y, 1));
            unit_assert_operator_equal(8, test.interpolate(x, y, 2));
            unit_assert_operator_equal(64, test.interpolate(x, y, 5));
            unit_assert_operator_equal(27, test.interpolate(x, y, 7));
            unit_assert_operator_equal(8, test.interpolate(x, y, 8));
            unit_assert_operator_equal(1, test.interpolate(x, y, 9));

            test.resample(x, y);
            unit_assert_operator_equal(18, x.size() + y.size());
            unit_assert_operator_equal(1, x[0]);
            unit_assert_operator_equal(2, x[1]);
            unit_assert_operator_equal(8, x[7]);
            unit_assert_operator_equal(9, x[8]);

            unit_assert_operator_equal(1, y[0]);
            unit_assert_operator_equal(8, y[1]);
            unit_assert_operator_equal(27, y[2]);
            unit_assert_operator_equal(64, y[3]);
            unit_assert_operator_equal(64, y[4]);
            unit_assert_operator_equal(64, y[5]);
            unit_assert_operator_equal(27, y[6]);
            unit_assert_operator_equal(8, y[7]);
            unit_assert_operator_equal(1, y[8]);
        }
    }
    catch (exception& e)
    {
        cerr << e.what() << endl;
        return 1;
    }

    return 0;
}

max_stars_repo_name: shze/pwizard-deb

max_issues_repo_name: shze/pwizard-deb

max_forks_repo_name: shze/pwizard-deb


text:
//
//  SeqGenOptions.h
//  testing system
//
//  Created by Miloš Šimek on 14.04.15.
//  Copyright (c) 2015 Miloš Šimek. All rights reserved.
//

#ifndef testing_system_SeqGenOptions_h
#define testing_system_SeqGenOptions_h

#include <string>
#include <iostream>
#include <exception>
#include <boost/program_options.hpp>

#include "../global/Optional.hpp"
#include "../global/GlobalSetup.hpp"

using namespace std;
namespace po = boost::program_options;
typedef unsigned long long ULL;

enum OptionsState {
    OPS_OK, OPS_HELP, OPS_ERR
};

class SeqGenOptions {
    OptionsState opState = OPS_OK;
    po::variables_map optionMap;

public:
    SeqGenOptions(int argc, const char * argv[]);

    string      getGenomeFileName();
    float       getCoverage();
    unsigned    getSeqLength();
    string      getOutputSequenceFileName();
    string      getOutputMapFileName();
    Optional<unsigned> randGenSeed();

    //only one way to retrieve probability is valid in given run
    Optional<float>  uniformProbability();
    Optional<string> probabilityFileName();

    OptionsState optionsState();

private:
    void checkOptionValidity();
    void checkForExistence(const char * option, const char * errOutput);
    void setOptionError(string message);
};

#endif