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; 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
  39 sort INST_PATTERN_LIST_TYPE \
  40     Cardinality::INTEGERS \
  41     not-well-founded \
  42     "the type of instantiation pattern lists"
  43
  44 # a list of instantiation patterns
  45 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
  46
  47 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule
  48 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule
  49 typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule
  50 typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
  51 typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule
  52 typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule
  53 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule
  54
  55 # for rewrite rules
  56 # types...
  57 sort RRHB_TYPE \
  58     Cardinality::INTEGERS \
  59     not-well-founded \
  60     "head and body of the rule type (for rewrite-rules theory)"
  61
  62 # operators...
  63
  64 # variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
  65 operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)"
  66 #HEAD/BODY/TRIGGER
  67 operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)"
  68 operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)"
  69 operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)"
  70
  71 typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule
  72 typerule RR_REWRITE   ::CVC4::theory::quantifiers::RRRewriteTypeRule
  73 typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
  74 typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
  75
  76 endtheory