blob: 6a32969e309e3e0e5dce5c8d03991c9ce09a5767 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_QUANTIFIERS ::CVC5::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
properties check presolve
rewriter ::CVC5::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"
operator INST_ATTRIBUTE 1 "instantiation attribute"
operator INST_POOL 1: "instantiation pool"
operator INST_ADD_TO_POOL 2 "instantiation add to pool"
operator SKOLEM_ADD_TO_POOL 2 "skolemization add to pool"
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 ::CVC5::theory::quantifiers::QuantifierTypeRule
typerule EXISTS ::CVC5::theory::quantifiers::QuantifierTypeRule
typerule BOUND_VAR_LIST ::CVC5::theory::quantifiers::QuantifierBoundVarListTypeRule
typerule INST_PATTERN_LIST ::CVC5::theory::quantifiers::QuantifierInstPatternListTypeRule
typerule INST_PATTERN ::CVC5::theory::quantifiers::QuantifierInstPatternTypeRule
typerule INST_NO_PATTERN ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
typerule INST_ATTRIBUTE ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
typerule INST_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
typerule INST_ADD_TO_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
typerule SKOLEM_ADD_TO_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
endtheory
|
