GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_arith_white.cpp Lines: 52 52 100.0 %
Date: 2021-03-23 Branches: 155 402 38.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arith_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, Dejan Jovanovic
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 Whitebox tests for theory Arithmetic.
13
 **/
14
15
#include <list>
16
#include <vector>
17
18
#include "context/context.h"
19
#include "expr/node.h"
20
#include "test_smt.h"
21
#include "theory/arith/theory_arith.h"
22
#include "theory/quantifiers_engine.h"
23
#include "theory/theory.h"
24
#include "theory/theory_engine.h"
25
#include "util/rational.h"
26
27
namespace CVC4 {
28
29
using namespace theory;
30
using namespace theory::arith;
31
using namespace expr;
32
using namespace context;
33
using namespace kind;
34
using namespace smt;
35
36
namespace test {
37
38
8
class TestTheoryWhiteArith : public TestSmtNoFinishInit
39
{
40
 protected:
41
4
  void SetUp() override
42
  {
43
4
    TestSmtNoFinishInit::SetUp();
44
4
    d_smtEngine->setOption("incremental", "false");
45
4
    d_smtEngine->finishInit();
46
4
    d_arith = static_cast<TheoryArith*>(
47
4
        d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
48
49
4
    d_realType.reset(new TypeNode(d_nodeManager->realType()));
50
4
    d_intType.reset(new TypeNode(d_nodeManager->integerType()));
51
4
  }
52
53
2
  void fakeTheoryEnginePreprocess(TNode input)
54
  {
55
2
    Assert(input == Rewriter::rewrite(input));
56
2
    d_smtEngine->getTheoryEngine()->preRegister(input);
57
2
  }
58
59
  Theory::Effort d_level = Theory::EFFORT_FULL;
60
  TheoryArith* d_arith;
61
  std::unique_ptr<TypeNode> d_realType;
62
  std::unique_ptr<TypeNode> d_intType;
63
  const Rational d_zero = 0;
64
  const Rational d_one = 1;
65
};
66
67
11
TEST_F(TestTheoryWhiteArith, assert)
68
{
69
4
  Node x = d_nodeManager->mkVar(*d_realType);
70
4
  Node c = d_nodeManager->mkConst<Rational>(d_zero);
71
72
4
  Node gt = d_nodeManager->mkNode(GT, x, c);
73
4
  Node leq = Rewriter::rewrite(gt.notNode());
74
2
  fakeTheoryEnginePreprocess(leq);
75
76
2
  d_arith->assertFact(leq, true);
77
78
2
  d_arith->check(d_level);
79
2
}
80
81
11
TEST_F(TestTheoryWhiteArith, int_normal_form)
82
{
83
4
  Node x = d_nodeManager->mkVar(*d_intType);
84
4
  Node xr = d_nodeManager->mkVar(*d_realType);
85
4
  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
86
4
  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
87
4
  Node c2 = d_nodeManager->mkConst<Rational>(Rational(2));
88
89
4
  Node geq0 = d_nodeManager->mkNode(GEQ, x, c0);
90
4
  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
91
4
  Node geq2 = d_nodeManager->mkNode(GEQ, x, c2);
92
93
2
  ASSERT_EQ(Rewriter::rewrite(geq0), geq0);
94
2
  ASSERT_EQ(Rewriter::rewrite(geq1), geq1);
95
96
4
  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
97
4
  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
98
99
2
  ASSERT_EQ(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1));
100
2
  ASSERT_EQ(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2));
101
102
4
  Node lt0 = d_nodeManager->mkNode(LT, x, c0);
103
4
  Node lt1 = d_nodeManager->mkNode(LT, x, c1);
104
105
2
  ASSERT_EQ(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode()));
106
2
  ASSERT_EQ(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode()));
107
108
4
  Node leq0 = d_nodeManager->mkNode(LEQ, x, c0);
109
4
  Node leq1 = d_nodeManager->mkNode(LEQ, x, c1);
110
111
2
  ASSERT_EQ(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode()));
112
2
  ASSERT_EQ(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode()));
113
114
  // (abs x) --> (abs x)
115
4
  Node absX = d_nodeManager->mkNode(ABS, x);
116
2
  ASSERT_EQ(Rewriter::rewrite(absX), absX);
117
118
  // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1))
119
  Node t =
120
4
      d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(PLUS, c2, xr))
121
4
          .eqNode(c0);
122
2
  ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t));
123
}
124
}  // namespace test
125
213415
}  // namespace CVC4