diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-08-31 16:48:20 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-08-31 16:48:20 +0000 |
| commit | 3c4935c7c0c6774588af94c82307a960e58a1154 (patch) | |
| tree | e518c60ec182e91300fe53293c42cd4b85e49d29 /src/theory/quantifiers/kinds | |
| parent | ec9e426df607f13e5a0c0f52fbc6ed5dbb79fdf9 (diff) | |
merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
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 |