def Std.Tactic.BVDecide.LRAT.Internal.CNF.lift (cnf : Std.Sat.CNF Nat) : Std.Sat.CNF (Std.Tactic.BVDecide.LRAT.Internal.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.

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

def Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' {n : Nat} (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : Option (Std.Tactic.BVDecide.LRAT.Internal.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 : Std.Sat.CNF (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : List (Option (Std.Tactic.BVDecide.LRAT.Internal.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 : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)} {lratClause : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n} (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (h1 : l ∈ clause) (h2 : Std.Tactic.BVDecide.LRAT.Internal.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 : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n} {assign : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool} (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (h : Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' clause = some lratClause) : Std.Sat.CNF.Clause.eval assign clause = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval assign lratClause

def Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT (cnf : Std.Sat.CNF Nat) : Std.Tactic.BVDecide.LRAT.Internal.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.

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

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

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

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