src/theory/quantifiers/kinds

   1 # kinds                                                               -*- sh -*-
   2 #
   3 # For documentation on this file format, please refer to
   4 # src/theory/builtin/kinds.
   5 #
   6
   7 theory THEORY_QUANTIFIERS ::cvc5::internal::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
   8 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
   9
  10 properties check presolve
  11
  12 rewriter ::cvc5::internal::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
  13
  14 operator FORALL 2:3 "universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST"
  15
  16 operator EXISTS 2:3 "existentially quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST"
  17
  18 variable INST_CONSTANT "instantiation constant"
  19
  20 sort BOUND_VAR_LIST_TYPE \
  21     Cardinality::INTEGERS \
  22     not-well-founded \
  23     "the type of bound variable lists"
  24
  25 operator BOUND_VAR_LIST 1: "a list of bound variables (used to bind variables under a quantifier)"
  26
  27 sort INST_PATTERN_TYPE \
  28     Cardinality::INTEGERS \
  29     not-well-founded \
  30     "instantiation pattern type"
  31
  32 # Instantiation pattern, also called trigger.
  33 # This node is used for specifying hints for quantifier instantiation.
  34 # An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger.
  35 operator INST_PATTERN 1: "instantiation pattern"
  36 operator INST_NO_PATTERN 1 "instantiation no-pattern"
  37 operator INST_ATTRIBUTE 1: "instantiation attribute"
  38 operator INST_POOL 1: "instantiation pool"
  39 operator INST_ADD_TO_POOL 2 "instantiation add to pool"
  40 operator SKOLEM_ADD_TO_POOL 2 "skolemization add to pool"
  41
  42 sort INST_PATTERN_LIST_TYPE \
  43     Cardinality::INTEGERS \
  44     not-well-founded \
  45     "the type of instantiation pattern lists"
  46
  47 # a list of instantiation patterns
  48 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
  49
  50 typerule FORALL ::cvc5::internal::theory::quantifiers::QuantifierTypeRule
  51 typerule EXISTS ::cvc5::internal::theory::quantifiers::QuantifierTypeRule
  52 typerule BOUND_VAR_LIST ::cvc5::internal::theory::quantifiers::QuantifierBoundVarListTypeRule
  53 typerule INST_PATTERN_LIST ::cvc5::internal::theory::quantifiers::QuantifierInstPatternListTypeRule
  54
  55 typerule INST_PATTERN ::cvc5::internal::theory::quantifiers::QuantifierInstPatternTypeRule
  56 typerule INST_NO_PATTERN ::cvc5::internal::theory::quantifiers::QuantifierAnnotationTypeRule
  57 typerule INST_ATTRIBUTE ::cvc5::internal::theory::quantifiers::QuantifierAnnotationTypeRule
  58 typerule INST_POOL ::cvc5::internal::theory::quantifiers::QuantifierAnnotationTypeRule
  59 typerule INST_ADD_TO_POOL ::cvc5::internal::theory::quantifiers::QuantifierAnnotationTypeRule
  60 typerule SKOLEM_ADD_TO_POOL ::cvc5::internal::theory::quantifiers::QuantifierAnnotationTypeRule
  61
  62 endtheory