Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/type_checker_util.h	Lines:	36	48	75.0 %
Date:	2021-08-01	Branches:	171	1552	11.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   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.
 * ****************************************************************************
 *
 * Templates for simple type rules
 *
 * This file defines templates for simple type rules. If a kind has the a
 * type rule where each argument matches exactly a specific sort, these
 * templates can be used to define typechecks without writing dedicated classes
 * for them.
 */

#include <sstream>

#include "cvc5_private.h"
#include "expr/kind.h"
#include "expr/node.h"
#include "expr/node_manager.h"
#include "expr/type_node.h"

namespace cvc5 {
namespace expr {

/** Type check returns the builtin operator sort */
struct RBuiltinOperator
{
  static TypeNode mkType(NodeManager* nm) { return nm->builtinOperatorType(); }
};

/** Type check returns the Boolean sort */
struct RBool
{
  static TypeNode mkType(NodeManager* nm) { return nm->booleanType(); }
};

/** Type check returns the integer sort */
struct RInteger
{
  static TypeNode mkType(NodeManager* nm) { return nm->integerType(); }
};

/** Type check returns the real sort */
struct RReal
{
  static TypeNode mkType(NodeManager* nm) { return nm->realType(); }
};

/** Type check returns the regexp sort */
struct RRegExp
{
  static TypeNode mkType(NodeManager* nm) { return nm->regExpType(); }
};

/** Type check returns the string sort */
struct RString
{
  static TypeNode mkType(NodeManager* nm) { return nm->stringType(); }
};

/** Argument does not exist */
struct ANone
{
  static bool checkArg(TNode n, size_t arg)
  {
    Assert(arg >= n.getNumChildren());
    return true;
  }
  constexpr static const char* typeName = "<none>";
};

/** Argument is optional */
template<class A>
struct AOptional
{
  static bool checkArg(TNode n, size_t arg)
  {
    if (arg < n.getNumChildren()) {
      return A::checkArg(n, arg);
    }
    return true;
  }
  constexpr static const char* typeName = A::typeName;
};

/** Argument is an integer */
struct AInteger
{
  static bool checkArg(TNode n, size_t arg)
  {
    TypeNode t = n[arg].getType(true);
    return t.isInteger();
  }
  constexpr static const char* typeName = "integer";
};

/** Argument is a real */
struct AReal
{
  static bool checkArg(TNode n, size_t arg)
  {
    TypeNode t = n[arg].getType(true);
    return t.isReal();
  }
  constexpr static const char* typeName = "real";
};

/** Argument is a regexp */
struct ARegExp
{
  static bool checkArg(TNode n, size_t arg)
  {
    TypeNode t = n[arg].getType(true);
    return t.isRegExp();
  }
  constexpr static const char* typeName = "regexp";
};

/** Argument is a string */
struct AString
{
  static bool checkArg(TNode n, size_t arg)
  {
    TypeNode t = n[arg].getType(true);
    return t.isString();
  }
  constexpr static const char* typeName = "string";
};

/**
 * The SimpleTypeRule template can be used to obtain a simple type rule by
 * defining a return type and the argument types (up to three arguments are
 * supported).
 * */
template <class R, class A0 = ANone, class A1 = ANone, class A2 = ANone>
class SimpleTypeRule
{
 public:
  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
  {
    if (check)
    {
      if (!A0::checkArg(n, 0))
      {
        std::stringstream msg;
        msg << "Expecting a " << A0::typeName
            << " term as the first argument in '" << n.getKind() << "'";
        throw TypeCheckingExceptionPrivate(n, msg.str());
      }
      if (!A1::checkArg(n, 1))
      {
        std::stringstream msg;
        msg << "Expecting a " << A1::typeName
            << " term as the second argument in '" << n.getKind() << "'";
        throw TypeCheckingExceptionPrivate(n, msg.str());
      }
      if (!A2::checkArg(n, 2))
      {
        std::stringstream msg;
        msg << "Expecting a " << A2::typeName
            << " term as the third argument in '" << n.getKind() << "'";
        throw TypeCheckingExceptionPrivate(n, msg.str());
      }
    }
    return R::mkType(nm);
  }
};

/**
 * The SimpleTypeRuleVar template can be used to obtain a simple type rule for
 * operators with a variable number of arguments. It takes the return type and
 * the type of the arguments as template parameters.
 * */
template <class R, class A>
class SimpleTypeRuleVar
{
 public:
  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
  {
    if (check)
    {
      for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
      {
        if (!A::checkArg(n, i))
        {
          std::stringstream msg;
          msg << "Expecting a " << A::typeName << " term as argument " << i
              << " in '" << n.getKind() << "'";
          throw TypeCheckingExceptionPrivate(n, msg.str());
        }
      }
    }
    return R::mkType(nm);
  }
};

}  // namespace expr
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* 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		* Templates for simple type rules
14		*
15		* This file defines templates for simple type rules. If a kind has the a
16		* type rule where each argument matches exactly a specific sort, these
17		* templates can be used to define typechecks without writing dedicated classes
18		* for them.
19		*/
20
21		#include <sstream>
22
23		#include "cvc5_private.h"
24		#include "expr/kind.h"
25		#include "expr/node.h"
26		#include "expr/node_manager.h"
27		#include "expr/type_node.h"
28
29		namespace cvc5 {
30		namespace expr {
31
32		/** Type check returns the builtin operator sort */
33		struct RBuiltinOperator
34		{
35	4595	static TypeNode mkType(NodeManager* nm) { return nm->builtinOperatorType(); }
36		};
37
38		/** Type check returns the Boolean sort */
39		struct RBool
40		{
41	891511	static TypeNode mkType(NodeManager* nm) { return nm->booleanType(); }
42		};
43
44		/** Type check returns the integer sort */
45		struct RInteger
46		{
47	11122	static TypeNode mkType(NodeManager* nm) { return nm->integerType(); }
48		};
49
50		/** Type check returns the real sort */
51		struct RReal
52		{
53	1989	static TypeNode mkType(NodeManager* nm) { return nm->realType(); }
54		};
55
56		/** Type check returns the regexp sort */
57		struct RRegExp
58		{
59	34153	static TypeNode mkType(NodeManager* nm) { return nm->regExpType(); }
60		};
61
62		/** Type check returns the string sort */
63		struct RString
64		{
65	32824	static TypeNode mkType(NodeManager* nm) { return nm->stringType(); }
66		};
67
68		/** Argument does not exist */
69		struct ANone
70		{
71	1092305	static bool checkArg(TNode n, size_t arg)
72		{
73	1092305	Assert(arg >= n.getNumChildren());
74	1092305	return true;
75		}
76		constexpr static const char* typeName = "<none>";
77		};
78
79		/** Argument is optional */
80		template<class A>
81		struct AOptional
82		{
83		static bool checkArg(TNode n, size_t arg)
84		{
85		if (arg < n.getNumChildren()) {
86		return A::checkArg(n, arg);
87		}
88		return true;
89		}
90		constexpr static const char* typeName = A::typeName;
91		};
92
93		/** Argument is an integer */
94		struct AInteger
95		{
96	15102	static bool checkArg(TNode n, size_t arg)
97		{
98	30204	TypeNode t = n[arg].getType(true);
99	30204	return t.isInteger();
100		}
101		constexpr static const char* typeName = "integer";
102		};
103
104		/** Argument is a real */
105		struct AReal
106		{
107	1766014	static bool checkArg(TNode n, size_t arg)
108		{
109	3532028	TypeNode t = n[arg].getType(true);
110	3532028	return t.isReal();
111		}
112		constexpr static const char* typeName = "real";
113		};
114
115		/** Argument is a regexp */
116		struct ARegExp
117		{
118	26076	static bool checkArg(TNode n, size_t arg)
119		{
120	52152	TypeNode t = n[arg].getType(true);
121	52152	return t.isRegExp();
122		}
123		constexpr static const char* typeName = "regexp";
124		};
125
126		/** Argument is a string */
127		struct AString
128		{
129	23433	static bool checkArg(TNode n, size_t arg)
130		{
131	46866	TypeNode t = n[arg].getType(true);
132	46866	return t.isString();
133		}
134		constexpr static const char* typeName = "string";
135		};
136
137		/**
138		* The SimpleTypeRule template can be used to obtain a simple type rule by
139		* defining a return type and the argument types (up to three arguments are
140		* supported).
141		* */
142		template <class R, class A0 = ANone, class A1 = ANone, class A2 = ANone>
143		class SimpleTypeRule
144		{
145		public:
146	973390	static TypeNode computeType(NodeManager* nm, TNode n, bool check)
147		{
148	973390	if (check)
149		{
150	971756	if (!A0::checkArg(n, 0))
151		{
152	4	std::stringstream msg;
153	2	msg << "Expecting a " << A0::typeName
154	2	<< " term as the first argument in '" << n.getKind() << "'";
155	2	throw TypeCheckingExceptionPrivate(n, msg.str());
156		}
157	971754	if (!A1::checkArg(n, 1))
158		{
159		std::stringstream msg;
160		msg << "Expecting a " << A1::typeName
161		<< " term as the second argument in '" << n.getKind() << "'";
162		throw TypeCheckingExceptionPrivate(n, msg.str());
163		}
164	971754	if (!A2::checkArg(n, 2))
165		{
166		std::stringstream msg;
167		msg << "Expecting a " << A2::typeName
168		<< " term as the third argument in '" << n.getKind() << "'";
169		throw TypeCheckingExceptionPrivate(n, msg.str());
170		}
171		}
172	973388	return R::mkType(nm);
173		}
174		};
175
176		/**
177		* The SimpleTypeRuleVar template can be used to obtain a simple type rule for
178		* operators with a variable number of arguments. It takes the return type and
179		* the type of the arguments as template parameters.
180		* */
181		template <class R, class A>
182		class SimpleTypeRuleVar
183		{
184		public:
185	2806	static TypeNode computeType(NodeManager* nm, TNode n, bool check)
186		{
187	2806	if (check)
188		{
189	10472	for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
190		{
191	7666	if (!A::checkArg(n, i))
192		{
193		std::stringstream msg;
194		msg << "Expecting a " << A::typeName << " term as argument " << i
195		<< " in '" << n.getKind() << "'";
196		throw TypeCheckingExceptionPrivate(n, msg.str());
197		}
198		}
199		}
200	2806	return R::mkType(nm);
201		}
202		};
203
204		} // namespace expr
205		} // namespace cvc5