From 90cde45ee963b994054f96f97111684cce808d82 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 21 Apr 2021 15:57:49 -0700 Subject: [PATCH] Arithmetic: Move implementation of type rules to cpp. (#6419) --- src/CMakeLists.txt | 1 + src/theory/arith/theory_arith_type_rules.cpp | 158 +++++++++++++++++++ src/theory/arith/theory_arith_type_rules.h | 152 +++--------------- 3 files changed, 184 insertions(+), 127 deletions(-) create mode 100644 src/theory/arith/theory_arith_type_rules.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 052e65adb..7d7aca8e8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -436,6 +436,7 @@ libcvc5_add_sources( theory/arith/theory_arith.h theory/arith/theory_arith_private.cpp theory/arith/theory_arith_private.h + theory/arith/theory_arith_type_rules.cpp theory/arith/theory_arith_type_rules.h theory/arith/type_enumerator.h theory/arrays/array_info.cpp diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp new file mode 100644 index 000000000..ba4c7dcb5 --- /dev/null +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -0,0 +1,158 @@ +/****************************************************************************** + * 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().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 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 diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 2d56a26c7..f7ef64e2d 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -10,9 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * [[ Add brief comments here ]] - * - * [[ Add file-specific comments here ]] + * Typing and cardinality rules for theory arithmetic. */ #include "cvc5_private.h" @@ -20,148 +18,48 @@ #ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H #define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H +#include "expr/node.h" +#include "expr/type_node.h" + namespace cvc5 { namespace theory { namespace arith { +class ArithConstantTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class ArithConstantTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::CONST_RATIONAL); - if(n.getConst().isIntegral()){ - return nodeManager->integerType(); - }else{ - return nodeManager->realType(); - } - } -};/* class ArithConstantTypeRule */ - -class ArithOperatorTypeRule { -public: - inline static TypeNode 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); - } - } - } -};/* class ArithOperatorTypeRule */ +class ArithOperatorTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class RealNullaryOperatorTypeRule { -public: - inline static TypeNode 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; - } -};/* class RealNullaryOperatorTypeRule */ +class RealNullaryOperatorTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; class IAndOpTypeRule { public: - inline static TypeNode 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 argTypes; - argTypes.push_back(iType); - argTypes.push_back(iType); - return nodeManager->mkFunctionType(argTypes, iType); - } -}; /* class IAndOpTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; class IAndTypeRule { public: - inline static TypeNode 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(); - } -}; /* class BitVectorConversionTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; class IndexedRootPredicateTypeRule { public: - inline static TypeNode 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(); - } -}; /* class IndexedRootPredicateTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; } // namespace arith } // namespace theory -- 2.30.2