bv2int: quantifiers support (#5080)

This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index b84726878..41d8f4904 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -254,6 +254,16 @@ class BVToInt : public PreprocessingPass
   void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess);
 
   /**
+   * @param quantifiedNode a node whose main operator is forall/exists.
+   * @return a node opbtained from quantifiedNode by:
+   * 1. Replacing all bound BV variables by new bound integer variables.
+   * 2. Add range constraints for the new variables, induced by the original
+   * bit-width. These range constraints are added with "AND" in case of exists
+   * and with "IMPLIES" in case of forall.
+   */
+  Node translateQuantifiedFormula(Node quantifiedNode);
+
+  /**
    * Reconstructs a node whose main operator cannot be
    * translated to integers.
    * Reconstruction is done by casting to integers/bit-vectors