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
    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
      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)