Final touches for artifact submission

.gitignore

@@ -14,6 +14,7 @@ gradle.properties
 *.jar
 *.so
 *.dll
+atlas
 
 # Nix
 result

atlas.properties

@@ -36,7 +36,7 @@ org.slf4j.simpleLogger.showThreadName=true
 # Timeout 15M
 #com.microsoft.z3.timeout=900000
 # Timeout 2H
-#com.microsoft.z3.timeout=7200000
+com.microsoft.z3.timeout=7200000
 com.microsoft.z3.memory_max_size=25769803776
 com.microsoft.z3.unsat_core=true
 com.microsoft.z3.trace=false

flake.nix

@@ -244,13 +244,17 @@
             virtualbox = {
               vmName = "atlas";
               vmFileName = "atlas.ova";
-              #params = { usb = "off"; };
+              params = {
+                usb = "on";
+                usbehci = "off";
+                vram = 48;
+              };
             };
             environment.systemPackages = utils
-              ++ [ self.packages.${system}.atlas pkgs.evince ];
+              ++ [ self.packages.${system}.atlas pkgs.evince pkgs.vim ];
             networking.hostName = "atlas";
             users.users = {
-              atlas = {
+              evaluator = {
                 isNormalUser = true;
                 extraGroups = [ "wheel" ];
                 uid = 1000;
@@ -259,31 +263,44 @@
               };
               root.initialHashedPassword = "";
             };
-            home-manager.users.atlas.home = {
+            home-manager.users.evaluator.home = {
               file = let
                 referText = ''
-                  Please refer to
+                  To prepare evaluation, please open a terminal and execute
+
+                    /home/evaluator/prepare-evaluation.sh
+
+                  This will mount an overlay filesystem at
 
-                    /home/atlas/atlas/ARTIFACT.md
-                    (artifact information)
+                    /home/evaluator/atlas
 
-                    /home/atlas/${submission}
-                    (associated paper)
+                  Then, please refer to
+
+                    /home/evaluator/atlas/ARTIFACT.md
 
                   Note that `atlas` (command) is in `$PATH`, it can be executed in a terminal.
+
+                  Note that the associated paper is available at
+
+                    /home/evaluator/${submission}
                 '';
                 pdf = (self.packages.${system}.atlas-cav + "/" + submission);
               in {
-                "atlas".source = self.packages.${system}.atlas-src;
-
                 ${submission}.source = pdf;
                 "README.md".text = referText;
 
                 "Desktop/README.md".text = referText;
                 "Desktop/${submission}".source = pdf;
+
+                "prepare-evaluation.sh".source = pkgs.writeScript "prepare-evaluation" '' 
+                  #! ${pkgs.bash}/bin/bash
+                  set -xeuo pipefail
+                  mkdir --verbose --parents $HOME/.overlay/{upper,work} $HOME/atlas
+                  sudo mount --verbose --types overlay overlay --options upperdir=$HOME/.overlay/upper,workdir=$HOME/.overlay/work,lowerdir=${self.packages.${system}.atlas-src} $HOME/atlas
+                '';
               };
               stateVersion = "20.09";
-              sessionVariables.LAC_HOME = "${examples}";
+              sessionVariables.ATLAS_HOME = "${examples}";
             };
             security.sudo.wheelNeedsPassword = false;
             services = {
@@ -298,7 +315,7 @@
                 displayManager = {
                   autoLogin = {
                     enable = true;
-                    user = "atlas";
+                    user = "evaluator";
                   };
                   defaultSession = "xfce";
                 };

reproduce.sh

@@ -0,0 +1,25 @@
+#! /usr/bin/env bash
+
+set -euo pipefail
+
+function atlas_run () {
+	(set -x ;atlas --home src/test/resources/examples \
+	  run --tactics src/test/resources/tactics \
+	  $@ )
+}
+
+
+echo -e '\nSplayTree (inference)\n'
+atlas_run --infer "SplayTree\\.(splay(_max)?|insert|delete)"
+
+echo -e '\nSplayHeap (inference)\n'
+atlas_run --infer "SplayHeap\\.(insert|del_min)"
+
+echo -e '\nPairingHeap EXCEPT merge (inference)\n'
+atlas_run --infer "PairingHeap\\.(insert|merge_pairs|del_min_via_merge_pairs)_isolated"
+
+echo -e '\nPairingHeap.merge (checking)\n'
+atlas_run "PairingHeap\\.merge_isolated"
+
+echo -e '\nPairingHeap WITH merge (inference)\n'
+atlas_run --infer "PairingHeap\\.(insert|merge_pairs|del_min_via_merge_pairs|merge)_isolated"

src/main/java/xyz/leutgeb/lorenz/atlas/commands/Run.java

@@ -146,7 +146,10 @@ public void run() {
 
     final var result = program.solve(new HashMap<>(), tacticsMap, infer, Collections.emptySet());
     if (!result.isSatisfiable()) {
+      System.out.println("UNSAT");
       System.exit(1);
+    } else {
+      System.out.println("SAT");
     }
 
     System.out.println("Signatures:");

src/main/java/xyz/leutgeb/lorenz/atlas/module/Loader.java

@@ -1,5 +1,6 @@
 package xyz.leutgeb.lorenz.atlas.module;
 
+import static java.nio.file.FileVisitOption.FOLLOW_LINKS;
 import static java.util.Collections.synchronizedMap;
 import static java.util.Optional.ofNullable;
 import static java.util.function.Predicate.not;
@@ -145,7 +146,8 @@ public void autoload() throws IOException {
             home,
             8,
             ((path, basicFileAttributes) ->
-                path.getFileName().toString().endsWith(DOT_EXTENSION) && Util.goodForReading(path)))
+                path.getFileName().toString().endsWith(DOT_EXTENSION) && Util.goodForReading(path)),
+            FOLLOW_LINKS)
         .flatMap(
             path -> {
               try {

src/main/java/xyz/leutgeb/lorenz/atlas/typing/resources/Annotation.java

@@ -484,14 +484,21 @@ public String toLongString(List<String> parameters) {
                 e -> {
                   final var index = e.getKey();
                   final var coefficient = e.getValue();
-                  var result = "";
-                  if (!coefficient.equals(new KnownCoefficient(Fraction.ONE))) {
-                    result = coefficient.toString();
+
+                  final boolean cancelIndex = isUnitIndex(index);
+                  final boolean cancelCoefficient =
+                      coefficient.equals(new KnownCoefficient(Fraction.ONE));
+
+                  if (cancelCoefficient && cancelIndex) {
+                    return "1";
                   }
-                  if (isUnitIndex(index)) {
-                    return result;
+                  if (cancelIndex) {
+                    return coefficient.toString();
+                  }
+                  if (cancelCoefficient) {
+                    return toPotential(parameters, index);
                   }
-                  return result + " · " + toPotential(parameters, index);
+                  return coefficient + " · " + toPotential(parameters, index);
                 })
             .collect(Collectors.joining(" + "));
 

src/main/java/xyz/leutgeb/lorenz/atlas/typing/resources/CombinedFunctionAnnotation.java

@@ -66,10 +66,6 @@ public String getBounds(List<String> arguments) {
       return "?";
     }
 
-    if (withCost.from.size() != withCost.to.size()) {
-      return toString();
-    }
-
     final var withCost = this.withCost.getBound(arguments);
     final var withoutCost =
         this.withoutCost.stream()

src/main/java/xyz/leutgeb/lorenz/atlas/typing/resources/FunctionAnnotation.java

@@ -36,6 +36,14 @@ public boolean isZero() {
   }
 
   public String getBound(List<String> arguments) {
-    return Annotation.subtract(from, to).toLongString(arguments);
+    if (from.size() == to.size()) {
+      return Annotation.subtract(from, to).toLongString(arguments);
+    }
+
+    final var right = to.toLongString();
+    if ("0".equals(right)) {
+      return from.toLongString(arguments);
+    }
+    return from.toLongString(arguments) + " - [" + to.toLongString() + "]";
   }
 }

version.sh

@@ -3,4 +3,9 @@
 # This script is called whenever we need to know
 # the current version of the project.
 
-git describe --tags --always --dirty=-dirty
+if [ -x "$(command -v git)" ]
+then
+	git describe --tags --always --dirty=-dirty
+else
+	echo "v0"
+fi