From 10a4e43ad9a56a3a72878b24ec24c2e4fbccea57 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 20 Apr 2021 15:55:56 -0700 Subject: [PATCH] Sep: Move implementation of type rules to cpp. (#6402) --- src/CMakeLists.txt | 1 + src/theory/sep/theory_sep_type_rules.cpp | 120 +++++++++++++++++++++++ src/theory/sep/theory_sep_type_rules.h | 104 +++++--------------- 3 files changed, 148 insertions(+), 77 deletions(-) create mode 100644 src/theory/sep/theory_sep_type_rules.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b86e59877..81e598f2b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -892,6 +892,7 @@ libcvc4_add_sources( theory/sep/theory_sep.h theory/sep/theory_sep_rewriter.cpp theory/sep/theory_sep_rewriter.h + theory/sep/theory_sep_type_rules.cpp theory/sep/theory_sep_type_rules.h theory/sets/cardinality_extension.cpp theory/sets/cardinality_extension.h diff --git a/src/theory/sep/theory_sep_type_rules.cpp b/src/theory/sep/theory_sep_type_rules.cpp new file mode 100644 index 000000000..28dfa5c40 --- /dev/null +++ b/src/theory/sep/theory_sep_type_rules.cpp @@ -0,0 +1,120 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Tim King, Mathias Preiner + * + * 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 sep. + */ + +#include "theory/sep/theory_sep_type_rules.h" + +namespace cvc5 { +namespace theory { +namespace sep { + +TypeNode SepEmpTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::SEP_EMP); + return nodeManager->booleanType(); +} + +TypeNode SepPtoTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::SEP_PTO); + if (check) + { + TypeNode refType = n[0].getType(check); + TypeNode ptType = n[1].getType(check); + } + return nodeManager->booleanType(); +} + +TypeNode SepStarTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TypeNode btype = nodeManager->booleanType(); + Assert(n.getKind() == kind::SEP_STAR); + if (check) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + TypeNode ctype = n[i].getType(check); + if (ctype != btype) + { + throw TypeCheckingExceptionPrivate(n, + "child of sep star is not Boolean"); + } + } + } + return btype; +} + +TypeNode SepWandTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TypeNode btype = nodeManager->booleanType(); + Assert(n.getKind() == kind::SEP_WAND); + if (check) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + TypeNode ctype = n[i].getType(check); + if (ctype != btype) + { + throw TypeCheckingExceptionPrivate( + n, "child of sep magic wand is not Boolean"); + } + } + } + return btype; +} + +TypeNode SepLabelTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TypeNode btype = nodeManager->booleanType(); + Assert(n.getKind() == kind::SEP_LABEL); + if (check) + { + TypeNode ctype = n[0].getType(check); + if (ctype != btype) + { + throw TypeCheckingExceptionPrivate(n, + "child of sep label is not Boolean"); + } + TypeNode stype = n[1].getType(check); + if (!stype.isSet()) + { + throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set"); + } + } + return btype; +} + +TypeNode SepNilTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::SEP_NIL); + Assert(check); + TypeNode type = n.getType(); + return type; +} + +} // namespace sep +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 676cb8d9d..f437ba2d7 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -18,93 +18,43 @@ #ifndef CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H #define CVC5__THEORY__SEP__THEORY_SEP_TYPE_RULES_H +#include "expr/node.h" +#include "expr/type_node.h" + namespace cvc5 { namespace theory { namespace sep { -class SepEmpTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::SEP_EMP); - return nodeManager->booleanType(); - } +class SepEmpTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -struct SepPtoTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::SEP_PTO); - if( check ) { - TypeNode refType = n[0].getType(check); - TypeNode ptType = n[1].getType(check); - } - return nodeManager->booleanType(); - } -};/* struct SepSelectTypeRule */ +struct SepPtoTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct SepStarTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TypeNode btype = nodeManager->booleanType(); - Assert(n.getKind() == kind::SEP_STAR); - if( check ){ - for( unsigned i=0; ibooleanType(); - Assert(n.getKind() == kind::SEP_WAND); - if( check ){ - for( unsigned i=0; ibooleanType(); - Assert(n.getKind() == kind::SEP_LABEL); - if( check ){ - TypeNode ctype = n[0].getType( check ); - if( ctype!=btype ){ - throw TypeCheckingExceptionPrivate(n, "child of sep label is not Boolean"); - } - TypeNode stype = n[1].getType( check ); - if( !stype.isSet() ){ - throw TypeCheckingExceptionPrivate(n, "label of sep label is not a set"); - } - } - return btype; - } -};/* struct SepLabelTypeRule */ +struct SepLabelTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct SepNilTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::SEP_NIL); - Assert(check); - TypeNode type = n.getType(); - return type; - } -};/* struct SepLabelTypeRule */ +struct SepNilTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; } // namespace sep } // namespace theory -- 2.30.2