GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bv_gauss.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_gauss.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mathias Preiner, Andres Noetzli
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Gaussian Elimination preprocessing pass.
13
 **
14
 ** Simplify a given equation system modulo a (prime) number via Gaussian
15
 ** Elimination if possible.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
21
#define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
22
23
#include "expr/node.h"
24
#include "preprocessing/preprocessing_pass.h"
25
26
namespace CVC4 {
27
namespace preprocessing {
28
namespace passes {
29
30
17994
class BVGauss : public PreprocessingPass
31
{
32
 public:
33
  BVGauss(PreprocessingPassContext* preprocContext,
34
          const std::string& name = "bv-gauss");
35
36
 protected:
37
  /**
38
   * Apply Gaussian Elimination on (possibly multiple) set(s) of equations
39
   * modulo some (prime) number given as bit-vector equations.
40
   *
41
   * Note that these sets of equations do not have to be modulo some prime
42
   * but can be modulo any arbitrary number. However, GE is guaranteed to
43
   * succeed modulo a prime number, which is not necessarily the case if a
44
   * given set of equations is modulo a non-prime number.
45
   */
46
  PreprocessingPassResult applyInternal(
47
      AssertionPipeline* assertionsToPreprocess) override;
48
49
 private:
50
  /* Note: The following functionality is only exposed for unit testing in
51
   * pass_bv_gauss_white.h. */
52
53
  /**
54
   *  Represents the result of Gaussian Elimination where the solution
55
   *  of the given equation system is
56
   *
57
   *   INVALID ... i.e., NOT of the form c1*x1 + c2*x2 + ... % p = b,
58
   *               where ci, b and p are
59
   *                 - bit-vector constants
60
   *                 - extracts or zero extensions on bit-vector constants
61
   *                 - of arbitrary nesting level
62
   *               and p is co-prime to all bit-vector constants for which
63
   *               a multiplicative inverse has to be computed.
64
   *
65
   *   UNIQUE  ... determined for all unknowns, e.g., x = 4
66
   *
67
   *   PARTIAL ... e.g., x = 4 - 2z
68
   *
69
   *   NONE    ... no solution
70
   *
71
   *   Given a matrix A representing an equation system, the resulting
72
   *   matrix B after applying GE represents, e.g.:
73
   *
74
   *   B = 1 0 0 2 <-    UNIQUE
75
   *       0 1 0 3 <-
76
   *       0 0 1 1 <-
77
   *
78
   *   B = 1 0 2 4 <-    PARTIAL
79
   *       0 1 3 2 <-
80
   *       0 0 1 1
81
   *
82
   *   B = 1 0 0 1       NONE
83
   *       0 1 1 2
84
   *       0 0 0 2 <-
85
   */
86
  enum class Result
87
  {
88
    INVALID,
89
    UNIQUE,
90
    PARTIAL,
91
    NONE
92
  };
93
94
  static Result gaussElim(Integer prime,
95
                          std::vector<Integer>& rhs,
96
                          std::vector<std::vector<Integer>>& lhs);
97
98
  static Result gaussElimRewriteForUrem(
99
      const std::vector<Node>& equations,
100
      std::unordered_map<Node, Node, NodeHashFunction>& res);
101
102
  static unsigned getMinBwExpr(Node expr);
103
};
104
105
}  // namespace passes
106
}  // namespace preprocessing
107
}  // namespace CVC4
108
109
#endif