# kinds                                                               -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#

theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"

properties check propagate presolve getNextDecisionRequest

rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"

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"

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"

variable INST_CONSTANT "instantiation constant"

sort BOUND_VAR_LIST_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "the type of bound variable lists"

operator BOUND_VAR_LIST 1: "a list of bound variables (used to bind variables under a quantifier)"

sort INST_PATTERN_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "instantiation pattern type"

# Instantiation pattern, also called trigger.
# This node is used for specifying hints for quantifier instantiation.
# An instantiation pattern may have more than 1 child, in which case it specifies a multi-trigger.
operator INST_PATTERN 1: "instantiation pattern"
operator INST_NO_PATTERN 1 "instantiation no-pattern"

sort INST_PATTERN_LIST_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "the type of instantiation pattern lists"

# a list of instantiation patterns
operator INST_PATTERN_LIST 1: "a list of instantiation patterns"

typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule 
typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule 
typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule 
typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 

# for rewrite rules
# types...
sort RRHB_TYPE \
    Cardinality::INTEGERS \
    not-well-founded \
    "head and body of the rule type (for rewrite-rules theory)"

# operators...

# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)"
#HEAD/BODY/TRIGGER
operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)"
operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)"
operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)"

typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule
typerule RR_REWRITE   ::CVC4::theory::quantifiers::RRRewriteTypeRule
typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule

endtheory