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-19	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"

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
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26
27	9942	QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
28	9942	bool isFmf)
29	9942	: d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
30		{
31	9942	}
32
33	6839	void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }
34
35	10385	bool QuantifiersBoundInference::mayComplete(TypeNode tn)
36		{
37	10385	std::unordered_map<TypeNode, bool>::iterator it = d_may_complete.find(tn);
38	10385	if (it == d_may_complete.end())
39		{
40		// cache
41	514	bool mc = mayComplete(tn, d_cardMax);
42	514	d_may_complete[tn] = mc;
43	514	return mc;
44		}
45	9871	return it->second;
46		}
47
48	514	bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
49		{
50	514	if (!tn.isClosedEnumerable())
51		{
52	200	return false;
53		}
54	314	bool mc = false;
55		// we cannot use FMF to complete interpreted types, thus we pass
56		// false for fmfEnabled here
57	314	if (isCardinalityClassFinite(tn.getCardinalityClass(), false))
58		{
59	84	Cardinality c = tn.getCardinality();
60	42	if (!c.isLargeFinite())
61		{
62	38	NodeManager* nm = NodeManager::currentNM();
63	76	Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
64		// check if less than fixed upper bound
65	76	Node oth = nm->mkConst(Rational(maxCard));
66	76	Node eq = nm->mkNode(LEQ, card, oth);
67	38	eq = Rewriter::rewrite(eq);
68	38	mc = eq.isConst() && eq.getConst<bool>();
69		}
70		}
71	314	return mc;
72		}
73
74	5989	bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
75		{
76	5989	if (d_bint && d_bint->isBound(q, v))
77		{
78	88	return true;
79		}
80	11802	TypeNode tn = v.getType();
81	5901	if (tn.isSort() && d_isFmf)
82		{
83	1310	return true;
84		}
85	4591	else if (mayComplete(tn))
86		{
87	79	return true;
88		}
89	4512	return false;
90		}
91
92	5734	BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
93		{
94	5734	if (d_bint)
95		{
96	4372	return d_bint->getBoundVarType(q, v);
97		}
98	1362	return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
99		}
100
101	5439	void QuantifiersBoundInference::getBoundVarIndices(
102		Node q, std::vector<unsigned>& indices) const
103		{
104	5439	Assert(indices.empty());
105		// we take the bounded variables first
106	5439	if (d_bint)
107		{
108	4475	d_bint->getBoundVarIndices(q, indices);
109		}
110		// then get the remaining ones
111	12929	for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
112		{
113	7490	if (std::find(indices.begin(), indices.end(), i) == indices.end())
114		{
115	1674	indices.push_back(i);
116		}
117		}
118	5439	}
119
120	2851	bool QuantifiersBoundInference::getBoundElements(
121		RepSetIterator* rsi,
122		bool initial,
123		Node q,
124		Node v,
125		std::vector<Node>& elements) const
126		{
127	2851	if (d_bint)
128		{
129	2839	return d_bint->getBoundElements(rsi, initial, q, v, elements);
130		}
131	12	return false;
132		}
133
134		} // namespace quantifiers
135		} // namespace theory
136	29577	} // namespace cvc5