def Std.Tactic.BVDecide.LRAT.Internal.CNF.lift (cnf : Sat.CNF Nat) : Sat.CNF (PosFin (cnf.numLiterals + 1))

Turn a CNF Nat, that might contain 0 as a variable, to a CNF PosFin. This representation is guaranteed to not have 0 and is limited to an upper bound of variable indices.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.CNF.lift cnf = Std.Sat.CNF.relabel (fun (lit : Fin cnf.numLiterals) => ⟨↑lit + 1, ⋯⟩) cnf.relabelFin

theorem Std.Tactic.BVDecide.LRAT.Internal.CNF.unsat_of_lift_unsat (cnf : Sat.CNF Nat) : (lift cnf).Unsat → cnf.Unsat

def Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' {n : Nat} (clause : Sat.CNF.Clause (PosFin n)) : Option (DefaultClause n)

Turn a CNF.Clause PosFin into the representation used by the LRAT checker.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' clause = Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray (List.toArray clause)

def Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT' {n : Nat} (clauses : Sat.CNF (PosFin n)) : List (Option (DefaultClause n))

Turn a CNF PosFin into the representation used by the LRAT checker.

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.mem_lrat_of_mem {n : Nat} {l : Sat.Literal (PosFin n)} {lratClause : DefaultClause n} (clause : Sat.CNF.Clause (PosFin n)) (h1 : l ∈ clause) (h2 : DefaultClause.ofArray (List.toArray clause) = some lratClause) : l ∈ lratClause.clause

theorem Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT_sat_of_sat {n : Nat} {lratClause : DefaultClause n} {assign : PosFin n → Bool} (clause : Sat.CNF.Clause (PosFin n)) (h : convertLRAT' clause = some lratClause) : Sat.CNF.Clause.eval assign clause = true → Entails.eval assign lratClause

def Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT (cnf : Sat.CNF Nat) : DefaultFormula (cnf.numLiterals + 1)

Convert a CNF Nat with a certain maximum variable number into the DefaultFormula format for usage with bv_decide's LRAT.Internal.

Notably this:

1. Increments all variables as DIMACS variables start at 1 instead of 0
2. Adds a leading none clause. This clause must be persistent as the LRAT checker wants to have the DIMACS file line by line and the DIMACS file begins with the p cnf x y meta instruction.

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT_readyForRupAdd (cnf : Sat.CNF Nat) : (convertLRAT cnf).ReadyForRupAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT_readyForRatAdd (cnf : Sat.CNF Nat) : (convertLRAT cnf).ReadyForRatAdd

theorem Std.Tactic.BVDecide.LRAT.Internal.unsat_of_cons_none_unsat {n : Nat} (clauses : List (Option (DefaultClause n))) : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray) → Unsatisfiable (PosFin n) (DefaultFormula.ofArray clauses.toArray)

theorem Std.Tactic.BVDecide.LRAT.Internal.CNF.unsat_of_convertLRAT_unsat (cnf : Sat.CNF Nat) : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf) → cnf.Unsat