diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-09 22:06:57 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-09 22:06:57 -0700 |
commit | ccca2e76be3412fc24e1bb0a4eccae1133e519f4 (patch) | |
tree | 9c3953d7ef494eab54f5e0ea6e9f586c40121908 /src | |
parent | 5cbc35e70c2a80094dade1a58605882e3eb1d326 (diff) |
Document bv-to-bool recursion (#3848)
The BV-to-bool pass is implemented recursively.
This commit documents that.
We may want to change it at some point.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/bv_to_bool.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 0637c541f..de9504503 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -12,6 +12,7 @@ ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. ** ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** Implemented recursively. **/ #include "preprocessing/passes/bv_to_bool.h" @@ -258,6 +259,7 @@ Node BVToBool::liftNode(TNode current) } for (unsigned i = 0; i < current.getNumChildren(); ++i) { + // Recursively lift children Node converted = liftNode(current[i]); Assert(converted.getType() == current[i].getType()); builder << converted; |