Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quant_bound_inference.cpp	Lines:	52	52	100.0 %
Date:	2021-09-29	Branches:	81	142	57.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * 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 quantifiers bound inference.
 */

#include "theory/quantifiers/quant_bound_inference.h"

#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/rewriter.h"
#include "util/rational.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
                                                     bool isFmf)
    : d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
{
}

void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }

bool QuantifiersBoundInference::mayComplete(TypeNode tn)
{
  std::unordered_map<TypeNode, bool>::iterator it = d_may_complete.find(tn);
  if (it == d_may_complete.end())
  {
    // cache
    bool mc = mayComplete(tn, d_cardMax);
    d_may_complete[tn] = mc;
    return mc;
  }
  return it->second;
}

bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
{
  if (!tn.isClosedEnumerable())
  {
    return false;
  }
  bool mc = false;
  // we cannot use FMF to complete interpreted types, thus we pass
  // false for fmfEnabled here
  if (isCardinalityClassFinite(tn.getCardinalityClass(), false))
  {
    Cardinality c = tn.getCardinality();
    if (!c.isLargeFinite())
    {
      NodeManager* nm = NodeManager::currentNM();
      Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
      // check if less than fixed upper bound
      Node oth = nm->mkConst(Rational(maxCard));
      Node eq = nm->mkNode(LEQ, card, oth);
      eq = Rewriter::rewrite(eq);
      mc = eq.isConst() && eq.getConst<bool>();
    }
  }
  return mc;
}

bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
{
  if (d_bint && d_bint->isBound(q, v))
  {
    return true;
  }
  TypeNode tn = v.getType();
  if (tn.isSort() && d_isFmf)
  {
    return true;
  }
  else if (mayComplete(tn))
  {
    return true;
  }
  return false;
}

BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
{
  if (d_bint)
  {
    return d_bint->getBoundVarType(q, v);
  }
  return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
}

void QuantifiersBoundInference::getBoundVarIndices(
    Node q, std::vector<unsigned>& indices) const
{
  Assert(indices.empty());
  // we take the bounded variables first
  if (d_bint)
  {
    d_bint->getBoundVarIndices(q, indices);
  }
  // then get the remaining ones
  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
  {
    if (std::find(indices.begin(), indices.end(), i) == indices.end())
    {
      indices.push_back(i);
    }
  }
}

bool QuantifiersBoundInference::getBoundElements(
    RepSetIterator* rsi,
    bool initial,
    Node q,
    Node v,
    std::vector<Node>& elements) const
{
  if (d_bint)
  {
    return d_bint->getBoundElements(rsi, initial, q, v, elements);
  }
  return false;
}

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


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
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 quantifiers bound inference.
14		*/
15
16		#include "theory/quantifiers/quant_bound_inference.h"
17
18		#include "theory/quantifiers/fmf/bounded_integers.h"
19		#include "theory/rewriter.h"
20		#include "util/rational.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28	6271	QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
29	6271	bool isFmf)
30	6271	: d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
31		{
32	6271	}
33
34	4762	void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }
35
36	6861	bool QuantifiersBoundInference::mayComplete(TypeNode tn)
37		{
38	6861	std::unordered_map<TypeNode, bool>::iterator it = d_may_complete.find(tn);
39	6861	if (it == d_may_complete.end())
40		{
41		// cache
42	273	bool mc = mayComplete(tn, d_cardMax);
43	273	d_may_complete[tn] = mc;
44	273	return mc;
45		}
46	6588	return it->second;
47		}
48
49	273	bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
50		{
51	273	if (!tn.isClosedEnumerable())
52		{
53	71	return false;
54		}
55	202	bool mc = false;
56		// we cannot use FMF to complete interpreted types, thus we pass
57		// false for fmfEnabled here
58	202	if (isCardinalityClassFinite(tn.getCardinalityClass(), false))
59		{
60	48	Cardinality c = tn.getCardinality();
61	24	if (!c.isLargeFinite())
62		{
63	23	NodeManager* nm = NodeManager::currentNM();
64	46	Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
65		// check if less than fixed upper bound
66	46	Node oth = nm->mkConst(Rational(maxCard));
67	46	Node eq = nm->mkNode(LEQ, card, oth);
68	23	eq = Rewriter::rewrite(eq);
69	23	mc = eq.isConst() && eq.getConst<bool>();
70		}
71		}
72	202	return mc;
73		}
74
75	2718	bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
76		{
77	2718	if (d_bint && d_bint->isBound(q, v))
78		{
79	72	return true;
80		}
81	5292	TypeNode tn = v.getType();
82	2646	if (tn.isSort() && d_isFmf)
83		{
84	1069	return true;
85		}
86	1577	else if (mayComplete(tn))
87		{
88	73	return true;
89		}
90	1504	return false;
91		}
92
93	5264	BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
94		{
95	5264	if (d_bint)
96		{
97	4143	return d_bint->getBoundVarType(q, v);
98		}
99	1121	return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
100		}
101
102	4803	void QuantifiersBoundInference::getBoundVarIndices(
103		Node q, std::vector<unsigned>& indices) const
104		{
105	4803	Assert(indices.empty());
106		// we take the bounded variables first
107	4803	if (d_bint)
108		{
109	4114	d_bint->getBoundVarIndices(q, indices);
110		}
111		// then get the remaining ones
112	11500	for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
113		{
114	6697	if (std::find(indices.begin(), indices.end(), i) == indices.end())
115		{
116	1369	indices.push_back(i);
117		}
118		}
119	4803	}
120
121	2667	bool QuantifiersBoundInference::getBoundElements(
122		RepSetIterator* rsi,
123		bool initial,
124		Node q,
125		Node v,
126		std::vector<Node>& elements) const
127		{
128	2667	if (d_bint)
129		{
130	2655	return d_bint->getBoundElements(rsi, initial, q, v, elements);
131		}
132	12	return false;
133		}
134
135		} // namespace quantifiers
136		} // namespace theory
137	22746	} // namespace cvc5