Fix BVGauss unit tests. (#3142)

pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the
anonymous namespace, which resulted in ODR (one definition rule)
violations reported by ASAN.

This commit exposes the functionality required in the unit tests as
private static members of the BVGauss class. Since this is a white unit
test, we can access private members in the tests.

1 files changed, 58 insertions, 3 deletions

diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 862777a9b..93d61be9e 100644
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -30,7 +30,7 @@ namespace passes {
 class BVGauss : public PreprocessingPass
 {
  public:
-   BVGauss(PreprocessingPassContext* preprocContext);
+  BVGauss(PreprocessingPassContext* preprocContext);
 
  protected:
   /**
@@ -42,8 +42,63 @@ class BVGauss : public PreprocessingPass
    * succeed modulo a prime number, which is not necessarily the case if a
    * given set of equations is modulo a non-prime number.
    */
-   PreprocessingPassResult applyInternal(
-       AssertionPipeline* assertionsToPreprocess) override;
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  /* Note: The following functionality is only exposed for unit testing in
+   * pass_bv_gauss_white.h. */
+
+  /**
+   *  Represents the result of Gaussian Elimination where the solution
+   *  of the given equation system is
+   *
+   *   INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b,
+   *               where ci, b and p are
+   *                 - bit-vector constants
+   *                 - extracts or zero extensions on bit-vector constants
+   *                 - of arbitrary nesting level
+   *               and p is co-prime to all bit-vector constants for which
+   *               a multiplicative inverse has to be computed.
+   *
+   *   UNIQUE  ... determined for all unknowns, e.g., x = 4
+   *
+   *   PARTIAL ... e.g., x = 4 - 2z
+   *
+   *   NONE    ... no solution
+   *
+   *   Given a matrix A representing an equation system, the resulting
+   *   matrix B after applying GE represents, e.g.:
+   *
+   *   B = 1 0 0 2 <-    UNIQUE
+   *       0 1 0 3 <-
+   *       0 0 1 1 <-
+   *
+   *   B = 1 0 2 4 <-    PARTIAL
+   *       0 1 3 2 <-
+   *       0 0 1 1
+   *
+   *   B = 1 0 0 1       NONE
+   *       0 1 1 2
+   *       0 0 0 2 <-
+   */
+  enum class Result
+  {
+    INVALID,
+    UNIQUE,
+    PARTIAL,
+    NONE
+  };
+
+  static Result gaussElim(Integer prime,
+                          std::vector<Integer>& rhs,
+                          std::vector<std::vector<Integer>>& lhs);
+
+  static Result gaussElimRewriteForUrem(
+      const std::vector<Node>& equations,
+      std::unordered_map<Node, Node, NodeHashFunction>& res);
+
+  static unsigned getMinBwExpr(Node expr);
 };
 
 }  // namespace passes