From baeb7af81166d709bfbbc7b8da13ac238c1e9579 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 26 Apr 2021 20:33:03 -0700 Subject: [PATCH] Bool: Move implementation of type rules to cpp. (#6420) --- src/CMakeLists.txt | 1 + .../arrays/theory_arrays_type_rules.cpp | 3 +- .../booleans/theory_bool_type_rules.cpp | 76 +++++++++++++++++++ src/theory/booleans/theory_bool_type_rules.h | 62 ++++----------- 4 files changed, 93 insertions(+), 49 deletions(-) create mode 100644 src/theory/booleans/theory_bool_type_rules.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 95fa90fe3..c03c2d591 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -498,6 +498,7 @@ libcvc5_add_sources( theory/booleans/theory_bool.h theory/booleans/theory_bool_rewriter.cpp theory/booleans/theory_bool_rewriter.h + theory/booleans/theory_bool_type_rules.cpp theory/booleans/theory_bool_type_rules.h theory/booleans/type_enumerator.h theory/builtin/proof_checker.cpp diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index e0c27419f..04a2f1a74 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -15,7 +15,8 @@ #include "theory/arrays/theory_arrays_type_rules.h" -#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes +// for array-constant attributes +#include "theory/arrays/theory_arrays_rewriter.h" #include "theory/type_enumerator.h" namespace cvc5 { diff --git a/src/theory/booleans/theory_bool_type_rules.cpp b/src/theory/booleans/theory_bool_type_rules.cpp new file mode 100644 index 000000000..11210a869 --- /dev/null +++ b/src/theory/booleans/theory_bool_type_rules.cpp @@ -0,0 +1,76 @@ +/****************************************************************************** + * Top contributors (to current version): + * Dejan Jovanovic, Morgan Deters, Christopher L. Conway + * + * 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 boolean. + */ + +#include "theory/booleans/theory_bool_type_rules.h" + +#include + +namespace cvc5 { +namespace theory { +namespace boolean { + +TypeNode BooleanTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TypeNode booleanType = nodeManager->booleanType(); + if (check) + { + for (const auto& child : n) + { + if (!child.getType(check).isBoolean()) + { + Debug("pb") << "failed type checking: " << child << std::endl; + Debug("pb") << " integer: " << child.getType(check).isInteger() + << std::endl; + Debug("pb") << " real: " << child.getType(check).isReal() << std::endl; + throw TypeCheckingExceptionPrivate(n, + "expecting a Boolean subexpression"); + } + } + } + return booleanType; +} + +TypeNode IteTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) +{ + TypeNode thenType = n[1].getType(check); + TypeNode elseType = n[2].getType(check); + TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType); + if (check) + { + TypeNode booleanType = nodeManager->booleanType(); + if (n[0].getType(check) != booleanType) + { + throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); + } + if (iteType.isNull()) + { + std::stringstream ss; + ss << "Both branches of the ITE must be a subtype of a common type." + << std::endl + << "then branch: " << n[1] << std::endl + << "its type : " << thenType << std::endl + << "else branch: " << n[2] << std::endl + << "its type : " << elseType << std::endl; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + return iteType; +} + +} // namespace boolean +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 6c9aea0ae..6d8eb0a6d 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_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 boolean. */ #include "cvc5_private.h" @@ -20,56 +18,24 @@ #ifndef CVC5__THEORY_BOOL_TYPE_RULES_H #define CVC5__THEORY_BOOL_TYPE_RULES_H +#include "expr/node.h" +#include "expr/type_node.h" + namespace cvc5 { namespace theory { namespace boolean { -class BooleanTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TypeNode booleanType = nodeManager->booleanType(); - if( check ) { - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - for(; child_it != child_it_end; ++child_it) { - if(!(*child_it).getType(check).isBoolean()) { - Debug("pb") << "failed type checking: " << *child_it << std::endl; - Debug("pb") << " integer: " << (*child_it).getType(check).isInteger() << std::endl; - Debug("pb") << " real: " << (*child_it).getType(check).isReal() << std::endl; - throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression"); - } - } - } - return booleanType; - } -};/* class BooleanTypeRule */ +class BooleanTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -class IteTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TypeNode thenType = n[1].getType(check); - TypeNode elseType = n[2].getType(check); - TypeNode iteType = TypeNode::leastCommonTypeNode(thenType, elseType); - if( check ) { - TypeNode booleanType = nodeManager->booleanType(); - if (n[0].getType(check) != booleanType) { - throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); - } - if (iteType.isNull()) { - std::stringstream ss; - ss << "Both branches of the ITE must be a subtype of a common type." << std::endl - << "then branch: " << n[1] << std::endl - << "its type : " << thenType << std::endl - << "else branch: " << n[2] << std::endl - << "its type : " << elseType << std::endl; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - return iteType; - } -};/* class IteTypeRule */ +class IteTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; } // namespace boolean } // namespace theory -- 2.30.2