Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/theory_uf_type_rules.cpp	Lines:	77	113	68.1 %
Date:	2021-11-07	Branches:	151	478	31.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Typing and cardinality rules for the theory of UF.
 */

#include "theory/uf/theory_uf_type_rules.h"

#include <climits>
#include <sstream>

#include "expr/cardinality_constraint.h"
#include "theory/uf/function_const.h"
#include "util/cardinality.h"
#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace uf {

TypeNode UfTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check)
{
  TNode f = n.getOperator();
  TypeNode fType = f.getType(check);
  if (!fType.isFunction())
  {
    throw TypeCheckingExceptionPrivate(n,
                                       "operator does not have function type");
  }
  if (check)
  {
    if (n.getNumChildren() != fType.getNumChildren() - 1)
    {
      throw TypeCheckingExceptionPrivate(
          n, "number of arguments does not match the function type");
    }
    TNode::iterator argument_it = n.begin();
    TNode::iterator argument_it_end = n.end();
    TypeNode::iterator argument_type_it = fType.begin();
    for (; argument_it != argument_it_end; ++argument_it, ++argument_type_it)
    {
      TypeNode currentArgument = (*argument_it).getType();
      TypeNode currentArgumentType = *argument_type_it;
      if (!currentArgument.isSubtypeOf(currentArgumentType))
      {
        std::stringstream ss;
        ss << "argument type is not a subtype of the function's argument "
           << "type:\n"
           << "argument:  " << *argument_it << "\n"
           << "has type:  " << (*argument_it).getType() << "\n"
           << "not subtype: " << *argument_type_it << "\n"
           << "in term : " << n;
        throw TypeCheckingExceptionPrivate(n, ss.str());
      }
    }
  }
  return fType.getRangeType();
}

TypeNode CardinalityConstraintOpTypeRule::computeType(NodeManager* nodeManager,
                                                      TNode n,
                                                      bool check)
{
  if (check)
  {
    const CardinalityConstraint& cc = n.getConst<CardinalityConstraint>();
    if (!cc.getType().isSort())
    {
      throw TypeCheckingExceptionPrivate(
          n, "cardinality constraint must apply to uninterpreted sort");
    }
    if (cc.getUpperBound().sgn() != 1)
    {
      throw TypeCheckingExceptionPrivate(
          n, "cardinality constraint must be positive");
    }
  }
  return nodeManager->booleanType();
}

TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager,
                                                    TNode n,
                                                    bool check)
{
  return nodeManager->booleanType();
}

TypeNode CombinedCardinalityConstraintOpTypeRule::computeType(
    NodeManager* nodeManager, TNode n, bool check)
{
  if (check)
  {
    const CombinedCardinalityConstraint& cc =
        n.getConst<CombinedCardinalityConstraint>();
    if (cc.getUpperBound().sgn() != 1)
    {
      throw TypeCheckingExceptionPrivate(
          n, "combined cardinality constraint must be positive");
    }
  }
  return nodeManager->booleanType();
}

TypeNode CombinedCardinalityConstraintTypeRule::computeType(
    NodeManager* nodeManager, TNode n, bool check)
{
  return nodeManager->booleanType();
}

TypeNode PartialTypeRule::computeType(NodeManager* nodeManager,
                                      TNode n,
                                      bool check)
{
  return n.getOperator().getType().getRangeType();
}

TypeNode HoApplyTypeRule::computeType(NodeManager* nodeManager,
                                      TNode n,
                                      bool check)
{
  Assert(n.getKind() == kind::HO_APPLY);
  TypeNode fType = n[0].getType(check);
  if (!fType.isFunction())
  {
    throw TypeCheckingExceptionPrivate(
        n, "first argument does not have function type");
  }
  Assert(fType.getNumChildren() >= 2);
  if (check)
  {
    TypeNode aType = n[1].getType(check);
    if (!aType.isSubtypeOf(fType[0]))
    {
      throw TypeCheckingExceptionPrivate(
          n, "argument does not match function type");
    }
  }
  if (fType.getNumChildren() == 2)
  {
    return fType.getRangeType();
  }
  else
  {
    std::vector<TypeNode> children;
    TypeNode::iterator argument_type_it = fType.begin();
    TypeNode::iterator argument_type_it_end = fType.end();
    ++argument_type_it;
    for (; argument_type_it != argument_type_it_end; ++argument_type_it)
    {
      children.push_back(*argument_type_it);
    }
    return nodeManager->mkFunctionType(children);
  }
}

