more tests

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -503,29 +503,37 @@ Decides which variable to run Fourier-Motzkin elimination on, and returns the as
 We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations,
 and break ties by the number of new inequalities introduced.
 -/
-def fourierMotzkinSelect (data : Array FourierMotzkinData) : FourierMotzkinData := Id.run do
+def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzkinData := do
   let data := data.filter fun d => ¬ d.isEmpty
+  trace[omega] "Selecting variable to eliminate from (idx, size, exact) triples:\n\
+    {data.map fun d => (d.var, d.size, d.exact)}"
   let mut bestIdx := 0
   let mut bestSize := data[0]!.size
   let mut bestExact := data[0]!.exact
-  if bestSize = 0 then return data[0]!
+  if bestSize = 0 then
+    trace[omega] "Selected variable {data[0]!.var}."
+    return data[0]!
   for i in [1:data.size] do
     let exact := data[i]!.exact
     let size := data[i]!.size
-    if size = 0 || !bestExact && exact || size < bestSize then
-      if size = 0 then return data[i]!
+    if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then
+      if size = 0 then
+        trace[omega] "Selected variable {data[i]!.var}"
+        return data[i]!
       bestIdx := i
       bestExact := exact
       bestSize := size
+  trace[omega] "Selected variable {data[bestIdx]!.var}."
   return data[bestIdx]!
 
 /--
 Run Fourier-Motzkin elimination on one variable.
 -/
-def fourierMotzkin (p : Problem) : Problem := Id.run do
+-- This is only in MetaM to enable tracing.
+def fourierMotzkin (p : Problem) : MetaM Problem := do
   let data := p.fourierMotzkinData
   -- Now perform the elimination.
-  let ⟨_, irrelevant, lower, upper, _, _⟩ := fourierMotzkinSelect data
+  let ⟨_, irrelevant, lower, upper, _, _⟩ ← fourierMotzkinSelect data
   let mut r : Problem := { assumptions := p.assumptions, eliminations := p.eliminations }
   for f in irrelevant do
     r := r.insertConstraint f
@@ -554,7 +562,7 @@ partial def elimination (p : Problem) : OmegaM Problem :=
       return p
     else do
       trace[omega] "Running Fourier-Motzkin elimination on:\n{p}"
-      runOmega p.fourierMotzkin
+      runOmega (← p.fourierMotzkin)
   else
     return p
 

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -505,7 +505,6 @@ partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withCont
     trace[omega] "Justification:\n{p'.explanation?.get}"
     let prf ← instantiateMVars (← prf)
     trace[omega] "omega found a contradiction, proving {← inferType prf}"
-    trace[omega] "{prf}"
     g.assign prf
 
 end

tests/lean/run/omega.lean

@@ -380,3 +380,27 @@ example (i j : Nat) (p : i ≥ j) : True := by
 example (i : Fin 7) : (i : Nat) < 8 := by omega
 
 example (x y z i : Nat) (hz : z ≤ 1) : x % 2 ^ i + y % 2 ^ i + z < 2 * 2^ i := by omega
+
+/-! ### BitVec -/
+-- Currently these tests require calling `simp` with many lemmas,
+-- and sometimes adding `toNat_lt` as a hypothesis.
+-- We need a good `BitVec` to `Nat` preprocessor.
+
+open Std BitVec
+
+example (x y : BitVec 8) (hx : x < 16) (hy : y < 16) : x + y < 31 := by
+  simp [BitVec.lt_def] at *
+  omega
+
+example (x y z : BitVec 8) (hx : x >>> 1 < 16) (hy : y < 16) (hz : z = x + 2 * y) : z ≤ 64 := by
+  simp [BitVec.lt_def, BitVec.le_def, BitVec.toNat_eq, Nat.shiftRight_eq_div_pow, BitVec.toNat_mul] at *
+  omega
+
+example (x : BitVec 8) (hx : (x + 1) <<< 1 = 3) : False := by
+  simp [BitVec.toNat_eq, Nat.shiftLeft_eq] at *
+  omega
+
+example (x : BitVec 8) (hx : (x + 1) <<< 1 = 4) : x = 1 ∨ x = 129 := by
+  have := toNat_lt x
+  simp [BitVec.toNat_eq, Nat.shiftLeft_eq, BitVec.lt_def] at *
+  omega