From 8ee1078b5385cc03283fb2374f1f11261551b55a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Sat, 26 Mar 2022 00:27:11 -0700 Subject: [PATCH] builtin: Move type rules implementation to .cpp file. (#8407) --- .../builtin/theory_builtin_type_rules.cpp | 104 +++++++++++++++ .../builtin/theory_builtin_type_rules.h | 123 +++--------------- 2 files changed, 123 insertions(+), 104 deletions(-) diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index b7207edcb..00700bef9 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -23,6 +23,69 @@ namespace cvc5 { namespace theory { namespace builtin { +TypeNode EqualityTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TypeNode booleanType = nodeManager->booleanType(); + + if (check) + { + TypeNode lhsType = n[0].getType(check); + TypeNode rhsType = n[1].getType(check); + + if (TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull()) + { + std::stringstream ss; + ss << "Subexpressions must have a common base type:" << std::endl; + ss << "Equation: " << n << std::endl; + ss << "Type 1: " << lhsType << std::endl; + ss << "Type 2: " << rhsType << std::endl; + + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + // TODO : check isFirstClass for these types? (github issue #1202) + } + return booleanType; +} + +TypeNode DistinctTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (check) + { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + TypeNode joinType = (*child_it).getType(check); + for (++child_it; child_it != child_it_end; ++child_it) + { + TypeNode currentType = (*child_it).getType(); + joinType = TypeNode::leastCommonTypeNode(joinType, currentType); + if (joinType.isNull()) + { + throw TypeCheckingExceptionPrivate( + n, "Not all arguments are of the same type"); + } + } + } + return nodeManager->booleanType(); +} + +TypeNode SExprTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (check) + { + for (TNode c : n) + { + c.getType(check); + } + } + return nodeManager->sExprType(); +} + TypeNode UninterpretedSortValueTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) @@ -30,6 +93,47 @@ TypeNode UninterpretedSortValueTypeRule::computeType(NodeManager* nodeManager, return n.getConst().getType(); } +TypeNode WitnessTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (n[0].getType(check) != nodeManager->boundVarListType()) + { + std::stringstream ss; + ss << "expected a bound var list for WITNESS expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (n[0].getNumChildren() != 1) + { + std::stringstream ss; + ss << "expected a bound var list with one argument for WITNESS expression"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (check) + { + TypeNode rangeType = n[1].getType(check); + if (!rangeType.isBoolean()) + { + std::stringstream ss; + ss << "expected a body of a WITNESS expression to have Boolean type"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (n.getNumChildren() == 3) + { + if (n[2].getType(check) != nodeManager->instPatternListType()) + { + throw TypeCheckingExceptionPrivate( + n, + "third argument of witness is not instantiation " + "pattern list"); + } + } + } + // The type of a witness function is the type of its bound variable. + return n[0][0].getType(); +} + /** * Attribute for caching the ground term for each type. Maps TypeNode to the * skolem to return for mkGroundTerm. diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 12e6b05a1..a91cda26b 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -27,127 +27,42 @@ namespace cvc5 { namespace theory { namespace builtin { -class EqualityTypeRule { +class EqualityTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - TypeNode booleanType = nodeManager->booleanType(); - - if (check) - { - TypeNode lhsType = n[0].getType(check); - TypeNode rhsType = n[1].getType(check); - - if (TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull()) - { - std::stringstream ss; - ss << "Subexpressions must have a common base type:" << std::endl; - ss << "Equation: " << n << std::endl; - ss << "Type 1: " << lhsType << std::endl; - ss << "Type 2: " << rhsType << std::endl; - - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - // TODO : check isFirstClass for these types? (github issue #1202) - } - return booleanType; - } -};/* class EqualityTypeRule */ - + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class DistinctTypeRule { +class DistinctTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - if( check ) { - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - TypeNode joinType = (*child_it).getType(check); - for (++child_it; child_it != child_it_end; ++child_it) { - TypeNode currentType = (*child_it).getType(); - joinType = TypeNode::leastCommonTypeNode(joinType, currentType); - if (joinType.isNull()) { - throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); - } - } - } - return nodeManager->booleanType(); - } -};/* class DistinctTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class SExprTypeRule { +class SExprTypeRule +{ public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - if (check) - { - for (TNode c : n) - { - c.getType(check); - } - } - return nodeManager->sExprType(); - } -};/* class SExprTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; class UninterpretedSortValueTypeRule { public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; /* class UninterpretedSortValueTypeRule */ +}; class WitnessTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - if (n[0].getType(check) != nodeManager->boundVarListType()) - { - std::stringstream ss; - ss << "expected a bound var list for WITNESS expression, got `" - << n[0].getType().toString() << "'"; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - if (n[0].getNumChildren() != 1) - { - std::stringstream ss; - ss << "expected a bound var list with one argument for WITNESS expression"; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - if (check) - { - TypeNode rangeType = n[1].getType(check); - if (!rangeType.isBoolean()) - { - std::stringstream ss; - ss << "expected a body of a WITNESS expression to have Boolean type"; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - if (n.getNumChildren() == 3) - { - if (n[2].getType(check) != nodeManager->instPatternListType()) - { - throw TypeCheckingExceptionPrivate( - n, - "third argument of witness is not instantiation " - "pattern list"); - } - } - } - // The type of a witness function is the type of its bound variable. - return n[0][0].getType(); - } -}; /* class WitnessTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class SortProperties { +class SortProperties +{ public: - inline static bool isWellFounded(TypeNode type) { - return true; - } + static bool isWellFounded(TypeNode type) { return true; } static Node mkGroundTerm(TypeNode type); -};/* class SortProperties */ +}; } // namespace builtin } // namespace theory -- 2.30.2