GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/printer/smt2_printer_black.cpp Lines: 18 18 100.0 %
Date: 2021-03-22 Branches: 39 86 45.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file smt2_printer_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Black box testing of the SMT2 printer
13
 **
14
 ** Black box testing of the SMT2 printer.
15
 **/
16
17
#include <iostream>
18
19
#include "api/cvc4cpp.h"
20
#include "expr/node.h"
21
#include "expr/node_manager.h"
22
#include "options/language.h"
23
#include "smt/smt_engine.h"
24
#include "test_smt.h"
25
26
namespace CVC4 {
27
28
using namespace kind;
29
30
namespace test {
31
32
8
class TestPrinterBlackSmt2 : public TestSmt
33
{
34
 protected:
35
4
  void checkToString(TNode n, const std::string& expected)
36
  {
37
8
    std::stringstream ss;
38
    ss << Node::setdepth(-1)
39
4
       << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n;
40
4
    ASSERT_EQ(ss.str(), expected);
41
  }
42
};
43
44
11
TEST_F(TestPrinterBlackSmt2, regexp_repeat)
45
{
46
  Node n = d_nodeManager->mkNode(
47
4
      d_nodeManager->mkConst(RegExpRepeat(5)),
48
6
      d_nodeManager->mkNode(STRING_TO_REGEXP,
49
14
                            d_nodeManager->mkConst(String("x"))));
50
2
  checkToString(n, "((_ re.^ 5) (str.to_re \"x\"))");
51
2
}
52
53
11
TEST_F(TestPrinterBlackSmt2, regexp_loop)
54
{
55
  Node n = d_nodeManager->mkNode(
56
4
      d_nodeManager->mkConst(RegExpLoop(1, 3)),
57
6
      d_nodeManager->mkNode(STRING_TO_REGEXP,
58
14
                            d_nodeManager->mkConst(String("x"))));
59
2
  checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))");
60
2
}
61
}  // namespace test
62
27371
}  // namespace CVC4