From 0d89f0194b4e7c949fea28626891d81a31d5625c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 2 Dec 2024 15:27:49 +0100 Subject: [PATCH] perf: bv_decide uses rfl in reflection if possible (#6286) This PR ensure `bv_decide` uses definitional equality in its reflection procedure as much as possible. Previously it would build up explicit congruence proofs for the kernel to check. This reduces the size of proof terms passed to kernel speeds up checking of large reflection proofs. --- .../BVDecide/Frontend/BVDecide/Reflect.lean | 35 +++++++++++++++---- .../Frontend/BVDecide/ReifiedBVExpr.lean | 10 +++--- .../Frontend/BVDecide/ReifiedBVLogical.lean | 27 ++++++++++---- .../Frontend/BVDecide/ReifiedBVPred.lean | 16 ++++++--- .../Frontend/BVDecide/ReifiedLemmas.lean | 2 +- .../BVDecide/Frontend/BVDecide/Reify.lean | 35 +++++++++++++------ .../Frontend/BVDecide/SatAtBVLogical.lean | 2 +- tests/lean/run/bv_preprocess_stress.lean | 16 +++++++++ tests/lean/run/bv_reflection_stress.lean | 21 ++++------- 9 files changed, 113 insertions(+), 51 deletions(-) create mode 100644 tests/lean/run/bv_preprocess_stress.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean index 6723a4150d20..bfc42764f8bc 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean @@ -157,9 +157,9 @@ structure ReifiedBVExpr where -/ bvExpr : BVExpr width /-- - A proof that `bvExpr.eval atomsAssignment = originalBVExpr`. + A proof that `bvExpr.eval atomsAssignment = originalBVExpr`, none if it holds by `rfl`. -/ - evalsAtAtoms : M Expr + evalsAtAtoms : M (Option Expr) /-- A cache for `toExpr bvExpr`. -/ @@ -174,9 +174,9 @@ structure ReifiedBVPred where -/ bvPred : BVPred /-- - A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`. + A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`, none if it holds by `rfl`. -/ - evalsAtAtoms : M Expr + evalsAtAtoms : M (Option Expr) /-- A cache for `toExpr bvPred` -/ @@ -191,9 +191,9 @@ structure ReifiedBVLogical where -/ bvExpr : BVLogicalExpr /-- - A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`. + A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`, none if it holds by `rfl`. -/ - evalsAtAtoms : M Expr + evalsAtAtoms : M (Option Expr) /-- A cache for `toExpr bvExpr` -/ @@ -263,6 +263,29 @@ where let newAtomsAssignment ← mkListLit packedType packed modify fun s => { s with atomsAssignmentCache := newAtomsAssignment } +@[specialize] +def simplifyBinaryProof' (mkFRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) + (mkSRefl : Expr → Expr) (snd : Expr) (sproof : Option Expr) : Option (Expr × Expr) := do + match fproof, sproof with + | some fproof, some sproof => some (fproof, sproof) + | some fproof, none => some (fproof, mkSRefl snd) + | none, some sproof => some (mkFRefl fst, sproof) + | none, none => none + +@[specialize] +def simplifyBinaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr) + (sproof : Option Expr) : Option (Expr × Expr) := do + simplifyBinaryProof' mkRefl fst fproof mkRefl snd sproof + +@[specialize] +def simplifyTernaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr) + (sproof : Option Expr) (thd : Expr) (tproof : Option Expr) : Option (Expr × Expr × Expr) := do + match fproof, simplifyBinaryProof mkRefl snd sproof thd tproof with + | some fproof, some stproof => some (fproof, stproof) + | some fproof, none => some (fproof, mkRefl snd, mkRefl thd) + | none, some stproof => some (mkRefl fst, stproof) + | none, none => none + end M /-- diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean index a7e5d1fb5505..ff3853ec3362 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean @@ -37,9 +37,8 @@ Register `e` as an atom of `width` that might potentially be `synthetic`. def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do let ident ← M.lookup e width synthetic let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident) - let proof := do - let evalExpr ← mkEvalExpr width expr - return mkBVRefl width evalExpr + -- This is safe because this proof always holds definitionally. + let proof := pure none return ⟨width, .var ident, proof, expr⟩ /-- @@ -70,9 +69,8 @@ Build a reified version of the constant `val`. def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do let bvExpr : BVExpr w := .const val let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val) - let proof := do - let evalExpr ← ReifiedBVExpr.mkEvalExpr w expr - return ReifiedBVExpr.mkBVRefl w evalExpr + -- This is safe because this proof always holds definitionally. + let proof := pure none return ⟨w, bvExpr, proof, expr⟩ end ReifiedBVExpr diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean index b0c1335284fa..3ea51fca3aba 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean @@ -49,7 +49,8 @@ Build a reified version of the constant `val`. def mkBoolConst (val : Bool) : M ReifiedBVLogical := do let boolExpr := .const val let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val) - let proof := pure <| ReifiedBVLogical.mkRefl (toExpr val) + -- This is safe because this proof always holds definitionally. + let proof := pure none return ⟨boolExpr, proof, expr⟩ /-- @@ -71,8 +72,13 @@ def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : let proof := do let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr - let lhsProof ← lhs.evalsAtAtoms - let rhsProof ← rhs.evalsAtAtoms + let lhsProof? ← lhs.evalsAtAtoms + let rhsProof? ← rhs.evalsAtAtoms + let some (lhsProof, rhsProof) := + M.simplifyBinaryProof + ReifiedBVLogical.mkRefl + lhsEvalExpr lhsProof? + rhsEvalExpr rhsProof? | return none return mkApp6 (mkConst congrThm) lhsExpr rhsExpr @@ -95,8 +101,9 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do let boolExpr := .not sub.bvExpr let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr let proof := do + -- This is safe as `not_congr` holds definitionally if the arguments are defeq. + let some subProof ← sub.evalsAtAtoms | return none let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr - let subProof ← sub.evalsAtAtoms return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof return ⟨boolExpr, proof, expr⟩ @@ -119,9 +126,15 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) let discrEvalExpr ← ReifiedBVLogical.mkEvalExpr discr.expr let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr - let discrProof ← discr.evalsAtAtoms - let lhsProof ← lhs.evalsAtAtoms - let rhsProof ← rhs.evalsAtAtoms + let discrProof? ← discr.evalsAtAtoms + let lhsProof? ← lhs.evalsAtAtoms + let rhsProof? ← rhs.evalsAtAtoms + let some (discrProof, lhsProof, rhsProof) := + M.simplifyTernaryProof + ReifiedBVLogical.mkRefl + discrEvalExpr discrProof? + lhsEvalExpr lhsProof? + rhsEvalExpr rhsProof? | return none return mkApp9 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr) discrExpr lhsExpr rhsExpr diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean index 31cabd742f2a..d700b43be187 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean @@ -35,8 +35,10 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do let bvExpr : BVPred := .getLsbD atom.bvExpr 0 let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0) let proof := do + -- ofBool_congr does not hold definitionally, if this ever becomes an issue we need to find + -- a more clever encoding for boolean atoms let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr - let atomProof ← atom.evalsAtAtoms + let atomProof := (← atom.evalsAtAtoms).getD (ReifiedBVExpr.mkBVRefl atom.width atomEval) return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr) t @@ -63,9 +65,14 @@ def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPr rhs.expr let proof := do let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr - let lhsProof ← lhs.evalsAtAtoms let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr - let rhsProof ← rhs.evalsAtAtoms + let lhsProof? ← lhs.evalsAtAtoms + let rhsProof? ← rhs.evalsAtAtoms + let some (lhsProof, rhsProof) := + M.simplifyBinaryProof + (ReifiedBVExpr.mkBVRefl lhs.width) + lhsEval lhsProof? + rhsEval rhsProof? | return none return mkApp7 (mkConst congrThm) (toExpr lhs.width) @@ -90,8 +97,9 @@ def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPr let idxExpr := toExpr idx let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr let proof := do + -- This is safe as `getLsbD_congr` holds definitionally if the arguments are defeq. + let some subProof ← sub.evalsAtAtoms | return none let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr - let subProof ← sub.evalsAtAtoms return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr) idxExpr diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean index 372279f4e444..87afcbadaf61 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean @@ -62,7 +62,7 @@ where let proof := do let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr - let congrProof ← imp.evalsAtAtoms + let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr) let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr let trueExpr := mkConst ``Bool.true diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean index 1845b3e13262..29ea6d5efabe 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean @@ -112,7 +112,8 @@ where inner.expr let proof := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms + -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq. + let some innerProof ← inner.evalsAtAtoms | return none return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr) newWidthExpr (toExpr inner.width) @@ -132,7 +133,8 @@ where inner.expr let proof := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms + -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq. + let some innerProof ← inner.evalsAtAtoms | return none return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr) newWidthExpr (toExpr inner.width) @@ -150,9 +152,13 @@ where lhs.expr rhs.expr let proof := do let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr - let lhsProof ← lhs.evalsAtAtoms - let rhsProof ← rhs.evalsAtAtoms let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr + let lhsProof? ← lhs.evalsAtAtoms + let rhsProof? ← rhs.evalsAtAtoms + let some (lhsProof, rhsProof) := + M.simplifyBinaryProof' + (ReifiedBVExpr.mkBVRefl lhs.width) lhsEval lhsProof? + (ReifiedBVExpr.mkBVRefl rhs.width) rhsEval rhsProof? | return none return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr) (toExpr lhs.width) (toExpr rhs.width) lhsExpr lhsEval @@ -169,7 +175,8 @@ where inner.expr let proof := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms + -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq. + let some innerProof ← inner.evalsAtAtoms | return none return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr) (toExpr n) (toExpr inner.width) @@ -189,7 +196,8 @@ where inner.expr let proof := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms + -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq. + let some innerProof ← inner.evalsAtAtoms | return none return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr) startExpr lenExpr @@ -301,11 +309,16 @@ where return none binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (congrThm : Expr) : - M Expr := do + M (Option Expr) := do let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr - let lhsProof ← lhs.evalsAtAtoms - let rhsProof ← rhs.evalsAtAtoms let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr + let lhsProof? ← lhs.evalsAtAtoms + let rhsProof? ← rhs.evalsAtAtoms + let some (lhsProof, rhsProof) := + M.simplifyBinaryProof + (ReifiedBVExpr.mkBVRefl lhs.width) + lhsEval lhsProof? + rhsEval rhsProof? | return none return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) : @@ -316,9 +329,9 @@ where let proof := unaryCongrProof inner innerExpr (mkConst congrThm) return some ⟨inner.width, bvExpr, proof, expr⟩ - unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M Expr := do + unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M (Option Expr) := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms + let some innerProof ← inner.evalsAtAtoms | return none return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean index 64f0349fcef1..9e570abeb5d4 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean @@ -37,7 +37,7 @@ partial def of (h : Expr) : LemmaM (Option SatAtBVLogical) := do let proof := do let evalLogic ← ReifiedBVLogical.mkEvalExpr bvLogical.expr -- this is evalLogic = lhsExpr - let evalProof ← bvLogical.evalsAtAtoms + let evalProof := (← bvLogical.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalLogic) -- h is lhsExpr = true -- we prove evalLogic = true by evalLogic = lhsExpr = true return ReifiedBVLogical.mkTrans evalLogic lhsExpr (mkConst ``Bool.true) evalProof h diff --git a/tests/lean/run/bv_preprocess_stress.lean b/tests/lean/run/bv_preprocess_stress.lean new file mode 100644 index 000000000000..516720614876 --- /dev/null +++ b/tests/lean/run/bv_preprocess_stress.lean @@ -0,0 +1,16 @@ +import Std.Tactic.BVDecide + +/- +The benchmarks are binary and trees with 2^n variables where n increases each line +-/ + +-- Our benchmark terms are huge, no need to waste time on linting +set_option linter.all false + +-- All of these are ~subsecond +theorem t1 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) : x0 = true := by bv_decide +theorem t2 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) : x00 = true := by bv_decide +theorem t3 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) : x000 = true := by bv_decide +theorem t4 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) : x0000 = true := by bv_decide +theorem t5 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x11111 : Bool) (x11110 : Bool) (_ : (x11110 && x11111) = x1111) (x11101 : Bool) (x11100 : Bool) (_ : (x11100 && x11101) = x1110) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x11011 : Bool) (x11010 : Bool) (_ : (x11010 && x11011) = x1101) (x11001 : Bool) (x11000 : Bool) (_ : (x11000 && x11001) = x1100) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x10111 : Bool) (x10110 : Bool) (_ : (x10110 && x10111) = x1011) (x10101 : Bool) (x10100 : Bool) (_ : (x10100 && x10101) = x1010) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x10011 : Bool) (x10010 : Bool) (_ : (x10010 && x10011) = x1001) (x10001 : Bool) (x10000 : Bool) (_ : (x10000 && x10001) = x1000) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x01111 : Bool) (x01110 : Bool) (_ : (x01110 && x01111) = x0111) (x01101 : Bool) (x01100 : Bool) (_ : (x01100 && x01101) = x0110) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x01011 : Bool) (x01010 : Bool) (_ : (x01010 && x01011) = x0101) (x01001 : Bool) (x01000 : Bool) (_ : (x01000 && x01001) = x0100) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x00111 : Bool) (x00110 : Bool) (_ : (x00110 && x00111) = x0011) (x00101 : Bool) (x00100 : Bool) (_ : (x00100 && x00101) = x0010) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) (x00011 : Bool) (x00010 : Bool) (_ : (x00010 && x00011) = x0001) (x00001 : Bool) (x00000 : Bool) (_ : (x00000 && x00001) = x0000) : x00000 = true := by bv_decide +theorem t6 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x11111 : Bool) (x11110 : Bool) (_ : (x11110 && x11111) = x1111) (x111111 : Bool) (x111110 : Bool) (_ : (x111110 && x111111) = x11111) (x111101 : Bool) (x111100 : Bool) (_ : (x111100 && x111101) = x11110) (x11101 : Bool) (x11100 : Bool) (_ : (x11100 && x11101) = x1110) (x111011 : Bool) (x111010 : Bool) (_ : (x111010 && x111011) = x11101) (x111001 : Bool) (x111000 : Bool) (_ : (x111000 && x111001) = x11100) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x11011 : Bool) (x11010 : Bool) (_ : (x11010 && x11011) = x1101) (x110111 : Bool) (x110110 : Bool) (_ : (x110110 && x110111) = x11011) (x110101 : Bool) (x110100 : Bool) (_ : (x110100 && x110101) = x11010) (x11001 : Bool) (x11000 : Bool) (_ : (x11000 && x11001) = x1100) (x110011 : Bool) (x110010 : Bool) (_ : (x110010 && x110011) = x11001) (x110001 : Bool) (x110000 : Bool) (_ : (x110000 && x110001) = x11000) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x10111 : Bool) (x10110 : Bool) (_ : (x10110 && x10111) = x1011) (x101111 : Bool) (x101110 : Bool) (_ : (x101110 && x101111) = x10111) (x101101 : Bool) (x101100 : Bool) (_ : (x101100 && x101101) = x10110) (x10101 : Bool) (x10100 : Bool) (_ : (x10100 && x10101) = x1010) (x101011 : Bool) (x101010 : Bool) (_ : (x101010 && x101011) = x10101) (x101001 : Bool) (x101000 : Bool) (_ : (x101000 && x101001) = x10100) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x10011 : Bool) (x10010 : Bool) (_ : (x10010 && x10011) = x1001) (x100111 : Bool) (x100110 : Bool) (_ : (x100110 && x100111) = x10011) (x100101 : Bool) (x100100 : Bool) (_ : (x100100 && x100101) = x10010) (x10001 : Bool) (x10000 : Bool) (_ : (x10000 && x10001) = x1000) (x100011 : Bool) (x100010 : Bool) (_ : (x100010 && x100011) = x10001) (x100001 : Bool) (x100000 : Bool) (_ : (x100000 && x100001) = x10000) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x01111 : Bool) (x01110 : Bool) (_ : (x01110 && x01111) = x0111) (x011111 : Bool) (x011110 : Bool) (_ : (x011110 && x011111) = x01111) (x011101 : Bool) (x011100 : Bool) (_ : (x011100 && x011101) = x01110) (x01101 : Bool) (x01100 : Bool) (_ : (x01100 && x01101) = x0110) (x011011 : Bool) (x011010 : Bool) (_ : (x011010 && x011011) = x01101) (x011001 : Bool) (x011000 : Bool) (_ : (x011000 && x011001) = x01100) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x01011 : Bool) (x01010 : Bool) (_ : (x01010 && x01011) = x0101) (x010111 : Bool) (x010110 : Bool) (_ : (x010110 && x010111) = x01011) (x010101 : Bool) (x010100 : Bool) (_ : (x010100 && x010101) = x01010) (x01001 : Bool) (x01000 : Bool) (_ : (x01000 && x01001) = x0100) (x010011 : Bool) (x010010 : Bool) (_ : (x010010 && x010011) = x01001) (x010001 : Bool) (x010000 : Bool) (_ : (x010000 && x010001) = x01000) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x00111 : Bool) (x00110 : Bool) (_ : (x00110 && x00111) = x0011) (x001111 : Bool) (x001110 : Bool) (_ : (x001110 && x001111) = x00111) (x001101 : Bool) (x001100 : Bool) (_ : (x001100 && x001101) = x00110) (x00101 : Bool) (x00100 : Bool) (_ : (x00100 && x00101) = x0010) (x001011 : Bool) (x001010 : Bool) (_ : (x001010 && x001011) = x00101) (x001001 : Bool) (x001000 : Bool) (_ : (x001000 && x001001) = x00100) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) (x00011 : Bool) (x00010 : Bool) (_ : (x00010 && x00011) = x0001) (x000111 : Bool) (x000110 : Bool) (_ : (x000110 && x000111) = x00011) (x000101 : Bool) (x000100 : Bool) (_ : (x000100 && x000101) = x00010) (x00001 : Bool) (x00000 : Bool) (_ : (x00000 && x00001) = x0000) (x000011 : Bool) (x000010 : Bool) (_ : (x000010 && x000011) = x00001) (x000001 : Bool) (x000000 : Bool) (_ : (x000000 && x000001) = x00000) : x000000 = true := by bv_decide diff --git a/tests/lean/run/bv_reflection_stress.lean b/tests/lean/run/bv_reflection_stress.lean index f30cbc537da0..3b79e2a079bd 100644 --- a/tests/lean/run/bv_reflection_stress.lean +++ b/tests/lean/run/bv_reflection_stress.lean @@ -1,7 +1,5 @@ import Std.Tactic.BVDecide -open Lean - /- The benchmarks are binary and trees with 2^n variables where n increases each line -/ @@ -9,16 +7,9 @@ The benchmarks are binary and trees with 2^n variables where n increases each li -- Our benchmark terms are huge, no need to waste time on linting set_option linter.all false --- All of these are ~subsecond -theorem t1 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) : x0 = true := by bv_decide -theorem t2 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) : x00 = true := by bv_decide -theorem t3 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) : x000 = true := by bv_decide -theorem t4 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) : x0000 = true := by bv_decide -theorem t5 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x11111 : Bool) (x11110 : Bool) (_ : (x11110 && x11111) = x1111) (x11101 : Bool) (x11100 : Bool) (_ : (x11100 && x11101) = x1110) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x11011 : Bool) (x11010 : Bool) (_ : (x11010 && x11011) = x1101) (x11001 : Bool) (x11000 : Bool) (_ : (x11000 && x11001) = x1100) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x10111 : Bool) (x10110 : Bool) (_ : (x10110 && x10111) = x1011) (x10101 : Bool) (x10100 : Bool) (_ : (x10100 && x10101) = x1010) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x10011 : Bool) (x10010 : Bool) (_ : (x10010 && x10011) = x1001) (x10001 : Bool) (x10000 : Bool) (_ : (x10000 && x10001) = x1000) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x01111 : Bool) (x01110 : Bool) (_ : (x01110 && x01111) = x0111) (x01101 : Bool) (x01100 : Bool) (_ : (x01100 && x01101) = x0110) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x01011 : Bool) (x01010 : Bool) (_ : (x01010 && x01011) = x0101) (x01001 : Bool) (x01000 : Bool) (_ : (x01000 && x01001) = x0100) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x00111 : Bool) (x00110 : Bool) (_ : (x00110 && x00111) = x0011) (x00101 : Bool) (x00100 : Bool) (_ : (x00100 && x00101) = x0010) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) (x00011 : Bool) (x00010 : Bool) (_ : (x00010 && x00011) = x0001) (x00001 : Bool) (x00000 : Bool) (_ : (x00000 && x00001) = x0000) : x00000 = true := by bv_decide -theorem t6 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x11111 : Bool) (x11110 : Bool) (_ : (x11110 && x11111) = x1111) (x111111 : Bool) (x111110 : Bool) (_ : (x111110 && x111111) = x11111) (x111101 : Bool) (x111100 : Bool) (_ : (x111100 && x111101) = x11110) (x11101 : Bool) (x11100 : Bool) (_ : (x11100 && x11101) = x1110) (x111011 : Bool) (x111010 : Bool) (_ : (x111010 && x111011) = x11101) (x111001 : Bool) (x111000 : Bool) (_ : (x111000 && x111001) = x11100) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x11011 : Bool) (x11010 : Bool) (_ : (x11010 && x11011) = x1101) (x110111 : Bool) (x110110 : Bool) (_ : (x110110 && x110111) = x11011) (x110101 : Bool) (x110100 : Bool) (_ : (x110100 && x110101) = x11010) (x11001 : Bool) (x11000 : Bool) (_ : (x11000 && x11001) = x1100) (x110011 : Bool) (x110010 : Bool) (_ : (x110010 && x110011) = x11001) (x110001 : Bool) (x110000 : Bool) (_ : (x110000 && x110001) = x11000) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x10111 : Bool) (x10110 : Bool) (_ : (x10110 && x10111) = x1011) (x101111 : Bool) (x101110 : Bool) (_ : (x101110 && x101111) = x10111) (x101101 : Bool) (x101100 : Bool) (_ : (x101100 && x101101) = x10110) (x10101 : Bool) (x10100 : Bool) (_ : (x10100 && x10101) = x1010) (x101011 : Bool) (x101010 : Bool) (_ : (x101010 && x101011) = x10101) (x101001 : Bool) (x101000 : Bool) (_ : (x101000 && x101001) = x10100) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x10011 : Bool) (x10010 : Bool) (_ : (x10010 && x10011) = x1001) (x100111 : Bool) (x100110 : Bool) (_ : (x100110 && x100111) = x10011) (x100101 : Bool) (x100100 : Bool) (_ : (x100100 && x100101) = x10010) (x10001 : Bool) (x10000 : Bool) (_ : (x10000 && x10001) = x1000) (x100011 : Bool) (x100010 : Bool) (_ : (x100010 && x100011) = x10001) (x100001 : Bool) (x100000 : Bool) (_ : (x100000 && x100001) = x10000) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x01111 : Bool) (x01110 : Bool) (_ : (x01110 && x01111) = x0111) (x011111 : Bool) (x011110 : Bool) (_ : (x011110 && x011111) = x01111) (x011101 : Bool) (x011100 : Bool) (_ : (x011100 && x011101) = x01110) (x01101 : Bool) (x01100 : Bool) (_ : (x01100 && x01101) = x0110) (x011011 : Bool) (x011010 : Bool) (_ : (x011010 && x011011) = x01101) (x011001 : Bool) (x011000 : Bool) (_ : (x011000 && x011001) = x01100) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x01011 : Bool) (x01010 : Bool) (_ : (x01010 && x01011) = x0101) (x010111 : Bool) (x010110 : Bool) (_ : (x010110 && x010111) = x01011) (x010101 : Bool) (x010100 : Bool) (_ : (x010100 && x010101) = x01010) (x01001 : Bool) (x01000 : Bool) (_ : (x01000 && x01001) = x0100) (x010011 : Bool) (x010010 : Bool) (_ : (x010010 && x010011) = x01001) (x010001 : Bool) (x010000 : Bool) (_ : (x010000 && x010001) = x01000) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x00111 : Bool) (x00110 : Bool) (_ : (x00110 && x00111) = x0011) (x001111 : Bool) (x001110 : Bool) (_ : (x001110 && x001111) = x00111) (x001101 : Bool) (x001100 : Bool) (_ : (x001100 && x001101) = x00110) (x00101 : Bool) (x00100 : Bool) (_ : (x00100 && x00101) = x0010) (x001011 : Bool) (x001010 : Bool) (_ : (x001010 && x001011) = x00101) (x001001 : Bool) (x001000 : Bool) (_ : (x001000 && x001001) = x00100) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) (x00011 : Bool) (x00010 : Bool) (_ : (x00010 && x00011) = x0001) (x000111 : Bool) (x000110 : Bool) (_ : (x000110 && x000111) = x00011) (x000101 : Bool) (x000100 : Bool) (_ : (x000100 && x000101) = x00010) (x00001 : Bool) (x00000 : Bool) (_ : (x00000 && x00001) = x0000) (x000011 : Bool) (x000010 : Bool) (_ : (x000010 && x000011) = x00001) (x000001 : Bool) (x000000 : Bool) (_ : (x000000 && x000001) = x00000) : x000000 = true := by bv_decide - -/-! -# Binary `and` of 2^7 variables -~2.3s --/ -theorem t7 (_ : x = true) (x1 : Bool) (x0 : Bool) (_ : (x0 && x1) = x) (x11 : Bool) (x10 : Bool) (_ : (x10 && x11) = x1) (x111 : Bool) (x110 : Bool) (_ : (x110 && x111) = x11) (x1111 : Bool) (x1110 : Bool) (_ : (x1110 && x1111) = x111) (x11111 : Bool) (x11110 : Bool) (_ : (x11110 && x11111) = x1111) (x111111 : Bool) (x111110 : Bool) (_ : (x111110 && x111111) = x11111) (x1111111 : Bool) (x1111110 : Bool) (_ : (x1111110 && x1111111) = x111111) (x1111101 : Bool) (x1111100 : Bool) (_ : (x1111100 && x1111101) = x111110) (x111101 : Bool) (x111100 : Bool) (_ : (x111100 && x111101) = x11110) (x1111011 : Bool) (x1111010 : Bool) (_ : (x1111010 && x1111011) = x111101) (x1111001 : Bool) (x1111000 : Bool) (_ : (x1111000 && x1111001) = x111100) (x11101 : Bool) (x11100 : Bool) (_ : (x11100 && x11101) = x1110) (x111011 : Bool) (x111010 : Bool) (_ : (x111010 && x111011) = x11101) (x1110111 : Bool) (x1110110 : Bool) (_ : (x1110110 && x1110111) = x111011) (x1110101 : Bool) (x1110100 : Bool) (_ : (x1110100 && x1110101) = x111010) (x111001 : Bool) (x111000 : Bool) (_ : (x111000 && x111001) = x11100) (x1110011 : Bool) (x1110010 : Bool) (_ : (x1110010 && x1110011) = x111001) (x1110001 : Bool) (x1110000 : Bool) (_ : (x1110000 && x1110001) = x111000) (x1101 : Bool) (x1100 : Bool) (_ : (x1100 && x1101) = x110) (x11011 : Bool) (x11010 : Bool) (_ : (x11010 && x11011) = x1101) (x110111 : Bool) (x110110 : Bool) (_ : (x110110 && x110111) = x11011) (x1101111 : Bool) (x1101110 : Bool) (_ : (x1101110 && x1101111) = x110111) (x1101101 : Bool) (x1101100 : Bool) (_ : (x1101100 && x1101101) = x110110) (x110101 : Bool) (x110100 : Bool) (_ : (x110100 && x110101) = x11010) (x1101011 : Bool) (x1101010 : Bool) (_ : (x1101010 && x1101011) = x110101) (x1101001 : Bool) (x1101000 : Bool) (_ : (x1101000 && x1101001) = x110100) (x11001 : Bool) (x11000 : Bool) (_ : (x11000 && x11001) = x1100) (x110011 : Bool) (x110010 : Bool) (_ : (x110010 && x110011) = x11001) (x1100111 : Bool) (x1100110 : Bool) (_ : (x1100110 && x1100111) = x110011) (x1100101 : Bool) (x1100100 : Bool) (_ : (x1100100 && x1100101) = x110010) (x110001 : Bool) (x110000 : Bool) (_ : (x110000 && x110001) = x11000) (x1100011 : Bool) (x1100010 : Bool) (_ : (x1100010 && x1100011) = x110001) (x1100001 : Bool) (x1100000 : Bool) (_ : (x1100000 && x1100001) = x110000) (x101 : Bool) (x100 : Bool) (_ : (x100 && x101) = x10) (x1011 : Bool) (x1010 : Bool) (_ : (x1010 && x1011) = x101) (x10111 : Bool) (x10110 : Bool) (_ : (x10110 && x10111) = x1011) (x101111 : Bool) (x101110 : Bool) (_ : (x101110 && x101111) = x10111) (x1011111 : Bool) (x1011110 : Bool) (_ : (x1011110 && x1011111) = x101111) (x1011101 : Bool) (x1011100 : Bool) (_ : (x1011100 && x1011101) = x101110) (x101101 : Bool) (x101100 : Bool) (_ : (x101100 && x101101) = x10110) (x1011011 : Bool) (x1011010 : Bool) (_ : (x1011010 && x1011011) = x101101) (x1011001 : Bool) (x1011000 : Bool) (_ : (x1011000 && x1011001) = x101100) (x10101 : Bool) (x10100 : Bool) (_ : (x10100 && x10101) = x1010) (x101011 : Bool) (x101010 : Bool) (_ : (x101010 && x101011) = x10101) (x1010111 : Bool) (x1010110 : Bool) (_ : (x1010110 && x1010111) = x101011) (x1010101 : Bool) (x1010100 : Bool) (_ : (x1010100 && x1010101) = x101010) (x101001 : Bool) (x101000 : Bool) (_ : (x101000 && x101001) = x10100) (x1010011 : Bool) (x1010010 : Bool) (_ : (x1010010 && x1010011) = x101001) (x1010001 : Bool) (x1010000 : Bool) (_ : (x1010000 && x1010001) = x101000) (x1001 : Bool) (x1000 : Bool) (_ : (x1000 && x1001) = x100) (x10011 : Bool) (x10010 : Bool) (_ : (x10010 && x10011) = x1001) (x100111 : Bool) (x100110 : Bool) (_ : (x100110 && x100111) = x10011) (x1001111 : Bool) (x1001110 : Bool) (_ : (x1001110 && x1001111) = x100111) (x1001101 : Bool) (x1001100 : Bool) (_ : (x1001100 && x1001101) = x100110) (x100101 : Bool) (x100100 : Bool) (_ : (x100100 && x100101) = x10010) (x1001011 : Bool) (x1001010 : Bool) (_ : (x1001010 && x1001011) = x100101) (x1001001 : Bool) (x1001000 : Bool) (_ : (x1001000 && x1001001) = x100100) (x10001 : Bool) (x10000 : Bool) (_ : (x10000 && x10001) = x1000) (x100011 : Bool) (x100010 : Bool) (_ : (x100010 && x100011) = x10001) (x1000111 : Bool) (x1000110 : Bool) (_ : (x1000110 && x1000111) = x100011) (x1000101 : Bool) (x1000100 : Bool) (_ : (x1000100 && x1000101) = x100010) (x100001 : Bool) (x100000 : Bool) (_ : (x100000 && x100001) = x10000) (x1000011 : Bool) (x1000010 : Bool) (_ : (x1000010 && x1000011) = x100001) (x1000001 : Bool) (x1000000 : Bool) (_ : (x1000000 && x1000001) = x100000) (x01 : Bool) (x00 : Bool) (_ : (x00 && x01) = x0) (x011 : Bool) (x010 : Bool) (_ : (x010 && x011) = x01) (x0111 : Bool) (x0110 : Bool) (_ : (x0110 && x0111) = x011) (x01111 : Bool) (x01110 : Bool) (_ : (x01110 && x01111) = x0111) (x011111 : Bool) (x011110 : Bool) (_ : (x011110 && x011111) = x01111) (x0111111 : Bool) (x0111110 : Bool) (_ : (x0111110 && x0111111) = x011111) (x0111101 : Bool) (x0111100 : Bool) (_ : (x0111100 && x0111101) = x011110) (x011101 : Bool) (x011100 : Bool) (_ : (x011100 && x011101) = x01110) (x0111011 : Bool) (x0111010 : Bool) (_ : (x0111010 && x0111011) = x011101) (x0111001 : Bool) (x0111000 : Bool) (_ : (x0111000 && x0111001) = x011100) (x01101 : Bool) (x01100 : Bool) (_ : (x01100 && x01101) = x0110) (x011011 : Bool) (x011010 : Bool) (_ : (x011010 && x011011) = x01101) (x0110111 : Bool) (x0110110 : Bool) (_ : (x0110110 && x0110111) = x011011) (x0110101 : Bool) (x0110100 : Bool) (_ : (x0110100 && x0110101) = x011010) (x011001 : Bool) (x011000 : Bool) (_ : (x011000 && x011001) = x01100) (x0110011 : Bool) (x0110010 : Bool) (_ : (x0110010 && x0110011) = x011001) (x0110001 : Bool) (x0110000 : Bool) (_ : (x0110000 && x0110001) = x011000) (x0101 : Bool) (x0100 : Bool) (_ : (x0100 && x0101) = x010) (x01011 : Bool) (x01010 : Bool) (_ : (x01010 && x01011) = x0101) (x010111 : Bool) (x010110 : Bool) (_ : (x010110 && x010111) = x01011) (x0101111 : Bool) (x0101110 : Bool) (_ : (x0101110 && x0101111) = x010111) (x0101101 : Bool) (x0101100 : Bool) (_ : (x0101100 && x0101101) = x010110) (x010101 : Bool) (x010100 : Bool) (_ : (x010100 && x010101) = x01010) (x0101011 : Bool) (x0101010 : Bool) (_ : (x0101010 && x0101011) = x010101) (x0101001 : Bool) (x0101000 : Bool) (_ : (x0101000 && x0101001) = x010100) (x01001 : Bool) (x01000 : Bool) (_ : (x01000 && x01001) = x0100) (x010011 : Bool) (x010010 : Bool) (_ : (x010010 && x010011) = x01001) (x0100111 : Bool) (x0100110 : Bool) (_ : (x0100110 && x0100111) = x010011) (x0100101 : Bool) (x0100100 : Bool) (_ : (x0100100 && x0100101) = x010010) (x010001 : Bool) (x010000 : Bool) (_ : (x010000 && x010001) = x01000) (x0100011 : Bool) (x0100010 : Bool) (_ : (x0100010 && x0100011) = x010001) (x0100001 : Bool) (x0100000 : Bool) (_ : (x0100000 && x0100001) = x010000) (x001 : Bool) (x000 : Bool) (_ : (x000 && x001) = x00) (x0011 : Bool) (x0010 : Bool) (_ : (x0010 && x0011) = x001) (x00111 : Bool) (x00110 : Bool) (_ : (x00110 && x00111) = x0011) (x001111 : Bool) (x001110 : Bool) (_ : (x001110 && x001111) = x00111) (x0011111 : Bool) (x0011110 : Bool) (_ : (x0011110 && x0011111) = x001111) (x0011101 : Bool) (x0011100 : Bool) (_ : (x0011100 && x0011101) = x001110) (x001101 : Bool) (x001100 : Bool) (_ : (x001100 && x001101) = x00110) (x0011011 : Bool) (x0011010 : Bool) (_ : (x0011010 && x0011011) = x001101) (x0011001 : Bool) (x0011000 : Bool) (_ : (x0011000 && x0011001) = x001100) (x00101 : Bool) (x00100 : Bool) (_ : (x00100 && x00101) = x0010) (x001011 : Bool) (x001010 : Bool) (_ : (x001010 && x001011) = x00101) (x0010111 : Bool) (x0010110 : Bool) (_ : (x0010110 && x0010111) = x001011) (x0010101 : Bool) (x0010100 : Bool) (_ : (x0010100 && x0010101) = x001010) (x001001 : Bool) (x001000 : Bool) (_ : (x001000 && x001001) = x00100) (x0010011 : Bool) (x0010010 : Bool) (_ : (x0010010 && x0010011) = x001001) (x0010001 : Bool) (x0010000 : Bool) (_ : (x0010000 && x0010001) = x001000) (x0001 : Bool) (x0000 : Bool) (_ : (x0000 && x0001) = x000) (x00011 : Bool) (x00010 : Bool) (_ : (x00010 && x00011) = x0001) (x000111 : Bool) (x000110 : Bool) (_ : (x000110 && x000111) = x00011) (x0001111 : Bool) (x0001110 : Bool) (_ : (x0001110 && x0001111) = x000111) (x0001101 : Bool) (x0001100 : Bool) (_ : (x0001100 && x0001101) = x000110) (x000101 : Bool) (x000100 : Bool) (_ : (x000100 && x000101) = x00010) (x0001011 : Bool) (x0001010 : Bool) (_ : (x0001010 && x0001011) = x000101) (x0001001 : Bool) (x0001000 : Bool) (_ : (x0001000 && x0001001) = x000100) (x00001 : Bool) (x00000 : Bool) (_ : (x00000 && x00001) = x0000) (x000011 : Bool) (x000010 : Bool) (_ : (x000010 && x000011) = x00001) (x0000111 : Bool) (x0000110 : Bool) (_ : (x0000110 && x0000111) = x000011) (x0000101 : Bool) (x0000100 : Bool) (_ : (x0000100 && x0000101) = x000010) (x000001 : Bool) (x000000 : Bool) (_ : (x000000 && x000001) = x00000) (x0000011 : Bool) (x0000010 : Bool) (_ : (x0000010 && x0000011) = x000001) (x0000001 : Bool) (x0000000 : Bool) (_ : (x0000000 && x0000001) = x000000) : x0000000 = true := by bv_decide +example (_ : x = 1#1) (x1 : BitVec 1) (x0 : BitVec 1) (_ : (x0 &&& x1) = x) : x0 = 1#1 := by bv_decide (config := { embeddedConstraintSubst := false, andFlattening := false}) +example (_ : x = 1#1) (x1 : BitVec 1) (x0 : BitVec 1) (_ : (x0 &&& x1) = x) (x11 : BitVec 1) (x10 : BitVec 1) (_ : (x10 &&& x11) = x1) (x01 : BitVec 1) (x00 : BitVec 1) (_ : (x00 &&& x01) = x0) : x00 = 1#1 := by bv_decide (config := { embeddedConstraintSubst := false, andFlattening := false}) +example (_ : x = 1#1) (x1 : BitVec 1) (x0 : BitVec 1) (_ : (x0 &&& x1) = x) (x11 : BitVec 1) (x10 : BitVec 1) (_ : (x10 &&& x11) = x1) (x111 : BitVec 1) (x110 : BitVec 1) (_ : (x110 &&& x111) = x11) (x101 : BitVec 1) (x100 : BitVec 1) (_ : (x100 &&& x101) = x10) (x01 : BitVec 1) (x00 : BitVec 1) (_ : (x00 &&& x01) = x0) (x011 : BitVec 1) (x010 : BitVec 1) (_ : (x010 &&& x011) = x01) (x001 : BitVec 1) (x000 : BitVec 1) (_ : (x000 &&& x001) = x00) : x000 = 1#1 := by bv_decide (config := { embeddedConstraintSubst := false, andFlattening := false}) +example (_ : x = 1#1) (x1 : BitVec 1) (x0 : BitVec 1) (_ : (x0 &&& x1) = x) (x11 : BitVec 1) (x10 : BitVec 1) (_ : (x10 &&& x11) = x1) (x111 : BitVec 1) (x110 : BitVec 1) (_ : (x110 &&& x111) = x11) (x1111 : BitVec 1) (x1110 : BitVec 1) (_ : (x1110 &&& x1111) = x111) (x1101 : BitVec 1) (x1100 : BitVec 1) (_ : (x1100 &&& x1101) = x110) (x101 : BitVec 1) (x100 : BitVec 1) (_ : (x100 &&& x101) = x10) (x1011 : BitVec 1) (x1010 : BitVec 1) (_ : (x1010 &&& x1011) = x101) (x1001 : BitVec 1) (x1000 : BitVec 1) (_ : (x1000 &&& x1001) = x100) (x01 : BitVec 1) (x00 : BitVec 1) (_ : (x00 &&& x01) = x0) (x011 : BitVec 1) (x010 : BitVec 1) (_ : (x010 &&& x011) = x01) (x0111 : BitVec 1) (x0110 : BitVec 1) (_ : (x0110 &&& x0111) = x011) (x0101 : BitVec 1) (x0100 : BitVec 1) (_ : (x0100 &&& x0101) = x010) (x001 : BitVec 1) (x000 : BitVec 1) (_ : (x000 &&& x001) = x00) (x0011 : BitVec 1) (x0010 : BitVec 1) (_ : (x0010 &&& x0011) = x001) (x0001 : BitVec 1) (x0000 : BitVec 1) (_ : (x0000 &&& x0001) = x000) : x0000 = 1#1 := by bv_decide (config := { embeddedConstraintSubst := false, andFlattening := false}) +example (_ : x = 1#1) (x1 : BitVec 1) (x0 : BitVec 1) (_ : (x0 &&& x1) = x) (x11 : BitVec 1) (x10 : BitVec 1) (_ : (x10 &&& x11) = x1) (x111 : BitVec 1) (x110 : BitVec 1) (_ : (x110 &&& x111) = x11) (x1111 : BitVec 1) (x1110 : BitVec 1) (_ : (x1110 &&& x1111) = x111) (x11111 : BitVec 1) (x11110 : BitVec 1) (_ : (x11110 &&& x11111) = x1111) (x11101 : BitVec 1) (x11100 : BitVec 1) (_ : (x11100 &&& x11101) = x1110) (x1101 : BitVec 1) (x1100 : BitVec 1) (_ : (x1100 &&& x1101) = x110) (x11011 : BitVec 1) (x11010 : BitVec 1) (_ : (x11010 &&& x11011) = x1101) (x11001 : BitVec 1) (x11000 : BitVec 1) (_ : (x11000 &&& x11001) = x1100) (x101 : BitVec 1) (x100 : BitVec 1) (_ : (x100 &&& x101) = x10) (x1011 : BitVec 1) (x1010 : BitVec 1) (_ : (x1010 &&& x1011) = x101) (x10111 : BitVec 1) (x10110 : BitVec 1) (_ : (x10110 &&& x10111) = x1011) (x10101 : BitVec 1) (x10100 : BitVec 1) (_ : (x10100 &&& x10101) = x1010) (x1001 : BitVec 1) (x1000 : BitVec 1) (_ : (x1000 &&& x1001) = x100) (x10011 : BitVec 1) (x10010 : BitVec 1) (_ : (x10010 &&& x10011) = x1001) (x10001 : BitVec 1) (x10000 : BitVec 1) (_ : (x10000 &&& x10001) = x1000) (x01 : BitVec 1) (x00 : BitVec 1) (_ : (x00 &&& x01) = x0) (x011 : BitVec 1) (x010 : BitVec 1) (_ : (x010 &&& x011) = x01) (x0111 : BitVec 1) (x0110 : BitVec 1) (_ : (x0110 &&& x0111) = x011) (x01111 : BitVec 1) (x01110 : BitVec 1) (_ : (x01110 &&& x01111) = x0111) (x01101 : BitVec 1) (x01100 : BitVec 1) (_ : (x01100 &&& x01101) = x0110) (x0101 : BitVec 1) (x0100 : BitVec 1) (_ : (x0100 &&& x0101) = x010) (x01011 : BitVec 1) (x01010 : BitVec 1) (_ : (x01010 &&& x01011) = x0101) (x01001 : BitVec 1) (x01000 : BitVec 1) (_ : (x01000 &&& x01001) = x0100) (x001 : BitVec 1) (x000 : BitVec 1) (_ : (x000 &&& x001) = x00) (x0011 : BitVec 1) (x0010 : BitVec 1) (_ : (x0010 &&& x0011) = x001) (x00111 : BitVec 1) (x00110 : BitVec 1) (_ : (x00110 &&& x00111) = x0011) (x00101 : BitVec 1) (x00100 : BitVec 1) (_ : (x00100 &&& x00101) = x0010) (x0001 : BitVec 1) (x0000 : BitVec 1) (_ : (x0000 &&& x0001) = x000) (x00011 : BitVec 1) (x00010 : BitVec 1) (_ : (x00010 &&& x00011) = x0001) (x00001 : BitVec 1) (x00000 : BitVec 1) (_ : (x00000 &&& x00001) = x0000) : x00000 = 1#1 := by bv_decide (config := { embeddedConstraintSubst := false, andFlattening := false}) +example (_ : x = 1#1) (x1 : BitVec 1) (x0 : BitVec 1) (_ : (x0 &&& x1) = x) (x11 : BitVec 1) (x10 : BitVec 1) (_ : (x10 &&& x11) = x1) (x111 : BitVec 1) (x110 : BitVec 1) (_ : (x110 &&& x111) = x11) (x1111 : BitVec 1) (x1110 : BitVec 1) (_ : (x1110 &&& x1111) = x111) (x11111 : BitVec 1) (x11110 : BitVec 1) (_ : (x11110 &&& x11111) = x1111) (x111111 : BitVec 1) (x111110 : BitVec 1) (_ : (x111110 &&& x111111) = x11111) (x111101 : BitVec 1) (x111100 : BitVec 1) (_ : (x111100 &&& x111101) = x11110) (x11101 : BitVec 1) (x11100 : BitVec 1) (_ : (x11100 &&& x11101) = x1110) (x111011 : BitVec 1) (x111010 : BitVec 1) (_ : (x111010 &&& x111011) = x11101) (x111001 : BitVec 1) (x111000 : BitVec 1) (_ : (x111000 &&& x111001) = x11100) (x1101 : BitVec 1) (x1100 : BitVec 1) (_ : (x1100 &&& x1101) = x110) (x11011 : BitVec 1) (x11010 : BitVec 1) (_ : (x11010 &&& x11011) = x1101) (x110111 : BitVec 1) (x110110 : BitVec 1) (_ : (x110110 &&& x110111) = x11011) (x110101 : BitVec 1) (x110100 : BitVec 1) (_ : (x110100 &&& x110101) = x11010) (x11001 : BitVec 1) (x11000 : BitVec 1) (_ : (x11000 &&& x11001) = x1100) (x110011 : BitVec 1) (x110010 : BitVec 1) (_ : (x110010 &&& x110011) = x11001) (x110001 : BitVec 1) (x110000 : BitVec 1) (_ : (x110000 &&& x110001) = x11000) (x101 : BitVec 1) (x100 : BitVec 1) (_ : (x100 &&& x101) = x10) (x1011 : BitVec 1) (x1010 : BitVec 1) (_ : (x1010 &&& x1011) = x101) (x10111 : BitVec 1) (x10110 : BitVec 1) (_ : (x10110 &&& x10111) = x1011) (x101111 : BitVec 1) (x101110 : BitVec 1) (_ : (x101110 &&& x101111) = x10111) (x101101 : BitVec 1) (x101100 : BitVec 1) (_ : (x101100 &&& x101101) = x10110) (x10101 : BitVec 1) (x10100 : BitVec 1) (_ : (x10100 &&& x10101) = x1010) (x101011 : BitVec 1) (x101010 : BitVec 1) (_ : (x101010 &&& x101011) = x10101) (x101001 : BitVec 1) (x101000 : BitVec 1) (_ : (x101000 &&& x101001) = x10100) (x1001 : BitVec 1) (x1000 : BitVec 1) (_ : (x1000 &&& x1001) = x100) (x10011 : BitVec 1) (x10010 : BitVec 1) (_ : (x10010 &&& x10011) = x1001) (x100111 : BitVec 1) (x100110 : BitVec 1) (_ : (x100110 &&& x100111) = x10011) (x100101 : BitVec 1) (x100100 : BitVec 1) (_ : (x100100 &&& x100101) = x10010) (x10001 : BitVec 1) (x10000 : BitVec 1) (_ : (x10000 &&& x10001) = x1000) (x100011 : BitVec 1) (x100010 : BitVec 1) (_ : (x100010 &&& x100011) = x10001) (x100001 : BitVec 1) (x100000 : BitVec 1) (_ : (x100000 &&& x100001) = x10000) (x01 : BitVec 1) (x00 : BitVec 1) (_ : (x00 &&& x01) = x0) (x011 : BitVec 1) (x010 : BitVec 1) (_ : (x010 &&& x011) = x01) (x0111 : BitVec 1) (x0110 : BitVec 1) (_ : (x0110 &&& x0111) = x011) (x01111 : BitVec 1) (x01110 : BitVec 1) (_ : (x01110 &&& x01111) = x0111) (x011111 : BitVec 1) (x011110 : BitVec 1) (_ : (x011110 &&& x011111) = x01111) (x011101 : BitVec 1) (x011100 : BitVec 1) (_ : (x011100 &&& x011101) = x01110) (x01101 : BitVec 1) (x01100 : BitVec 1) (_ : (x01100 &&& x01101) = x0110) (x011011 : BitVec 1) (x011010 : BitVec 1) (_ : (x011010 &&& x011011) = x01101) (x011001 : BitVec 1) (x011000 : BitVec 1) (_ : (x011000 &&& x011001) = x01100) (x0101 : BitVec 1) (x0100 : BitVec 1) (_ : (x0100 &&& x0101) = x010) (x01011 : BitVec 1) (x01010 : BitVec 1) (_ : (x01010 &&& x01011) = x0101) (x010111 : BitVec 1) (x010110 : BitVec 1) (_ : (x010110 &&& x010111) = x01011) (x010101 : BitVec 1) (x010100 : BitVec 1) (_ : (x010100 &&& x010101) = x01010) (x01001 : BitVec 1) (x01000 : BitVec 1) (_ : (x01000 &&& x01001) = x0100) (x010011 : BitVec 1) (x010010 : BitVec 1) (_ : (x010010 &&& x010011) = x01001) (x010001 : BitVec 1) (x010000 : BitVec 1) (_ : (x010000 &&& x010001) = x01000) (x001 : BitVec 1) (x000 : BitVec 1) (_ : (x000 &&& x001) = x00) (x0011 : BitVec 1) (x0010 : BitVec 1) (_ : (x0010 &&& x0011) = x001) (x00111 : BitVec 1) (x00110 : BitVec 1) (_ : (x00110 &&& x00111) = x0011) (x001111 : BitVec 1) (x001110 : BitVec 1) (_ : (x001110 &&& x001111) = x00111) (x001101 : BitVec 1) (x001100 : BitVec 1) (_ : (x001100 &&& x001101) = x00110) (x00101 : BitVec 1) (x00100 : BitVec 1) (_ : (x00100 &&& x00101) = x0010) (x001011 : BitVec 1) (x001010 : BitVec 1) (_ : (x001010 &&& x001011) = x00101) (x001001 : BitVec 1) (x001000 : BitVec 1) (_ : (x001000 &&& x001001) = x00100) (x0001 : BitVec 1) (x0000 : BitVec 1) (_ : (x0000 &&& x0001) = x000) (x00011 : BitVec 1) (x00010 : BitVec 1) (_ : (x00010 &&& x00011) = x0001) (x000111 : BitVec 1) (x000110 : BitVec 1) (_ : (x000110 &&& x000111) = x00011) (x000101 : BitVec 1) (x000100 : BitVec 1) (_ : (x000100 &&& x000101) = x00010) (x00001 : BitVec 1) (x00000 : BitVec 1) (_ : (x00000 &&& x00001) = x0000) (x000011 : BitVec 1) (x000010 : BitVec 1) (_ : (x000010 &&& x000011) = x00001) (x000001 : BitVec 1) (x000000 : BitVec 1) (_ : (x000000 &&& x000001) = x00000) : x000000 = 1#1 := by bv_decide (config := { embeddedConstraintSubst := false, andFlattening := false})