From ccca2e76be3412fc24e1bb0a4eccae1133e519f4 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 9 Mar 2020 22:06:57 -0700 Subject: 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. --- src/preprocessing/passes/bv_to_bool.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') 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; -- cgit v1.2.3