diff options
Diffstat (limited to 'src/theory/quantifiers/kinds')
| -rw-r--r-- | src/theory/quantifiers/kinds | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 106d95cef..c81816528 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -8,7 +8,7 @@ theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory typechecker "theory/quantifiers/theory_quantifiers_type_rules.h" instantiator ::CVC4::theory::quantifiers::InstantiatorTheoryQuantifiers "theory/quantifiers/theory_quantifiers_instantiator.h" -properties check propagate presolve +properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h" @@ -30,6 +30,9 @@ sort INST_PATTERN_TYPE \ 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" sort INST_PATTERN_LIST_TYPE \ @@ -37,6 +40,7 @@ sort INST_PATTERN_LIST_TYPE \ not-well-founded \ "Instantiation pattern list type" +# a list of instantiation patterns operator INST_PATTERN_LIST 1: "instantiation pattern list" typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule |