GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp Lines: 16 16 100.0 %
Date: 2021-03-22 Branches: 43 102 42.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file pass_foreign_theory_rewrite_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Yoni Zohar
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 Unit tests for Foreign Theory Rerwrite prepricessing pass
13
 ** Unit tests for Foreign Theory Rerwrite prepricessing pass
14
 **/
15
16
#include "expr/node_manager.h"
17
#include "preprocessing/passes/foreign_theory_rewrite.h"
18
#include "smt/smt_engine.h"
19
#include "test_smt.h"
20
21
namespace CVC4 {
22
23
using namespace preprocessing::passes;
24
25
namespace test {
26
27
4
class TestPPWhiteForeignTheoryRewrite : public TestSmt
28
{
29
};
30
31
10
TEST_F(TestPPWhiteForeignTheoryRewrite, simplify)
32
{
33
2
  std::cout << "len(x) >= 0 is simplified to true" << std::endl;
34
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType());
35
4
  Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x);
36
4
  Node zero = d_nodeManager->mkConst<Rational>(0);
37
4
  Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero);
38
4
  Node tt = d_nodeManager->mkConst<bool>(true);
39
4
  Node simplified1 = ForeignTheoryRewrite::foreignRewrite(geq1);
40
2
  ASSERT_EQ(simplified1, tt);
41
42
2
  std::cout << "len(x) >= n is not simplified to true" << std::endl;
43
4
  Node n = d_nodeManager->mkVar("n", d_nodeManager->integerType());
44
4
  Node geq2 = d_nodeManager->mkNode(kind::GEQ, len_x, n);
45
4
  Node simplified2 = ForeignTheoryRewrite::foreignRewrite(geq2);
46
2
  ASSERT_NE(simplified2, tt);
47
}
48
49
}  // namespace test
50
24170
}  // namespace CVC4