Skip to content

Commit

Permalink
Updating duper2 to match main
Browse files Browse the repository at this point in the history
  • Loading branch information
@JOSHCLUNE
JOSHCLUNE committed Mar 26, 2024
2 parents 1b48353 + 1507142 commit 041898f
Show file tree
Hide file tree
Showing 12 changed files with 256 additions and 234 deletions.
2 changes: 1 addition & 1 deletion Auto/Embedding/LamBase.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3672,7 +3672,7 @@ def LamWF.bvarApps
have tyeq : ty = lctxr ex.length := by
have exlt : List.length ex < List.length (List.reverse (ty :: ex)) := by
rw [List.length_reverse]; apply Nat.le_refl
rw [lctxr_def, ← List.reverseAux, List.reverseAux_eq]
dsimp [lctxr]; rw [← List.reverseAux, List.reverseAux_eq]
rw [pushLCtxs_lt (by rw [List.length_append]; apply Nat.le_trans exlt (Nat.le_add_right _ _))]
dsimp [List.getD]; rw [List.get?_append exlt];
rw [List.get?_reverse _ (by dsimp [List.length]; apply Nat.le_refl _)]
Expand Down
187 changes: 104 additions & 83 deletions Auto/Embedding/LamBitVec.lean
View file

Large diffs are not rendered by default.

