From 5450ab256acb51664467e7350cca5284ffe04319 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 21 Apr 2021 15:48:38 -0700 Subject: [PATCH] UF: Move implementation of type rules to cpp. (#6403) --- src/CMakeLists.txt | 1 + src/theory/uf/theory_uf_type_rules.cpp | 189 +++++++++++++++++++++++++ src/theory/uf/theory_uf_type_rules.h | 168 ++++------------------ 3 files changed, 217 insertions(+), 141 deletions(-) create mode 100644 src/theory/uf/theory_uf_type_rules.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8f5b7d67f..052e65adb 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1066,6 +1066,7 @@ libcvc5_add_sources( theory/uf/theory_uf_model.cpp theory/uf/theory_uf_model.h theory/uf/theory_uf_rewriter.h + theory/uf/theory_uf_type_rules.cpp theory/uf/theory_uf_type_rules.h theory/valuation.cpp theory/valuation.h diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp new file mode 100644 index 000000000..f81abdca1 --- /dev/null +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -0,0 +1,189 @@ +/****************************************************************************** + * 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 +#include + +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 CardinalityConstraintTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (check) + { + // don't care what it is, but it should be well-typed + n[0].getType(check); + + TypeNode valType = n[1].getType(check); + if (valType != nodeManager->integerType()) + { + throw TypeCheckingExceptionPrivate( + n, "cardinality constraint must be integer"); + } + if (n[1].getKind() != kind::CONST_RATIONAL) + { + throw TypeCheckingExceptionPrivate( + n, "cardinality constraint must be a constant"); + } + cvc5::Rational r(INT_MAX); + if (n[1].getConst() > r) + { + throw TypeCheckingExceptionPrivate( + n, "Exceeded INT_MAX in cardinality constraint"); + } + if (n[1].getConst().getNumerator().sgn() != 1) + { + throw TypeCheckingExceptionPrivate( + n, "cardinality constraint must be positive"); + } + } + return nodeManager->booleanType(); +} + +TypeNode CombinedCardinalityConstraintTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + if (check) + { + TypeNode valType = n[0].getType(check); + if (valType != nodeManager->integerType()) + { + throw TypeCheckingExceptionPrivate( + n, "combined cardinality constraint must be integer"); + } + if (n[0].getKind() != kind::CONST_RATIONAL) + { + throw TypeCheckingExceptionPrivate( + n, "combined cardinality constraint must be a constant"); + } + cvc5::Rational r(INT_MAX); + if (n[0].getConst() > r) + { + throw TypeCheckingExceptionPrivate( + n, "Exceeded INT_MAX in combined cardinality constraint"); + } + if (n[0].getConst().getNumerator().sgn() == -1) + { + throw TypeCheckingExceptionPrivate( + n, "combined cardinality constraint must be non-negative"); + } + } + return nodeManager->booleanType(); +} + +TypeNode PartialTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getOperator().getType().getRangeType(); +} + +TypeNode CardinalityValueTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (check) + { + n[0].getType(check); + } + return nodeManager->integerType(); +} + +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 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); + } +} + +} // namespace uf +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index e6383f80e..d786f5f24 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_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 the theory of UF. */ #include "cvc5_private.h" @@ -20,162 +18,50 @@ #ifndef CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H #define CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H -#include +#include "expr/node.h" +#include "expr/type_node.h" namespace cvc5 { namespace theory { namespace uf { -class UfTypeRule { +class UfTypeRule +{ public: - inline static TypeNode 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(); - } -}; /* class UfTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class CardinalityConstraintTypeRule { +class CardinalityConstraintTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - if (check) { - // don't care what it is, but it should be well-typed - n[0].getType(check); - - TypeNode valType = n[1].getType(check); - if (valType != nodeManager->integerType()) { - throw TypeCheckingExceptionPrivate( - n, "cardinality constraint must be integer"); - } - if (n[1].getKind() != kind::CONST_RATIONAL) { - throw TypeCheckingExceptionPrivate( - n, "cardinality constraint must be a constant"); - } - cvc5::Rational r(INT_MAX); - if (n[1].getConst() > r) { - throw TypeCheckingExceptionPrivate( - n, "Exceeded INT_MAX in cardinality constraint"); - } - if (n[1].getConst().getNumerator().sgn() != 1) { - throw TypeCheckingExceptionPrivate( - n, "cardinality constraint must be positive"); - } - } - return nodeManager->booleanType(); - } -}; /* class CardinalityConstraintTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class CombinedCardinalityConstraintTypeRule { +class CombinedCardinalityConstraintTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - if (check) { - TypeNode valType = n[0].getType(check); - if (valType != nodeManager->integerType()) { - throw TypeCheckingExceptionPrivate( - n, "combined cardinality constraint must be integer"); - } - if (n[0].getKind() != kind::CONST_RATIONAL) { - throw TypeCheckingExceptionPrivate( - n, "combined cardinality constraint must be a constant"); - } - cvc5::Rational r(INT_MAX); - if (n[0].getConst() > r) { - throw TypeCheckingExceptionPrivate( - n, "Exceeded INT_MAX in combined cardinality constraint"); - } - if (n[0].getConst().getNumerator().sgn() == -1) { - throw TypeCheckingExceptionPrivate( - n, "combined cardinality constraint must be non-negative"); - } - } - return nodeManager->booleanType(); - } -}; /* class CardinalityConstraintTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class PartialTypeRule { +class PartialTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - return n.getOperator().getType().getRangeType(); - } -}; /* class PartialTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class CardinalityValueTypeRule { +class CardinalityValueTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - if (check) { - n[0].getType(check); - } - return nodeManager->integerType(); - } -}; /* class CardinalityValueTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; // class with the typing rule for HO_APPLY terms -class HoApplyTypeRule { +class HoApplyTypeRule +{ public: // the typing rule for HO_APPLY terms - inline static TypeNode 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 ); - } - } -}; /* class HoApplyTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; } // namespace uf } // namespace theory -- 2.30.2