TypeNode LambdaTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  if (n[0].getType(check) != nodeManager->boundVarListType())
  {
    std::stringstream ss;
    ss << "expected a bound var list for LAMBDA expression, got `"
       << n[0].getType().toString() << "'";
    throw TypeCheckingExceptionPrivate(n, ss.str());
  }
  std::vector<TypeNode> argTypes;
  for (TNode::iterator i = n[0].begin(); i != n[0].end(); ++i)
  {
    argTypes.push_back((*i).getType());
  }
  TypeNode rangeType = n[1].getType(check);
  return nodeManager->mkFunctionType(argTypes, rangeType);
}

bool LambdaTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
{
  Assert(n.getKind() == kind::LAMBDA);
  // get array representation of this function, if possible
  Node na = FunctionConst::getArrayRepresentationForLambda(n);
  if (!na.isNull())
  {
    Assert(na.getType().isArray());
    Trace("lambda-const") << "Array representation for " << n << " is " << na
                          << " " << na.getType() << std::endl;
    // must have the standard bound variable list
    Node bvl =
        NodeManager::currentNM()->getBoundVarListForFunctionType(n.getType());
    if (bvl == n[0])
    {
      // array must be constant
      if (na.isConst())
      {
        Trace("lambda-const") << "*** Constant lambda : " << n;
        Trace("lambda-const") << " since its array representation : " << na
                              << " is constant." << std::endl;
        return true;
      }
      else
      {
        Trace("lambda-const") << "Non-constant lambda : " << n
                              << " since array is not constant." << std::endl;
      }
    }
    else
    {
      Trace("lambda-const")
          << "Non-constant lambda : " << n
          << " since its varlist is not standard." << std::endl;
      Trace("lambda-const") << "  standard : " << bvl << std::endl;
      Trace("lambda-const") << "   current : " << n[0] << std::endl;
    }
  }
  else
  {
    Trace("lambda-const") << "Non-constant lambda : " << n
                          << " since it has no array representation."
                          << std::endl;
  }
  return false;
}

Cardinality FunctionProperties::computeCardinality(TypeNode type)
{
  // Don't assert this; allow other theories to use this cardinality
  // computation.
  //
  // Assert(type.getKind() == kind::FUNCTION_TYPE);

  Cardinality argsCard(1);
  // get the largest cardinality of function arguments/return type
  for (size_t i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i)
  {
    argsCard *= type[i].getCardinality();
  }

  Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality();

  return valueCard ^ argsCard;
}

bool FunctionProperties::isWellFounded(TypeNode type)
{
  for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end; ++i)
  {
    if (!(*i).isWellFounded())
    {
      return false;
    }
  }
  return true;
}