6 changes: 4 additions & 2 deletions Auto/Embedding/LamChecker.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1648,7 +1648,8 @@ theorem EtomStep.eval_correct
exists replaceAtDep eVarVal' r.maxEVarSucc eV
apply And.intro ?left (And.intro hsk ?right)
case left =>
intro n hlt; dsimp [replaceAt, replaceAtDep]
-- Note how the result of `dsimp` remains seemingly unchanged while `rw` fails when we remove `levt'`
intro n hlt; dsimp [levt', replaceAt, replaceAtDep]
rw [Nat.beq_eq_false_of_ne (Nat.ne_of_lt hlt)]
case right =>
apply Nat.le_trans (LamTerm.maxEVarSucc_skolemize? h₂)
Expand All @@ -1675,7 +1676,8 @@ theorem EtomStep.eval_correct
exists replaceAtDep eVarVal' r.maxEVarSucc eV
apply And.intro ?left (And.intro hdef ?right)
case left =>
intro n hlt; dsimp [replaceAt, replaceAtDep]
-- Note how the result of `dsimp` remains seemingly unchanged while `rw` fails when we remove `levt'`
intro n hlt; dsimp [levt', replaceAt, replaceAtDep]
rw [Nat.beq_eq_false_of_ne (Nat.ne_of_lt hlt)]
case right =>
rw [LamTerm.maxEVarSucc_mkEq]; dsimp [LamTerm.maxEVarSucc]
Expand Down
6 changes: 3 additions & 3 deletions Auto/Embedding/LamSystem.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1699,7 +1699,7 @@ theorem LamGenModify.rwGenAtIfSign {modify} (H : LamGenModify lval modify weaken
dsimp; have ⟨.ofApp _ (.ofApp _ _ wfArgI') _, _⟩ := IH
apply LamValid.impLift (LamValid.and_imp_and_of_right_imp wfArgII wfArgI' wfArgI) IH
case false =>
cases h₂ : LamTerm.rwGenAt occ modify (.app (.base .prop) (.base .and) argII) <;> intro h <;> cases h
cases h₂ : LamTerm.rwGenAt occ modify (.app (.base .prop) (.base (.pcst .and)) argII) <;> intro h <;> cases h
case refl argAp' =>
cases occ <;> try cases h₁
case cons b' occ =>
Expand Down Expand Up @@ -1733,7 +1733,7 @@ theorem LamGenModify.rwGenAtIfSign {modify} (H : LamGenModify lval modify weaken
dsimp; have ⟨.ofApp _ (.ofApp _ _ wfArgI') _, _⟩ := IH
apply LamValid.impLift (LamValid.or_imp_or_of_right_imp wfArgII wfArgI' wfArgI) IH
case false =>
cases h₂ : LamTerm.rwGenAt occ modify (.app (.base .prop) (.base .or) argII) <;> intro h <;> cases h
cases h₂ : LamTerm.rwGenAt occ modify (.app (.base .prop) (.base (.pcst .or)) argII) <;> intro h <;> cases h
case refl argAp' =>
cases occ <;> try cases h₁
case cons b' occ =>
Expand Down Expand Up @@ -1767,7 +1767,7 @@ theorem LamGenModify.rwGenAtIfSign {modify} (H : LamGenModify lval modify weaken
dsimp; have ⟨.ofApp _ (.ofApp _ _ wfArgI') _, _⟩ := IH
apply LamValid.impLift (LamValid.imp_trans' wfArgII wfArgI' wfArgI) IH
case false =>
cases h₂ : LamTerm.rwGenAt occ modify (.app (.base .prop) (.base .imp) argII) <;> intro h <;> cases h
cases h₂ : LamTerm.rwGenAt occ modify (.app (.base .prop) (.base (.pcst .imp)) argII) <;> intro h <;> cases h
case refl argAp' =>
cases occ <;> try cases h₁
case cons b' occ =>
Expand Down
1 change: 0 additions & 1 deletion Auto/Lib/NatExtra.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
import Std.Data.Nat.Lemmas
import Auto.Lib.BoolExtra

namespace Auto
Expand Down
66 changes: 33 additions & 33 deletions Auto/Translation/Lam2D.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ def interpLamSortAsUnlifted : LamSort → ExternM Expr
| .xH => return .const ``String []
| .xO .xH => return .const ``Empty []
| _ => return .const ``Empty []
| .bv n => return .app (.const ``Std.BitVec []) (.lit (.natVal n))
| .bv n => return .app (.const ``BitVec []) (.lit (.natVal n))
| .func s₁ s₂ => do
return .forallE `_ (← interpLamSortAsUnlifted s₁) (← interpLamSortAsUnlifted s₂) .default

Expand Down Expand Up @@ -191,59 +191,59 @@ def interpStringConstAsUnlifted : StringConst → Expr

open Embedding in
def interpBitVecConstAsUnlifted : BitVecConst → Expr
| .bvVal n i => mkApp2 (.const ``Std.BitVec.ofNat []) (.lit (.natVal n)) (.lit (.natVal i))
| .bvofNat n => .app (.const ``Std.BitVec.ofNat []) (.lit (.natVal n))
| .bvtoNat n => .app (.const ``Std.BitVec.toNat []) (.lit (.natVal n))
| .bvofInt n => .app (.const ``Std.BitVec.ofInt []) (.lit (.natVal n))
| .bvtoInt n => .app (.const ``Std.BitVec.toInt []) (.lit (.natVal n))
| .bvmsb n => .app (.const ``Std.BitVec.msb []) (.lit (.natVal n))
| .bvVal n i => mkApp2 (.const ``BitVec.ofNat []) (.lit (.natVal n)) (.lit (.natVal i))
| .bvofNat n => .app (.const ``BitVec.ofNat []) (.lit (.natVal n))
| .bvtoNat n => .app (.const ``BitVec.toNat []) (.lit (.natVal n))
| .bvofInt n => .app (.const ``BitVec.ofInt []) (.lit (.natVal n))
| .bvtoInt n => .app (.const ``BitVec.toInt []) (.lit (.natVal n))
| .bvmsb n => .app (.const ``BitVec.msb []) (.lit (.natVal n))
| .bvaOp n op =>
match op with
| .add => .app (.const ``Std.BitVec.add []) (.lit (.natVal n))
| .sub => .app (.const ``Std.BitVec.sub []) (.lit (.natVal n))
| .mul => .app (.const ``Std.BitVec.mul []) (.lit (.natVal n))
| .udiv => .app (.const ``Std.BitVec.smtUDiv []) (.lit (.natVal n))
| .urem => .app (.const ``Std.BitVec.umod []) (.lit (.natVal n))
| .sdiv => .app (.const ``Std.BitVec.smtSDiv []) (.lit (.natVal n))
| .srem => .app (.const ``Std.BitVec.srem []) (.lit (.natVal n))
| .smod => .app (.const ``Std.BitVec.smod []) (.lit (.natVal n))
| .bvneg n => .app (.const ``Std.BitVec.neg []) (.lit (.natVal n))
| .bvabs n => .app (.const ``Std.BitVec.abs []) (.lit (.natVal n))
| .add => .app (.const ``BitVec.add []) (.lit (.natVal n))
| .sub => .app (.const ``BitVec.sub []) (.lit (.natVal n))
| .mul => .app (.const ``BitVec.mul []) (.lit (.natVal n))
| .udiv => .app (.const ``BitVec.smtUDiv []) (.lit (.natVal n))
| .urem => .app (.const ``BitVec.umod []) (.lit (.natVal n))
| .sdiv => .app (.const ``BitVec.smtSDiv []) (.lit (.natVal n))
| .srem => .app (.const ``BitVec.srem []) (.lit (.natVal n))
| .smod => .app (.const ``BitVec.smod []) (.lit (.natVal n))
| .bvneg n => .app (.const ``BitVec.neg []) (.lit (.natVal n))
| .bvabs n => .app (.const ``BitVec.abs []) (.lit (.natVal n))
| .bvcmp n prop? op =>
match prop? with
| false =>
match op with
| .ult => .app (.const ``Std.BitVec.ult []) (.lit (.natVal n))
| .ule => .app (.const ``Std.BitVec.ule []) (.lit (.natVal n))
| .slt => .app (.const ``Std.BitVec.slt []) (.lit (.natVal n))
| .sle => .app (.const ``Std.BitVec.sle []) (.lit (.natVal n))
| .ult => .app (.const ``BitVec.ult []) (.lit (.natVal n))
| .ule => .app (.const ``BitVec.ule []) (.lit (.natVal n))
| .slt => .app (.const ``BitVec.slt []) (.lit (.natVal n))
| .sle => .app (.const ``BitVec.sle []) (.lit (.natVal n))
| true =>
match op with
| .ult => .app (.const ``BitVec.propult []) (.lit (.natVal n))
| .ule => .app (.const ``BitVec.propule []) (.lit (.natVal n))
| .slt => .app (.const ``BitVec.propslt []) (.lit (.natVal n))
| .sle => .app (.const ``BitVec.propsle []) (.lit (.natVal n))
| .bvand n => .app (.const ``Std.BitVec.and []) (.lit (.natVal n))
| .bvor n => .app (.const ``Std.BitVec.or []) (.lit (.natVal n))
| .bvxor n => .app (.const ``Std.BitVec.xor []) (.lit (.natVal n))
| .bvnot n => .app (.const ``Std.BitVec.not []) (.lit (.natVal n))
| .bvand n => .app (.const ``BitVec.and []) (.lit (.natVal n))
| .bvor n => .app (.const ``BitVec.or []) (.lit (.natVal n))
| .bvxor n => .app (.const ``BitVec.xor []) (.lit (.natVal n))
| .bvnot n => .app (.const ``BitVec.not []) (.lit (.natVal n))
| .bvshOp n smt? op =>
match smt? with
| false =>
match op with
| .shl => .app (.const ``Std.BitVec.shiftLeft []) (.lit (.natVal n))
| .lshr => .app (.const ``Std.BitVec.ushiftRight []) (.lit (.natVal n))
| .ashr => .app (.const ``Std.BitVec.sshiftRight []) (.lit (.natVal n))
| .shl => .app (.const ``BitVec.shiftLeft []) (.lit (.natVal n))
| .lshr => .app (.const ``BitVec.ushiftRight []) (.lit (.natVal n))
| .ashr => .app (.const ``BitVec.sshiftRight []) (.lit (.natVal n))
| true =>
match op with
| .shl => mkApp2 (.const ``BitVec.smtHshiftLeft []) (.lit (.natVal n)) (.lit (.natVal n))
| .lshr => mkApp2 (.const ``BitVec.smtHushiftRight []) (.lit (.natVal n)) (.lit (.natVal n))
| .ashr => mkApp2 (.const ``BitVec.smtHsshiftRight []) (.lit (.natVal n)) (.lit (.natVal n))
| .bvappend n m => mkApp2 (.const ``Std.BitVec.append []) (.lit (.natVal n)) (.lit (.natVal m))
| .bvextract n h l => mkApp3 (.const ``Std.BitVec.extractLsb []) (.lit (.natVal n)) (.lit (.natVal h)) (.lit (.natVal l))
| .bvrepeat w i => mkApp2 (.const ``Std.BitVec.replicate []) (.lit (.natVal w)) (.lit (.natVal i))
| .bvzeroExtend w v => mkApp2 (.const ``Std.BitVec.zeroExtend []) (.lit (.natVal w)) (.lit (.natVal v))
| .bvsignExtend w v => mkApp2 (.const ``Std.BitVec.signExtend []) (.lit (.natVal w)) (.lit (.natVal v))
| .bvappend n m => mkApp2 (.const ``BitVec.append []) (.lit (.natVal n)) (.lit (.natVal m))
| .bvextract n h l => mkApp3 (.const ``BitVec.extractLsb []) (.lit (.natVal n)) (.lit (.natVal h)) (.lit (.natVal l))
| .bvrepeat w i => mkApp2 (.const ``BitVec.replicate []) (.lit (.natVal w)) (.lit (.natVal i))
| .bvzeroExtend w v => mkApp2 (.const ``BitVec.zeroExtend []) (.lit (.natVal w)) (.lit (.natVal v))
| .bvsignExtend w v => mkApp2 (.const ``BitVec.signExtend []) (.lit (.natVal w)) (.lit (.natVal v))

open Embedding in
def interpLamBaseTermAsUnlifted : LamBaseTerm → ExternM Expr
Expand Down
2 changes: 1 addition & 1 deletion Auto/Translation/LamFOL2SMT.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -205,7 +205,7 @@ private def lamBaseTerm2STerm_Arity1 (arg : STerm) : LamBaseTerm → TransM LamA
let arg1 := .qStrApp "-" #[.qStrApp (← lamBvToNat2String n) #[arg], .sConst (.num (2 ^ n))]
let arg2 := .qStrApp (← lamBvToNat2String n) #[arg]
return .qStrApp "ite" #[msbExpr, arg1, arg2]
-- @Std.BitVec.msb n a = not ((a &&& (1 <<< (n - 1))) = 0#n)
-- @BitVec.msb n a = not ((a &&& (1 <<< (n - 1))) = 0#n)
| .bvcst (.bvmsb n) => return mkSMTMsbExpr n arg
| .bvcst (.bvneg _) => return .qStrApp "bvneg" #[arg]
| .bvcst (.bvabs _) => return .qStrApp "bvabs" #[arg]
Expand Down
Loading

0 comments on commit 041898f

Please sign in to comment.