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 ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
   8 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
   9
  10 properties check propagate presolve getNextDecisionRequest
  11
  12 rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
  13
  14 operator FORALL 2:3 "universally quantified formula"
  15
  16 operator EXISTS 2:3 "existentially quantified formula"
  17
  18 variable INST_CONSTANT "instantiation constant"
  19
  20 sort BOUND_VAR_LIST_TYPE \
  21     Cardinality::INTEGERS \
  22     not-well-founded \
  23     "Bound Var type"
  24
  25 operator BOUND_VAR_LIST 1: "bound variables"
  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
  37 sort INST_PATTERN_LIST_TYPE \
  38     Cardinality::INTEGERS \
  39     not-well-founded \
  40     "Instantiation pattern list type"
  41
  42 # a list of instantiation patterns
  43 operator INST_PATTERN_LIST 1: "instantiation pattern list"
  44
  45 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule
  46 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule
  47 typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule
  48 typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
  49 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
  50
  51 endtheory