This module contains the default implementation of the Formula typeclass that is used in the surface level LRAT checker.

structure Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula (numVarsSucc : Nat) : Type

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.

• clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc))
• rupUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
• ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
• assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ext {numVarsSucc : Nat} {x y : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc} (clauses : x.clauses = y.clauses) (rupUnits : x.rupUnits = y.rupUnits) (ratUnits : x.ratUnits = y.ratUnits) (assignments : x.assignments = y.assignments) : x = y

instance Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instInhabited {n : Nat} : Inhabited (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.toList {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : List (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)

Note: This function is only for reasoning about semantics. Its efficiency doesn't actually matter

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn assignments none = assignments

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray {n : Nat} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n

Note: This function assumes that the provided clauses Array is indexed according to the clauses field invariant described in the DefaultFormula doc comment.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.delete {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (ids : Array Nat) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n

Equations

• f.delete ids = Array.foldl (fun (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) => f.deleteOne id) f ids

instance Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instEntailsPosFin {n : Nat} : Std.Tactic.BVDecide.LRAT.Internal.Entails (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.formulaEntails_def {n : Nat} (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool) (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f = ((f.toList.all fun (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) => decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)) = true)

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit {n : Nat} : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) × Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool → Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) × Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (ls : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool

Returns an updated formula f and a bool which indicates whether a contradiction was found in the process of updating f.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRatUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (ls : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool

Returns an updated formula f and a bool which indicates whether a contradiction was found in the process of updating f.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit {n : Nat} : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit x (l, b) = x.modify l.val (Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment b)

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearRatUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (derivedLits : List (Std.Tactic.BVDecide.LRAT.Internal.PosFin n × Bool)) : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment

Reverts assignments to the array it was prior to adding derivedLits.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments assignments derivedLits = List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments derivedLits

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint {n : Nat} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool → Nat → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool

The fold function used for performRupCheck.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool

Takes in a formula f and an array of rupHints and attempts to verify that f is unsatisfiable. It returns:

• f', which is the same as f but the assignments field has been updated to be consistent with anything learned over the course of the rupCheck
• derivedLits, which is the list of literals that were derived over the course of the rupCheck (these are needed to eventually reconstruct the original assignment)
• derivedEmpty, which indicates whether the empty clause or a contradiction was derived
• encounteredError, which is true if the rupCheck failed and false otherwise

Note: This function assumes that any rupUnits and ratUnits corresponding to this rup check have already been added to f.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRupAdd {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool

Attempts to verify that c can be added to f via unit propagation. If it can, it returns ((f.insert c), true). If it can't, it returns false as the second part of the tuple (and no guarantees are made about what formula is returned).

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.getRatClauseIndices {n : Nat} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Array Nat

Returns an array of indices corresponding to clauses that contain the negation of l

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratHintsExhaustive {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (Nat × Array Nat)) : Bool

Checks that for each clause c ∈ f such that (Literal.negate pivot) ∈ c, c's index is in ratHints.map (fun x => x.1). This function assumes that ratHints are ordered by the value of their first argument, which is consistent with LRAT's specification

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (negPivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHint : Nat × Array Nat) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool

Takes in a formula f and a single ratHint and attempts to verify that f is inconsistent with the negation of the ratHint's clause. It returns:

• f which is the same as the original f (including the ratUnits and assignment fields)
  • Although the ratUnits and assignments fields are updated during the procedure, they are restored prior to returning..
• success, which indicates whether empty was successfully derived without any errors

Note: This function assumes that the ratUnits corresponding to this rat check have NOT already been added to f. In terms of input expectations and output guarantees, this function is more analogous to performRupAdd than performRupCheck.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatAdd {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool

Attempts to verify that c can be added to f via unit propagation. If it can, it returns ((f.insert c), true). If it can't, it returns false as the second part of the tuple (and no guarantees are made about what formula is returned).

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.numClausesInFormula {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) : Nat