From 9cb7212d58d42cf1433dc086d305f1a202c3771b Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 20 Apr 2021 15:33:39 -0700 Subject: [PATCH] Quantifiers: Move implementation of type rules to cpp. (#6404) --- src/CMakeLists.txt | 1 + .../theory_quantifiers_type_rules.cpp | 137 ++++++++++++++++++ .../theory_quantifiers_type_rules.h | 110 ++------------ 3 files changed, 154 insertions(+), 94 deletions(-) create mode 100644 src/theory/quantifiers/theory_quantifiers_type_rules.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c24ab31ec..b86e59877 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -877,6 +877,7 @@ libcvc4_add_sources( theory/quantifiers/term_util.h theory/quantifiers/theory_quantifiers.cpp theory/quantifiers/theory_quantifiers.h + theory/quantifiers/theory_quantifiers_type_rules.cpp theory/quantifiers/theory_quantifiers_type_rules.h theory/quantifiers_engine.cpp theory/quantifiers_engine.h diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp new file mode 100644 index 000000000..6fb377a56 --- /dev/null +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp @@ -0,0 +1,137 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Morgan Deters, Tim King + * + * 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. + * **************************************************************************** + * + * Theory of quantifiers. + */ + +#include "theory/quantifiers/theory_quantifiers_type_rules.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +TypeNode QuantifierTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Debug("typecheck-q") << "type check for fa " << n << std::endl; + Assert((n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS) + && n.getNumChildren() > 0); + if (check) + { + if (n[0].getType(check) != nodeManager->boundVarListType()) + { + throw TypeCheckingExceptionPrivate( + n, "first argument of quantifier is not bound var list"); + } + if (n[1].getType(check) != nodeManager->booleanType()) + { + throw TypeCheckingExceptionPrivate(n, + "body of quantifier is not boolean"); + } + if (n.getNumChildren() == 3) + { + if (n[2].getType(check) != nodeManager->instPatternListType()) + { + throw TypeCheckingExceptionPrivate( + n, + "third argument of quantifier is not instantiation " + "pattern list"); + } + for (const Node& p : n[2]) + { + if (p.getKind() == kind::INST_POOL + && p.getNumChildren() != n[0].getNumChildren()) + { + throw TypeCheckingExceptionPrivate( + n, + "expected number of arguments to pool to be the same as the " + "number of bound variables of the quantified formula"); + } + } + } + } + return nodeManager->booleanType(); +} + +TypeNode QuantifierBoundVarListTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::BOUND_VAR_LIST); + if (check) + { + for (int i = 0; i < (int)n.getNumChildren(); i++) + { + if (n[i].getKind() != kind::BOUND_VARIABLE) + { + throw TypeCheckingExceptionPrivate( + n, "argument of bound var list is not bound variable"); + } + } + } + return nodeManager->boundVarListType(); +} + +TypeNode QuantifierInstPatternTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::INST_PATTERN); + if (check) + { + TypeNode tn = n[0].getType(check); + // this check catches the common mistake writing :pattern (f x) instead of + // :pattern ((f x)) + if (n[0].isVar() && n[0].getKind() != kind::BOUND_VARIABLE + && tn.isFunction()) + { + throw TypeCheckingExceptionPrivate( + n[0], "Pattern must be a list of fully-applied terms."); + } + } + return nodeManager->instPatternType(); +} + +TypeNode QuantifierAnnotationTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return nodeManager->instPatternType(); +} + +TypeNode QuantifierInstPatternListTypeRule::computeType( + NodeManager* nodeManager, TNode n, bool check) +{ + Assert(n.getKind() == kind::INST_PATTERN_LIST); + if (check) + { + for (const Node& nc : n) + { + Kind k = nc.getKind(); + if (k != kind::INST_PATTERN && k != kind::INST_NO_PATTERN + && k != kind::INST_ATTRIBUTE && k != kind::INST_POOL + && k != kind::INST_ADD_TO_POOL && k != kind::SKOLEM_ADD_TO_POOL) + { + throw TypeCheckingExceptionPrivate( + n, + "argument of inst pattern list is not a legal quantifiers " + "annotation"); + } + } + } + return nodeManager->instPatternListType(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 7783c65d6..80d7b0e03 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -27,106 +27,28 @@ namespace quantifiers { struct QuantifierTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Debug("typecheck-q") << "type check for fa " << n << std::endl; - Assert((n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS) - && n.getNumChildren() > 0); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate( - n, "first argument of quantifier is not bound var list"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, - "body of quantifier is not boolean"); - } - if (n.getNumChildren() == 3) - { - if (n[2].getType(check) != nodeManager->instPatternListType()) - { - throw TypeCheckingExceptionPrivate( - n, - "third argument of quantifier is not instantiation " - "pattern list"); - } - for (const Node& p : n[2]) - { - if (p.getKind() == kind::INST_POOL - && p.getNumChildren() != n[0].getNumChildren()) - { - throw TypeCheckingExceptionPrivate( - n, - "expected number of arguments to pool to be the same as the " - "number of bound variables of the quantified formula"); - } - } - } - } - return nodeManager->booleanType(); - } -}; /* struct QuantifierTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct QuantifierBoundVarListTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::BOUND_VAR_LIST); - if( check ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=kind::BOUND_VARIABLE ){ - throw TypeCheckingExceptionPrivate(n, "argument of bound var list is not bound variable"); - } - } - } - return nodeManager->boundVarListType(); - } -};/* struct QuantifierBoundVarListTypeRule */ +struct QuantifierBoundVarListTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct QuantifierInstPatternTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::INST_PATTERN); - if( check ){ - TypeNode tn = n[0].getType(check); - // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x)) - if( n[0].isVar() && n[0].getKind()!=kind::BOUND_VARIABLE && tn.isFunction() ){ - throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms."); - } - } - return nodeManager->instPatternType(); - } -};/* struct QuantifierInstPatternTypeRule */ +struct QuantifierInstPatternTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; struct QuantifierAnnotationTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - return nodeManager->instPatternType(); - } -}; /* struct QuantifierAnnotationTypeRule */ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; -struct QuantifierInstPatternListTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::INST_PATTERN_LIST); - if( check ){ - for (const Node& nc : n) - { - Kind k = nc.getKind(); - if (k != kind::INST_PATTERN && k != kind::INST_NO_PATTERN - && k != kind::INST_ATTRIBUTE && k != kind::INST_POOL - && k != kind::INST_ADD_TO_POOL && k != kind::SKOLEM_ADD_TO_POOL) - { - throw TypeCheckingExceptionPrivate( - n, - "argument of inst pattern list is not a legal quantifiers " - "annotation"); - } - } - } - return nodeManager->instPatternListType(); - } -};/* struct QuantifierInstPatternListTypeRule */ +struct QuantifierInstPatternListTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; } // namespace quantifiers } // namespace theory -- 2.30.2