diff --git a/OpusSolver/IO/SolutionWriter.cs b/OpusSolver/IO/SolutionWriter.cs index 3123ee2..c92244d 100644 --- a/OpusSolver/IO/SolutionWriter.cs +++ b/OpusSolver/IO/SolutionWriter.cs @@ -41,7 +41,7 @@ public void WriteSolution() m_writer.Write(7); // Solution format m_writer.Write(m_solution.Puzzle.FileName); m_writer.Write(m_solution.Name); - m_writer.Write(0); // TODO: Write metrics + WriteMetrics(m_solution.Metrics); IEnumerable realObjects = m_solution.GetObjects(); realObjects = realObjects.Concat(m_solution.GetObjects()) @@ -56,6 +56,27 @@ public void WriteSolution() } } + private void WriteMetrics(Metrics metrics) + { + if (metrics == null) + { + m_writer.Write(0); + return; + } + + // Number of metrics + m_writer.Write(4); + + m_writer.Write(0); + m_writer.Write(metrics.Cycles); + m_writer.Write(1); + m_writer.Write(metrics.Cost); + m_writer.Write(2); + m_writer.Write(metrics.Area); + m_writer.Write(3); + m_writer.Write(metrics.Instructions); + } + private void WriteObject(GameObject obj) { m_writer.Write(GetObjectName(obj)); diff --git a/OpusSolver/OpusSolver.csproj b/OpusSolver/OpusSolver.csproj index 20c5f80..ce58a78 100644 --- a/OpusSolver/OpusSolver.csproj +++ b/OpusSolver/OpusSolver.csproj @@ -60,6 +60,7 @@ + @@ -132,6 +133,9 @@ + + + diff --git a/OpusSolver/ProgramMain.cs b/OpusSolver/ProgramMain.cs index 1436aad..d56f96a 100644 --- a/OpusSolver/ProgramMain.cs +++ b/OpusSolver/ProgramMain.cs @@ -1,5 +1,6 @@ using OpusSolver.IO; using OpusSolver.Solver; +using OpusSolver.Verifier; using System; using System.Collections.Generic; using System.IO; @@ -16,10 +17,13 @@ private class CommandLineArguments { public List PuzzleFiles = new(); public string OutputDir; + public bool SkipVerification = false; } public static int Main(string[] args) { + sm_log.Debug($"Starting up"); + CommandLineArguments commandArgs; try { @@ -38,13 +42,14 @@ public static int Main(string[] args) foreach (var puzzleFile in commandArgs.PuzzleFiles) { string solutionFile = Path.Combine(commandArgs.OutputDir, Path.GetFileNameWithoutExtension(puzzleFile) + ".solution"); - if (SolvePuzzle(puzzleFile, solutionFile)) + if (SolvePuzzle(puzzleFile, solutionFile, commandArgs.SkipVerification)) { totalPuzzlesSolved++; } } - Console.WriteLine($"Generated solutions for {totalPuzzlesSolved}/{commandArgs.PuzzleFiles.Count} puzzles."); + string verifyMessage = commandArgs.SkipVerification ? "" : "and verified "; + sm_log.Info($"Successfully generated {verifyMessage}solutions for {totalPuzzlesSolved}/{commandArgs.PuzzleFiles.Count} puzzles."); } catch (Exception e) { @@ -86,6 +91,9 @@ private static CommandLineArguments ParseArguments(string[] args) excludedFiles.Add(args[++i]); break; } + case "--noverify": + commandArgs.SkipVerification = true; + break; default: puzzlePaths.Add(args[i]); break; @@ -127,11 +135,12 @@ private static void ShowUsage() sm_log.Error("Usage: OpusSolver.exe [] ..."); sm_log.Error(""); sm_log.Error("Options:"); - sm_log.Error(" --output Directory to write solutions to (default is current dir)"); - sm_log.Error(" --exclude Name of a puzzle file to skip"); + sm_log.Error(" --output Directory to write solutions to (default is current dir)"); + sm_log.Error(" --exclude Name of a puzzle file to skip"); + sm_log.Error(" --noverify Skip solution verification (useful if you don't have a copy of libverify)"); } - private static bool SolvePuzzle(string puzzleFile, string solutionFile) + private static bool SolvePuzzle(string puzzleFile, string solutionFile, bool skipVerification) { try { @@ -144,8 +153,23 @@ private static bool SolvePuzzle(string puzzleFile, string solutionFile) var solution = solver.Solve(); sm_log.Info($"Writing solution to \"{solutionFile}\""); + // It might be more efficient to write the solution to a byte array first and pass that to the verifier, + // rather than writing it to disk twice. But it's also convenient having a copy on disk even if the + // verification fails so that we can debug it in the game. SolutionWriter.WriteSolution(solution, solutionFile); + if (!skipVerification) + { + sm_log.Debug("Verifying solution"); + using var verifier = new SolutionVerifier(puzzleFile, solutionFile); + var metrics = verifier.CalculateMetrics(); + sm_log.Info($"Cost/cycles/area/instructions: {metrics.Cost}/{metrics.Cycles}/{metrics.Area}/{metrics.Instructions}"); + + sm_log.Debug($"Writing metrics to solution file"); + solution.Metrics = metrics; + SolutionWriter.WriteSolution(solution, solutionFile); + } + return true; } catch (ParseException e) @@ -155,7 +179,12 @@ private static bool SolvePuzzle(string puzzleFile, string solutionFile) } catch (SolverException e) { - sm_log.Error($"Unable to solve puzzle \"{puzzleFile}\": {e.Message}"); + sm_log.Error($"Error solving puzzle \"{puzzleFile}\": {e.Message}"); + return false; + } + catch (VerifierException e) + { + sm_log.Error($"Error verifying solution to puzzle \"{puzzleFile}\": {e.Message}"); return false; } catch (Exception e) diff --git a/OpusSolver/Solution/Metrics.cs b/OpusSolver/Solution/Metrics.cs new file mode 100644 index 0000000..e10317c --- /dev/null +++ b/OpusSolver/Solution/Metrics.cs @@ -0,0 +1,10 @@ +namespace OpusSolver +{ + public class Metrics + { + public int Cost { get; set; } + public int Cycles { get; set; } + public int Area { get; set; } + public int Instructions { get; set; } + } +} diff --git a/OpusSolver/Solution/Solution.cs b/OpusSolver/Solution/Solution.cs index 7d7ed93..a1bc4b0 100644 --- a/OpusSolver/Solution/Solution.cs +++ b/OpusSolver/Solution/Solution.cs @@ -13,6 +13,8 @@ public class Solution public List Objects { get; private set; } public Program Program { get; private set; } + public Metrics Metrics { get; set; } + public Solution(Puzzle puzzle, IEnumerable objects, Program program) { Puzzle = puzzle; diff --git a/OpusSolver/Verifier/NativeMethods.cs b/OpusSolver/Verifier/NativeMethods.cs new file mode 100644 index 0000000..44d5a82 --- /dev/null +++ b/OpusSolver/Verifier/NativeMethods.cs @@ -0,0 +1,42 @@ +using System; +using System.Runtime.InteropServices; + +namespace OpusSolver.Verifier +{ + internal static class NativeMethods + { + [DllImport("libverify")] + public static extern IntPtr verifier_create(string puzzle_filename, string solution_filename); + + [DllImport("libverify")] + public static extern void verifier_destroy(IntPtr verifier); + + [DllImport("libverify")] + private static extern IntPtr verifier_error(IntPtr verifier); + + /// + /// Wrapper function for calling verifier_error safely. This is required because verifier_error + /// returns a const char* which should not be freed. If we simply declare it as returning a string + /// then the default .NET marshalling will attempt to free the returned pointer, crashing the program. + /// + public static string GetVerifierError(IntPtr verifier) + { + return Marshal.PtrToStringAnsi(verifier_error(verifier)); + } + + [DllImport("libverify")] + public static extern int verifier_error_cycle(IntPtr verifier); + + [DllImport("libverify")] + public static extern int verifier_error_location_u(IntPtr verifier); + + [DllImport("libverify")] + public static extern int verifier_error_location_v(IntPtr verifier); + + [DllImport("libverify")] + public static extern void verifier_error_clear(IntPtr verifier); + + [DllImport("libverify")] + public static extern int verifier_evaluate_metric(IntPtr verifier, string metric); + } +} diff --git a/OpusSolver/Verifier/SolutionVerifier.cs b/OpusSolver/Verifier/SolutionVerifier.cs new file mode 100644 index 0000000..2377afc --- /dev/null +++ b/OpusSolver/Verifier/SolutionVerifier.cs @@ -0,0 +1,47 @@ +using System; + +namespace OpusSolver.Verifier +{ + public class SolutionVerifier : IDisposable + { + private IntPtr m_verifier; + + public SolutionVerifier(string puzzleFile, string solutionFile) + { + m_verifier = NativeMethods.verifier_create(puzzleFile, solutionFile); + CheckForError(); + } + + private int GetMetric(string metricName) + { + int metric = NativeMethods.verifier_evaluate_metric(m_verifier, metricName); + CheckForError(includeCycleAndLocation: true); + return metric; + } + + public Metrics CalculateMetrics() => new Metrics + { + Cost = GetMetric("cost"), + Cycles = GetMetric("cycles"), + Area = GetMetric("area"), + Instructions = GetMetric("instructions"), + }; + + public void Dispose() + { + if (m_verifier != IntPtr.Zero) + { + NativeMethods.verifier_destroy(m_verifier); + m_verifier = IntPtr.Zero; + } + } + + private void CheckForError(bool includeCycleAndLocation = false) + { + if (NativeMethods.GetVerifierError(m_verifier) != null) + { + throw new VerifierException(m_verifier, includeCycleAndLocation); + } + } + } +} diff --git a/OpusSolver/Verifier/VerifierException.cs b/OpusSolver/Verifier/VerifierException.cs new file mode 100644 index 0000000..5e6ebce --- /dev/null +++ b/OpusSolver/Verifier/VerifierException.cs @@ -0,0 +1,43 @@ +using System; +using System.Text; + +namespace OpusSolver.Verifier +{ + public class VerifierException : Exception + { + public int? Cycle { get; set; } + public Vector2? Location { get; set; } + + public VerifierException(IntPtr verifier, bool includeCycleAndLocation) + : base(NativeMethods.GetVerifierError(verifier)) + { + // These don't make sense for some types of errors (e.g. failing to load a puzzle) so only + // get them if requested + if (includeCycleAndLocation) + { + Cycle = NativeMethods.verifier_error_cycle(verifier); + Location = new Vector2(NativeMethods.verifier_error_location_u(verifier), NativeMethods.verifier_error_location_v(verifier)); + } + + NativeMethods.verifier_error_clear(verifier); + } + + public override string Message + { + get + { + var message = new StringBuilder(base.Message); + if (Cycle.HasValue) + { + message.Append($" on cycle {Cycle}"); + } + if (Location.HasValue) + { + message.Append($" at {Location}"); + } + + return message.ToString(); + } + } + } +}