From 508032d31340cfe4b888c3b9c87c1e29f0c93f68 Mon Sep 17 00:00:00 2001 From: Lorenz Leutgeb Date: Sat, 24 Oct 2020 01:54:59 +0200 Subject: [PATCH] tcr: Add configuration properties, improve output --- typechecker/lac.properties | 39 ++++++++++ .../java/xyz/leutgeb/lorenz/lac/Main.java | 23 ++++++ .../xyz/leutgeb/lorenz/lac/ast/Program.java | 16 ++-- .../leutgeb/lorenz/lac/commands/Haskell.java | 4 +- .../xyz/leutgeb/lorenz/lac/commands/Run.java | 31 ++++---- .../xyz/leutgeb/lorenz/lac/module/Loader.java | 17 ++++- .../resources/constraints/Constraint.java | 4 +- .../lac/typing/resources/proving/Prover.java | 21 +++--- .../lorenz/lac/typing/resources/rules/W.java | 33 ++++----- .../solving/ConstraintSystemSolver.java | 74 +++++++++---------- .../xyz/leutgeb/lorenz/lac/util/Util.java | 13 +++- .../leutgeb/lorenz/lac/util/Z3Support.java | 42 +++++++++++ .../main/resources/simplelogger.properties | 5 -- .../test/java/xyz/leutgeb/lorenz/lac/S61.java | 2 +- .../java/xyz/leutgeb/lorenz/lac/S62Eager.java | 6 +- .../xyz/leutgeb/lorenz/lac/S62EqLazy.java | 4 +- .../java/xyz/leutgeb/lorenz/lac/Tactics.java | 4 +- .../java/xyz/leutgeb/lorenz/lac/Tests.java | 4 +- .../xyz/leutgeb/lorenz/lac/rules/WTest.java | 5 +- typechecker/tacas.sh | 1 + typechecker/tacas/Readme.txt | 16 ++-- 21 files changed, 241 insertions(+), 123 deletions(-) create mode 100644 typechecker/lac.properties create mode 100644 typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Z3Support.java delete mode 100644 typechecker/src/main/resources/simplelogger.properties diff --git a/typechecker/lac.properties b/typechecker/lac.properties new file mode 100644 index 0000000..8a9e9dd --- /dev/null +++ b/typechecker/lac.properties @@ -0,0 +1,39 @@ +# Logging +# See http://www.slf4j.org/api/org/slf4j/impl/SimpleLogger.html +org.slf4j.simpleLogger.defaultLogLevel=info +org.slf4j.simpleLogger.showLogName=false +org.slf4j.simpleLogger.dateTimeFormat="" +org.slf4j.simpleLogger.showThreadName=false +org.slf4j.simplelogger.levelInBrackets=true + +org.slf4j.simpleLogger.log.io.micronaut=info + +# Z3 +# Configuration properties for Z3 must be prefixed with `com.microsoft.z3`. +# A list can be obtained by running `z3 -p` in a shell. The complete list +# of parameters is very long. The most important ones are global parameters: +# auto_config (bool) (default: true) +# debug_ref_count (bool) (default: false) +# dot_proof_file (string) (default: proof.dot) +# dump_models (bool) (default: false) +# memory_high_watermark (unsigned int) (default: 0) +# memory_max_alloc_count (unsigned int) (default: 0) +# memory_max_size (unsigned int) (default: 0) [bytes] +# model (bool) (default: true) +# model_validate (bool) (default: false) +# proof (bool) (default: false) +# rlimit (unsigned int) (default: 0) +# smtlib2_compliant (bool) (default: false) +# stats (bool) (default: false) +# timeout (unsigned int) (default: 4294967295) [milliseconds] +# trace (bool) (default: false) +# trace_file_name (string) (default: z3.log) +# type_check (bool) (default: true) +# unsat_core (bool) (default: false) +# verbose (unsigned int) (default: 0) +# warning (bool) (default: true) +# well_sorted_check (bool) (default: false) +com.microsoft.z3.timeout=900000 +com.microsoft.z3.memory_max_size=25769803776 +com.microsoft.z3.unsat_core=true +com.microsoft.z3.trace=false diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/Main.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/Main.java index 6f4f8ff..6649599 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/Main.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/Main.java @@ -1,5 +1,9 @@ package xyz.leutgeb.lorenz.lac; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.Properties; import picocli.CommandLine; import picocli.CommandLine.Command; import xyz.leutgeb.lorenz.lac.commands.Haskell; @@ -11,8 +15,27 @@ subcommands = {LNF.class, Haskell.class, Run.class}) public class Main implements Runnable { public static void main(String[] args) { + readProperties(); new CommandLine(new Main()).execute(args); } + private static void readProperties() { + final var propertiesFile = Paths.get("lac.properties"); + if (Files.exists(propertiesFile) && Files.isReadable(propertiesFile)) { + try (final var reader = Files.newBufferedReader(propertiesFile)) { + final Properties properties = new Properties(); + properties.load(reader); + for (final var property : properties.entrySet()) { + if (!(property.getKey() instanceof String && property.getValue() instanceof String)) { + continue; + } + System.setProperty((String) property.getKey(), (String) property.getValue()); + } + } catch (IOException ioException) { + ioException.printStackTrace(); + } + } + } + public void run() {} } diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java index 69d995d..1d12223 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java @@ -7,7 +7,6 @@ import java.io.IOException; import java.io.PrintStream; import java.nio.file.Path; -import java.nio.file.Paths; import java.util.Collections; import java.util.HashMap; import java.util.HashSet; @@ -48,13 +47,16 @@ public class Program { @Getter private final List> order; @Getter @Setter private String name; - private final Path basePath; + @Getter private final Path basePath; - public Program(Map functionDefinitions, List> order) { + public Program( + Map functionDefinitions, + List> order, + Path basePath) { this.functionDefinitions = functionDefinitions; this.order = order; this.name = flatten(this.order).stream().map(Util::fqnToFlatFilename).collect(joining("+")); - this.basePath = Paths.get(".", "out"); + this.basePath = basePath; } public void infer() throws UnificationError, TypeError { @@ -88,7 +90,7 @@ public Optional> solve() { return solve( new HashMap<>(), new HashSet<>(), - (program, constraints) -> ConstraintSystemSolver.solve(constraints, name)); + (program, constraints) -> ConstraintSystemSolver.solve(constraints, basePath)); } public Optional> solve( @@ -96,7 +98,7 @@ public Optional> solve( return solve( functionAnnotations, new HashSet<>(), - (program, constraints) -> ConstraintSystemSolver.solve(constraints, name)); + (program, constraints) -> ConstraintSystemSolver.solve(constraints, basePath)); } public Optional> solve( @@ -105,7 +107,7 @@ public Optional> solve( return solve( functionAnnotations, outsideConstraints, - (program, constraints) -> ConstraintSystemSolver.solve(constraints, name)); + (program, constraints) -> ConstraintSystemSolver.solve(constraints, basePath)); } public Optional prove( diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Haskell.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Haskell.java index 032484c..8555062 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Haskell.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Haskell.java @@ -11,6 +11,7 @@ import java.nio.file.Path; import java.util.regex.Pattern; import java.util.stream.Collectors; +import lombok.extern.slf4j.Slf4j; import picocli.CommandLine; import xyz.leutgeb.lorenz.lac.ast.FunctionDefinition; import xyz.leutgeb.lorenz.lac.ast.Program; @@ -19,6 +20,7 @@ import xyz.leutgeb.lorenz.lac.unification.UnificationError; @CommandLine.Command(name = "hs") +@Slf4j public class Haskell implements Runnable { @CommandLine.Parameters( index = "0", @@ -91,7 +93,7 @@ public void run() { } catch (IOException ex) { ex.printStackTrace(); } - System.out.println(path); + log.info("{}", path); } } } diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Run.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Run.java index 4115df8..6f165a7 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Run.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Run.java @@ -22,6 +22,7 @@ import java.util.Set; import java.util.regex.Pattern; import java.util.stream.Collectors; +import lombok.extern.slf4j.Slf4j; import picocli.CommandLine; import xyz.leutgeb.lorenz.lac.ast.FunctionDefinition; import xyz.leutgeb.lorenz.lac.ast.Program; @@ -39,6 +40,7 @@ import xyz.leutgeb.lorenz.lac.unification.UnificationError; @CommandLine.Command(name = "run") +@Slf4j public class Run implements Runnable { @CommandLine.Parameters( index = "0", @@ -108,7 +110,7 @@ public void run() { } catch (UnificationError | TypeError unificationError) { throw new RuntimeException(unificationError); } - // System.out.println("Loaded definitions:"); + // log.info("Loaded definitions:"); // program.printAllSimpleSignaturesInOrder(System.out); Multimap output = ArrayListMultimap.create(); Multimap imports = HashMultimap.create(); @@ -122,9 +124,11 @@ public void run() { } } + log.info("Output will go to {}", program.getBasePath().toAbsolutePath()); + Map tacticsMap = new HashMap<>(); - // System.out.println(infer ? "Given for comparison:" : "Will check following types:"); + // log.info(infer ? "Given for comparison:" : "Will check following types:"); for (int i = 0; i < program.getOrder().size(); i++) { final var stratum = program.getOrder().get(i); @@ -139,29 +143,28 @@ public void run() { } } - System.out.println(fd.getAnnotatedSignatureString()); + log.info(fd.getAnnotatedSignatureString()); - System.out.println("\tDependencies: " + fd.getOcurringFunctionsNonRecursive()); - System.out.println("\tSource: " + fd.getBody().getSource().getRoot()); + log.info("\tDependencies: " + fd.getOcurringFunctionsNonRecursive()); + log.info("\tSource: " + fd.getBody().getSource().getRoot()); if (tactics != null) { final var p = tacticsMap.get(fd.getFullyQualifiedName()); if (p == null) { - System.out.println("\tTactic: n/a (will use automatic proof generation)"); + log.info("\tTactic: n/a (will use automatic proof generation)"); } else { - System.out.println("\tTactic: " + p.toAbsolutePath()); + log.info("\tTactic: " + p.toAbsolutePath()); } } } } - System.out.println(); - System.out.println("Generating constraints..."); + log.info("Generating constraints..."); Optional optionalProver = program.proveWithTactics(new HashMap<>(), tacticsMap, infer); - System.out.println("Done."); + log.info("Done."); if (optionalProver.isEmpty()) { - System.out.println("Nonterminating function definition detected. Aborting."); + log.info("Nonterminating function definition detected. Aborting."); System.exit(1); return; } @@ -187,7 +190,7 @@ public void run() { Optional> solution = Optional.empty(); - System.out.println("Solving constraints..."); + log.info("Solving constraints..."); if (infer) { final List setCountingRankCoefficients = new ArrayList<>(); final List setCountingNonRankCoefficients = new ArrayList<>(); @@ -249,9 +252,9 @@ public void run() { solution = prover.solve(outsideConstraints, emptyList(), "sat", domain); } - System.out.println("Done. Result(s): "); + log.info("Done. Result(s): "); if (solution.isEmpty()) { - System.out.println("UNSAT"); + log.info("UNSAT"); System.exit(1); return; } diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/module/Loader.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/module/Loader.java index 2d5e517..bbd93d6 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/module/Loader.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/module/Loader.java @@ -1,13 +1,21 @@ package xyz.leutgeb.lorenz.lac.module; -import static java.util.stream.Collectors.*; +import static java.util.stream.Collectors.toList; +import static java.util.stream.Collectors.toMap; +import static java.util.stream.Collectors.toUnmodifiableList; import com.google.common.base.Functions; import java.io.IOException; import java.io.OutputStream; import java.nio.file.Files; import java.nio.file.Path; -import java.util.*; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.Spliterators; +import java.util.Stack; import java.util.function.Predicate; import java.util.regex.Pattern; import java.util.stream.Collectors; @@ -40,6 +48,8 @@ public class Loader { private final Graph g = new DefaultDirectedGraph<>(null, DefaultEdge::new, false); + @Getter private final String id = String.format("%08x", System.currentTimeMillis() * 31); + public Loader(Path home) { if (!Files.exists(home) || !Files.isDirectory(home) || !Files.isReadable(home)) { throw new IllegalArgumentException("home must be an existing readable directory"); @@ -174,7 +184,8 @@ public Program load(Set names) throws IOException { .collect(toMap(Functions.identity(), functionDefinitions::get)), stronglyConnectedSubgraphs.stream() .map(g -> g.vertexSet().stream().sorted().collect(toUnmodifiableList())) - .collect(toList())); + .collect(toList()), + Path.of(".", "out", id)); } private Path path(String moduleName) { diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/constraints/Constraint.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/constraints/Constraint.java index 8dc177e..34af3d2 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/constraints/Constraint.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/constraints/Constraint.java @@ -3,6 +3,7 @@ import static guru.nidi.graphviz.model.Factory.graph; import static guru.nidi.graphviz.model.Factory.node; import static xyz.leutgeb.lorenz.lac.util.Util.append; +import static xyz.leutgeb.lorenz.lac.util.Util.output; import static xyz.leutgeb.lorenz.lac.util.Util.rawObjectNode; import com.google.common.collect.BiMap; @@ -18,7 +19,6 @@ import guru.nidi.graphviz.model.Graph; import guru.nidi.graphviz.model.Link; import guru.nidi.graphviz.model.Node; -import java.nio.file.Files; import java.nio.file.Path; import java.util.Collections; import java.util.HashMap; @@ -90,7 +90,7 @@ public static void plot(String name, Set constraints, Path path) { Graphviz.useEngine(lel); var viz = Graphviz.fromGraph(graph); Path target = path.resolve(name + "-constraints.svg"); - try (final var out = Files.newOutputStream(target)) { + try (final var out = output(target)) { viz.engine(Engine.DOT).render(Format.SVG).toOutputStream(out); log.info("Wrote plot to {}", target); } diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/proving/Prover.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/proving/Prover.java index 2675315..0895f78 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/proving/Prover.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/proving/Prover.java @@ -7,10 +7,11 @@ import static java.util.stream.Collectors.toUnmodifiableMap; import static xyz.leutgeb.lorenz.lac.ast.Identifier.LEAF_NAME; import static xyz.leutgeb.lorenz.lac.util.Util.bug; -import static xyz.leutgeb.lorenz.lac.util.Util.loadZ3; +import static xyz.leutgeb.lorenz.lac.util.Util.output; import static xyz.leutgeb.lorenz.lac.util.Util.stack; import static xyz.leutgeb.lorenz.lac.util.Util.supply; import static xyz.leutgeb.lorenz.lac.util.Util.undefinedText; +import static xyz.leutgeb.lorenz.lac.util.Z3Support.load; import com.google.common.collect.Sets; import com.google.common.collect.Streams; @@ -18,7 +19,6 @@ import guru.nidi.graphviz.engine.Format; import guru.nidi.graphviz.engine.Graphviz; import java.io.IOException; -import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; import java.util.Collection; @@ -158,12 +158,13 @@ private static class RuleApplication { } public Prover(String name, AnnotatingGlobals globals, Path basePath) { - loadZ3(); + load(); this.name = name; this.globals = globals; this.basePath = basePath; } + @Deprecated public Prover(String name, AnnotatingGlobals globals) { this(name, globals, Paths.get("out")); } @@ -431,11 +432,11 @@ public void plot() { Graphviz transformed = Graphviz.fromGraph(exporter.transform(proof)); final var target = basePath.resolve(name + "-proof.svg"); - transformed.render(Format.SVG).toOutputStream(Files.newOutputStream(target)); + transformed.render(Format.SVG).toOutputStream(output(target)); log.info("Proof plotted to {}", target); final var dotTarget = basePath.resolve(name + "-proof.dot"); - transformed.render(Format.DOT).toOutputStream(Files.newOutputStream(dotTarget)); + transformed.render(Format.DOT).toOutputStream(output(dotTarget)); log.info("Proof exported to {}", dotTarget); } catch (Exception e) { log.warn("Non-critical exception thrown.", e); @@ -463,11 +464,11 @@ public void plotWithSolution(Map solution) { Graphviz transformed = Graphviz.fromGraph(exporter.transform(proof)); final var target = basePath.resolve(name + "-proof.svg"); - transformed.render(Format.SVG).toOutputStream(Files.newOutputStream(target)); + transformed.render(Format.SVG).toOutputStream(output(target)); log.info("Proof plotted to {}", target); final var dotTarget = basePath.resolve(name + "-proof.xdot"); - transformed.render(Format.XDOT).toOutputStream(Files.newOutputStream(dotTarget)); + transformed.render(Format.XDOT).toOutputStream(output(dotTarget)); log.info("Proof exported to {}", dotTarget); } catch (Exception e) { log.warn("Non-critical exception thrown.", e); @@ -486,7 +487,7 @@ public Optional> solve( Set outsideConstraints, List target) { return ConstraintSystemSolver.solve( Sets.union(outsideConstraints, Sets.union(accumulatedConstraints, externalConstraints)), - name, + basePath, target); } @@ -494,7 +495,7 @@ public Optional> solve( Set outsideConstraints, List target, String suffix) { return ConstraintSystemSolver.solve( Sets.union(outsideConstraints, Sets.union(accumulatedConstraints, externalConstraints)), - name + suffix, + basePath.resolve(suffix), target); } @@ -505,7 +506,7 @@ public Optional> solve( ConstraintSystemSolver.Domain domain) { return ConstraintSystemSolver.solve( Sets.union(outsideConstraints, Sets.union(accumulatedConstraints, externalConstraints)), - name + suffix, + basePath.resolve(suffix), target, domain); } diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/rules/W.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/rules/W.java index 964d6fd..834ab12 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/rules/W.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/rules/W.java @@ -152,27 +152,23 @@ public static List compareCoefficientsLessOrEqualUsingFarkas( final List, List>> lemmaPlus2Instances = LEMMA_PLUS2_ENABLED ? lemmaPlus2(potentialFunctions) : emptyList(); - // TODO(lorenz.leutgeb): Make this a log.trace(...); - // List identifierNames = identifiers.stream().map(Object::toString).collect(toList()); - /* - System.out.println("(w) --- " + left.getId() + " <= " + right.getId() + " --- "); - System.out.println("pot: " + potentialFunctions); - System.out.println("ids: " + identifiers); - System.out.println( + log.trace("(w) --- " + left.getId() + " <= " + right.getId() + " --- "); + log.trace("pot: " + potentialFunctions); + log.trace("ids: " + identifiers); + log.trace( "lts: " + knowLt.stream().map(x -> x.map(identifiers::get)).collect(toUnmodifiableList())); - System.out.println( + log.trace( "eqs: " + knowEq.stream().map(x -> x.map(identifiers::get)).collect(toUnmodifiableList())); - System.out.println( - "one: " + knowOne.stream().map(identifiers::get).collect(toUnmodifiableList())); + log.trace("one: " + knowOne.stream().map(identifiers::get).collect(toUnmodifiableList())); - System.out.println("monotony:"); + log.trace("monotony:"); monotonyInstances.forEach(System.out::println); - System.out.println("lemma2XY:"); + log.trace("lemma2XY:"); lemma2XYInstances.forEach( instance -> { - System.out.println( + log.trace( "2 * [...0, 2] + " + instance.get(0) + " + " @@ -181,20 +177,19 @@ public static List compareCoefficientsLessOrEqualUsingFarkas( + instance.get(2)); }); - System.out.println("lemma1Plus:"); + log.trace("lemma1Plus:"); lemmaPlus1Instances.forEach( instance -> { - System.out.println(instance.getRight() + " <= 1 * [...0, 2] + " + instance.getLeft()); + log.trace(instance.getRight() + " <= 1 * [...0, 2] + " + instance.getLeft()); }); - System.out.println("lemma2Plus:"); + log.trace("lemma2Plus:"); lemmaPlus2Instances.forEach( instance -> { - System.out.println(instance.getRight() + " <= 2 * [...0, 2] + " + instance.getLeft()); + log.trace(instance.getRight() + " <= 2 * [...0, 2] + " + instance.getLeft()); }); - System.out.println(" --- "); - */ + log.trace(" --- "); // m is the number of rows of expert knowledge. final var m = diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/solving/ConstraintSystemSolver.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/solving/ConstraintSystemSolver.java index af57b9d..05da1ca 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/solving/ConstraintSystemSolver.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/solving/ConstraintSystemSolver.java @@ -5,25 +5,26 @@ import static java.util.Collections.emptyList; import static java.util.Optional.empty; import static xyz.leutgeb.lorenz.lac.util.Util.bug; -import static xyz.leutgeb.lorenz.lac.util.Util.loadZ3; +import static xyz.leutgeb.lorenz.lac.util.Util.output; import static xyz.leutgeb.lorenz.lac.util.Util.randomHex; import static xyz.leutgeb.lorenz.lac.util.Util.signum; +import static xyz.leutgeb.lorenz.lac.util.Z3Support.load; import com.google.common.collect.HashBiMap; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; -import com.microsoft.z3.Global; import com.microsoft.z3.IntNum; import com.microsoft.z3.Model; import com.microsoft.z3.Optimize; -import com.microsoft.z3.Params; import com.microsoft.z3.RatNum; import com.microsoft.z3.Statistics; import com.microsoft.z3.Status; -import java.io.File; -import java.io.FileNotFoundException; +import java.io.IOException; +import java.io.PrintStream; import java.io.PrintWriter; +import java.nio.file.Path; +import java.nio.file.Paths; import java.time.Duration; import java.time.Instant; import java.util.Arrays; @@ -47,48 +48,33 @@ @Slf4j public class ConstraintSystemSolver { - private static final long BYTES_IN_A_GIBIBYTE = 1 << 30; - - static { - Global.setParameter("timeout", String.valueOf(Duration.ofMinutes(15).toMillis())); - Global.setParameter("memory_max_size", String.valueOf(24L * BYTES_IN_A_GIBIBYTE)); - } - private static Map z3Config(boolean unsatCore) { // Execute `z3 -p` to get a list of parameters. return Map.of("unsat_core", String.valueOf(unsatCore)); } public static Optional> solve(Set constraints) { - return solve(constraints, randomHex(), emptyList(), Domain.INTEGER); + return solve(constraints, Paths.get("out", randomHex()), emptyList(), Domain.INTEGER); } public static Optional> solve( - Set constraints, String name) { - return solve(constraints, name, emptyList(), Domain.INTEGER); + Set constraints, Path outPath) { + return solve(constraints, outPath, emptyList(), Domain.INTEGER); } public static Optional> solve( - Set constraints, String name, List target) { - return solve(constraints, name, target, Domain.INTEGER); + Set constraints, Path outPath, List target) { + return solve(constraints, outPath, target, Domain.INTEGER); } public static Optional> solve( - Set constraints, String name, List target, Domain domain) { - loadZ3(); + Set constraints, Path outPath, List target, Domain domain) { + load(); final var unsatCore = target.isEmpty(); - // domain = Domain.RATIONAL; - try (final var ctx = new Context(z3Config(unsatCore))) { - // final var solver = Domain.INTEGER.equals(domain) && target.isEmpty() ? - // ctx.mkSolver("QF_LIA") - // : ctx.mkSolver(); final var solver = ctx.mkSolver(); - Params solver_params = ctx.mkParams(); - solver_params.add("ignore_solver1", true); - solver.setParameters(solver_params); var optimize = !target.isEmpty(); final Optimize opt = optimize ? ctx.mkOptimize() : null; @@ -159,13 +145,14 @@ public static Optional> solve( log.trace("Z3 Scopes: " + (optimize ? "?" : solver.getNumScopes())); log.trace("Z3 Assertions: " + (optimize ? "?" : solver.getAssertions().length)); - // TODO(lorenz.leutgeb): Parameterize location. - File smtFile = new File("out", name + ".smt"); - try (PrintWriter out = new PrintWriter(smtFile)) { + final Path smtFile = outPath.resolve("instance.smt"); + + try (final var out = new PrintWriter(output(smtFile))) { out.println(optimize ? opt : solver); log.debug("Wrote SMT instance to {}.", smtFile); - } catch (FileNotFoundException e) { - log.warn("Failed to write SMT instance to {}.", smtFile, e); + } catch (IOException ioException) { + log.warn("Failed to write SMT instance to {}.", smtFile, ioException); + ioException.printStackTrace(); } Optional optionalModel = Optional.empty(); @@ -178,7 +165,8 @@ public static Optional> solve( opt::getUnsatCore, unsatCore, opt::toString, - opt::getStatistics); + opt::getStatistics, + outPath); } else { optionalModel = check( @@ -187,7 +175,8 @@ public static Optional> solve( solver::getUnsatCore, unsatCore, solver::toString, - solver::getStatistics); + solver::getStatistics, + outPath); } if (optionalModel.isEmpty()) { return empty(); @@ -238,18 +227,25 @@ private static Optional check( Supplier getUnsatCore, boolean unsatCore, Supplier program, - Supplier statistics) { + Supplier statistics, + Path outPath) { final var start = Instant.now(); log.debug("Solving start: " + start); var status = check.get(); final var stop = Instant.now(); log.debug("Solving duration: " + (Duration.between(start, stop))); if (SATISFIABLE.equals(status)) { - /* - for (var entry : statistics.get().getEntries()) { - log.info("{}={}", entry.Key, entry.getValueString()); + try { + try (final var out = output(outPath.resolve("z3-statistics.txt"))) { + final var printer = new PrintStream(out); + for (var entry : statistics.get().getEntries()) { + log.trace("{}={}", entry.Key, entry.getValueString()); + printer.println(entry.Key + "=" + entry.getValueString()); + } + } + } catch (Exception exception) { + // ignored } - */ return Optional.of(getModel.get()); } else if (UNKNOWN.equals(status)) { log.error("Attempt to solve constraint system yielded unknown result."); diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Util.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Util.java index 4de0b2b..375f120 100644 --- a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Util.java +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Util.java @@ -9,7 +9,11 @@ import com.microsoft.z3.RatNum; import guru.nidi.graphviz.model.Node; +import java.io.IOException; +import java.io.OutputStream; import java.io.PrintStream; +import java.nio.file.Files; +import java.nio.file.Path; import java.util.ArrayList; import java.util.Collection; import java.util.Comparator; @@ -154,10 +158,6 @@ public static void loadLibrary(String name) { } } - public static void loadZ3() { - loadLibrary("z3java"); - } - public static Fraction toFraction(RatNum x) { return new Fraction( x.getBigIntNumerator().intValueExact(), x.getBigIntDenominator().intValueExact()); @@ -333,4 +333,9 @@ public static Stream mapToString(Stream stream) { public Iterable toIterable(Stream stream) { return stream::iterator; } + + public static OutputStream output(Path path) throws IOException { + Files.createDirectories(path.getParent()); + return Files.newOutputStream(path); + } } diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Z3Support.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Z3Support.java new file mode 100644 index 0000000..b398860 --- /dev/null +++ b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/util/Z3Support.java @@ -0,0 +1,42 @@ +package xyz.leutgeb.lorenz.lac.util; + +import static java.lang.System.getProperties; + +import com.microsoft.z3.Global; +import lombok.extern.slf4j.Slf4j; + +@Slf4j +public class Z3Support { + private static boolean loaded = false; + private static final String PROPERTY_PREFIX = "com.microsoft.z3."; + + public static synchronized void load() { + if (!loaded) { + Util.loadLibrary("z3java"); + } + loaded = true; + + try { + for (var property : getProperties().entrySet()) { + if (!(property.getKey() instanceof String && property.getValue() instanceof String)) { + continue; + } + + final var key = (String) property.getKey(); + + if (!key.startsWith(PROPERTY_PREFIX)) { + continue; + } + + final var value = (String) property.getValue(); + + final String parameter = key.substring(PROPERTY_PREFIX.length()); + log.trace("Setting Z3 parameter '{}' to '{}'", key, value); + + Global.setParameter(parameter, value); + } + } catch (Throwable throwable) { + log.debug("Error setting Z3 parameters.", throwable); + } + } +} diff --git a/typechecker/src/main/resources/simplelogger.properties b/typechecker/src/main/resources/simplelogger.properties deleted file mode 100644 index 427d970..0000000 --- a/typechecker/src/main/resources/simplelogger.properties +++ /dev/null @@ -1,5 +0,0 @@ -org.slf4j.simpleLogger.showThreadName=false -org.slf4j.simpleLogger.showDateTime=true -org.slf4j.simpleLogger.showShortLogName=true -org.slf4j.simpleLogger.showLogName=false -org.slf4j.simpleLogger.defaultLogLevel=info \ No newline at end of file diff --git a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S61.java b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S61.java index 1a573bd..cb2035f 100644 --- a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S61.java +++ b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S61.java @@ -185,7 +185,7 @@ public void lnf() { constraints.addAll(sumConstraints); Optional> optionalSolution = - ConstraintSystemSolver.solve(constraints, NAME /*, singletonList(target)*/); + ConstraintSystemSolver.solve(constraints /*, singletonList(target)*/); assertTrue(optionalSolution.isPresent()); diff --git a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62Eager.java b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62Eager.java index 6594f93..5a873d3 100644 --- a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62Eager.java +++ b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62Eager.java @@ -186,7 +186,7 @@ public void zigzigAbove() throws IOException, ConstraintSystemException { prover.plot(); final var constraints = prover.getAccumulatedConstraints(); - final var solution = ConstraintSystemSolver.solve(constraints, "splay"); + final var solution = ConstraintSystemSolver.solve(constraints); try { Constraint.plot("splay-above", constraints, Path.of("out")); } catch (Exception e) { @@ -240,7 +240,7 @@ public void zigzigBelow() throws ConstraintSystemException { assertEquals(E3, first.get(1).getExpression()); final var constraints = prover.getAccumulatedConstraints(); - final var solution = ConstraintSystemSolver.solve(constraints, "splay-below"); + final var solution = ConstraintSystemSolver.solve(constraints); assertTrue(solution.isPresent()); final var assertions = new ArrayList(); for (Obligation o : prover.getProof()) { @@ -288,7 +288,7 @@ public void costFree() throws IOException, ConstraintSystemException { prover.plot(); final var constraints = prover.getAccumulatedConstraints(); - final var solution = ConstraintSystemSolver.solve(constraints, "splay-cf"); + final var solution = ConstraintSystemSolver.solve(constraints); assertTrue(solution.isPresent()); final var assertions = new ArrayList(); diff --git a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62EqLazy.java b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62EqLazy.java index 282b3ad..0f21467 100644 --- a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62EqLazy.java +++ b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/S62EqLazy.java @@ -1058,14 +1058,14 @@ public void zigzigWithCf() throws IOException { emptySet() /*cfProver.getAccumulatedConstraints()*/), sumConstraints); - final var solution = ConstraintSystemSolver.solve(combined, SPLAY_FQN); + final var solution = ConstraintSystemSolver.solve(combined); // final var solution = // prover.solve(); // (Sets.union(fixQ3, fixQ2)); // ;Sets.union(sumConstraints, fixQ2)); // Constraint.plot(FQN, prover.getAccumulatedConstraints(), Paths.get("out")); assertTrue(solution.isPresent()); final var minSolution = ConstraintSystemSolver.solve( - sumConstraints, SPLAY_FQN, List.of(rankCoefficientSum, coefficientSum)); + sumConstraints, Paths.get("TODO"), List.of(rankCoefficientSum, coefficientSum)); System.out.println( "splay_eq w/out minimization: " diff --git a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tactics.java b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tactics.java index c6df68d..c3fea61 100644 --- a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tactics.java +++ b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tactics.java @@ -14,8 +14,8 @@ import static xyz.leutgeb.lorenz.lac.typing.resources.coefficients.KnownCoefficient.ZERO; import static xyz.leutgeb.lorenz.lac.typing.resources.coefficients.UnknownCoefficient.unknown; import static xyz.leutgeb.lorenz.lac.util.Util.append; -import static xyz.leutgeb.lorenz.lac.util.Util.loadZ3; import static xyz.leutgeb.lorenz.lac.util.Util.randomHex; +import static xyz.leutgeb.lorenz.lac.util.Z3Support.load; import java.io.IOException; import java.nio.file.Paths; @@ -50,7 +50,7 @@ public class Tactics { @BeforeAll public static void beforeAll() { - loadZ3(); + load(); } protected static final Annotation Q = diff --git a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tests.java b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tests.java index 1730639..ced1d12 100644 --- a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tests.java +++ b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/Tests.java @@ -18,7 +18,7 @@ import static xyz.leutgeb.lorenz.lac.typing.simple.TypeVariable.ALPHA; import static xyz.leutgeb.lorenz.lac.typing.simple.TypeVariable.BETA; import static xyz.leutgeb.lorenz.lac.util.Util.fqnToFlatFilename; -import static xyz.leutgeb.lorenz.lac.util.Util.loadZ3; +import static xyz.leutgeb.lorenz.lac.util.Z3Support.load; import java.io.File; import java.io.FileOutputStream; @@ -209,7 +209,7 @@ public static Program loadAndNormalizeAndInferAndUnshare(String fqn) @BeforeAll public static void beforeAll() { - loadZ3(); + load(); } @ParameterizedTest diff --git a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/rules/WTest.java b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/rules/WTest.java index 9bdc9c9..518771a 100644 --- a/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/rules/WTest.java +++ b/typechecker/src/test/java/xyz/leutgeb/lorenz/lac/rules/WTest.java @@ -63,7 +63,7 @@ public void constant() { Annotation.constant(1, "expected", ONE), "test")); - final var solution = ConstraintSystemSolver.solve(constraints, "test"); + final var solution = ConstraintSystemSolver.solve(constraints); assertTrue(solution.isPresent()); } @@ -112,8 +112,7 @@ void withGtKnowledge( List.of(smallerTree, biggerTree), smallerPotential, biggerPotential, - sizeAnalysis)), - testInfo.getDisplayName()); + sizeAnalysis))); assertEquals(expectedSolution, solution.isPresent()); } diff --git a/typechecker/tacas.sh b/typechecker/tacas.sh index 1ffba61..bdbc55f 100755 --- a/typechecker/tacas.sh +++ b/typechecker/tacas.sh @@ -16,6 +16,7 @@ mkdir -p $DIST/tacas/artifact/{dependencies,resources/grammars} # Copy over executable and remove version specifier. cp -v build/native-image/$PROJECT-$VERSION $DIST/tacas/artifact/lac +cp -v lac.properties $DIST/tacas/artifact/lac.properties # Target Ubuntu patchelf $DIST/tacas/artifact/lac \ diff --git a/typechecker/tacas/Readme.txt b/typechecker/tacas/Readme.txt index 790bfde..489a045 100644 --- a/typechecker/tacas/Readme.txt +++ b/typechecker/tacas/Readme.txt @@ -7,6 +7,12 @@ The presented system compiled as an x86-64 ELF binary. It will dynamically link to `libc`. Usage of is explained below. +### `lac.properties` + +Configuration file that can be used to change Z3 parameters and +logging settings. By setting the log level to "debug" or "trace", +much more detailled output can be obtained. + ### `dependencies` Contains the Ubuntu package dependencies. They must be installed before the @@ -38,10 +44,6 @@ subcommand ./lac run --help -Create a directory where output can be placed - - mkdir out - For example, to check the type annotation of the function definition `PairingHeap.link`, run @@ -116,10 +118,12 @@ These correspond to the following lines/names in the paper (line by line): ## Resource Limits -The artifact imposes following resource limits: +The artifact imposes following resource limits on Z3: Wall clock runtime: 15 minutes - Limit for Z3 memory: 24GiB + Limit for memory: 24GiB + +These (and other) parameters as well as logging configuration can be changed in `lac.properties`. All results were computed on a machine with 32GiB main memory, and computations took on the order of less than a second up to fifteen minutes.