From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 20 Jun 2014 23:59:54 +0000 (-0400)
Subject: Quantifiers kinds documentation
X-Git-Tag: cvc5-1.0.0~6726^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=88ff88ba783aa91895e6b03ef21287a051ae9c99;p=cvc5.git

Quantifiers kinds documentation
---

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 795bc1ab4..6fb480c3d 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -11,23 +11,23 @@ properties check propagate presolve getNextDecisionRequest
 
 rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
 
-operator FORALL 2:3 "universally quantified formula"
+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"
+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 \
-    "Bound Var type"
+    "the type of bound variable lists"
 
-operator BOUND_VAR_LIST 1: "bound variables"
+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 type"
 
 # Instantiation pattern, also called trigger.
 # This node is used for specifying hints for quantifier instantiation.
@@ -37,10 +37,10 @@ operator INST_PATTERN 1: "instantiation pattern"
 sort INST_PATTERN_LIST_TYPE \
     Cardinality::INTEGERS \
     not-well-founded \
-    "Instantiation pattern list type"
+    "the type of instantiation pattern lists"
 
 # a list of instantiation patterns
-operator INST_PATTERN_LIST 1: "instantiation pattern list"
+operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
@@ -53,16 +53,16 @@ typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternLis
 sort RRHB_TYPE \
     Cardinality::INTEGERS \
     not-well-founded \
-    "head and body of the rule type"
+    "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"
+operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)"
 #HEAD/BODY/TRIGGER
-operator RR_REWRITE 2:3 "actual rewrite rule"
-operator RR_REDUCTION 2:3 "actual reduction rule"
-operator RR_DEDUCTION 2:3 "actual deduction rule"
+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