From de17a103657642a8e770091bcf7b1038c43431e3 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 23 Oct 2024 14:06:03 -0700
Subject: [PATCH] Use axiom instead of variable for globals, consts

This performs much better in Lean. Large examples that would run out of
memory before now go through relatively quickly.

Also, add some more tests to the list of those expected to pass.
---
 Source/Provers/LeanAuto/LeanAutoGenerator.cs | 25 +++++++-------------
 Test/lean-auto/lean-tests                    | 10 ++++++++
 2 files changed, 19 insertions(+), 16 deletions(-)

diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
index 82684398f..5ca9b8b43 100644
--- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs
+++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
@@ -18,8 +18,6 @@ public class LeanAutoGenerator : ReadOnlyVisitor
 {
   private readonly TextWriter writer;
   private readonly VCGenOptions options;
-  private readonly List<NamedDeclaration> globalVars = new();
-  private readonly HashSet<string> usedNames = new();
   private bool usesMaps;
   private readonly List<string> mapAxiomNames =
     new(new[]
@@ -216,7 +214,6 @@ public override ReturnCmd VisitReturnCmd(ReturnCmd node)
   public override Expr VisitIdentifierExpr(IdentifierExpr node)
   {
     var name = SanitizeNameForLean(node.Name);
-    usedNames.Add(name);
     WriteText(name);
     return node;
   }
@@ -279,13 +276,13 @@ public override Type VisitBvType(BvType node)
   public override Constant VisitConstant(Constant node)
   {
     var ti = node.TypedIdent;
-    WriteText("variable ");
-    Visit(ti);
+    var name = SanitizeNameForLean(ti.Name);
+    WriteText($"axiom {name} : ");
+    Visit(ti.Type);
     if (node.Unique) {
       AddUniqueConst(ti.Type, Name(node));
     }
     WriteLine();
-    globalVars.Add(node);
     return node;
   }
 
@@ -340,10 +337,8 @@ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
 
   public override TypedIdent VisitTypedIdent(TypedIdent node)
   {
-    WriteText("(");
     var name = SanitizeNameForLean(node.Name);
-    WriteText(name);
-    WriteText(" : ");
+    WriteText($"( {name} : ");
     Visit(node.Type);
     WriteText(")");
     return node;
@@ -385,10 +380,11 @@ public override Expr VisitLetExpr(LetExpr node)
 
   public override GlobalVariable VisitGlobalVariable(GlobalVariable node)
   {
-    WriteText("variable ");
-    Visit(node.TypedIdent);
+    var ti = node.TypedIdent;
+    var name = SanitizeNameForLean(ti.Name);
+    WriteText($"axiom {name} : ");
+    Visit(ti.Type);
     WriteLine();
-    globalVars.Add(node);
     return node;
   }
 
@@ -822,7 +818,6 @@ public override Implementation VisitImplementation(Implementation node)
     var name = Name(node);
     var entryLabel = BlockName(node.Blocks[0]);
 
-    usedNames.Clear(); // Skip any globals used only by axioms, etc.
     WriteLine();
     WriteLine($"namespace impl_{name}");
     WriteLine();
@@ -837,8 +832,7 @@ public override Implementation VisitImplementation(Implementation node)
     WriteLine($"theorem {name}_correct");
     WriteParams(node);
     var paramNames =
-      globalVars.Select(Name).Where(x => usedNames.Contains(x))
-        .Concat(node.InParams.Select(Name))
+        node.InParams.Select(Name)
         .Concat(node.OutParams.Select(Name))
         .Concat(node.LocVars.Select(Name));
     var paramString = String.Join(' ', paramNames);
@@ -852,7 +846,6 @@ public override Implementation VisitImplementation(Implementation node)
     WriteLine($"end impl_{name}");
 
     usesMaps = false; // Skip map axioms in the next implementation if it doesn't need them
-    usedNames.Clear(); // Skip any globals not used by the next implementation
 
     return node;
   }
diff --git a/Test/lean-auto/lean-tests b/Test/lean-auto/lean-tests
index 516c1604a..d2d53a3f0 100644
--- a/Test/lean-auto/lean-tests
+++ b/Test/lean-auto/lean-tests
@@ -1,3 +1,13 @@
+../extractloops/detLoopExtract.bpl
+../extractloops/detLoopExtractNested.bpl
+../extractloops/t1.bpl
+../extractloops/t2.bpl
+../inline/expansion4.bpl
+../inline/inline_n_0.bpl
+../inline/test1.bpl
+../inline/test2.bpl
+../inline/test3.bpl
+../inline/test6.bpl
 ../textbook/TuringFactorial.bpl
 ../textbook/DutchFlag.bpl
 ../textbook/Bubble.bpl