Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/theory/theory_opt_multigoal_white.cpp	Lines:	149	149	100.0 %
Date:	2021-09-18	Branches:	356	906	39.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   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 multigoal optimization.
 */
#include <iostream>

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

namespace cvc5 {

using namespace theory;
using namespace smt;

namespace test {

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

    d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
  }

  std::unique_ptr<TypeNode> d_BV32Type;
};

TEST_F(TestTheoryWhiteOptMultigoal, box)
{
  d_smtEngine->resetAssertions();
  Node x = d_nodeManager->mkVar(*d_BV32Type);
  Node y = d_nodeManager->mkVar(*d_BV32Type);
  Node z = d_nodeManager->mkVar(*d_BV32Type);

  // 18 <= x
  d_smtEngine->assertFormula(d_nodeManager->mkNode(
      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));

  // y <= x
  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));

  OptimizationSolver optSolver(d_smtEngine.get());

  // minimize x
  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
  // maximize y with `signed` comparison over bit-vectors.
  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
  // maximize z
  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);

  // Box optimization
  Result r = optSolver.checkOpt(OptimizationSolver::BOX);

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

  std::vector<OptimizationResult> results = optSolver.getValues();

  // x == 18
  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));

  // y == 0x7FFFFFFF
  ASSERT_EQ(results[1].getValue().getConst<BitVector>(),
            BitVector(32u, (unsigned)0x7FFFFFFF));

  // z == 0xFFFFFFFF
  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
            BitVector(32u, (unsigned)0xFFFFFFFF));
}

TEST_F(TestTheoryWhiteOptMultigoal, lex)
{
  d_smtEngine->resetAssertions();
  Node x = d_nodeManager->mkVar(*d_BV32Type);
  Node y = d_nodeManager->mkVar(*d_BV32Type);
  Node z = d_nodeManager->mkVar(*d_BV32Type);

  // 18 <= x
  d_smtEngine->assertFormula(d_nodeManager->mkNode(
      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));

  // y <= x
  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));

  OptimizationSolver optSolver(d_smtEngine.get());

  // minimize x
  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
  // maximize y with `signed` comparison over bit-vectors.
  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
  // maximize z
  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);

  Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);

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

  std::vector<OptimizationResult> results = optSolver.getValues();

  // x == 18
  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));

  // y == 18
  ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));

  // z == 0xFFFFFFFF
  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
            BitVector(32u, (unsigned)0xFFFFFFFF));
}

