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 # for rewrite rules
  52 # types...
  53 sort RRHB_TYPE \
  54     Cardinality::INTEGERS \
  55     not-well-founded \
  56     "head and body of the rule type"
  57
  58 # operators...
  59
  60 # variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
  61 operator REWRITE_RULE 3 "general rewrite rule"
  62 #HEAD/BODY/TRIGGER
  63 operator RR_REWRITE 2:3 "actual rewrite rule"
  64 operator RR_REDUCTION 2:3 "actual reduction rule"
  65 operator RR_DEDUCTION 2:3 "actual deduction rule"
  66
  67 typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule
  68 typerule RR_REWRITE   ::CVC4::theory::quantifiers::RRRewriteTypeRule
  69 typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
  70 typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
  71
  72 endtheory