Documentation

Std.Tactic.BVDecide.LRAT.Internal.Convert

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
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For
              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 nBool} (clause : Sat.CNF.Clause (PosFin n)) (h : convertLRAT' clause = some lratClause) :
              Sat.CNF.Clause.eval assign clause = trueEntails.eval assign lratClause

              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
                Instances For