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

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.

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.