use HSat for BoolExpr

LeanSAT/BitBlast/BoolExpr/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import LeanSAT.Sat.Basic
+
 set_option linter.missingDocs false
 
 open Lean Meta
@@ -68,14 +70,16 @@ def eval (f : α → Bool) : BoolExpr α → Bool
 @[simp] theorem eval_not : eval f (.not x) = !eval f x := rfl
 @[simp] theorem eval_gate : eval f (.gate g x y) = g.eval (eval f x) (eval f y) := rfl
 
-def sat (x : BoolExpr α) (f : α → Bool) : Prop := eval f x = true
+def sat (f : α → Bool) (x : BoolExpr α) : Prop := eval f x = true
 
-theorem sat_and {x y : BoolExpr α} {f} (hx : sat x f) (hy : sat y f) : sat (.gate .and x y) f := by
-  simp only [sat] at *
-  simp [hx, hy, Gate.eval]
+instance : HSat α (BoolExpr α) where
+  eval := sat
 
-theorem sat_true : sat (.const true) f := rfl
+theorem sat_and {x y : BoolExpr α} {f : α → Bool} (hx : f ⊨ x) (hy : f ⊨ y)
+    : f ⊨ (BoolExpr.gate .and x y) := by
+  simp only [(· ⊨ ·), sat] at *
+  simp [hx, hy, Gate.eval]
 
-def unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false
+theorem sat_true {f : α → Bool} : f ⊨ (BoolExpr.const true : BoolExpr α) := rfl
 
 end BoolExpr

LeanSAT/BitBlast/BoolExpr/BitBlast.lean

@@ -148,7 +148,9 @@ theorem ofBoolExprCachedDirect_eval_eq_eval (expr : BoolExpr α) (assign) :
     ⟦ofBoolExprCachedDirect expr, assign⟧ = expr.eval assign := by
   apply ofBoolExprCached.go_eval_eq_eval
 
-theorem ofBoolExprCachedDirect_unsat_iff {expr : BoolExpr α} : (ofBoolExprCachedDirect expr).unsat ↔ expr.unsat := by
+theorem ofBoolExprCachedDirect_unsat_iff {expr : BoolExpr α}
+    : (ofBoolExprCachedDirect expr).unsat ↔ unsatisfiable α expr := by
+  simp [unsatisfiable, (· ⊨ ·), BoolExpr.sat]
   constructor
   all_goals
     intro h assign