diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-20 15:21:57 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-20 15:21:57 -0800 |
commit | ef8e8f34d7df54142f35dad80a09822235153f70 (patch) | |
tree | 19bebaef46714a7cb8d98bcabe496ca4d28e7b7b /src/theory/bv | |
parent | 52ea3ae37d71393d8cb4d213465a2aec44863c4d (diff) |
Improve documentation of bv::utils::isCoreTerm (#1617)
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 12 |
1 files 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); |