Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/omt/bitvector_optimizer.cpp	Lines:	87	95	91.6 %
Date:	2021-05-21	Branches:	174	342	50.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Yancheng Ou, Michael Chang
 *
 * 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.
 * ****************************************************************************
 *
 * Optimizer for BitVector type.
 */

#include "omt/bitvector_optimizer.h"

#include "options/smt_options.h"
#include "smt/smt_engine.h"

using namespace cvc5::smt;
namespace cvc5::omt {

OMTOptimizerBitVector::OMTOptimizerBitVector(bool isSigned)
    : d_isSigned(isSigned)
{
}

BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a,
                                                const BitVector& b,
                                                bool isSigned)
{
  // computes (a + b) / 2 without overflow
  // rounding towards -infinity: -1.5 --> -2,  1.5 --> 1
  // average = (a / 2) + (b / 2) + (((a % 2) + (b % 2)) / 2)
  uint32_t aMod2 = static_cast<uint32_t>(a.isBitSet(0));
  uint32_t bMod2 = static_cast<uint32_t>(b.isBitSet(0));
  BitVector aMod2PlusbMod2Div2(a.getSize(), (aMod2 + bMod2) / 2);
  BitVector bv1 = BitVector::mkOne(a.getSize());
  return (isSigned) ? ((a.arithRightShift(bv1) + b.arithRightShift(bv1)
                        + aMod2PlusbMod2Div2))
                    : ((a.logicalRightShift(bv1) + b.logicalRightShift(bv1)
                        + aMod2PlusbMod2Div2));
}

OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
                                                   TNode target)
{
  // the smt engine to which we send intermediate queries
  // for the binary search.
  NodeManager* nm = optChecker->getNodeManager();
  Result intermediateSatResult = optChecker->checkSat();
  // Model-value of objective (used in optimization loop)
  Node value;
  if (intermediateSatResult.isUnknown())
  {
    return OptimizationResult(OptimizationResult::UNKNOWN, value);
  }
  if (intermediateSatResult.isSat() == Result::UNSAT)
  {
    return OptimizationResult(OptimizationResult::UNSAT, value);
  }

  // value equals to upperBound
  value = optChecker->getValue(target);

  // this gets the bitvector!
  BitVector bvValue = value.getConst<BitVector>();
  unsigned int bvSize = bvValue.getSize();

  // lowerbound
  BitVector lowerBound = ((this->d_isSigned) ? (BitVector::mkMinSigned(bvSize))
                                             : (BitVector::mkZero(bvSize)));
  // upperbound must be a satisfying value
  // and value == upperbound
  BitVector upperBound = bvValue;

  Kind LTOperator =
      ((d_isSigned) ? (kind::BITVECTOR_SLT) : (kind::BITVECTOR_ULT));
  Kind GEOperator =
      ((d_isSigned) ? (kind::BITVECTOR_SGE) : (kind::BITVECTOR_UGE));

  // the pivot value for binary search,
  // pivot = (lowerBound + upperBound) / 2
  // rounded towards -infinity
  BitVector pivot;
  while ((d_isSigned && lowerBound.signedLessThan(upperBound))
         || (!d_isSigned && lowerBound.unsignedLessThan(upperBound)))
  {
    pivot = computeAverage(lowerBound, upperBound, d_isSigned);
    optChecker->push();
    if (lowerBound == pivot)
    {
      optChecker->assertFormula(
          nm->mkNode(kind::EQUAL, target, nm->mkConst(lowerBound)));
    }
    else
    {
      // lowerBound <= target < pivot
      optChecker->assertFormula(
          nm->mkNode(kind::AND,
                     nm->mkNode(GEOperator, target, nm->mkConst(lowerBound)),
                     nm->mkNode(LTOperator, target, nm->mkConst(pivot))));
    }
    intermediateSatResult = optChecker->checkSat();
    if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
    {
      return OptimizationResult(OptimizationResult::UNKNOWN, value);
    }
    if (intermediateSatResult.isSat() == Result::SAT)
    {
      value = optChecker->getValue(target);
      upperBound = value.getConst<BitVector>();
    }
    else if (intermediateSatResult.isSat() == Result::UNSAT)
    {
      if (lowerBound == pivot)
      {
        // lowerBound == pivot ==> upperbound = lowerbound + 1
        // and lowerbound <= target < upperbound is UNSAT
        // return the upperbound
        return OptimizationResult(OptimizationResult::OPTIMAL, value);
      }
      else
      {
        lowerBound = pivot;
      }
    }
    else
    {
      return OptimizationResult(OptimizationResult::UNKNOWN, value);
    }
    optChecker->pop();
  }
  return OptimizationResult(OptimizationResult::OPTIMAL, value);
}

OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
                                                   TNode target)
{
  // the smt engine to which we send intermediate queries
  // for the binary search.
  NodeManager* nm = optChecker->getNodeManager();
  Result intermediateSatResult = optChecker->checkSat();
  // Model-value of objective (used in optimization loop)
  Node value;
  if (intermediateSatResult.isUnknown())
  {
    return OptimizationResult(OptimizationResult::UNKNOWN, value);
  }
  if (intermediateSatResult.isSat() == Result::UNSAT)
  {
    return OptimizationResult(OptimizationResult::UNSAT, value);
  }

  // value equals to upperBound
  value = optChecker->getValue(target);

  // this gets the bitvector!
  BitVector bvValue = value.getConst<BitVector>();
  unsigned int bvSize = bvValue.getSize();

  // lowerbound must be a satisfying value
  // and value == lowerbound
  BitVector lowerBound = bvValue;

  // upperbound
  BitVector upperBound = ((this->d_isSigned) ? (BitVector::mkMaxSigned(bvSize))
                                             : (BitVector::mkOnes(bvSize)));

  Kind LEOperator =
      ((d_isSigned) ? (kind::BITVECTOR_SLE) : (kind::BITVECTOR_ULE));
  Kind GTOperator =
      ((d_isSigned) ? (kind::BITVECTOR_SGT) : (kind::BITVECTOR_UGT));

  // the pivot value for binary search,
  // pivot = (lowerBound + upperBound) / 2
  // rounded towards -infinity
  BitVector pivot;
  while ((d_isSigned && lowerBound.signedLessThan(upperBound))
         || (!d_isSigned && lowerBound.unsignedLessThan(upperBound)))
  {
    pivot = computeAverage(lowerBound, upperBound, d_isSigned);

    optChecker->push();
    // notice that we don't have boundary condition here
    // because lowerBound == pivot / lowerBound == upperBound + 1 is also
    // covered
    // pivot < target <= upperBound
    optChecker->assertFormula(
        nm->mkNode(kind::AND,
                   nm->mkNode(GTOperator, target, nm->mkConst(pivot)),
                   nm->mkNode(LEOperator, target, nm->mkConst(upperBound))));
    intermediateSatResult = optChecker->checkSat();
    if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
    {
      return OptimizationResult(OptimizationResult::UNKNOWN, value);
    }
    if (intermediateSatResult.isSat() == Result::SAT)
    {
      value = optChecker->getValue(target);
      lowerBound = value.getConst<BitVector>();
    }
    else if (intermediateSatResult.isSat() == Result::UNSAT)
    {
      if (lowerBound == pivot)
      {
        // upperbound = lowerbound + 1
        // and lowerbound < target <= upperbound is UNSAT
        // return the lowerbound
        return OptimizationResult(OptimizationResult::OPTIMAL, value);
      }
      else
      {
        upperBound = pivot;
      }
    }
    else
    {
      return OptimizationResult(OptimizationResult::UNKNOWN, value);
    }
    optChecker->pop();
  }
  return OptimizationResult(OptimizationResult::OPTIMAL, value);
}

}  // namespace cvc5::omt


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yancheng Ou, Michael Chang
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		* Optimizer for BitVector type.
14		*/
15
16		#include "omt/bitvector_optimizer.h"
17
18		#include "options/smt_options.h"
19		#include "smt/smt_engine.h"
20
21		using namespace cvc5::smt;
22		namespace cvc5::omt {
23
24	10	OMTOptimizerBitVector::OMTOptimizerBitVector(bool isSigned)
25	10	: d_isSigned(isSigned)
26		{
27	10	}
28
29	226	BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a,
30		const BitVector& b,
31		bool isSigned)
32		{
33		// computes (a + b) / 2 without overflow
34		// rounding towards -infinity: -1.5 --> -2, 1.5 --> 1
35		// average = (a / 2) + (b / 2) + (((a % 2) + (b % 2)) / 2)
36	226	uint32_t aMod2 = static_cast<uint32_t>(a.isBitSet(0));
37	226	uint32_t bMod2 = static_cast<uint32_t>(b.isBitSet(0));
38	452	BitVector aMod2PlusbMod2Div2(a.getSize(), (aMod2 + bMod2) / 2);
39	452	BitVector bv1 = BitVector::mkOne(a.getSize());
40	290	return (isSigned) ? ((a.arithRightShift(bv1) + b.arithRightShift(bv1)
41		+ aMod2PlusbMod2Div2))
42	388	: ((a.logicalRightShift(bv1) + b.logicalRightShift(bv1)
43	678	+ aMod2PlusbMod2Div2));
44		}
45
46	6	OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
47		TNode target)
48		{
49		// the smt engine to which we send intermediate queries
50		// for the binary search.
51	6	NodeManager* nm = optChecker->getNodeManager();
52	12	Result intermediateSatResult = optChecker->checkSat();
53		// Model-value of objective (used in optimization loop)
54	12	Node value;
55	6	if (intermediateSatResult.isUnknown())
56		{
57		return OptimizationResult(OptimizationResult::UNKNOWN, value);
58		}
59	6	if (intermediateSatResult.isSat() == Result::UNSAT)
60		{
61		return OptimizationResult(OptimizationResult::UNSAT, value);
62		}
63
64		// value equals to upperBound
65	6	value = optChecker->getValue(target);
66
67		// this gets the bitvector!
68	12	BitVector bvValue = value.getConst<BitVector>();
69	6	unsigned int bvSize = bvValue.getSize();
70
71		// lowerbound
72	6	BitVector lowerBound = ((this->d_isSigned) ? (BitVector::mkMinSigned(bvSize))
73	12	: (BitVector::mkZero(bvSize)));
74		// upperbound must be a satisfying value
75		// and value == upperbound
76	12	BitVector upperBound = bvValue;
77
78	6	Kind LTOperator =
79	6	((d_isSigned) ? (kind::BITVECTOR_SLT) : (kind::BITVECTOR_ULT));
80	6	Kind GEOperator =
81	6	((d_isSigned) ? (kind::BITVECTOR_SGE) : (kind::BITVECTOR_UGE));
82
83		// the pivot value for binary search,
84		// pivot = (lowerBound + upperBound) / 2
85		// rounded towards -infinity
86	12	BitVector pivot;
87	206	while ((d_isSigned && lowerBound.signedLessThan(upperBound))
88	206	\|\| (!d_isSigned && lowerBound.unsignedLessThan(upperBound)))
89		{
90	100	pivot = computeAverage(lowerBound, upperBound, d_isSigned);
91	100	optChecker->push();
92	100	if (lowerBound == pivot)
93		{
94	4	optChecker->assertFormula(
95	8	nm->mkNode(kind::EQUAL, target, nm->mkConst(lowerBound)));
96		}
97		else
98		{
99		// lowerBound <= target < pivot
100	96	optChecker->assertFormula(
101	384	nm->mkNode(kind::AND,
102	192	nm->mkNode(GEOperator, target, nm->mkConst(lowerBound)),
103	192	nm->mkNode(LTOperator, target, nm->mkConst(pivot))));
104		}
105	100	intermediateSatResult = optChecker->checkSat();
106	100	if (intermediateSatResult.isUnknown() \|\| intermediateSatResult.isNull())
107		{
108		return OptimizationResult(OptimizationResult::UNKNOWN, value);
109		}
110	100	if (intermediateSatResult.isSat() == Result::SAT)
111		{
112	32	value = optChecker->getValue(target);
113	32	upperBound = value.getConst<BitVector>();
114		}
115	68	else if (intermediateSatResult.isSat() == Result::UNSAT)
116		{
117	68	if (lowerBound == pivot)
118		{
119		// lowerBound == pivot ==> upperbound = lowerbound + 1
120		// and lowerbound <= target < upperbound is UNSAT
121		// return the upperbound
122	2	return OptimizationResult(OptimizationResult::OPTIMAL, value);
123		}
124		else
125		{
126	66	lowerBound = pivot;
127		}
128		}
129		else
130		{
131		return OptimizationResult(OptimizationResult::UNKNOWN, value);
132		}
133	98	optChecker->pop();
134		}
135	4	return OptimizationResult(OptimizationResult::OPTIMAL, value);
136		}
137
138	4	OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
139		TNode target)
140		{
141		// the smt engine to which we send intermediate queries
142		// for the binary search.
143	4	NodeManager* nm = optChecker->getNodeManager();
144	8	Result intermediateSatResult = optChecker->checkSat();
145		// Model-value of objective (used in optimization loop)
146	8	Node value;
147	4	if (intermediateSatResult.isUnknown())
148		{
149		return OptimizationResult(OptimizationResult::UNKNOWN, value);
150		}
151	4	if (intermediateSatResult.isSat() == Result::UNSAT)
152		{
153		return OptimizationResult(OptimizationResult::UNSAT, value);
154		}
155
156		// value equals to upperBound
157	4	value = optChecker->getValue(target);
158
159		// this gets the bitvector!
160	8	BitVector bvValue = value.getConst<BitVector>();
161	4	unsigned int bvSize = bvValue.getSize();
162
163		// lowerbound must be a satisfying value
164		// and value == lowerbound
165	8	BitVector lowerBound = bvValue;
166
167		// upperbound
168	4	BitVector upperBound = ((this->d_isSigned) ? (BitVector::mkMaxSigned(bvSize))
169	8	: (BitVector::mkOnes(bvSize)));
170
171	4	Kind LEOperator =
172	4	((d_isSigned) ? (kind::BITVECTOR_SLE) : (kind::BITVECTOR_ULE));
173	4	Kind GTOperator =
174	4	((d_isSigned) ? (kind::BITVECTOR_SGT) : (kind::BITVECTOR_UGT));
175
176		// the pivot value for binary search,
177		// pivot = (lowerBound + upperBound) / 2
178		// rounded towards -infinity
179	8	BitVector pivot;
180	314	while ((d_isSigned && lowerBound.signedLessThan(upperBound))
181	194	\|\| (!d_isSigned && lowerBound.unsignedLessThan(upperBound)))
182		{
183	126	pivot = computeAverage(lowerBound, upperBound, d_isSigned);
184
185	126	optChecker->push();
186		// notice that we don't have boundary condition here
187		// because lowerBound == pivot / lowerBound == upperBound + 1 is also
188		// covered
189		// pivot < target <= upperBound
190	126	optChecker->assertFormula(
191	504	nm->mkNode(kind::AND,
192	252	nm->mkNode(GTOperator, target, nm->mkConst(pivot)),
193	252	nm->mkNode(LEOperator, target, nm->mkConst(upperBound))));
194	126	intermediateSatResult = optChecker->checkSat();
195	126	if (intermediateSatResult.isUnknown() \|\| intermediateSatResult.isNull())
196		{
197		return OptimizationResult(OptimizationResult::UNKNOWN, value);
198		}
199	126	if (intermediateSatResult.isSat() == Result::SAT)
200		{
201	6	value = optChecker->getValue(target);
202	6	lowerBound = value.getConst<BitVector>();
203		}
204	120	else if (intermediateSatResult.isSat() == Result::UNSAT)
205		{
206	120	if (lowerBound == pivot)
207		{
208		// upperbound = lowerbound + 1
209		// and lowerbound < target <= upperbound is UNSAT
210		// return the lowerbound
211	2	return OptimizationResult(OptimizationResult::OPTIMAL, value);
212		}
213		else
214		{
215	118	upperBound = pivot;
216		}
217		}
218		else
219		{
220		return OptimizationResult(OptimizationResult::UNKNOWN, value);
221		}
222	124	optChecker->pop();
223		}
224	2	return OptimizationResult(OptimizationResult::OPTIMAL, value);
225		}
226
227	27735	} // namespace cvc5::omt