1 files changed, 28 insertions, 34 deletions

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index a44d64904..ce2a58695 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -44,47 +44,22 @@ class BvInverterQuery
   virtual Node getBoundVariable(TypeNode tn) = 0;
 };
 
-// class for storing information about the solved status
-class BvInverterStatus {
- public:
-  BvInverterStatus() : d_status(0) {}
-  ~BvInverterStatus() {}
-  int d_status;
-};
-
 // inverter class
 // TODO : move to theory/bv/ if generally useful?
-class BvInverter {
+class BvInverter
+{
  public:
   BvInverter() {}
   ~BvInverter() {}
   /** get dummy fresh variable of type tn, used as argument for sv */
   Node getSolveVariable(TypeNode tn);
 
-  /** get inversion node
-   *
-   * This expects a condition cond where:
-   *   (exists x. cond)
-   * is a BV tautology where x is getSolveVariable( tn ).
-   *
-   * It returns a term of the form:
-   *   (choice y. cond { x -> y })
-   * where y is a bound variable and x is getSolveVariable( tn ).
-   *
-   * In some cases, we may return a term t
-   * if cond implies an equality on the solve variable.
-   * For example, if cond is x = t where x is
-   * getSolveVariable( tn ), then we return t
-   * instead of introducing the choice function.
-   */
-  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
-
   /** Get path to pv in lit, replace that occurrence by sv and all others by
    * pvs. If return value R is non-null, then : lit.path = pv R.path = sv
    *   R.path' = pvs for all lit.path' = pv, where path' != path
    */
-  Node getPathToPv(Node lit, Node pv, Node sv, Node pvs,
-                   std::vector<unsigned>& path);
+  Node getPathToPv(
+      Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path);
 
   /** solveBvLit
    * solve for sv in lit, where lit.path = sv
@@ -93,16 +68,35 @@ class BvInverter {
   Node solveBvLit(Node sv,
                   Node lit,
                   std::vector<unsigned>& path,
-                  BvInverterQuery* m,
-                  BvInverterStatus& status);
+                  BvInverterQuery* m);
 
  private:
-  /** dummy variables for each type */
+  /** Dummy variables for each type */
   std::map<TypeNode, Node> d_solve_var;
 
-  /** helper function for getPathToPv */
-  Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
+  /** Helper function for getPathToPv */
+  Node getPathToPv(Node lit,
+                   Node pv,
+                   Node sv,
+                   std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
+
+  /** Helper function for getInv.
+   *
+   * This expects a condition cond where:
+   *   (exists x. cond)
+   * is a BV tautology where x is getSolveVariable( tn ).
+   *
+   * It returns a term of the form:
+   *   (choice y. cond { x -> y })
+   * where y is a bound variable and x is getSolveVariable( tn ).
+   *
+   * In some cases, we may return a term t if cond implies an equality on
+   * the solve variable. For example, if cond is x = t where x is
+   * getSolveVariable(tn), then we return t instead of introducing the choice
+   * function.
+   */
+  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
 };
 
 }  // namespace quantifiers