From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 20 Feb 2018 23:21:57 +0000 (-0800)
Subject: Improve documentation of bv::utils::isCoreTerm (#1617)
X-Git-Tag: cvc5-1.0.0~5275
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ef8e8f34d7df54142f35dad80a09822235153f70;p=cvc5.git

Improve documentation of bv::utils::isCoreTerm (#1617)
---

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 4bf84525d..e4bf90462 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -54,20 +54,28 @@ unsigned getSignExtendAmount(TNode node);
 
 /* Returns true if given node represents a zero bit-vector.  */
 bool isZero(TNode node);
+
 /* If node is a constant of the form 2^c or -2^c, then this function returns
  * c+1. Otherwise, this function returns 0. The flag isNeg is updated to
  * indicate whether node is negative.  */
 unsigned isPow2Const(TNode node, bool& isNeg);
+
 /* Returns true if node or all of its children is const. */
 bool isBvConstTerm(TNode node);
+
 /* Returns true if node is a predicate over bit-vector nodes. */
 bool isBVPredicate(TNode node);
-/* Returns true if given term is a THEORY_BV \Sigma_core term.
- * \Sigma_core = { concat, extract, =, bv constants, bv variables } */
+
+/* Returns true if given term is
+ *   - not a THEORY_BV term
+ *   - a THEORY_BV \Sigma_core term, where
+ *     \Sigma_core = { concat, extract, =, bv constants, bv variables } */
 bool isCoreTerm(TNode term, TNodeBoolMap& cache);
+
 /* Returns true if given term is a THEORY_BV \Sigma_equality term.
  * \Sigma_equality = { =, bv constants, bv variables }  */
 bool isEqualityTerm(TNode term, TNodeBoolMap& cache);
+
 /* Returns true if given node is an atom that is bit-blasted.  */
 bool isBitblastAtom(Node lit);