Node FunctionProperties::mkGroundTerm(TypeNode type)
{
  NodeManager* nm = NodeManager::currentNM();
  Node bvl = nm->getBoundVarListForFunctionType(type);
  Node ret = type.getRangeType().mkGroundTerm();
  return nm->mkNode(kind::LAMBDA, bvl, ret);
}

}  // namespace uf
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, Morgan Deters
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		* Typing and cardinality rules for the theory of UF.
14		*/
15
16		#include "theory/uf/theory_uf_type_rules.h"
17
18		#include <climits>
19		#include <sstream>
20
21		#include "expr/cardinality_constraint.h"
22		#include "theory/uf/function_const.h"
23		#include "util/cardinality.h"
24		#include "util/rational.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace uf {
29
30	480369	TypeNode UfTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check)
31		{
32	960738	TNode f = n.getOperator();
33	960738	TypeNode fType = f.getType(check);
34	480369	if (!fType.isFunction())
35		{
36		throw TypeCheckingExceptionPrivate(n,
37		"operator does not have function type");
38		}
39	480369	if (check)
40		{
41	480369	if (n.getNumChildren() != fType.getNumChildren() - 1)
42		{
43		throw TypeCheckingExceptionPrivate(
44		n, "number of arguments does not match the function type");
45		}
46	480369	TNode::iterator argument_it = n.begin();
47	480369	TNode::iterator argument_it_end = n.end();
48	480369	TypeNode::iterator argument_type_it = fType.begin();
49	14474803	for (; argument_it != argument_it_end; ++argument_it, ++argument_type_it)
50		{
51	13994434	TypeNode currentArgument = (*argument_it).getType();
52	13994434	TypeNode currentArgumentType = *argument_type_it;
53	6997217	if (!currentArgument.isSubtypeOf(currentArgumentType))
54		{
55		std::stringstream ss;
56		ss << "argument type is not a subtype of the function's argument "
57		<< "type:\n"
58		<< "argument: " << *argument_it << "\n"
59		<< "has type: " << (*argument_it).getType() << "\n"
60		<< "not subtype: " << *argument_type_it << "\n"
61		<< "in term : " << n;
62		throw TypeCheckingExceptionPrivate(n, ss.str());
63		}
64		}
65		}
66	960738	return fType.getRangeType();
67		}
68
69		TypeNode CardinalityConstraintOpTypeRule::computeType(NodeManager* nodeManager,
70		TNode n,
71		bool check)
72		{
73		if (check)
74		{
75		const CardinalityConstraint& cc = n.getConst<CardinalityConstraint>();
76		if (!cc.getType().isSort())
77		{
78		throw TypeCheckingExceptionPrivate(
79		n, "cardinality constraint must apply to uninterpreted sort");
80		}
81		if (cc.getUpperBound().sgn() != 1)
82		{
83		throw TypeCheckingExceptionPrivate(
84		n, "cardinality constraint must be positive");
85		}
86		}
87		return nodeManager->booleanType();
88		}
89
90	909	TypeNode CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager,
91		TNode n,
92		bool check)
93		{
94	909	return nodeManager->booleanType();
95		}
96
97		TypeNode CombinedCardinalityConstraintOpTypeRule::computeType(
98		NodeManager* nodeManager, TNode n, bool check)
99		{
100		if (check)
101		{
102		const CombinedCardinalityConstraint& cc =
103		n.getConst<CombinedCardinalityConstraint>();
104		if (cc.getUpperBound().sgn() != 1)
105		{
106		throw TypeCheckingExceptionPrivate(
107		n, "combined cardinality constraint must be positive");
108		}
109		}
110		return nodeManager->booleanType();
111		}
112
113	641	TypeNode CombinedCardinalityConstraintTypeRule::computeType(
114		NodeManager* nodeManager, TNode n, bool check)
115		{
116	641	return nodeManager->booleanType();
117		}
118
119		TypeNode PartialTypeRule::computeType(NodeManager* nodeManager,
120		TNode n,
121		bool check)
122		{
123		return n.getOperator().getType().getRangeType();
124		}
125
126	13099	TypeNode HoApplyTypeRule::computeType(NodeManager* nodeManager,
127		TNode n,
128		bool check)
129		{
130	13099	Assert(n.getKind() == kind::HO_APPLY);
131	26198	TypeNode fType = n[0].getType(check);
132	13099	if (!fType.isFunction())
133		{
134		throw TypeCheckingExceptionPrivate(
135		n, "first argument does not have function type");
136		}
137	13099	Assert(fType.getNumChildren() >= 2);
138	13099	if (check)
139		{
140	26198	TypeNode aType = n[1].getType(check);
141	13099	if (!aType.isSubtypeOf(fType[0]))
142		{
143		throw TypeCheckingExceptionPrivate(
144		n, "argument does not match function type");
145		}
146		}
147	13099	if (fType.getNumChildren() == 2)
148		{
149	5969	return fType.getRangeType();
150		}
151		else
152		{
153	14260	std::vector<TypeNode> children;
154	7130	TypeNode::iterator argument_type_it = fType.begin();
155	7130	TypeNode::iterator argument_type_it_end = fType.end();
156	7130	++argument_type_it;
157	39540	for (; argument_type_it != argument_type_it_end; ++argument_type_it)
158		{
159	16205	children.push_back(*argument_type_it);
160		}
161	7130	return nodeManager->mkFunctionType(children);
162		}
163		}
164
165	20905	TypeNode LambdaTypeRule::computeType(NodeManager* nodeManager,
166		TNode n,
167		bool check)
168		{
169	20905	if (n[0].getType(check) != nodeManager->boundVarListType())
170		{
171		std::stringstream ss;
172		ss << "expected a bound var list for LAMBDA expression, got `"
173		<< n[0].getType().toString() << "'";
174		throw TypeCheckingExceptionPrivate(n, ss.str());
175		}
176	41810	std::vector<TypeNode> argTypes;
177	88806	for (TNode::iterator i = n[0].begin(); i != n[0].end(); ++i)
178		{
179	67901	argTypes.push_back((*i).getType());
180		}
181	41810	TypeNode rangeType = n[1].getType(check);
182	41810	return nodeManager->mkFunctionType(argTypes, rangeType);
183		}
184
185	2021	bool LambdaTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
186		{
187	2021	Assert(n.getKind() == kind::LAMBDA);
188		// get array representation of this function, if possible
189	4042	Node na = FunctionConst::getArrayRepresentationForLambda(n);
190	2021	if (!na.isNull())
191		{
192	567	Assert(na.getType().isArray());
193	1134	Trace("lambda-const") << "Array representation for " << n << " is " << na
194	567	<< " " << na.getType() << std::endl;
195		// must have the standard bound variable list
196		Node bvl =
197	737	NodeManager::currentNM()->getBoundVarListForFunctionType(n.getType());
198	567	if (bvl == n[0])
199		{
200		// array must be constant
201	397	if (na.isConst())
202		{
203	397	Trace("lambda-const") << "*** Constant lambda : " << n;
204	794	Trace("lambda-const") << " since its array representation : " << na
205	397	<< " is constant." << std::endl;
206	397	return true;
207		}
208		else
209		{
210		Trace("lambda-const") << "Non-constant lambda : " << n
211		<< " since array is not constant." << std::endl;
212		}
213		}
214		else
215		{
216	340	Trace("lambda-const")
217	170	<< "Non-constant lambda : " << n
218	170	<< " since its varlist is not standard." << std::endl;
219	170	Trace("lambda-const") << " standard : " << bvl << std::endl;
220	170	Trace("lambda-const") << " current : " << n[0] << std::endl;
221		}
222		}
223		else
224		{
225	2908	Trace("lambda-const") << "Non-constant lambda : " << n
226	1454	<< " since it has no array representation."
227	1454	<< std::endl;
228		}
229	1624	return false;
230		}
231
232	156	Cardinality FunctionProperties::computeCardinality(TypeNode type)
233		{
234		// Don't assert this; allow other theories to use this cardinality
235		// computation.
236		//
237		// Assert(type.getKind() == kind::FUNCTION_TYPE);
238
239	312	Cardinality argsCard(1);
240		// get the largest cardinality of function arguments/return type
241	402	for (size_t i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i)
242		{
243	246	argsCard *= type[i].getCardinality();
244		}
245
246	312	Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality();
247
248	312	return valueCard ^ argsCard;
249		}
250
251		bool FunctionProperties::isWellFounded(TypeNode type)
252		{
253		for (TypeNode::iterator i = type.begin(), i_end = type.end(); i != i_end; ++i)
254		{
255		if (!(*i).isWellFounded())
256		{
257		return false;
258		}
259		}
260		return true;
261		}
262
263	2	Node FunctionProperties::mkGroundTerm(TypeNode type)
264		{
265	2	NodeManager* nm = NodeManager::currentNM();
266	4	Node bvl = nm->getBoundVarListForFunctionType(type);
267	4	Node ret = type.getRangeType().mkGroundTerm();
268	4	return nm->mkNode(kind::LAMBDA, bvl, ret);
269		}
270
271		} // namespace uf
272		} // namespace theory
273	31137	} // namespace cvc5