Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/theory/theory_int_opt_white.cpp	Lines:	65	65	100.0 %
Date:	2021-05-24	Branches:	139	334	41.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Michael Chang, Yancheng Ou
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * White-box testing for optimization module for Integers.
 */
#include <iostream>

#include "smt/optimization_solver.h"
#include "test_smt.h"

namespace cvc5 {

using namespace theory;
using namespace smt;

namespace test {

class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
{
 protected:
  void SetUp() override
  {
    TestSmtNoFinishInit::SetUp();
    d_smtEngine->setOption("produce-assertions", "true");
    d_smtEngine->finishInit();

    d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
    d_intType.reset(new TypeNode(d_nodeManager->integerType()));
  }

  std::unique_ptr<OptimizationSolver> d_optslv;
  std::unique_ptr<TypeNode> d_intType;
};

TEST_F(TestTheoryWhiteIntOpt, max)
{
  Node ub = d_nodeManager->mkConst(Rational("100"));
  Node lb = d_nodeManager->mkConst(Rational("0"));

  // Objectives to be optimized max_cost is max objective
  Node max_cost = d_nodeManager->mkVar(*d_intType);

  Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);

  /* Result of asserts is:
      0 < max_cost < 100
  */
  d_smtEngine->assertFormula(upb);
  d_smtEngine->assertFormula(lowb);


  // We activate our objective so the subsolver knows to optimize it
  d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);

  OptimizationResult::ResultType r = d_optslv->checkOpt();

  ASSERT_EQ(r, OptimizationResult::OPTIMAL);

  // We expect max_cost == 99
  ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
            Rational("99"));

  d_optslv->popObjective();
}

TEST_F(TestTheoryWhiteIntOpt, min)
{
  Node ub = d_nodeManager->mkConst(Rational("100"));
  Node lb = d_nodeManager->mkConst(Rational("0"));

  // Objectives to be optimized max_cost is max objective
  Node max_cost = d_nodeManager->mkVar(*d_intType);

  Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);

  /* Result of asserts is:
      0 < max_cost < 100
  */
  d_smtEngine->assertFormula(upb);
  d_smtEngine->assertFormula(lowb);


  // We activate our objective so the subsolver knows to optimize it
  d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE);

  OptimizationResult::ResultType r = d_optslv->checkOpt();

  ASSERT_EQ(r, OptimizationResult::OPTIMAL);

  // We expect max_cost == 99
  ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
            Rational("1"));

  d_optslv->popObjective();
}

TEST_F(TestTheoryWhiteIntOpt, result)
{
  Node ub = d_nodeManager->mkConst(Rational("100"));
  Node lb = d_nodeManager->mkConst(Rational("0"));

  // Objectives to be optimized max_cost is max objective
  Node max_cost = d_nodeManager->mkVar(*d_intType);

  Node upb = d_nodeManager->mkNode(kind::GT, lb, max_cost);
  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, ub);

  /* Result of asserts is:
      0 > max_cost > 100
  */
  d_smtEngine->assertFormula(upb);
  d_smtEngine->assertFormula(lowb);


  // We activate our objective so the subsolver knows to optimize it
  d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);

  // This should return OPT_UNSAT since 0 > x > 100 is impossible.
  OptimizationResult::ResultType r = d_optslv->checkOpt();

  // We expect our check to have returned UNSAT
  ASSERT_EQ(r, OptimizationResult::UNSAT);
  d_optslv->popObjective();
}

