#line 18 "${template}"
-#include "expr/type_checker.h"
#include "expr/node_manager.h"
#include "expr/node_manager_attributes.h"
+#include "expr/type_checker.h"
+#include "expr/type_checker_util.h"
${typechecker_includes}
-#line 26 "${template}"
+#line 27 "${template}"
namespace CVC4 {
namespace expr {
${typerules}
-#line 47 "${template}"
+#line 48 "${template}"
default:
Debug("getType") << "FAILURE" << std::endl;
switch(n.getKind()) {
${construles}
-#line 69 "${template}"
+#line 70 "${template}"
default:;
}
switch(n.getKind()) {
${neverconstrules}
-#line 85 "${template}"
+#line 86 "${template}"
default:;
}
--- /dev/null
+/********************* */
+/*! \file type_checker_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Templates for simple type rules
+ **
+ ** This file defines templates for simple type rules. If a kind has the a
+ ** type rule where each argument matches exactly a specific sort, these
+ ** templates can be used to define typechecks without writing dedicated classes
+ ** for them.
+ **/
+
+#include "cvc4_private.h"
+
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/** Type check returns the builtin operator sort */
+struct RBuiltinOperator
+{
+ static TypeNode mkType(NodeManager* nm) { return nm->builtinOperatorType(); }
+};
+
+/** Type check returns the Boolean sort */
+struct RBool
+{
+ static TypeNode mkType(NodeManager* nm) { return nm->booleanType(); }
+};
+
+/** Type check returns the integer sort */
+struct RInteger
+{
+ static TypeNode mkType(NodeManager* nm) { return nm->integerType(); }
+};
+
+/** Type check returns the real sort */
+struct RReal
+{
+ static TypeNode mkType(NodeManager* nm) { return nm->realType(); }
+};
+
+/** Type check returns the regexp sort */
+struct RRegExp
+{
+ static TypeNode mkType(NodeManager* nm) { return nm->regExpType(); }
+};
+
+/** Type check returns the string sort */
+struct RString
+{
+ static TypeNode mkType(NodeManager* nm) { return nm->stringType(); }
+};
+
+/** Argument does not exist */
+struct ANone
+{
+ static bool checkArg(TNode n, size_t arg)
+ {
+ Assert(arg >= n.getNumChildren());
+ return true;
+ }
+ constexpr static const char* typeName = "<none>";
+};
+
+/** Argument is optional */
+template<class A>
+struct AOptional
+{
+ static bool checkArg(TNode n, size_t arg)
+ {
+ if (arg < n.getNumChildren()) {
+ return A::checkArg(n, arg);
+ }
+ return true;
+ }
+ constexpr static const char* typeName = A::typeName;
+};
+
+/** Argument is an integer */
+struct AInteger
+{
+ static bool checkArg(TNode n, size_t arg)
+ {
+ TypeNode t = n[arg].getType(true);
+ return t.isInteger();
+ }
+ constexpr static const char* typeName = "integer";
+};
+
+/** Argument is a real */
+struct AReal
+{
+ static bool checkArg(TNode n, size_t arg)
+ {
+ TypeNode t = n[arg].getType(true);
+ return t.isReal();
+ }
+ constexpr static const char* typeName = "real";
+};
+
+/** Argument is a regexp */
+struct ARegExp
+{
+ static bool checkArg(TNode n, size_t arg)
+ {
+ TypeNode t = n[arg].getType(true);
+ return t.isRegExp();
+ }
+ constexpr static const char* typeName = "regexp";
+};
+
+/** Argument is a string */
+struct AString
+{
+ static bool checkArg(TNode n, size_t arg)
+ {
+ TypeNode t = n[arg].getType(true);
+ return t.isString();
+ }
+ constexpr static const char* typeName = "string";
+};
+
+/**
+ * The SimpleTypeRule template can be used to obtain a simple type rule by
+ * defining a return type and the argument types (up to three arguments are
+ * supported).
+ * */
+template <class R, class A0 = ANone, class A1 = ANone, class A2 = ANone>
+class SimpleTypeRule
+{
+ public:
+ static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+ {
+ if (check)
+ {
+ if (!A0::checkArg(n, 0))
+ {
+ std::stringstream msg;
+ msg << "Expecting a " << A0::typeName
+ << " term as the first argument in '" << n.getKind() << "'";
+ throw TypeCheckingExceptionPrivate(n, msg.str());
+ }
+ if (!A1::checkArg(n, 1))
+ {
+ std::stringstream msg;
+ msg << "Expecting a " << A1::typeName
+ << " term as the second argument in '" << n.getKind() << "'";
+ throw TypeCheckingExceptionPrivate(n, msg.str());
+ }
+ if (!A2::checkArg(n, 2))
+ {
+ std::stringstream msg;
+ msg << "Expecting a " << A2::typeName
+ << " term as the third argument in '" << n.getKind() << "'";
+ throw TypeCheckingExceptionPrivate(n, msg.str());
+ }
+ }
+ return R::mkType(nm);
+ }
+};
+
+/**
+ * The SimpleTypeRuleVar template can be used to obtain a simple type rule for
+ * operators with a variable number of arguments. It takes the return type and
+ * the type of the arguments as template parameters.
+ * */
+template <class R, class A>
+class SimpleTypeRuleVar
+{
+ public:
+ static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+ {
+ if (check)
+ {
+ for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
+ {
+ if (!A::checkArg(n, i))
+ {
+ std::stringstream msg;
+ msg << "Expecting a " << A::typeName << " term as argument " << i
+ << " in '" << n.getKind() << "'";
+ throw TypeCheckingExceptionPrivate(n, msg.str());
+ }
+ }
+ }
+ return R::mkType(nm);
+ }
+};
+
+} // namespace expr
+} // namespace CVC4
typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
-typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
+typerule LT "SimpleTypeRule<RBool, AReal, AReal>"
+typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
+typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
+typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
+typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
-typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
-typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
-typerule DIVISIBLE_OP ::CVC4::theory::arith::DivisibleOpTypeRule
+typerule ABS "SimpleTypeRule<RInteger, AInteger>"
+typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>"
+typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>"
typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
-
-typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule
-typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule SECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-
-typerule SQRT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
+
+typerule EXPONENTIAL "SimpleTypeRule<RReal, AReal>"
+typerule SINE "SimpleTypeRule<RReal, AReal>"
+typerule COSINE "SimpleTypeRule<RReal, AReal>"
+typerule TANGENT "SimpleTypeRule<RReal, AReal>"
+typerule COSECANT "SimpleTypeRule<RReal, AReal>"
+typerule SECANT "SimpleTypeRule<RReal, AReal>"
+typerule COTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule ARCSINE "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOSINE "SimpleTypeRule<RReal, AReal>"
+typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
+typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
+
+typerule SQRT "SimpleTypeRule<RReal, AReal>"
nullaryoperator PI "pi"
}
};/* class ArithOperatorTypeRule */
-class IntOperatorTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- TNode::iterator child_it = n.begin();
- TNode::iterator child_it_end = n.end();
- if(check) {
- for(; child_it != child_it_end; ++child_it) {
- TypeNode childType = (*child_it).getType(check);
- if (!childType.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
- }
- }
- }
- return nodeManager->integerType();
- }
-};/* class IntOperatorTypeRule */
-
-class RealOperatorTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- TNode::iterator child_it = n.begin();
- TNode::iterator child_it_end = n.end();
- if(check) {
- for(; child_it != child_it_end; ++child_it) {
- TypeNode childType = (*child_it).getType(check);
- if (!childType.isReal()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a real subterm");
- }
- }
- }
- return nodeManager->realType();
- }
-};/* class RealOperatorTypeRule */
-
-class ArithPredicateTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode lhsType = n[0].getType(check);
- if (!lhsType.isReal()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
- }
- TypeNode rhsType = n[1].getType(check);
- if (!rhsType.isReal()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
- }
- }
- return nodeManager->booleanType();
- }
-};/* class ArithPredicateTypeRule */
-
-class ArithUnaryPredicateTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isReal()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term");
- }
- }
- return nodeManager->booleanType();
- }
-};/* class ArithUnaryPredicateTypeRule */
-
-class IntUnaryPredicateTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term");
- }
- }
- return nodeManager->booleanType();
- }
-};/* class IntUnaryPredicateTypeRule */
-
class RealNullaryOperatorTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
}
};/* class RealNullaryOperatorTypeRule */
-class DivisibleOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::DIVISIBLE_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class DivisibleOpTypeRule */
-
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
### type rules for parameterized operator kinds -------------------------------
-typerule BITVECTOR_BITOF_OP ::CVC4::theory::bv::BitVectorBitOfOpTypeRule
+typerule BITVECTOR_BITOF_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
-typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
+typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
-typerule BITVECTOR_REPEAT_OP ::CVC4::theory::bv::BitVectorRepeatOpTypeRule
+typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
-typerule BITVECTOR_ROTATE_LEFT_OP ::CVC4::theory::bv::BitVectorRotateLeftOpTypeRule
+typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_ROTATE_RIGHT_OP ::CVC4::theory::bv::BitVectorRotateRightOpTypeRule
+typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SIGN_EXTEND_OP ::CVC4::theory::bv::BitVectorSignExtendOpTypeRule
+typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
-typerule BITVECTOR_ZERO_EXTEND_OP ::CVC4::theory::bv::BitVectorZeroExtendOpTypeRule
+typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
/* parameterized operator kinds */
/* -------------------------------------------------------------------------- */
-class BitVectorBitOfOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_BITOF_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorBitOfOpTypeRule */
-
class BitVectorBitOfTypeRule
{
public:
}
}; /* class BitVectorBitOfTypeRule */
-class BitVectorExtractOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorExtractOpTypeRule */
-
class BitVectorExtractTypeRule
{
public:
}
}; /* class BitVectorExtractTypeRule */
-class BitVectorRepeatOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_REPEAT_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorRepeatOpTypeRule */
-
class BitVectorRepeatTypeRule
{
public:
}
}; /* class BitVectorRepeatTypeRule */
-class BitVectorRotateLeftOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorRotateLeftOpTypeRule */
-
-class BitVectorRotateRightOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorRotateRightOpTypeRule */
-
-class BitVectorSignExtendOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_SIGN_EXTEND_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorSignExtendOpTypeRule */
-
-class BitVectorZeroExtendOpTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- Assert(n.getKind() == kind::BITVECTOR_ZERO_EXTEND_OP);
- return nodeManager->builtinOperatorType();
- }
-}; /* class BitVectorZeroExtendOpTypeRule */
-
class BitVectorExtendTypeRule
{
public:
"util/regexp.h" \
"a string of characters"
-typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
+typerule CONST_STRING "SimpleTypeRule<RString>"
# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
#internal
operator REGEXP_RV 1 "regexp rv (internal use only)"
-typerule REGEXP_RV ::CVC4::theory::strings::RegExpRVTypeRule
+typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>"
#typerules
-typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
-typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
-typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
-typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
-typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
-typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
+typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_INTER "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>"
+typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>"
+typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
-typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
-
-typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
-
-typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
-typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
-typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
-typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule
-typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule
-typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule
-typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
-typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
-typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule
-typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
-typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
-typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
-typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
-typerule STRING_CODE ::CVC4::theory::strings::StringStrToIntTypeRule
-typerule STRING_TOUPPER ::CVC4::theory::strings::StringStrToStrTypeRule
-typerule STRING_TOLOWER ::CVC4::theory::strings::StringStrToStrTypeRule
-
-typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
-
-typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
-typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule
+typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp, AInteger, AOptional<AInteger>>"
+
+typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
+
+typerule STRING_CONCAT "SimpleTypeRuleVar<RString, AString>"
+typerule STRING_LENGTH "SimpleTypeRule<RInteger, AString>"
+typerule STRING_SUBSTR "SimpleTypeRule<RString, AString, AInteger, AInteger>"
+typerule STRING_CHARAT "SimpleTypeRule<RString, AString, AInteger>"
+typerule STRING_STRCTN "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_LT "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_LEQ "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_STRIDOF "SimpleTypeRule<RInteger, AString, AString, AInteger>"
+typerule STRING_STRREPL "SimpleTypeRule<RString, AString, AString, AString>"
+typerule STRING_STRREPLALL "SimpleTypeRule<RString, AString, AString, AString>"
+typerule STRING_PREFIX "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
+typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
+typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
+typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
+typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
+
+typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
+
+typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
+typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
endtheory
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
- ** \brief Typing and cardinality rules for the theory of arrays
+ ** \brief Typing rules for the theory of strings and regexps
**
- ** Typing and cardinality rules for the theory of arrays.
+ ** Typing rules for the theory of strings and regexps
**/
#include "cvc4_private.h"
namespace theory {
namespace strings {
-class StringConstantTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- return nodeManager->stringType();
- }
-};
-
-class StringConcatTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ){
- TNode::iterator it = n.begin();
- TNode::iterator it_end = n.end();
- int size = 0;
- for (; it != it_end; ++ it) {
- TypeNode t = (*it).getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
- }
- ++size;
- }
- if(size < 2) {
- throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
- }
- }
- return nodeManager->stringType();
- }
-};
-
-class StringLengthTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
- }
- }
- return nodeManager->integerType();
- }
-};
-
-class StringSubstrTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
- }
- t = n[1].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
- }
- t = n[2].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
- }
- }
- return nodeManager->stringType();
- }
-};
-
-class StringRelationTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(
- n, "expecting a string term in string relation");
- }
- t = n[1].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(
- n, "expecting a string term in string relation");
- }
- }
- return nodeManager->booleanType();
- }
-};
-
-class StringCharAtTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
- }
- t = n[1].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
- }
- }
- return nodeManager->stringType();
- }
-};
-
-class StringIndexOfTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
- }
- t = n[1].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
- }
- t = n[2].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
- }
- }
- return nodeManager->integerType();
- }
-};
-
-class StringReplaceTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
- }
- t = n[1].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
- }
- t = n[2].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
- }
- }
- return nodeManager->stringType();
- }
-};
-
-class StringPrefixOfTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
- }
- t = n[1].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
- }
- }
- return nodeManager->booleanType();
- }
-};
-
-class StringSuffixOfTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
- }
- t = n[1].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
- }
- }
- return nodeManager->booleanType();
- }
-};
-
-class StringIntToStrTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
- }
- }
- return nodeManager->stringType();
- }
-};
-
-class StringStrToIntTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- std::stringstream ss;
- ss << "expecting a string term in argument of " << n.getKind();
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- return nodeManager->integerType();
- }
-};
-
-class StringStrToStrTypeRule
-{
- public:
- inline static TypeNode computeType(NodeManager* nodeManager,
- TNode n,
- bool check)
- {
- if (check)
- {
- TypeNode t = n[0].getType(check);
- if (!t.isString())
- {
- std::stringstream ss;
- ss << "expecting a string term in argument of " << n.getKind();
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- return nodeManager->stringType();
- }
-};
-
-class RegExpConcatTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TNode::iterator it = n.begin();
- TNode::iterator it_end = n.end();
- int size = 0;
- for (; it != it_end; ++ it) {
- TypeNode t = (*it).getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
- }
- ++size;
- }
- if(size < 2) {
- throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-class RegExpUnionTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TNode::iterator it = n.begin();
- TNode::iterator it_end = n.end();
- for (; it != it_end; ++ it) {
- TypeNode t = (*it).getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
- }
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-class RegExpInterTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TNode::iterator it = n.begin();
- TNode::iterator it_end = n.end();
- for (; it != it_end; ++ it) {
- TypeNode t = (*it).getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
- }
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-class RegExpStarTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-class RegExpPlusTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-class RegExpOptTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
- }
- }
- return nodeManager->regExpType();
- }
-};
-
class RegExpRangeTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
}
};
-class RegExpLoopTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TNode::iterator it = n.begin();
- TNode::iterator it_end = n.end();
- TypeNode t = (*it).getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
- }
- ++it; t = (*it).getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
- }
- //if(!(*it).isConst()) {
- //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
- //}
- ++it;
- if(it != it_end) {
- t = (*it).getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
- }
- //if(!(*it).isConst()) {
- //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
- //}
- //if(++it != it_end) {
- // throw TypeCheckingExceptionPrivate(n, "too many regexp");
- //}
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-class StringToRegExpTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting string terms");
- }
- //if( (*it).getKind() != kind::CONST_STRING ) {
- // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
- //}
- }
- return nodeManager->regExpType();
- }
-};
-
-class StringInRegExpTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TNode::iterator it = n.begin();
- TypeNode t = (*it).getType(check);
- if (!t.isString()) {
- throw TypeCheckingExceptionPrivate(n, "expecting string terms");
- }
- ++it;
- t = (*it).getType(check);
- if (!t.isRegExp()) {
- throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
- }
- }
- return nodeManager->booleanType();
- }
-};
-
-class EmptyRegExpTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- Assert(n.getKind() == kind::REGEXP_EMPTY);
- return nodeManager->regExpType();
- }
-};
-
-class SigmaRegExpTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- Assert(n.getKind() == kind::REGEXP_SIGMA);
- return nodeManager->regExpType();
- }
-};
-
-class RegExpRVTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- {
- if( check ) {
- TypeNode t = n[0].getType(check);
- if (!t.isInteger()) {
- throw TypeCheckingExceptionPrivate(n, "expecting an integer term in RV");
- }
- }
- return nodeManager->regExpType();
- }
-};
-
-
}/* CVC4::theory::strings namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff