From ef8e8f34d7df54142f35dad80a09822235153f70 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 20 Feb 2018 15:21:57 -0800 Subject: [PATCH] Improve documentation of bv::utils::isCoreTerm (#1617) --- src/theory/bv/theory_bv_utils.h | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) 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); -- 2.30.2