Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/theory_arith_type_rules.cpp	Lines:	54	71	76.1 %
Date:	2021-08-20	Branches:	73	225	32.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Dejan Jovanovic
 *
 * 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 theory arithmetic.
 */

#include "theory/arith/theory_arith_type_rules.h"

#include "util/rational.h"

namespace cvc5 {
namespace theory {
namespace arith {

TypeNode ArithConstantTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  Assert(n.getKind() == kind::CONST_RATIONAL);
  if (n.getConst<Rational>().isIntegral())
  {
    return nodeManager->integerType();
  }
  else
  {
    return nodeManager->realType();
  }
}

TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  TypeNode integerType = nodeManager->integerType();
  TypeNode realType = nodeManager->realType();
  TNode::iterator child_it = n.begin();
  TNode::iterator child_it_end = n.end();
  bool isInteger = true;
  Kind k = n.getKind();
  for (; child_it != child_it_end; ++child_it)
  {
    TypeNode childType = (*child_it).getType(check);
    if (!childType.isInteger())
    {
      isInteger = false;
      if (!check)
      {  // if we're not checking, nothing left to do
        break;
      }
    }
    if (check)
    {
      if (!childType.isReal())
      {
        throw TypeCheckingExceptionPrivate(n,
                                           "expecting an arithmetic subterm");
      }
      if (k == kind::TO_REAL && !childType.isInteger())
      {
        throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
      }
    }
  }
  switch (k)
  {
    case kind::TO_REAL:
    case kind::CAST_TO_REAL: return realType;
    case kind::TO_INTEGER: return integerType;
    default:
    {
      bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
      return (isInteger && !isDivision ? integerType : realType);
    }
  }
}

TypeNode RealNullaryOperatorTypeRule::computeType(NodeManager* nodeManager,
                                                  TNode n,
                                                  bool check)
{
  // for nullary operators, we only computeType for check=true, since they are
  // given TypeAttr() on creation
  Assert(check);
  TypeNode realType = n.getType();
  if (realType != NodeManager::currentNM()->realType())
  {
    throw TypeCheckingExceptionPrivate(n, "expecting real type");
  }
  return realType;
}

TypeNode IAndOpTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  if (n.getKind() != kind::IAND_OP)
  {
    InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
  }
  TypeNode iType = nodeManager->integerType();
  std::vector<TypeNode> argTypes;
  argTypes.push_back(iType);
  argTypes.push_back(iType);
  return nodeManager->mkFunctionType(argTypes, iType);
}

TypeNode IAndTypeRule::computeType(NodeManager* nodeManager,
                                   TNode n,
                                   bool check)
{
  if (n.getKind() != kind::IAND)
  {
    InternalError() << "IAND typerule invoked for IAND kind";
  }
  if (check)
  {
    TypeNode arg1 = n[0].getType(check);
    TypeNode arg2 = n[1].getType(check);
    if (!arg1.isInteger() || !arg2.isInteger())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
    }
  }
  return nodeManager->integerType();
}

TypeNode Pow2TypeRule::computeType(NodeManager* nodeManager,
                                   TNode n,
                                   bool check)
{
  if (n.getKind() != kind::POW2)
  {
    InternalError() << "POW2 typerule invoked for POW2 kind";
  }
  if (check)
  {
    TypeNode arg1 = n[0].getType(check);
    if (!arg1.isInteger())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
    }
  }
  return nodeManager->integerType();
}

TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager,
                                                   TNode n,
                                                   bool check)
{
  if (check)
  {
    TypeNode t1 = n[0].getType(check);
    if (!t1.isBoolean())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting boolean term as first argument");
    }
    TypeNode t2 = n[1].getType(check);
    if (!t2.isReal())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting polynomial as second argument");
    }
  }
  return nodeManager->booleanType();
}

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer, Dejan Jovanovic
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 theory arithmetic.
14		*/
15
16		#include "theory/arith/theory_arith_type_rules.h"
17
18		#include "util/rational.h"
19
20		namespace cvc5 {
21		namespace theory {
22		namespace arith {
23
24	255797	TypeNode ArithConstantTypeRule::computeType(NodeManager* nodeManager,
25		TNode n,
26		bool check)
27		{
28	255797	Assert(n.getKind() == kind::CONST_RATIONAL);
29	255797	if (n.getConst<Rational>().isIntegral())
30		{
31	120146	return nodeManager->integerType();
32		}
33		else
34		{
35	135651	return nodeManager->realType();
36		}
37		}
38
39	3639459	TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager,
40		TNode n,
41		bool check)
42		{
43	7278918	TypeNode integerType = nodeManager->integerType();
44	7278918	TypeNode realType = nodeManager->realType();
45	3639459	TNode::iterator child_it = n.begin();
46	3639459	TNode::iterator child_it_end = n.end();
47	3639459	bool isInteger = true;
48	3639459	Kind k = n.getKind();
49	22509819	for (; child_it != child_it_end; ++child_it)
50		{
51	18870360	TypeNode childType = (*child_it).getType(check);
52	9435180	if (!childType.isInteger())
53		{
54	1959345	isInteger = false;
55	1959345	if (!check)
56		{ // if we're not checking, nothing left to do
57		break;
58		}
59		}
60	9435180	if (check)
61		{
62	9435180	if (!childType.isReal())
63		{
64		throw TypeCheckingExceptionPrivate(n,
65		"expecting an arithmetic subterm");
66		}
67	9435180	if (k == kind::TO_REAL && !childType.isInteger())
68		{
69		throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
70		}
71		}
72		}
73	3639459	switch (k)
74		{
75	1556	case kind::TO_REAL:
76	1556	case kind::CAST_TO_REAL: return realType;
77	702	case kind::TO_INTEGER: return integerType;
78	3637201	default:
79		{
80	3637201	bool isDivision = k == kind::DIVISION \|\| k == kind::DIVISION_TOTAL;
81	3637201	return (isInteger && !isDivision ? integerType : realType);
82		}
83		}
84		}
85
86	1672	TypeNode RealNullaryOperatorTypeRule::computeType(NodeManager* nodeManager,
87		TNode n,
88		bool check)
89		{
90		// for nullary operators, we only computeType for check=true, since they are
91		// given TypeAttr() on creation
92	1672	Assert(check);
93	1672	TypeNode realType = n.getType();
94	1672	if (realType != NodeManager::currentNM()->realType())
95		{
96		throw TypeCheckingExceptionPrivate(n, "expecting real type");
97		}
98	1672	return realType;
99		}
100
101	67	TypeNode IAndOpTypeRule::computeType(NodeManager* nodeManager,
102		TNode n,
103		bool check)
104		{
105	67	if (n.getKind() != kind::IAND_OP)
106		{
107		InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
108		}
109	134	TypeNode iType = nodeManager->integerType();
110	134	std::vector<TypeNode> argTypes;
111	67	argTypes.push_back(iType);
112	67	argTypes.push_back(iType);
113	134	return nodeManager->mkFunctionType(argTypes, iType);
114		}
115
116	292	TypeNode IAndTypeRule::computeType(NodeManager* nodeManager,
117		TNode n,
118		bool check)
119		{
120	292	if (n.getKind() != kind::IAND)
121		{
122		InternalError() << "IAND typerule invoked for IAND kind";
123		}
124	292	if (check)
125		{
126	584	TypeNode arg1 = n[0].getType(check);
127	584	TypeNode arg2 = n[1].getType(check);
128	292	if (!arg1.isInteger() \|\| !arg2.isInteger())
129		{
130		throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
131		}
132		}
133	292	return nodeManager->integerType();
134		}
135
136		TypeNode Pow2TypeRule::computeType(NodeManager* nodeManager,
137		TNode n,
138		bool check)
139		{
140		if (n.getKind() != kind::POW2)
141		{
142		InternalError() << "POW2 typerule invoked for POW2 kind";
143		}
144		if (check)
145		{
146		TypeNode arg1 = n[0].getType(check);
147		if (!arg1.isInteger())
148		{
149		throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
150		}
151		}
152		return nodeManager->integerType();
153		}
154
155	5	TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager,
156		TNode n,
157		bool check)
158		{
159	5	if (check)
160		{
161	10	TypeNode t1 = n[0].getType(check);
162	5	if (!t1.isBoolean())
163		{
164		throw TypeCheckingExceptionPrivate(
165		n, "expecting boolean term as first argument");
166		}
167	10	TypeNode t2 = n[1].getType(check);
168	5	if (!t2.isReal())
169		{
170		throw TypeCheckingExceptionPrivate(
171		n, "expecting polynomial as second argument");
172		}
173		}
174	5	return nodeManager->booleanType();
175		}
176
177		} // namespace arith
178		} // namespace theory
179	29358	} // namespace cvc5