-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- The structure `DefaultFormula n` takes in a parameter `n` which is intended to be one greater than the total number of variables that
can appear in the formula (hence why the parameter `n` is called `numVarsSucc` below). The structure has 4 fields:
- The `clauses` field maintains the total set of clauses that appear in the formula. Additionally, when a default formula is created
  by parsing a CNF file and modified by a series of LRAT additions and deletions, the following informal invariant is maintained:
  1. `clauses[0]` is always set to `none`.
  2. The m clauses in the original CNF file are stored in indices 1 through m of the `clauses` field (and they are stored in the order
     in which they appear in the CNF file).
  3. Each subsequent LRAT addition is pushed to the very end of the `clauses` array, even if there are elements in the current array set
     to none.
  4. When a clause index is deleted via `delete`, that index in `clauses` is set to `none`

  The purpose of this invariant is to preserve a 1-to-1 correspondence between indices referenced by any external LRAT proof and the internal
  indices used within `clauses`

- The `rupUnits` field is empty except during the processing of RUP additions and RAT additions. During a RUP addition or a RAT addition, the
  `rupUnits` field is used to store negated units from the clause being evaluated for the addition. Regardless of whether the addition is
  successful, the `rupUnits` field is cleared prior to returning. The reason that `rupUnits` is included as part of the default formula
  structure (as opposed to simply being an Array that is passed through the helper functions relating to RUP and RAT additions) is to simplify
  the semantics of default formulas. Since `rupUnits` is part of the default formula structure, it can be taken into account in the `toList`
  function that defines its satisfiability semantics, making it possible to "add" negated units to a default formula and have it affect its
  semantics in an easily reversible manner.

- The `ratUnits` field is empty except during the processing of RAT additions. This field serves an extremely similar role to `rupUnits` in that
  it is used to temporarily store negated units during unit propagation. The primary difference between the `rupUnits` field and `ratUnits` field
  is that the `rupUnits` field is only updated twice for each RUP or RAT addition (once to add negated units and then once again to remove said
  negated units), the `ratUnits` field is updated zero times for each RUP addition and updated m times for each RAT addition where m is the number
  of negative hints in said RAT addition (i.e. the number of clauses in the formula containing the RAT addition's negated pivot literal).

- The `assignments` field is maintained to quickly look up which values (if any) are entailed for a variable by the formula. At most points in time,
  (i.e. at all points in time except during a RUP or RAT addition), the `assignments` field must satisfy the `StrongAssignmentsInvariant` defined
  in Formula.Lemmas.lean. During RUP and RAT additions, the `assignments` field must satisfy the `AssignmentsInvariant` defined in Formula.Lemmas.lean.
  The reason that the `assignments` field is contained as an explicit part of the default formula (as opposed to simply being an Array that is passed
  through the helper functions concerning unit propagation), is so that the (potentially large) Array does not need to repeatedly be allocated and
  deallocated. By having the `assignments` Array be a field of the default formula, it is easier to ensure that the Array is used linearly.
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula : ℕ → Type