Skip to content

Commit

Permalink
more llvm tests fixed
Browse files Browse the repository at this point in the history
  • Loading branch information
luisacicolini committed Nov 19, 2024
1 parent 716a2fd commit 9568154
Showing 1 changed file with 10 additions and 10 deletions.
20 changes: 10 additions & 10 deletions SSA/Projects/InstCombine/ScalingTest.lean
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ set_option maxRecDepth 1100
set_option maxHeartbeats 400000

def and_sequence_10_lhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
%v2 = llvm.and %v1, %C1
Expand All @@ -44,7 +44,7 @@ def and_sequence_10_lhs (w : Nat) :=
}]

def and_sequence_10_rhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
llvm.return %v1
Expand All @@ -57,7 +57,7 @@ theorem and_sequence_10_eq (w : Nat) :
alive_auto

def and_sequence_15_lhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
%v2 = llvm.and %v1, %C1
Expand All @@ -76,7 +76,7 @@ def and_sequence_15_lhs (w : Nat) :=
}]

def and_sequence_15_rhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
llvm.return %v1
Expand All @@ -90,7 +90,7 @@ theorem and_sequence_15_eq (w : Nat) :

set_option maxHeartbeats 500000 in
def and_sequence_20_lhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
%v2 = llvm.and %v1, %C1
Expand All @@ -116,7 +116,7 @@ def and_sequence_20_lhs (w : Nat) :=
}]

def and_sequence_20_rhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
llvm.return %v1
Expand All @@ -130,7 +130,7 @@ theorem and_sequence_20_eq (w : Nat) :

set_option maxHeartbeats 1700000 in
def and_sequence_30_lhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
%v2 = llvm.and %v1, %C1
Expand Down Expand Up @@ -166,7 +166,7 @@ def and_sequence_30_lhs (w : Nat) :=
}]

def and_sequence_30_rhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
llvm.return %v1
Expand All @@ -181,7 +181,7 @@ theorem and_sequence_30_eq (w : Nat) :
set_option maxHeartbeats 3800000 in
set_option maxRecDepth 1500 in
def and_sequence_40_lhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
%v2 = llvm.and %v1, %C1
Expand Down Expand Up @@ -227,7 +227,7 @@ def and_sequence_40_lhs (w : Nat) :=
}]

def and_sequence_40_rhs (w : Nat) :=
[llvm ( w )| {
[llvm( w )| {
^bb0(%C1 : _, %Z : _):
%v1 = llvm.and %Z, %C1
llvm.return %v1
Expand Down

0 comments on commit 9568154

Please sign in to comment.