-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Verify solutions using libverify (from omsim)
- Loading branch information
Showing
8 changed files
with
205 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
|
|
||
| /// <summary> | ||
| /// 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. | ||
| /// </summary> | ||
| 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); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
| } | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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(); | ||
| } | ||
| } | ||
| } | ||
| } |