From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Tue, 10 Mar 2020 05:06:57 +0000 (-0700)
Subject: Document bv-to-bool recursion (#3848)
X-Git-Tag: cvc5-1.0.0~3536
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ccca2e76be3412fc24e1bb0a4eccae1133e519f4;p=cvc5.git

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.
---

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;