Refactor: resolving ranks requires SmtContext

Author: kjcjohnson

ParserLibrary/Commands/GrammarBlockHelper.cs

@@ -192,7 +192,7 @@ public static (SemgusGrammar, IReadOnlyList<SemgusTermType>, SemgusTermType, Smt
                                                               semDatum.InputVariables.Where(v => v.Name == identifier).First());
                         }
                         else if (ctx.TryGetFunctionDeclaration(identifier, out var constant)
-                              && constant.TryResolveRank(out var rank, default))
+                              && constant.TryResolveRank(ctx, out var rank, default))
                         {
                             constructor = new(GensymUtils.Gensym("_SyProd", identifier.Symbol));
                             newProds.Add(new(ttDatum.NonTerminal, constructor, Enumerable.Empty<SemgusGrammar.NonTerminal>()));

ParserLibrary/Reader/Converters/TermConverter.cs

@@ -76,7 +76,7 @@ public override bool TryConvertImpl(Type tFrom, Type tTo, object from, [NotNullW
                 }
                 else if (_contextProvider.Context.TryGetFunctionDeclaration(qid.Id, out var defn))
                 {
-                    if (defn.TryResolveRank(out var rank, GetSortOrDie(qid.Sort) /* No arguments */))
+                    if (defn.TryResolveRank(_contextProvider.Context, out var rank, GetSortOrDie(qid.Sort) /* No arguments */))
                     {
                         to = new SmtFunctionApplication(defn, rank, new List<SmtTerm>());
                     }
@@ -362,7 +362,7 @@ public override bool TryConvertImpl(Type tFrom, Type tTo, object from, [NotNullW
                                                 return true;
                                             }
 
-                                            if (!orf!.TryResolveRank(out var rank, boolsort, Enumerable.Repeat(boolsort, convTerms.Count).ToArray()))
+                                            if (!orf!.TryResolveRank(_contextProvider.Context, out var rank, boolsort, Enumerable.Repeat(boolsort, convTerms.Count).ToArray()))
                                             {
                                                 throw new InvalidOperationException("Too many terms to match pattern.");
                                             }
@@ -434,7 +434,7 @@ public override bool TryConvertImpl(Type tFrom, Type tTo, object from, [NotNullW
                                 return true;
                             }
 
-                            if (defn.TryResolveRank(out var rank, GetSortOrDie(af.Id.Sort), argSorts))
+                            if (defn.TryResolveRank(_contextProvider.Context, out var rank, GetSortOrDie(af.Id.Sort), argSorts))
                             {
                                 to = new SmtFunctionApplication(defn, rank, args);
                             }

ParserTests/BitVectors/ExtractTests.cs

@@ -90,13 +90,13 @@ public void CanResolve(long i, long j, long m)
             var retSort = SmtBitVectorsTheory.BitVectorsSort.GetSort(n);
 
             // First, try without specifying the return sort
-            AssertTrue(function.TryResolveRank(out var rank, default, argSort));
+            AssertTrue(function.TryResolveRank(ctx, out var rank, default, argSort));
             Assert.Single(rank.ArgumentSorts);
             Assert.Equal(argSort, rank.ArgumentSorts[0]);
             Assert.Equal(retSort, rank.ReturnSort);
 
             // Then, with specifying the return sort
-            AssertTrue(function.TryResolveRank(out rank, retSort, argSort));
+            AssertTrue(function.TryResolveRank(ctx, out rank, retSort, argSort));
             Assert.Single(rank.ArgumentSorts);
             Assert.Equal(argSort, rank.ArgumentSorts[0]);
             Assert.Equal(retSort, rank.ReturnSort);
@@ -119,10 +119,10 @@ public void CannotResolve(long i, long j, long m, long? np = default)
             var retSort = SmtBitVectorsTheory.BitVectorsSort.GetSort(n);
 
             // First, try without specifying the return sort
-            AssertFalse(function.TryResolveRank(out var _, default, argSort));
+            AssertFalse(function.TryResolveRank(ctx, out var _, default, argSort));
 
             // Then, with specifying the return sort
-            AssertFalse(function.TryResolveRank(out _, retSort, argSort));
+            AssertFalse(function.TryResolveRank(ctx, out _, retSort, argSort));
         }
     }
 }

ParserTests/Issues/Issue43.cs

@@ -74,7 +74,7 @@ public void DoesNotThrowParseExceptionForBool()
         {
             SmtContext ctx = new();
             Assert.True(ctx.TryGetFunctionDeclaration(new("true"), out var truefn));
-            Assert.True(truefn!.TryResolveRank(out var rank, default));
+            Assert.True(truefn!.TryResolveRank(ctx, out var rank, default));
 
             SemgusToken testToken = new SymbolToken("test", default);
             SmtTerm testTerm = new SmtFunctionApplication(truefn, rank!, new List<SmtTerm>());

Semgus-Lib/Model/Smt/IApplicable.cs

@@ -25,11 +25,12 @@ public interface IApplicable
         /// <summary>
         /// Tries to get an appropriate rank for the given parameter and return sorts
         /// </summary>
+        /// <param name="ctx">The SMT context</param>
         /// <param name="rank">The resolved rank</param>
         /// <param name="returnSort">The return sort, if known</param>
         /// <param name="argumentSorts">The argument sorts</param>
         /// <returns>True if successfully resolved the rank</returns>
-        public bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts);
+        public bool TryResolveRank(SmtContext ctx, [NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts);
 
         /// <summary>
         /// Gets an informative string about available ranks

Semgus-Lib/Model/Smt/SmtFunction.cs

@@ -96,18 +96,19 @@ public void AddRankTemplate(SmtFunctionRank rank)
         /// <summary>
         /// Attempts to resolve a concrete rank for the given function signature
         /// </summary>
+        /// <param name="ctx">The SMT context</param>
         /// <param name="rank">The resolved rank</param>
         /// <param name="returnSort">Return sort of function call, if known</param>
         /// <param name="argumentSorts">Function call argument sorts</param>
         /// <returns>True if successfully resolved a concrete rank</returns>
-        public bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts)
+        public bool TryResolveRank(SmtContext ctx, [NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts)
         {
             var sameArity = _rankTemplates
                 .Where(r => r.Arity == argumentSorts.Length);
 
             foreach (var template in sameArity)
             {
-                if (TryResolveRank(out rank, template, returnSort, argumentSorts))
+                if (TryResolveRank(ctx, out rank, template, returnSort, argumentSorts))
                 {
                     return true; // We just pick the first one...maybe we need to check all templates and report ambiguities. TODO.
                 }
@@ -119,12 +120,13 @@ public bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtSor
         /// <summary>
         /// Attempts to resolve a concrete rank for the given function signature, from a single rank template
         /// </summary>
+        /// <param name="ctx">The SMT context</param>
         /// <param name="rank">The resolved rank</param>
         /// <param name="template">The rank template to try</param>
         /// <param name="returnSort">Return sort of function call, if known</param>
         /// <param name="argumentSorts">Function call argument sorts</param>
         /// <returns>True if successfully resolved a concrete rank</returns>
-        private bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtFunctionRank template, SmtSort? returnSort, params SmtSort[] argumentSorts)
+        private bool TryResolveRank(SmtContext ctx, [NotNullWhen(true)] out SmtFunctionRank? rank, SmtFunctionRank template, SmtSort? returnSort, params SmtSort[] argumentSorts)
         {
             Dictionary<SmtSort, SmtSort> resolvedParameters = new();
 

Semgus-Lib/Model/Smt/SmtMacro.cs

@@ -362,11 +362,12 @@ private bool CheckSortMatch(SmtSort a, SmtSort b, IDictionary<SmtSort, SmtSort>
         /// <summary>
         /// Tries to resolve a rank for this macro
         /// </summary>
+        /// <param name="ctx">The SMT context</param>
         /// <param name="rank">The resolved rank</param>
         /// <param name="returnSort">The return sort of the expression, if known</param>
         /// <param name="argumentSorts">Sorts of arguments</param>
         /// <returns>True if successfully resolved</returns>
-        public bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts)
+        public bool TryResolveRank(SmtContext ctx, [NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts)
         {
             var paramQueue = new Queue<MacroParameter>(_lambdaList);
             MacroParameter? formal = default;

Semgus-Lib/Model/Smt/Sorts/SmtDatatypeConstructor.cs

@@ -69,11 +69,12 @@ public bool IsArityPossible(int arity)
         /// <summary>
         /// Tries to get an appropriate rank for the given parameter and return sorts
         /// </summary>
+        /// <param name="ctx">The SMT context</param>
         /// <param name="rank">The resolved rank</param>
         /// <param name="returnSort">The return sort, if known</param>
         /// <param name="argumentSorts">The argument sorts</param>
         /// <returns>True if successfully resolved the rank</returns>
-        public bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts)
+        public bool TryResolveRank(SmtContext ctx, [NotNullWhen(true)] out SmtFunctionRank? rank, SmtSort? returnSort, params SmtSort[] argumentSorts)
         {
             // TODO: handle parameterized datatypes
             if (returnSort is not null && returnSort != Parent)

Semgus-Lib/Model/Smt/Terms/SmtTermBuilder.cs

@@ -74,7 +74,7 @@ public static SmtTerm Apply(SmtContext ctx, Action<object, string> onError, SmtI
                 throw new InvalidOperationException();
             }
 
-            if (!function.TryResolveRank(out SmtFunctionRank? rank, default, args.Select(a => a.Sort).ToArray()))
+            if (!function.TryResolveRank(ctx, out SmtFunctionRank? rank, default, args.Select(a => a.Sort).ToArray()))
             {
                 onError(id, $"Unable to resolve function rank: {id}, with arg sorts {args.Select(a => a.Sort).ToArray()}");
                 throw new InvalidOperationException();