Documentation

Std.Tactic.BVDecide.LRAT.Internal.Clause

An inductive datatype used specifically for the output of the reduce function. The intended meaning of each constructor is explained in the docstring of the reduce function.

Instances For

    Typeclass for clauses. An instance [Clause α β] indicates that β is the type of a clause with variables of type α.

    Instances
      def Std.Tactic.BVDecide.LRAT.Internal.Clause.eval {α : Type u_1} {β : Type u_2} [Clause α β] (a : αBool) (c : β) :
      Equations
        Instances For
          instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntails {α : Type u_1} {β : Type u_2} [Clause α β] :
          Entails α β
          Equations
            instance Std.Tactic.BVDecide.LRAT.Internal.Clause.instDecidableEval {α : Type u_1} {β : Type u_2} [Clause α β] (p : αBool) (c : β) :
            Equations

              The DefaultClause structure is primarily a list of literals. The additional field nodupkey is included to ensure that not_tautology is provable (which is needed to prove sat_of_insertRup and sat_of_insertRat in LRAT.Formula.Internal.RupAddSound and LRAT.Formula.Internal.RatAddSound). The additional field nodup is included to ensure that delete can be implemented by simply calling erase on the clause field. Without nodup, it would be necessary to iterate through the entire clause field and erase all instances of the literal to be deleted, since there would potentially be more than one.

              In principle, one could combine nodupkey and nodup to instead have one additional field that stipulates that ∀ l1 : PosFin numVarsSucc, ∀ l2 : PosFin numVarsSucc, l1.1 ≠ l2.1. This would work just as well, and the only reason that DefaultClause is structured in this manner is that the nodup field was only included in a later stage of the verification process when it became clear that it was needed.

              Instances For
                theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ext {numVarsSucc : Nat} {x y : DefaultClause numVarsSucc} (clause : x.clause = y.clause) :
                x = y
                instance Std.Tactic.BVDecide.LRAT.Internal.instBEqDefaultClause {numVarsSucc✝ : Nat} :
                BEq (DefaultClause numVarsSucc✝)
                Equations
                  @[inline]
                  Equations
                    Instances For

                      The reduce function takes in a clause c and takes in an array of assignments and attempts to eliminate every literal in the clause that is not compatible with the assignments argument.

                      • If reduce returns encounteredBoth, then this means that the assignments array has a both Assignment and is therefore fundamentally unsatisfiable.
                      • If reduce returns reducedToEmpty, then this means that every literal in c is incompatible with assignments. In other words, this means that the conjunction of assignments and c is unsatisfiable.
                      • If reduce returns reducedToUnit l, then this means that every literal in c is incompatible with assignments except for l. In other words, this means that the conjunction of assignments and c entail l.
                      • If reduce returns reducedToNonunit, then this means that there are multiple literals in c that are compatible with assignments. This is a failure condition for confirmRupHint (in LRAT.Formula.Implementation.lean) which calls reduce.
                      Equations
                        Instances For