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-08-01	Branches:	144	344	41.9 %


/******************************************************************************
 * 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"
#include "util/rational.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->addObjective(max_cost, OptimizationObjective::MAXIMIZE);

  Result r = d_optslv->checkOpt();

  ASSERT_EQ(r.isSat(), Result::SAT);

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

  d_smtEngine->resetAssertions();
}

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->addObjective(max_cost, OptimizationObjective::MINIMIZE);

  Result r = d_optslv->checkOpt();

  ASSERT_EQ(r.isSat(), Result::SAT);

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

  d_smtEngine->resetAssertions();
}

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->addObjective(max_cost, OptimizationObjective::MAXIMIZE);

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

  // We expect our check to have returned UNSAT
  ASSERT_EQ(r.isSat(), Result::UNSAT);
  d_smtEngine->resetAssertions();
}

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->addObjective(cost3, OptimizationObjective::MINIMIZE);

  Result r = d_optslv->checkOpt();

  ASSERT_EQ(r.isSat(), Result::SAT);

  // 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_smtEngine->resetAssertions();
}

}  // 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		#include "util/rational.h"
20
21		namespace cvc5 {
22
23		using namespace theory;
24		using namespace smt;
25
26		namespace test {
27
28	16	class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
29		{
30		protected:
31	8	void SetUp() override
32		{
33	8	TestSmtNoFinishInit::SetUp();
34	8	d_smtEngine->setOption("produce-assertions", "true");
35	8	d_smtEngine->finishInit();
36
37	8	d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
38	8	d_intType.reset(new TypeNode(d_nodeManager->integerType()));
39	8	}
40
41		std::unique_ptr<OptimizationSolver> d_optslv;
42		std::unique_ptr<TypeNode> d_intType;
43		};
44
45	13	TEST_F(TestTheoryWhiteIntOpt, max)
46		{
47	4	Node ub = d_nodeManager->mkConst(Rational("100"));
48	4	Node lb = d_nodeManager->mkConst(Rational("0"));
49
50		// Objectives to be optimized max_cost is max objective
51	4	Node max_cost = d_nodeManager->mkVar(*d_intType);
52
53	4	Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
54	4	Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
55
56		/* Result of asserts is:
57		0 < max_cost < 100
58		*/
59	2	d_smtEngine->assertFormula(upb);
60	2	d_smtEngine->assertFormula(lowb);
61
62		// We activate our objective so the subsolver knows to optimize it
63	2	d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
64
65	4	Result r = d_optslv->checkOpt();
66
67	2	ASSERT_EQ(r.isSat(), Result::SAT);
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_smtEngine->resetAssertions();
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		// We activate our objective so the subsolver knows to optimize it
94	2	d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE);
95
96	4	Result r = d_optslv->checkOpt();
97
98	2	ASSERT_EQ(r.isSat(), Result::SAT);
99
100		// We expect max_cost == 99
101	2	ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
102	2	Rational("1"));
103
104	2	d_smtEngine->resetAssertions();
105		}
106
107	13	TEST_F(TestTheoryWhiteIntOpt, result)
108		{
109	4	Node ub = d_nodeManager->mkConst(Rational("100"));
110	4	Node lb = d_nodeManager->mkConst(Rational("0"));
111
112		// Objectives to be optimized max_cost is max objective
113	4	Node max_cost = d_nodeManager->mkVar(*d_intType);
114
115	4	Node upb = d_nodeManager->mkNode(kind::GT, lb, max_cost);
116	4	Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, ub);
117
118		/* Result of asserts is:
119		0 > max_cost > 100
120		*/
121	2	d_smtEngine->assertFormula(upb);
122	2	d_smtEngine->assertFormula(lowb);
123
124		// We activate our objective so the subsolver knows to optimize it
125	2	d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
126
127		// This should return OPT_UNSAT since 0 > x > 100 is impossible.
128	4	Result r = d_optslv->checkOpt();
129
130		// We expect our check to have returned UNSAT
131	2	ASSERT_EQ(r.isSat(), Result::UNSAT);
132	2	d_smtEngine->resetAssertions();
133		}
134
135	13	TEST_F(TestTheoryWhiteIntOpt, open_interval)
136		{
137	4	Node ub1 = d_nodeManager->mkConst(Rational("100"));
138	4	Node lb1 = d_nodeManager->mkConst(Rational("0"));
139	4	Node lb2 = d_nodeManager->mkConst(Rational("110"));
140
141	4	Node cost1 = d_nodeManager->mkVar(*d_intType);
142	4	Node cost2 = d_nodeManager->mkVar(*d_intType);
143
144		/* Result of assertion is:
145		0 < cost1 < 100
146		110 < cost2
147		*/
148	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1));
149	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1));
150
151	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2));
152
153		/* Optimization objective:
154		cost1 + cost2
155		*/
156	4	Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);
157
158	2	d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE);
159
160	4	Result r = d_optslv->checkOpt();
161
162	2	ASSERT_EQ(r.isSat(), Result::SAT);
163
164		// expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
165	2	ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
166	2	Rational("112"));
167	2	d_smtEngine->resetAssertions();
168		}
169
170		} // namespace test
171	6057643	} // namespace cvc5