Module-level options

Source/DafnyCore/AST/Attributes.cs

@@ -18,6 +18,13 @@ void ObjectInvariant() {
   public static string ExternAttributeName = "extern";
   public static string VerifyAttributeName = "verify";
   public static string AutoGeneratedAttributeName = "auto_generated";
+  public static string TypeEncodingAttributeName = "type_encoding";
+  public static string PruneAttributeName = "prune";
+  public static string SolverAttributeName = "solver";
+  public static string NativeSeqAttributeName = "native_seq";
+  public static string NoLitAttributeName = "no_lit";
+  public static string IsolateAssertionsAttriubuteName = "isolate_assertions";
+  public static string ProverOptAttributeName = "prover_opt";
 
   public string Name;
   /*Frozen*/

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -3,6 +3,7 @@
 using System.Collections.Immutable;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using Microsoft.Boogie.SMTLib;
 using Microsoft.Dafny.Auditor;
 
 namespace Microsoft.Dafny;
@@ -49,6 +50,7 @@ public string FullName {
   public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface)
   private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.
 
+  public bool UsesFuel = false; // Set by Translator.ComputeFunctionFuel
   public DefaultClassDecl DefaultClass { get; set; }
 
   public readonly List<TopLevelDecl> SourceDecls = new();
@@ -69,6 +71,76 @@ public string FullName {
       : new[] { new Pointer<TopLevelDecl>(() => DefaultClass, v => DefaultClass = (DefaultClassDecl)v) }).
     Concat(SourceDecls.ToPointers()).Concat(ResolvedPrefixNamedModules.ToPointers());
 
+  public Boogie.CoreOptions.TypeEncoding? GetTypeEncodingAttribute {
+    get {
+      if (Attributes.Find(Attributes, Attributes.TypeEncodingAttributeName) is Attributes te 
+          && te.Args.Count == 1 
+          && te.Args[0] is LiteralExpr { Value: string encoding }) {
+        return encoding switch {
+          "p" => Boogie.CoreOptions.TypeEncoding.Predicates,
+          "a" => Boogie.CoreOptions.TypeEncoding.Arguments,
+          "m" => Boogie.CoreOptions.TypeEncoding.Monomorphic,
+          _ => null
+        };
+      }
+      return null;
+    }
+  }
+
+  public bool? GetPruneAttribute {
+    get {
+      if (Attributes.Find(Attributes, Attributes.PruneAttributeName) is Attributes pa 
+          && pa.Args.Count == 1 
+          && pa.Args[0] is LiteralExpr { Value: string prune }) {
+        return int.Parse(prune) switch {
+          1 => true,
+          0 => false,
+          _ => null
+        };
+      }
+      return null;
+    }
+  }
+
+  public List<(string, string)> GetAllProverOptAttributes {
+    get {
+      var allExpressions = Attributes.FindAllExpressions(Attributes, Attributes.ProverOptAttributeName);
+      if (allExpressions == null) {
+        return null;
+      }
+      return allExpressions
+        .SelectMany(exprs => exprs.Select(expr => expr?.AsStringLiteral()?.Split('=')))
+        .Where(splitArray => splitArray is {Length: 2})
+        .Select(splitArray => (splitArray[0], splitArray[1]))
+        .ToList();
+    }
+  }
+
+  public SolverKind? GetSolverAttribute {
+    get {
+      if (Attributes.Find(Attributes, Attributes.SolverAttributeName) is Attributes te 
+          && te.Args.Count == 1 
+          && te.Args[0] is LiteralExpr { Value: string encoding }) {
+        return encoding switch {
+          "cvc5" => SolverKind.CVC5,
+          "z3" => SolverKind.Z3,
+          "yices2" => SolverKind.YICES2,
+          _ => null
+        };
+      }
+      return null;
+    }
+  }
+
+  public bool UseNativeSeq =>
+    Attributes.Contains(Attributes, Attributes.NativeSeqAttributeName);
+
+  public bool NoLits =>
+    Attributes.Contains(Attributes, Attributes.NoLitAttributeName);
+
+  public bool IsolateAssertions =>
+    Attributes.Contains(Attributes, Attributes.IsolateAssertionsAttriubuteName);
+
   public IEnumerable<TopLevelDecl> DefaultClasses {
     get { return DefaultClass == null ? Enumerable.Empty<TopLevelDecl>() : new TopLevelDecl[] { DefaultClass }; }
   }

Source/DafnyCore/DafnyCore.csproj

@@ -38,6 +38,13 @@
 
   <ItemGroup>
     <Content Include="DafnyPrelude.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeSeqNative.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeSeqAxiom.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeSetAxiom.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeISetAxiom.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeMultiSetAxiom.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeMapAxiom.bpl" CopyToOutputDirectory="PreserveNewest" />
+    <Content Include="DafnyPreludeIMapAxiom.bpl" CopyToOutputDirectory="PreserveNewest" />
   </ItemGroup>
 
   <ItemGroup>

Source/DafnyCore/DafnyOptions.cs

@@ -12,6 +12,7 @@
 using System.Reflection;
 using System.Text.RegularExpressions;
 using JetBrains.Annotations;
+using Microsoft.Boogie.SMTLib;
 using Microsoft.Dafny;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;
@@ -311,6 +312,20 @@ public enum DiagnosticsFormats {
     public bool AllowSourceFolders = false;
     public List<string> SourceFolders { get; } = new(); // list of folders, for those commands that permit processing all source files in folders
 
+    public bool UseSeqs = true;
+    public bool UseSeqTheory = false; // Requires UseSeqs = true. TypeEncoding must be Monomorphic.
+    public bool InlineSeqTheoryFunctions = true; // Do not enable if theory functions are used in axiom triggers.
+    public bool UseSets = true;
+    public bool UseISets = true;
+    public bool UseMultiSets = true;
+    public bool UseMaps = true;
+    public bool UseIMaps = true;
+    public string CVC5Path = null;
+    public bool UseLits = true;
+
+    public SolverKind Solver = SolverKind.Z3; // TODO: Heads up: this is not currently used!
+    public int Z3CaseSplitValue = 3;
+
     public enum ContractTestingMode {
       None,
       Externs,
@@ -824,6 +839,18 @@ protected bool ParseDafnySpecificOption(string name, Bpl.CommandLineParseState p
             }
           }
           return true;
+
+        case "prune":
+          if (ps.ConfirmArgumentCount(1)) {
+            if (args[ps.i] == "1") {
+              Prune = true;
+            } else if (args[ps.i] == "0") {
+              Prune = false;
+            } else {
+              InvalidArgumentError(name, ps);
+            }
+          }
+          return true;
       }
 
       // Defer to superclass
@@ -872,6 +899,8 @@ public void ApplyDefaultOptionsWithoutSettingsDefault() {
         SetZ3Options(z3Version);
       }
 
+      SetCVC5ExecutablePath();
+
       // Ask Boogie to perform abstract interpretation
       UseAbstractInterpretation = true;
       Ai.J_Intervals = true;
@@ -1163,6 +1192,16 @@ private Version SetZ3ExecutablePath() {
       return null;
     }
 
+    private void SetCVC5ExecutablePath() {
+      var platform = System.Environment.OSVersion.Platform;
+      var isUnix = platform == PlatformID.Unix || platform == PlatformID.MacOSX;
+      CVC5Path ??= System.Environment
+        .GetEnvironmentVariable("PATH")?
+        .Split(isUnix ? ':' : ';')
+        .Select(s => Path.Combine(s, isUnix ? "cvc5" : "cvc5.exe"))
+        .FirstOrDefault(File.Exists);
+    }
+
     private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?<major>\d+)\.(?<minor>\d+)\.(?<patch>\d+)");
 
     [CanBeNull]
@@ -1193,9 +1232,13 @@ public static Version GetZ3Version(string proverPath) {
     }
 
     // Set a Z3 option, but only if it is not overwriting an existing option.
-    private void SetZ3Option(string name, string value) {
-      if (!ProverOptions.Any(o => o.StartsWith($"O:{name}="))) {
-        ProverOptions.Add($"O:{name}={value}");
+    public void SetZ3Option(string name, string value, bool overwrite = false) {
+      string optionPrefix = $"O:{name}=";
+      int index = ProverOptions.FindIndex(o => o.StartsWith(optionPrefix));
+      if (index == -1) {
+        ProverOptions.Add($"{optionPrefix}{value}");
+      } else if (overwrite) {
+        ProverOptions[index] = $"{optionPrefix}{value}";
       }
     }