Documentation

Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic

This module contains the definition of a generic boolean substructure for SMT problems with BoolExpr. For verification purposes BoolExpr.Sat and BoolExpr.Unsat are provided.

Instances For
    Equations
      Instances For
        Equations
          Instances For
            Instances For
              Equations
                Instances For
                  def Std.Tactic.BVDecide.BoolExpr.eval {α : Type} (a : αBool) :
                  BoolExpr αBool
                  Equations
                    Instances For
                      @[simp]
                      theorem Std.Tactic.BVDecide.BoolExpr.eval_literal {α✝ : Type} {a : α✝Bool} {l : α✝} :
                      eval a (literal l) = a l
                      @[simp]
                      theorem Std.Tactic.BVDecide.BoolExpr.eval_const {α✝ : Type} {a : α✝Bool} {b : Bool} :
                      eval a (const b) = b
                      @[simp]
                      theorem Std.Tactic.BVDecide.BoolExpr.eval_not {α✝ : Type} {a : α✝Bool} {x : BoolExpr α✝} :
                      eval a x.not = !eval a x
                      @[simp]
                      theorem Std.Tactic.BVDecide.BoolExpr.eval_gate {α✝ : Type} {a : α✝Bool} {g : Gate} {x y : BoolExpr α✝} :
                      eval a (gate g x y) = g.eval (eval a x) (eval a y)
                      @[simp]
                      theorem Std.Tactic.BVDecide.BoolExpr.eval_ite {α✝ : Type} {a : α✝Bool} {d l r : BoolExpr α✝} :
                      eval a (d.ite l r) = bif eval a d then eval a l else eval a r
                      def Std.Tactic.BVDecide.BoolExpr.Sat {α : Type} (a : αBool) (x : BoolExpr α) :
                      Equations
                        Instances For
                          Equations
                            Instances For
                              theorem Std.Tactic.BVDecide.BoolExpr.sat_and {α : Type} {x y : BoolExpr α} {a : αBool} (hx : Sat a x) (hy : Sat a y) :
                              Sat a (gate Gate.and x y)