TEST_F(TestTheoryWhiteOptMultigoal, pareto)
{
  d_smtEngine->resetAssertions();
  TypeNode bv4ty(d_nodeManager->mkBitVectorType(4u));
  Node a = d_nodeManager->mkVar(bv4ty);
  Node b = d_nodeManager->mkVar(bv4ty);

  Node bv1 = d_nodeManager->mkConst(BitVector(4u, 1u));
  Node bv2 = d_nodeManager->mkConst(BitVector(4u, 2u));
  Node bv3 = d_nodeManager->mkConst(BitVector(4u, 3u));

  std::vector<Node> stmts = {
      // (and (= a 1) (= b 1))
      d_nodeManager->mkNode(kind::AND,
                            d_nodeManager->mkNode(kind::EQUAL, a, bv1),
                            d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
      // (and (= a 2) (= b 1))
      d_nodeManager->mkNode(kind::AND,
                            d_nodeManager->mkNode(kind::EQUAL, a, bv2),
                            d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
      // (and (= a 1) (= b 2))
      d_nodeManager->mkNode(kind::AND,
                            d_nodeManager->mkNode(kind::EQUAL, a, bv1),
                            d_nodeManager->mkNode(kind::EQUAL, b, bv2)),
      // (and (= a 2) (= b 2))
      d_nodeManager->mkNode(kind::AND,
                            d_nodeManager->mkNode(kind::EQUAL, a, bv2),
                            d_nodeManager->mkNode(kind::EQUAL, b, bv2)),
      // (and (= a 3) (= b 1))
      d_nodeManager->mkNode(kind::AND,
                            d_nodeManager->mkNode(kind::EQUAL, a, bv3),
                            d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
      // (and (= a 1) (= b 3))
      d_nodeManager->mkNode(kind::AND,
                            d_nodeManager->mkNode(kind::EQUAL, a, bv1),
                            d_nodeManager->mkNode(kind::EQUAL, b, bv3)),
  };
  /*
  (assert (or
    (and (= a 1) (= b 1))
    (and (= a 2) (= b 1))
    (and (= a 1) (= b 2))
    (and (= a 2) (= b 2))
    (and (= a 3) (= b 1))
    (and (= a 1) (= b 3))
  ))
  */
  d_smtEngine->assertFormula(d_nodeManager->mkOr(stmts));

  /*
    (maximize a)
    (maximize b)
   */
  OptimizationSolver optSolver(d_smtEngine.get());
  optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
  optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);

  Result r;

  // all possible result pairs <a, b>
  std::set<std::pair<uint32_t, uint32_t>> possibleResults = {
      {1, 3}, {2, 2}, {3, 1}};

  r = optSolver.checkOpt(OptimizationSolver::PARETO);
  ASSERT_EQ(r.isSat(), Result::SAT);
  std::vector<OptimizationResult> results = optSolver.getValues();
  std::pair<uint32_t, uint32_t> res = {
      results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
      results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
  for (auto& rn : results)
  {
    std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
              << " ";
  }
  std::cout << std::endl;
  ASSERT_EQ(possibleResults.count(res), 1);
  possibleResults.erase(res);

  r = optSolver.checkOpt(OptimizationSolver::PARETO);
  ASSERT_EQ(r.isSat(), Result::SAT);
  results = optSolver.getValues();
  res = {
      results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
      results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
  for (auto& rn : results)
  {
    std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
              << " ";
  }
  std::cout << std::endl;
  ASSERT_EQ(possibleResults.count(res), 1);
  possibleResults.erase(res);

  r = optSolver.checkOpt(OptimizationSolver::PARETO);
  ASSERT_EQ(r.isSat(), Result::SAT);
  results = optSolver.getValues();
  res = {
      results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
      results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
  for (auto& rn : results)
  {
    std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
              << " ";
  }
  std::cout << std::endl;
  ASSERT_EQ(possibleResults.count(res), 1);
  possibleResults.erase(res);

  r = optSolver.checkOpt(OptimizationSolver::PARETO);
  ASSERT_EQ(r.isSat(), Result::UNSAT);
  ASSERT_EQ(possibleResults.size(), 0);
}

TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
{
  d_smtEngine->resetAssertions();
  Node x = d_nodeManager->mkVar(*d_BV32Type);
  Node y = d_nodeManager->mkVar(*d_BV32Type);
  Node z = d_nodeManager->mkVar(*d_BV32Type);

  // 18 <= x
  d_smtEngine->assertFormula(d_nodeManager->mkNode(
      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));

  // y <= x
  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));

  OptimizationSolver optSolver(d_smtEngine.get());

  // minimize x
  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);

  // push
  d_smtEngine->push();

  // maximize y with `signed` comparison over bit-vectors.
  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
  // maximize z
  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);

  // Lexico optimization
  Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);

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

  std::vector<OptimizationResult> results = optSolver.getValues();

  // x == 18
  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));

  // y == 18
  ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));

  // z == 0xFFFFFFFF
  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
            BitVector(32u, (unsigned)0xFFFFFFFF));

  // pop
  d_smtEngine->pop();

  // now we only have one objective: (minimize x)
  r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
  ASSERT_EQ(r.isSat(), Result::SAT);
  results = optSolver.getValues();
  ASSERT_EQ(results.size(), 1);
  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));

  // resetting the assertions also resets the optimization objectives
  d_smtEngine->resetAssertions();
  r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
  ASSERT_EQ(r.isSat(), Result::SAT);
  results = optSolver.getValues();
  ASSERT_EQ(results.size(), 0);
}

}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* 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 multigoal optimization.
14		*/
15		#include <iostream>
16
17		#include "smt/optimization_solver.h"
18		#include "test_smt.h"
19		#include "util/bitvector.h"
20
21		namespace cvc5 {
22
23		using namespace theory;
24		using namespace smt;
25
26		namespace test {
27
28	16	class TestTheoryWhiteOptMultigoal : 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_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
38	8	}
39
40		std::unique_ptr<TypeNode> d_BV32Type;
41		};
42
43	13	TEST_F(TestTheoryWhiteOptMultigoal, box)
44		{
45	2	d_smtEngine->resetAssertions();
46	4	Node x = d_nodeManager->mkVar(*d_BV32Type);
47	4	Node y = d_nodeManager->mkVar(*d_BV32Type);
48	4	Node z = d_nodeManager->mkVar(*d_BV32Type);
49
50		// 18 <= x
51	6	d_smtEngine->assertFormula(d_nodeManager->mkNode(
52	4	kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
53
54		// y <= x
55	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
56
57	4	OptimizationSolver optSolver(d_smtEngine.get());
58
59		// minimize x
60	2	optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
61		// maximize y with `signed` comparison over bit-vectors.
62	2	optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
63		// maximize z
64	2	optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
65
66		// Box optimization
67	4	Result r = optSolver.checkOpt(OptimizationSolver::BOX);
68
69	2	ASSERT_EQ(r.isSat(), Result::SAT);
70
71	4	std::vector<OptimizationResult> results = optSolver.getValues();
72
73		// x == 18
74	2	ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
75
76		// y == 0x7FFFFFFF
77	2	ASSERT_EQ(results[1].getValue().getConst<BitVector>(),
78	2	BitVector(32u, (unsigned)0x7FFFFFFF));
79
80		// z == 0xFFFFFFFF
81	2	ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
82	2	BitVector(32u, (unsigned)0xFFFFFFFF));
83		}
84
85	13	TEST_F(TestTheoryWhiteOptMultigoal, lex)
86		{
87	2	d_smtEngine->resetAssertions();
88	4	Node x = d_nodeManager->mkVar(*d_BV32Type);
89	4	Node y = d_nodeManager->mkVar(*d_BV32Type);
90	4	Node z = d_nodeManager->mkVar(*d_BV32Type);
91
92		// 18 <= x
93	6	d_smtEngine->assertFormula(d_nodeManager->mkNode(
94	4	kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
95
96		// y <= x
97	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
98
99	4	OptimizationSolver optSolver(d_smtEngine.get());
100
101		// minimize x
102	2	optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
103		// maximize y with `signed` comparison over bit-vectors.
104	2	optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
105		// maximize z
106	2	optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
107
108	4	Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
109
110	2	ASSERT_EQ(r.isSat(), Result::SAT);
111
112	4	std::vector<OptimizationResult> results = optSolver.getValues();
113
114		// x == 18
115	2	ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
116
117		// y == 18
118	2	ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));
119
120		// z == 0xFFFFFFFF
121	2	ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
122	2	BitVector(32u, (unsigned)0xFFFFFFFF));
123		}
124
125	13	TEST_F(TestTheoryWhiteOptMultigoal, pareto)
126		{
127	2	d_smtEngine->resetAssertions();
128	4	TypeNode bv4ty(d_nodeManager->mkBitVectorType(4u));
129	4	Node a = d_nodeManager->mkVar(bv4ty);
130	4	Node b = d_nodeManager->mkVar(bv4ty);
131
132	4	Node bv1 = d_nodeManager->mkConst(BitVector(4u, 1u));
133	4	Node bv2 = d_nodeManager->mkConst(BitVector(4u, 2u));
134	4	Node bv3 = d_nodeManager->mkConst(BitVector(4u, 3u));
135
136		std::vector<Node> stmts = {
137		// (and (= a 1) (= b 1))
138	2	d_nodeManager->mkNode(kind::AND,
139	4	d_nodeManager->mkNode(kind::EQUAL, a, bv1),
140	4	d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
141		// (and (= a 2) (= b 1))
142	2	d_nodeManager->mkNode(kind::AND,
143	4	d_nodeManager->mkNode(kind::EQUAL, a, bv2),
144	4	d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
145		// (and (= a 1) (= b 2))
146	2	d_nodeManager->mkNode(kind::AND,
147	4	d_nodeManager->mkNode(kind::EQUAL, a, bv1),
148	4	d_nodeManager->mkNode(kind::EQUAL, b, bv2)),
149		// (and (= a 2) (= b 2))
150	2	d_nodeManager->mkNode(kind::AND,
151	4	d_nodeManager->mkNode(kind::EQUAL, a, bv2),
152	4	d_nodeManager->mkNode(kind::EQUAL, b, bv2)),
153		// (and (= a 3) (= b 1))
154	2	d_nodeManager->mkNode(kind::AND,
155	4	d_nodeManager->mkNode(kind::EQUAL, a, bv3),
156	4	d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
157		// (and (= a 1) (= b 3))
158	2	d_nodeManager->mkNode(kind::AND,
159	4	d_nodeManager->mkNode(kind::EQUAL, a, bv1),
160	4	d_nodeManager->mkNode(kind::EQUAL, b, bv3)),
161	48	};
162		/*
163		(assert (or
164		(and (= a 1) (= b 1))
165		(and (= a 2) (= b 1))
166		(and (= a 1) (= b 2))
167		(and (= a 2) (= b 2))
168		(and (= a 3) (= b 1))
169		(and (= a 1) (= b 3))
170		))
171		*/
172	2	d_smtEngine->assertFormula(d_nodeManager->mkOr(stmts));
173
174		/*
175		(maximize a)
176		(maximize b)
177		*/
178	4	OptimizationSolver optSolver(d_smtEngine.get());
179	2	optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
180	2	optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);
181
182	4	Result r;
183
184		// all possible result pairs <a, b>
185		std::set<std::pair<uint32_t, uint32_t>> possibleResults = {
186	4	{1, 3}, {2, 2}, {3, 1}};
187
188	2	r = optSolver.checkOpt(OptimizationSolver::PARETO);
189	2	ASSERT_EQ(r.isSat(), Result::SAT);
190	4	std::vector<OptimizationResult> results = optSolver.getValues();
191		std::pair<uint32_t, uint32_t> res = {
192	4	results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
193	2	results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
194	6	for (auto& rn : results)
195		{
196	8	std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
197	4	<< " ";
198		}
199	2	std::cout << std::endl;
200	2	ASSERT_EQ(possibleResults.count(res), 1);
201	2	possibleResults.erase(res);
202
203	2	r = optSolver.checkOpt(OptimizationSolver::PARETO);
204	2	ASSERT_EQ(r.isSat(), Result::SAT);
205	2	results = optSolver.getValues();
206	2	res = {
207	4	results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
208	4	results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
209	6	for (auto& rn : results)
210		{
211	8	std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
212	4	<< " ";
213		}
214	2	std::cout << std::endl;
215	2	ASSERT_EQ(possibleResults.count(res), 1);
216	2	possibleResults.erase(res);
217
218	2	r = optSolver.checkOpt(OptimizationSolver::PARETO);
219	2	ASSERT_EQ(r.isSat(), Result::SAT);
220	2	results = optSolver.getValues();
221	2	res = {
222	4	results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
223	4	results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
224	6	for (auto& rn : results)
225		{
226	8	std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
227	4	<< " ";
228		}
229	2	std::cout << std::endl;
230	2	ASSERT_EQ(possibleResults.count(res), 1);
231	2	possibleResults.erase(res);
232
233	2	r = optSolver.checkOpt(OptimizationSolver::PARETO);
234	2	ASSERT_EQ(r.isSat(), Result::UNSAT);
235	2	ASSERT_EQ(possibleResults.size(), 0);
236		}
237
238	13	TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
239		{
240	2	d_smtEngine->resetAssertions();
241	4	Node x = d_nodeManager->mkVar(*d_BV32Type);
242	4	Node y = d_nodeManager->mkVar(*d_BV32Type);
243	4	Node z = d_nodeManager->mkVar(*d_BV32Type);
244
245		// 18 <= x
246	6	d_smtEngine->assertFormula(d_nodeManager->mkNode(
247	4	kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
248
249		// y <= x
250	2	d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
251
252	4	OptimizationSolver optSolver(d_smtEngine.get());
253
254		// minimize x
255	2	optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
256
257		// push
258	2	d_smtEngine->push();
259
260		// maximize y with `signed` comparison over bit-vectors.
261	2	optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
262		// maximize z
263	2	optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
264
265		// Lexico optimization
266	4	Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
267
268	2	ASSERT_EQ(r.isSat(), Result::SAT);
269
270	4	std::vector<OptimizationResult> results = optSolver.getValues();
271
272		// x == 18
273	2	ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
274
275		// y == 18
276	2	ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));
277
278		// z == 0xFFFFFFFF
279	2	ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
280	2	BitVector(32u, (unsigned)0xFFFFFFFF));
281
282		// pop
283	2	d_smtEngine->pop();
284
285		// now we only have one objective: (minimize x)
286	2	r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
287	2	ASSERT_EQ(r.isSat(), Result::SAT);
288	2	results = optSolver.getValues();
289	2	ASSERT_EQ(results.size(), 1);
290	2	ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
291
292		// resetting the assertions also resets the optimization objectives
293	2	d_smtEngine->resetAssertions();
294	2	r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
295	2	ASSERT_EQ(r.isSat(), Result::SAT);
296	2	results = optSolver.getValues();
297	2	ASSERT_EQ(results.size(), 0);
298		}
299
300		} // namespace test
301	15	} // namespace cvc5