Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp	Lines:	171	171	100.0 %
Date:	2021-08-06	Branches:	445	1064	41.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Aina Niemetz, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of ceg_bv_instantiator.
 */

#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"

#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {
namespace utils {

Node getPvCoeff(TNode pv, TNode n)
{
  bool neg = false;
  Node coeff;

  if (n.getKind() == BITVECTOR_NEG)
  {
    neg = true;
    n = n[0];
  }

  if (n == pv)
  {
    coeff = bv::utils::mkOne(bv::utils::getSize(pv));
  }
  /* All multiplications are normalized to pv * (t1 * t2). */
  else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute()))
  {
    Assert(n.getNumChildren() == 2);
    Assert(n[0] == pv);
    coeff = n[1];
  }
  else /* n is in no form to extract the coefficient for pv */
  {
    Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in "
                         << n << std::endl;
    return Node::null();
  }
  Assert(!coeff.isNull());

  if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff);
  return coeff;
}

Node normalizePvMult(TNode pv,
                     const std::vector<Node>& children,
                     std::unordered_map<Node, bool>& contains_pv)
{
  bool neg, neg_coeff = false;
  bool found_pv = false;
  NodeManager* nm;
  NodeBuilder nb(BITVECTOR_MULT);
  BvLinearAttribute is_linear;

  nm = NodeManager::currentNM();
  for (TNode nc : children)
  {
    if (!contains_pv[nc])
    {
      nb << nc;
      continue;
    }

    neg = false;
    if (nc.getKind() == BITVECTOR_NEG)
    {
      neg = true;
      nc = nc[0];
    }

    if (!found_pv && nc == pv)
    {
      found_pv = true;
      neg_coeff = neg;
      continue;
    }
    else if (!found_pv && nc.getKind() == BITVECTOR_MULT
             && nc.getAttribute(is_linear))
    {
      Assert(nc.getNumChildren() == 2);
      Assert(nc[0] == pv);
      Assert(!contains_pv[nc[1]]);
      found_pv = true;
      neg_coeff = neg;
      nb << nc[1];
      continue;
    }
    return Node::null(); /* non-linear */
  }
  Assert(nb.getNumChildren() > 0);

  Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode();
  if (neg_coeff)
  {
    coeff = nm->mkNode(BITVECTOR_NEG, coeff);
  }
  coeff = Rewriter::rewrite(coeff);
  unsigned size_coeff = bv::utils::getSize(coeff);
  Node zero = bv::utils::mkZero(size_coeff);
  if (coeff == zero)
  {
    return zero;
  }
  Node result;
  if (found_pv)
  {
    if (coeff == bv::utils::mkOne(size_coeff))
    {
      return pv;
    }
    result = nm->mkNode(BITVECTOR_MULT, pv, coeff);
    contains_pv[result] = true;
    result.setAttribute(is_linear, true);
  }
  else
  {
    result = coeff;
  }
  return result;
}

#ifdef CVC5_ASSERTIONS
namespace {
bool isLinearPlus(TNode n,
                  TNode pv,
                  std::unordered_map<Node, bool>& contains_pv)
{
  Node coeff;
  Assert(n.getAttribute(BvLinearAttribute()));
  Assert(n.getNumChildren() == 2);
  if (n[0] != pv)
  {
    Assert(n[0].getKind() == BITVECTOR_MULT);
    Assert(n[0].getNumChildren() == 2);
    Assert(n[0][0] == pv);
    Assert(!contains_pv[n[0][1]]);
  }
  Assert(!contains_pv[n[1]]);
  coeff = utils::getPvCoeff(pv, n[0]);
  Assert(!coeff.isNull());
  Assert(!contains_pv[coeff]);
  return true;
}
}  // namespace
#endif

