GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_int_opt_white.cpp Lines: 54 54 100.0 %
Date: 2021-03-23 Branches: 102 228 44.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_int_opt_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Michael Chang
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 White-box testing for optimization module.
13
 **/
14
#include <iostream>
15
#include "smt/optimization_solver.h"
16
#include "test_smt.h"
17
18
namespace CVC4 {
19
20
using namespace theory;
21
using namespace smt;
22
23
namespace test {
24
25
12
class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
26
{
27
 protected:
28
6
  void SetUp() override
29
  {
30
6
    TestSmtNoFinishInit::SetUp();
31
6
    d_smtEngine->setOption("produce-assertions", "true");
32
6
    d_smtEngine->finishInit();
33
34
6
    d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
35
6
    d_intType.reset(new TypeNode(d_nodeManager->integerType()));
36
6
  }
37
38
  std::unique_ptr<OptimizationSolver> d_optslv;
39
  std::unique_ptr<TypeNode> d_intType;
40
};
41
42
12
TEST_F(TestTheoryWhiteIntOpt, max)
43
{
44
4
  Node ub = d_nodeManager->mkConst(Rational("100"));
45
4
  Node lb = d_nodeManager->mkConst(Rational("0"));
46
47
  // Objectives to be optimized max_cost is max objective
48
4
  Node max_cost = d_nodeManager->mkVar(*d_intType);
49
50
4
  Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
51
4
  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
52
53
  /* Result of asserts is:
54
      0 < max_cost < 100
55
  */
56
2
  d_smtEngine->assertFormula(upb);
57
2
  d_smtEngine->assertFormula(lowb);
58
59
2
  const ObjectiveType max_type = OBJECTIVE_MAXIMIZE;
60
61
  // We activate our objective so the subsolver knows to optimize it
62
2
  d_optslv->activateObj(max_cost, max_type);
63
64
2
  OptResult r = d_optslv->checkOpt();
65
66
  // We expect max_cost == 99
67
2
  ASSERT_EQ(d_optslv->objectiveGetValue(),
68
2
                    d_nodeManager->mkConst(Rational("99")));
69
70
2
  std::cout << "Result is :" << r << std::endl;
71
2
  std::cout << "Optimized max value is: "
72
2
            << d_optslv->objectiveGetValue() << std::endl;
73
}
74
75
12
TEST_F(TestTheoryWhiteIntOpt, min)
76
{
77
4
  Node ub = d_nodeManager->mkConst(Rational("100"));
78
4
  Node lb = d_nodeManager->mkConst(Rational("0"));
79
80
  // Objectives to be optimized max_cost is max objective
81
4
  Node max_cost = d_nodeManager->mkVar(*d_intType);
82
83
4
  Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
84
4
  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
85
86
  /* Result of asserts is:
87
      0 < max_cost < 100
88
  */
89
2
  d_smtEngine->assertFormula(upb);
90
2
  d_smtEngine->assertFormula(lowb);
91
92
2
  const ObjectiveType min_type = OBJECTIVE_MINIMIZE;
93
94
  // We activate our objective so the subsolver knows to optimize it
95
2
  d_optslv->activateObj(max_cost, min_type);
96
97
2
  OptResult r = d_optslv->checkOpt();
98
99
  // We expect max_cost == 99
100
2
  ASSERT_EQ(d_optslv->objectiveGetValue(),
101
2
                    d_nodeManager->mkConst(Rational("1")));
102
103
2
  std::cout << "Result is :" << r << std::endl;
104
2
  std::cout << "Optimized max value is: "
105
2
            << d_optslv->objectiveGetValue() << std::endl;
106
}
107
108
12
TEST_F(TestTheoryWhiteIntOpt, result)
109
{
110
4
  Node ub = d_nodeManager->mkConst(Rational("100"));
111
4
  Node lb = d_nodeManager->mkConst(Rational("0"));
112
113
  // Objectives to be optimized max_cost is max objective
114
4
  Node max_cost = d_nodeManager->mkVar(*d_intType);
115
116
4
  Node upb = d_nodeManager->mkNode(kind::GT, lb, max_cost);
117
4
  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, ub);
118
119
  /* Result of asserts is:
120
      0 > max_cost > 100
121
  */
122
2
  d_smtEngine->assertFormula(upb);
123
2
  d_smtEngine->assertFormula(lowb);
124
125
2
  const ObjectiveType max_type = OBJECTIVE_MAXIMIZE;
126
127
  // We activate our objective so the subsolver knows to optimize it
128
2
  d_optslv->activateObj(max_cost, max_type);
129
130
  // This should return OPT_UNSAT since 0 > x > 100 is impossible.
131
2
  OptResult r = d_optslv->checkOpt();
132
133
  // We expect our check to have returned UNSAT
134
2
  ASSERT_EQ(r, OPT_UNSAT);
135
136
2
  std::cout << "Result is :" << r << std::endl;
137
}
138
}  // namespace test
139
6203082
}  // namespace CVC4