Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/theory_arith_type_rules.cpp	Lines:	54	63	85.7 %
Date:	2021-05-22	Branches:	73	203	36.0 %


/******************************************************************************
 * 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"

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 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		namespace cvc5 {
19		namespace theory {
20		namespace arith {
21
22	278354	TypeNode ArithConstantTypeRule::computeType(NodeManager* nodeManager,
23		TNode n,
24		bool check)
25		{
26	278354	Assert(n.getKind() == kind::CONST_RATIONAL);
27	278354	if (n.getConst<Rational>().isIntegral())
28		{
29	125569	return nodeManager->integerType();
30		}
31		else
32		{
33	152785	return nodeManager->realType();
34		}
35		}
36
37	3451014	TypeNode ArithOperatorTypeRule::computeType(NodeManager* nodeManager,
38		TNode n,
39		bool check)
40		{
41	6902028	TypeNode integerType = nodeManager->integerType();
42	6902028	TypeNode realType = nodeManager->realType();
43	3451014	TNode::iterator child_it = n.begin();
44	3451014	TNode::iterator child_it_end = n.end();
45	3451014	bool isInteger = true;
46	3451014	Kind k = n.getKind();
47	21278382	for (; child_it != child_it_end; ++child_it)
48		{
49	17827368	TypeNode childType = (*child_it).getType(check);
50	8913684	if (!childType.isInteger())
51		{
52	2027081	isInteger = false;
53	2027081	if (!check)
54		{ // if we're not checking, nothing left to do
55		break;
56		}
57		}
58	8913684	if (check)
59		{
60	8913684	if (!childType.isReal())
61		{
62		throw TypeCheckingExceptionPrivate(n,
63		"expecting an arithmetic subterm");
64		}
65	8913684	if (k == kind::TO_REAL && !childType.isInteger())
66		{
67		throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
68		}
69		}
70		}
71	3451014	switch (k)
72		{
73	1555	case kind::TO_REAL:
74	1555	case kind::CAST_TO_REAL: return realType;
75	635	case kind::TO_INTEGER: return integerType;
76	3448824	default:
77		{
78	3448824	bool isDivision = k == kind::DIVISION \|\| k == kind::DIVISION_TOTAL;
79	3448824	return (isInteger && !isDivision ? integerType : realType);
80		}
81		}
82		}
83
84	1530	TypeNode RealNullaryOperatorTypeRule::computeType(NodeManager* nodeManager,
85		TNode n,
86		bool check)
87		{
88		// for nullary operators, we only computeType for check=true, since they are
89		// given TypeAttr() on creation
90	1530	Assert(check);
91	1530	TypeNode realType = n.getType();
92	1530	if (realType != NodeManager::currentNM()->realType())
93		{
94		throw TypeCheckingExceptionPrivate(n, "expecting real type");
95		}
96	1530	return realType;
97		}
98
99	65	TypeNode IAndOpTypeRule::computeType(NodeManager* nodeManager,
100		TNode n,
101		bool check)
102		{
103	65	if (n.getKind() != kind::IAND_OP)
104		{
105		InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
106		}
107	130	TypeNode iType = nodeManager->integerType();
108	130	std::vector<TypeNode> argTypes;
109	65	argTypes.push_back(iType);
110	65	argTypes.push_back(iType);
111	130	return nodeManager->mkFunctionType(argTypes, iType);
112		}
113
114	292	TypeNode IAndTypeRule::computeType(NodeManager* nodeManager,
115		TNode n,
116		bool check)
117		{
118	292	if (n.getKind() != kind::IAND)
119		{
120		InternalError() << "IAND typerule invoked for IAND kind";
121		}
122	292	if (check)
123		{
124	584	TypeNode arg1 = n[0].getType(check);
125	584	TypeNode arg2 = n[1].getType(check);
126	292	if (!arg1.isInteger() \|\| !arg2.isInteger())
127		{
128		throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
129		}
130		}
131	292	return nodeManager->integerType();
132		}
133
134	5	TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager,
135		TNode n,
136		bool check)
137		{
138	5	if (check)
139		{
140	10	TypeNode t1 = n[0].getType(check);
141	5	if (!t1.isBoolean())
142		{
143		throw TypeCheckingExceptionPrivate(
144		n, "expecting boolean term as first argument");
145		}
146	10	TypeNode t2 = n[1].getType(check);
147	5	if (!t2.isReal())
148		{
149		throw TypeCheckingExceptionPrivate(
150		n, "expecting polynomial as second argument");
151		}
152		}
153	5	return nodeManager->booleanType();
154		}
155
156		} // namespace arith
157		} // namespace theory
158	28191	} // namespace cvc5