From 34e84a25a044e3af192bb69089467c2125911900 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 28 Oct 2017 09:13:13 -0500
Subject: Document term db (#1220)

* Document TermDb and related classes. Minor changes to quantifiers utils and their interface.  Address some comments left over from PR 1206.

* Minor

* Minor

* Change namespace style.

* Address review

* Fix incorrectly merged portion that led to regression failures.

* New clang format, fully document relevant domain.

* Clang format again.

* Minor
---
 src/theory/quantifiers/quantifiers_attributes.h | 63 +++++++++++++++++--------
 1 file changed, 44 insertions(+), 19 deletions(-)

(limited to 'src/theory/quantifiers/quantifiers_attributes.h')

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 1c35b646b..b618fc5d5 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -61,34 +61,53 @@ namespace quantifiers {
 //struct RrPriorityAttributeId {};
 //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
 
-
-/** This class stores attributes for quantified formulas 
-* TODO : document (as part of #1171, #1215)
-*/
-class QAttributes{
-public:
+/** This struct stores attributes for a single quantified formula */
+struct QAttributes
+{
+ public:
   QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
                   d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
   ~QAttributes(){}
+  /** does the quantified formula have a pattern? */
   bool d_hasPattern;
+  /** if non-null, this is the rewrite rule representation of the quantified
+   * formula */
   Node d_rr;
+  /** is this formula marked a conjecture? */
   bool d_conjecture;
+  /** is this formula marked an axiom? */
   bool d_axiom;
+  /** if non-null, this quantified formula is a function definition for function
+   * d_fundef_f */
   Node d_fundef_f;
+  /** is this formula marked as a sygus conjecture? */
   bool d_sygus;
+  /** is this formula marked as a synthesis (non-sygus) conjecture? */
   bool d_synthesis;
+  /** if a rewrite rule, then this is the priority value for the rewrite rule */
   int d_rr_priority;
+  /** stores the maximum instantiation level allowed for this quantified formula
+   * (-1 means allow any) */
   int d_qinstLevel;
+  /** is this formula marked for quantifier elimination? */
   bool d_quant_elim;
+  /** is this formula marked for partial quantifier elimination? */
   bool d_quant_elim_partial;
+  /** the instantiation pattern list for this quantified formula (its 3rd child)
+   */
   Node d_ipl;
+  /** the quantifier id associated with this formula */
   Node d_qid_num;
+  /** is this quantified formula a rewrite rule? */
   bool isRewriteRule() { return !d_rr.isNull(); }
+  /** is this quantified formula a function definition? */
   bool isFunDef() { return !d_fundef_f.isNull(); }
 };
 
-/** This class caches information about attributes of quantified formulas 
-* It also has static utility functions used for determining attributes and information about 
+/** This class caches information about attributes of quantified formulas
+*
+* It also has static utility functions used for determining attributes and
+* information about
 * quantified formulas.
 */
 class QuantAttributes
@@ -96,14 +115,23 @@ class QuantAttributes
 public:
   QuantAttributes( QuantifiersEngine * qe );
   ~QuantAttributes(){}
-  
   /** set user attribute
-    *   This function will apply a custom set of attributes to all top-level universal
-    *   quantifiers contained in n
-    */
-  static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value );
-  
-  //general queries concerning quantified formulas wrt modules
+  * This function applies an attribute
+  * This can be called when we mark expressions with attributes, e.g. (! q
+  * :attribute attr [node_values, str_value...]),
+  * It can also be called internally in various ways (for SyGus, quantifier
+  * elimination, etc.)
+  */
+  static void setUserAttribute(const std::string& attr,
+                               Node q,
+                               std::vector<Node>& node_values,
+                               std::string str_value);
+
+  /** compute quantifier attributes */
+  static void computeQuantAttributes(Node q, QAttributes& qa);
+  /** compute the attributes for q */
+  void computeAttributes(Node q);
+
   /** is quantifier treated as a rewrite rule? */
   static bool checkRewriteRule( Node q );
   /** get the rewrite rule associated with the quanfied formula */
@@ -145,10 +173,7 @@ public:
   int getQuantIdNum( Node q );
   /** get quant id num */
   Node getQuantIdNumNode( Node q );
-  /** compute quantifier attributes */
-  static void computeQuantAttributes( Node q, QAttributes& qa );
-  /** compute the attributes for q */
-  void computeAttributes( Node q );
+
 private:
   /** pointer to quantifiers engine */
   QuantifiersEngine * d_quantEngine;
-- 
cgit v1.2.3