TEST_F(TestTheoryWhiteIntOpt, open_interval)
{
  Node ub1 = d_nodeManager->mkConst(Rational("100"));
  Node lb1 = d_nodeManager->mkConst(Rational("0"));
  Node lb2 = d_nodeManager->mkConst(Rational("110"));

  Node cost1 = d_nodeManager->mkVar(*d_intType);
  Node cost2 = d_nodeManager->mkVar(*d_intType);

  /* Result of assertion is:
      0 < cost1 < 100
      110 < cost2
  */
  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1));
  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1));

  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2));

  /* Optimization objective:
      cost1 + cost2
  */
  Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);

  d_optslv->pushObjective(cost3, OptimizationObjective::MINIMIZE);

  OptimizationResult::ResultType r = d_optslv->checkOpt();

  ASSERT_EQ(r, OptimizationResult::OPTIMAL);

  // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
  ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
            Rational("112"));
  d_optslv->popObjective();
}

}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Michael Chang, Yancheng Ou
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* White-box testing for optimization module for Integers.
14		*/
15		#include <iostream>
16
17		#include "smt/optimization_solver.h"
18		#include "test_smt.h"
19
20		namespace cvc5 {
21
22		using namespace theory;
23		using namespace smt;
24
25		namespace test {
26
27	16	class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
28		{
29		protected:
30	8	void SetUp() override
31		{
32	8	TestSmtNoFinishInit::SetUp();
33	8	d_smtEngine->setOption("produce-assertions", "true");
34	8	d_smtEngine->finishInit();
35
36	8	d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
37	8	d_intType.reset(new TypeNode(d_nodeManager->integerType()));
38	8	}
39
40		std::unique_ptr<OptimizationSolver> d_optslv;
41		std::unique_ptr<TypeNode> d_intType;
42		};
43
44	13	TEST_F(TestTheoryWhiteIntOpt, max)
45		{
46	4	Node ub = d_nodeManager->mkConst(Rational("100"));
47	4	Node lb = d_nodeManager->mkConst(Rational("0"));
48
49		// Objectives to be optimized max_cost is max objective
50	4	Node max_cost = d_nodeManager->mkVar(*d_intType);
51
52	4	Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
53	4	Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
54
55		/* Result of asserts is:
56		0 < max_cost < 100
57		*/
58	2	d_smtEngine->assertFormula(upb);
59	2	d_smtEngine->assertFormula(lowb);
60
61
62		// We activate our objective so the subsolver knows to optimize it
63	2	d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
64
65	2	OptimizationResult::ResultType r = d_optslv->checkOpt();
66
67	2	ASSERT_EQ(r, OptimizationResult::OPTIMAL);
68
69		// We expect max_cost == 99
70	2	ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
71	2	Rational("99"));
72
73	2	d_optslv->popObjective();
74		}
75
76	13	TEST_F(TestTheoryWhiteIntOpt, min)
77		{
78	4	Node ub = d_nodeManager->mkConst(Rational("100"));
79	4	Node lb = d_nodeManager->mkConst(Rational("0"));
80
81		// Objectives to be optimized max_cost is max objective
82	4	Node max_cost = d_nodeManager->mkVar(*d_intType);
83
84	4	Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
85	4	Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
86
87		/* Result of asserts is:
88		0 < max_cost < 100
89		*/
90	2	d_smtEngine->assertFormula(upb);
91	2	d_smtEngine->assertFormula(lowb);
92
93
94		// We activate our objective so the subsolver knows to optimize it
95	2	d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE);
96
97	2	OptimizationResult::ResultType r = d_optslv->checkOpt();
98
99	2	ASSERT_EQ(r, OptimizationResult::OPTIMAL);
100
101		// We expect max_cost == 99
102	2	ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
103	2	Rational("1"));
104
105	2	d_optslv->popObjective();
106		}
107
108	13	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
126		// We activate our objective so the subsolver knows to optimize it
127	2	d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
128
129		// This should return OPT_UNSAT since 0 > x > 100 is impossible.
130	2	OptimizationResult::ResultType r = d_optslv->checkOpt();
131
132		// We expect our check to have returned UNSAT
133	2	ASSERT_EQ(r, OptimizationResult::UNSAT);
134	2	d_optslv->popObjective();
135		}
136
137	13	TEST_F(TestTheoryWhiteIntOpt, open_interval)
138		{
139	4	Node ub1 = d_nodeManager->mkConst(Rational("100"));
140	4	Node lb1 = d_nodeManager->mkConst(Rational("0"));
141	4	Node lb2 = d_nodeManager->mkConst(Rational("110"));
142
143	4	Node cost1 = d_nodeManager->mkVar(*d_intType);
144	4	Node cost2 = d_nodeManager->mkVar(*d_intType);
145
146		/* Result of assertion is:
147		0 < cost1 < 100
148		110 < cost2
149		*/
150	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1));
151	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1));
152
153	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2));
154
155		/* Optimization objective:
156		cost1 + cost2
157		*/
158	4	Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);
159
160	2	d_optslv->pushObjective(cost3, OptimizationObjective::MINIMIZE);
161
162	2	OptimizationResult::ResultType r = d_optslv->checkOpt();
163
164	2	ASSERT_EQ(r, OptimizationResult::OPTIMAL);
165
166		// expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
167	2	ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
168	2	Rational("112"));
169	2	d_optslv->popObjective();
170		}
171
172		} // namespace test
173	6235593	} // namespace cvc5