Node normalizePvPlus(Node pv,
                     const std::vector<Node>& children,
                     std::unordered_map<Node, bool>& contains_pv)
{
  NodeManager* nm;
  NodeBuilder nb_c(BITVECTOR_ADD);
  NodeBuilder nb_l(BITVECTOR_ADD);
  BvLinearAttribute is_linear;
  bool neg;

  nm = NodeManager::currentNM();
  for (TNode nc : children)
  {
    if (!contains_pv[nc])
    {
      nb_l << nc;
      continue;
    }

    neg = false;
    if (nc.getKind() == BITVECTOR_NEG)
    {
      neg = true;
      nc = nc[0];
    }

    if (nc == pv
        || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
    {
      Node coeff = utils::getPvCoeff(pv, nc);
      Assert(!coeff.isNull());
      if (neg)
      {
        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
      }
      nb_c << coeff;
      continue;
    }
    else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear))
    {
      Assert(isLinearPlus(nc, pv, contains_pv));
      Node coeff = utils::getPvCoeff(pv, nc[0]);
      Assert(!coeff.isNull());
      Node leaf = nc[1];
      if (neg)
      {
        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
        leaf = nm->mkNode(BITVECTOR_NEG, leaf);
      }
      nb_c << coeff;
      nb_l << leaf;
      continue;
    }
    /* can't collect coefficients of 'pv' in 'cur' -> non-linear */
    return Node::null();
  }
  Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0);

  Node pv_mult_coeffs, result;
  if (nb_c.getNumChildren() > 0)
  {
    Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
    coeffs = Rewriter::rewrite(coeffs);
    result = pv_mult_coeffs =
        utils::normalizePvMult(pv, {pv, coeffs}, contains_pv);
  }

  if (nb_l.getNumChildren() > 0)
  {
    Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
    leafs = Rewriter::rewrite(leafs);
    Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
    /* pv * 0 + t --> t */
    if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero)
    {
      result = leafs;
    }
    else
    {
      result = nm->mkNode(BITVECTOR_ADD, pv_mult_coeffs, leafs);
      contains_pv[result] = true;
      result.setAttribute(is_linear, true);
    }
  }
  Assert(!result.isNull());
  return result;
}

Node normalizePvEqual(Node pv,
                      const std::vector<Node>& children,
                      std::unordered_map<Node, bool>& contains_pv)
{
  Assert(children.size() == 2);

  NodeManager* nm = NodeManager::currentNM();
  BvLinearAttribute is_linear;
  Node coeffs[2], leafs[2];
  bool neg;
  TNode child;

  for (unsigned i = 0; i < 2; ++i)
  {
    child = children[i];
    neg = false;
    if (child.getKind() == BITVECTOR_NEG)
    {
      neg = true;
      child = child[0];
    }
    if (child.getAttribute(is_linear) || child == pv)
    {
      if (child.getKind() == BITVECTOR_ADD)
      {
        Assert(isLinearPlus(child, pv, contains_pv));
        coeffs[i] = utils::getPvCoeff(pv, child[0]);
        leafs[i] = child[1];
      }
      else
      {
        Assert(child.getKind() == BITVECTOR_MULT || child == pv);
        coeffs[i] = utils::getPvCoeff(pv, child);
      }
    }
    if (neg)
    {
      if (!coeffs[i].isNull())
      {
        coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]);
      }
      if (!leafs[i].isNull())
      {
        leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]);
      }
    }
  }

  if (coeffs[0].isNull() || coeffs[1].isNull())
  {
    return Node::null();
  }

  Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
  coeff = Rewriter::rewrite(coeff);
  std::vector<Node> mult_children = {pv, coeff};
  Node lhs = utils::normalizePvMult(pv, mult_children, contains_pv);

  Node rhs;
  if (!leafs[0].isNull() && !leafs[1].isNull())
  {
    rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]);
  }
  else if (!leafs[0].isNull())
  {
    rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]);
  }
  else if (!leafs[1].isNull())
  {
    rhs = leafs[1];
  }
  else
  {
    rhs = bv::utils::mkZero(bv::utils::getSize(pv));
  }
  rhs = Rewriter::rewrite(rhs);

  if (lhs == rhs)
  {
    return bv::utils::mkTrue();
  }

  Node result = lhs.eqNode(rhs);
  contains_pv[result] = true;
  return result;
}

}  // namespace utils
}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Aina Niemetz, Andres Noetzli
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		* Implementation of ceg_bv_instantiator.
14		*/
15
16		#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
17
18		#include "theory/bv/theory_bv_utils.h"
19		#include "theory/rewriter.h"
20
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26		namespace utils {
27
28	716	Node getPvCoeff(TNode pv, TNode n)
29		{
30	716	bool neg = false;
31	1432	Node coeff;
32
33	716	if (n.getKind() == BITVECTOR_NEG)
34		{
35	2	neg = true;
36	2	n = n[0];
37		}
38
39	716	if (n == pv)
40		{
41	610	coeff = bv::utils::mkOne(bv::utils::getSize(pv));
42		}
43		/* All multiplications are normalized to pv * (t1 * t2). */
44	106	else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute()))
45		{
46	104	Assert(n.getNumChildren() == 2);
47	104	Assert(n[0] == pv);
48	104	coeff = n[1];
49		}
50		else /* n is in no form to extract the coefficient for pv */
51		{
52	4	Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in "
53	2	<< n << std::endl;
54	2	return Node::null();
55		}
56	714	Assert(!coeff.isNull());
57
58	714	if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff);
59	712	return coeff;
60		}
61
62	952	Node normalizePvMult(TNode pv,
63		const std::vector<Node>& children,
64		std::unordered_map<Node, bool>& contains_pv)
65		{
66	952	bool neg, neg_coeff = false;
67	952	bool found_pv = false;
68		NodeManager* nm;
69	1904	NodeBuilder nb(BITVECTOR_MULT);
70		BvLinearAttribute is_linear;
71
72	952	nm = NodeManager::currentNM();
73	2822	for (TNode nc : children)
74		{
75	2860	if (!contains_pv[nc])
76		{
77	948	nb << nc;
78	948	continue;
79		}
80
81	964	neg = false;
82	964	if (nc.getKind() == BITVECTOR_NEG)
83		{
84	8	neg = true;
85	8	nc = nc[0];
86		}
87
88	1882	if (!found_pv && nc == pv)
89		{
90	918	found_pv = true;
91	918	neg_coeff = neg;
92	918	continue;
93		}
94	128	else if (!found_pv && nc.getKind() == BITVECTOR_MULT
95	50	&& nc.getAttribute(is_linear))
96		{
97	4	Assert(nc.getNumChildren() == 2);
98	4	Assert(nc[0] == pv);
99	4	Assert(!contains_pv[nc[1]]);
100	4	found_pv = true;
101	4	neg_coeff = neg;
102	4	nb << nc[1];
103	4	continue;
104		}
105	42	return Node::null(); /* non-linear */
106		}
107	910	Assert(nb.getNumChildren() > 0);
108
109	1820	Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode();
110	910	if (neg_coeff)
111		{
112	6	coeff = nm->mkNode(BITVECTOR_NEG, coeff);
113		}
114	910	coeff = Rewriter::rewrite(coeff);
115	910	unsigned size_coeff = bv::utils::getSize(coeff);
116	1820	Node zero = bv::utils::mkZero(size_coeff);
117	910	if (coeff == zero)
118		{
119	12	return zero;
120		}
121	1796	Node result;
122	898	if (found_pv)
123		{
124	896	if (coeff == bv::utils::mkOne(size_coeff))
125		{
126	532	return pv;
127		}
128	364	result = nm->mkNode(BITVECTOR_MULT, pv, coeff);
129	364	contains_pv[result] = true;
130	364	result.setAttribute(is_linear, true);
131		}
132		else
133		{
134	2	result = coeff;
135		}
136	366	return result;
137		}
138
139		#ifdef CVC5_ASSERTIONS
140		namespace {
141	28	bool isLinearPlus(TNode n,
142		TNode pv,
143		std::unordered_map<Node, bool>& contains_pv)
144		{
145	56	Node coeff;
146	28	Assert(n.getAttribute(BvLinearAttribute()));
147	28	Assert(n.getNumChildren() == 2);
148	28	if (n[0] != pv)
149		{
150	8	Assert(n[0].getKind() == BITVECTOR_MULT);
151	8	Assert(n[0].getNumChildren() == 2);
152	8	Assert(n[0][0] == pv);
153	8	Assert(!contains_pv[n[0][1]]);
154		}
155	28	Assert(!contains_pv[n[1]]);
156	28	coeff = utils::getPvCoeff(pv, n[0]);
157	28	Assert(!coeff.isNull());
158	28	Assert(!contains_pv[coeff]);
159	56	return true;
160		}
161		} // namespace
162		#endif
163
164	1377	Node normalizePvPlus(Node pv,
165		const std::vector<Node>& children,
166		std::unordered_map<Node, bool>& contains_pv)
167		{
168		NodeManager* nm;
169	2754	NodeBuilder nb_c(BITVECTOR_ADD);
170	2754	NodeBuilder nb_l(BITVECTOR_ADD);
171		BvLinearAttribute is_linear;
172		bool neg;
173
174	1377	nm = NodeManager::currentNM();
175	2703	for (TNode nc : children)
176		{
177	2783	if (!contains_pv[nc])
178		{
179	700	nb_l << nc;
180	700	continue;
181		}
182
183	1383	neg = false;
184	1383	if (nc.getKind() == BITVECTOR_NEG)
185		{
186	144	neg = true;
187	144	nc = nc[0];
188		}
189
190	2766	if (nc == pv
191	1383	\|\| (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
192		{
193	1228	Node coeff = utils::getPvCoeff(pv, nc);
194	614	Assert(!coeff.isNull());
195	614	if (neg)
196		{
197	32	coeff = nm->mkNode(BITVECTOR_NEG, coeff);
198		}
199	614	nb_c << coeff;
200	614	continue;
201		}
202	769	else if (nc.getKind() == BITVECTOR_ADD && nc.getAttribute(is_linear))
203		{
204	12	Assert(isLinearPlus(nc, pv, contains_pv));
205	24	Node coeff = utils::getPvCoeff(pv, nc[0]);
206	12	Assert(!coeff.isNull());
207	24	Node leaf = nc[1];
208	12	if (neg)
209		{
210	2	coeff = nm->mkNode(BITVECTOR_NEG, coeff);
211	2	leaf = nm->mkNode(BITVECTOR_NEG, leaf);
212		}
213	12	nb_c << coeff;
214	12	nb_l << leaf;
215	12	continue;
216		}
217		/* can't collect coefficients of 'pv' in 'cur' -> non-linear */
218	757	return Node::null();
219		}
220	620	Assert(nb_c.getNumChildren() > 0 \|\| nb_l.getNumChildren() > 0);
221
222	1240	Node pv_mult_coeffs, result;
223	620	if (nb_c.getNumChildren() > 0)
224		{
225	1236	Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
226	618	coeffs = Rewriter::rewrite(coeffs);
227	618	result = pv_mult_coeffs =
228	1236	utils::normalizePvMult(pv, {pv, coeffs}, contains_pv);
229		}
230
231	620	if (nb_l.getNumChildren() > 0)
232		{
233	1228	Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
234	614	leafs = Rewriter::rewrite(leafs);
235	1228	Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
236		/* pv * 0 + t --> t */
237	614	if (pv_mult_coeffs.isNull() \|\| pv_mult_coeffs == zero)
238		{
239	4	result = leafs;
240		}
241		else
242		{
243	610	result = nm->mkNode(BITVECTOR_ADD, pv_mult_coeffs, leafs);
244	610	contains_pv[result] = true;
245	610	result.setAttribute(is_linear, true);
246		}
247		}
248	620	Assert(!result.isNull());
249	620	return result;
250		}
251
252	33	Node normalizePvEqual(Node pv,
253		const std::vector<Node>& children,
254		std::unordered_map<Node, bool>& contains_pv)
255		{
256	33	Assert(children.size() == 2);
257
258	33	NodeManager* nm = NodeManager::currentNM();
259		BvLinearAttribute is_linear;
260	66	Node coeffs[2], leafs[2];
261		bool neg;
262	66	TNode child;
263
264	99	for (unsigned i = 0; i < 2; ++i)
265		{
266	66	child = children[i];
267	66	neg = false;
268	66	if (child.getKind() == BITVECTOR_NEG)
269		{
270	4	neg = true;
271	4	child = child[0];
272		}
273	66	if (child.getAttribute(is_linear) \|\| child == pv)
274		{
275	52	if (child.getKind() == BITVECTOR_ADD)
276		{
277	16	Assert(isLinearPlus(child, pv, contains_pv));
278	16	coeffs[i] = utils::getPvCoeff(pv, child[0]);
279	16	leafs[i] = child[1];
280		}
281		else
282		{
283	36	Assert(child.getKind() == BITVECTOR_MULT \|\| child == pv);
284	36	coeffs[i] = utils::getPvCoeff(pv, child);
285		}
286		}
287	66	if (neg)
288		{
289	4	if (!coeffs[i].isNull())
290		{
291	4	coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]);
292		}
293	4	if (!leafs[i].isNull())
294		{
295	2	leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]);
296		}
297		}
298		}
299
300	33	if (coeffs[0].isNull() \|\| coeffs[1].isNull())
301		{
302	11	return Node::null();
303		}
304
305	44	Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
306	22	coeff = Rewriter::rewrite(coeff);
307	44	std::vector<Node> mult_children = {pv, coeff};
308	44	Node lhs = utils::normalizePvMult(pv, mult_children, contains_pv);
309
310	44	Node rhs;
311	22	if (!leafs[0].isNull() && !leafs[1].isNull())
312		{
313	2	rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]);
314		}
315	20	else if (!leafs[0].isNull())
316		{
317	8	rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]);
318		}
319	12	else if (!leafs[1].isNull())
320		{
321	2	rhs = leafs[1];
322		}
323		else
324		{
325	10	rhs = bv::utils::mkZero(bv::utils::getSize(pv));
326		}
327	22	rhs = Rewriter::rewrite(rhs);
328
329	22	if (lhs == rhs)
330		{
331	2	return bv::utils::mkTrue();
332		}
333
334	40	Node result = lhs.eqNode(rhs);
335	20	contains_pv[result] = true;
336	20	return result;
337		}
338
339		} // namespace utils
340		} // namespace quantifiers
341		} // namespace theory
342	29322	} // namespace cvc5