Merge pull request #116 from SemGuS-git/kjcjohnson/theory-of-sequences

kjcjohnson · web-flow · commit 8956eebcbe0a · 2024-03-19T19:52:18.000-05:00
Add the (experimental cvc5) theory of sequences
diff --git a/IntegrationTests/data/sequences.sem b/IntegrationTests/data/sequences.sem
@@ -0,0 +1,34 @@
+(declare-term-types
+ ((Start 0))
+ ((($main))))
+
+(declare-const X (Seq Int))
+
+(define-funs-rec
+    ((Start.Sem ((Start_term_0 Start) (rq (Seq Int)) (x (_ BitVec 32))) Bool))
+
+    ((match Start_term_0
+            ((($main)
+              (exists ((rb (Seq String)) (ra (Seq String)))
+                      (and (= "Test" (seq.nth rb 7))
+                           (= rb (seq.++ ra (seq.unit "a")))
+                           (= rb (as seq.empty (Seq String)))
+                           (= rq (seq.rev rq))
+                           (= (seq.len ra) (seq.nth rq 1))
+                           (= (seq.update ra 7 rb) rb)
+                           (= ra (seq.extract rb 3 5))
+                           (= (seq.at rb 4) (seq.at ra 3))
+                           (seq.contains ra rb)
+                           (= 12 (seq.indexof ra rb 7))
+                           (= ra (seq.replace ra ra rb))
+                           (= (seq.replace_all ra ra rb) rb)
+                           (seq.prefixof ra rb)
+                           (seq.suffixof rb ra))))))))
+
+
+(synth-fun MyFunc () Start)
+
+
+(constraint (exists ((rq (Seq Int)) (y (_ BitVec 32))) (Start.Sem MyFunc rq y)))
+
+(check-synth)
diff --git a/IntegrationTests/tests/test-json-sequences.rsp b/IntegrationTests/tests/test-json-sequences.rsp
@@ -0,0 +1,6 @@
+--format
+json
+--mode
+batch
+--
+data/sequences.sem
diff --git a/IntegrationTests/tests/test-json-sequences.txt b/IntegrationTests/tests/test-json-sequences.txt
diff --git a/IntegrationTests/tests/test-sexpr-sequences.rsp b/IntegrationTests/tests/test-sexpr-sequences.rsp
@@ -0,0 +1,4 @@
+--format
+sexpr
+--
+data/sequences.sem
diff --git a/IntegrationTests/tests/test-sexpr-sequences.txt b/IntegrationTests/tests/test-sexpr-sequences.txt
diff --git a/ParserLibrary/Commands/GrammarBlockHelper.cs b/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>()));
diff --git a/ParserLibrary/Reader/Converters/TermConverter.cs b/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);
                             }
diff --git a/ParserTests/BitVectors/ExtractTests.cs b/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));
         }
     }
 }
diff --git a/ParserTests/Issues/Issue43.cs b/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>());
diff --git a/Semgus-Lib/Model/Smt/IApplicable.cs b/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
diff --git a/Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs b/Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs
@@ -17,6 +17,7 @@ public static class SmtCommonIdentifiers
         public static SmtIdentifier BitVectorsTheoryId { get; } = new("BitVectors");
         public static SmtIdentifier BitVectorsExtensionId { get; } = new("BitVectors", "extension");
         public static SmtIdentifier ArraysExTheoryId { get; } = new("ArraysEx");
+        public static SmtIdentifier SequencesTheoryId { get; } = new("Sequences");
 
         public static SmtSortIdentifier BoolSortId { get; } = new("Bool");
         public static SmtSortIdentifier IntSortId { get; } = new("Int");
@@ -34,6 +35,7 @@ public SmtSortIdentifier this[int size]
             }
         }
         public static SmtIdentifier ArraySortPrimaryId { get; } = new("Array");
+        public static SmtIdentifier SeqSortPrimaryId { get; } = new("Seq");
 
         public static SmtIdentifier AndFunctionId { get; } = new("and");
         public static SmtIdentifier OrFunctionId { get; } = new("or");
diff --git a/Semgus-Lib/Model/Smt/SmtContext.cs b/Semgus-Lib/Model/Smt/SmtContext.cs
@@ -65,7 +65,8 @@ public SmtContext()
                 SmtIntsTheory.Instance,
                 SmtStringsTheory.Instance,
                 SmtBitVectorsTheory.Instance,
-                SmtArraysExTheory.Instance
+                SmtArraysExTheory.Instance,
+                SmtSequencesTheory.Instance
             };
 
             _extensions = new HashSet<ISmtExtension>()
diff --git a/Semgus-Lib/Model/Smt/SmtFunction.cs b/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();
 
@@ -190,6 +192,8 @@ private bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtFu
                 var retSort = template.ReturnSort;
                 if (retSort.IsSortParameter)
                 {
+                    TraverseAndResolveTemplate(ctx, retSort, resolvedParameters, out _);
+
                     if (resolvedParameters.TryGetValue(retSort, out SmtSort? resRetSort))
                     {
                         // Case: the return value is a parameter we know about
@@ -227,6 +231,54 @@ private bool TryResolveRank([NotNullWhen(true)] out SmtFunctionRank? rank, SmtFu
             return template.Validator(rank);
         }
 
+        /// <summary>
+        /// Traverses the template and resolves parameters inside it, from already resolved pieces
+        /// </summary>
+        /// <param name="ctx">The SMT context</param>
+        /// <param name="template">The template to match</param>
+        /// <param name="resolvedParameters">Dictionary of templates to resolved parameters</param>
+        /// <param name="resolved">The resolved sort</param>
+        /// <returns>True if successfully resolved</returns>
+        internal static bool TraverseAndResolveTemplate(SmtContext ctx, SmtSort template, IDictionary<SmtSort, SmtSort> resolvedParameters, [NotNullWhen(true)] out SmtSort? resolved)
+        {
+            if (!template.IsSortParameter)
+            {
+                resolved = template;
+                return true;
+            }
+            else if (resolvedParameters.TryGetValue(template, out resolved))
+            {
+                return true;
+            }
+            else if (template.Arity == 0)
+            {
+                // An unresolved parameter! Resolution failed.
+                resolved = default;
+                return false;
+            }
+            else
+            {
+                List<SmtSortIdentifier> paramIds = new();
+                foreach (var parameter in template.Parameters)
+                {
+                    if (!TraverseAndResolveTemplate(ctx, parameter, resolvedParameters, out resolved))
+                    {
+                        resolved = default;
+                        return false;
+                    }
+                    paramIds.Add(resolved.Name);
+                }
+                if (!ctx.TryGetSortDeclaration(new(template.Name.Name, paramIds.ToArray()), out var sort, out string? _))
+                {
+                    resolved = default;
+                    return false;
+                }
+                resolvedParameters.Add(template, sort);
+                resolved = sort;
+                return true;
+            }
+        }
+
         /// <summary>
         /// Match a template sort and parameters against a concrete sort
         /// </summary>
diff --git a/Semgus-Lib/Model/Smt/SmtMacro.cs b/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;
diff --git a/Semgus-Lib/Model/Smt/Sorts/SmtDatatypeConstructor.cs b/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)
diff --git a/Semgus-Lib/Model/Smt/Terms/SmtTermBuilder.cs b/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();
diff --git a/Semgus-Lib/Model/Smt/Theories/SmtSequencesTheory.cs b/Semgus-Lib/Model/Smt/Theories/SmtSequencesTheory.cs

-Original file line number
+Diff line change
@@ @@ -0,0 +1,6 @@ @@
 +--format
 +json
 +--mode
 +batch
 +--
 +data/sequences.sem
Original file line number	Diff line number	Diff line change
`@@ -192,7 +192,7 @@ public static (SemgusGrammar, IReadOnlyList<SemgusTermType>, SemgusTermType, Smt`
`192`	`192`	`semDatum.InputVariables.Where(v => v.Name == identifier).First());`
`193`	`193`	`}`
`194`	`194`	`else if (ctx.TryGetFunctionDeclaration(identifier, out var constant)`
`195`		`- && constant.TryResolveRank(out var rank, default))`
	`195`	`+ && constant.TryResolveRank(ctx, out var rank, default))`
`196`	`196`	`{`
`197`	`197`	`constructor = new(GensymUtils.Gensym("_SyProd", identifier.Symbol));`
`198`	`198`	`newProds.Add(new(ttDatum.NonTerminal, constructor, Enumerable.Empty<SemgusGrammar.NonTerminal>()));`
Original file line number	Diff line number	Diff line change
`@@ -76,7 +76,7 @@ public override bool TryConvertImpl(Type tFrom, Type tTo, object from, [NotNullW`
`76`	`76`	`}`
`77`	`77`	`else if (_contextProvider.Context.TryGetFunctionDeclaration(qid.Id, out var defn))`
`78`	`78`	`{`
`79`		`- if (defn.TryResolveRank(out var rank, GetSortOrDie(qid.Sort) /* No arguments */))`
	`79`	`+ if (defn.TryResolveRank(_contextProvider.Context, out var rank, GetSortOrDie(qid.Sort) /* No arguments */))`
`80`	`80`	`{`
`81`	`81`	`to = new SmtFunctionApplication(defn, rank, new List<SmtTerm>());`
`82`	`82`	`}`
`@@ -362,7 +362,7 @@ public override bool TryConvertImpl(Type tFrom, Type tTo, object from, [NotNullW`
`362`	`362`	`return true;`
`363`	`363`	`}`
`364`	`364`
`365`		`- if (!orf!.TryResolveRank(out var rank, boolsort, Enumerable.Repeat(boolsort, convTerms.Count).ToArray()))`
	`365`	`+ if (!orf!.TryResolveRank(_contextProvider.Context, out var rank, boolsort, Enumerable.Repeat(boolsort, convTerms.Count).ToArray()))`
`366`	`366`	`{`
`367`	`367`	`throw new InvalidOperationException("Too many terms to match pattern.");`
`368`	`368`	`}`
`@@ -434,7 +434,7 @@ public override bool TryConvertImpl(Type tFrom, Type tTo, object from, [NotNullW`
`434`	`434`	`return true;`
`435`	`435`	`}`
`436`	`436`
`437`		`- if (defn.TryResolveRank(out var rank, GetSortOrDie(af.Id.Sort), argSorts))`
	`437`	`+ if (defn.TryResolveRank(_contextProvider.Context, out var rank, GetSortOrDie(af.Id.Sort), argSorts))`
`438`	`438`	`{`
`439`	`439`	`to = new SmtFunctionApplication(defn, rank, args);`
`440`	`440`	`}`
Original file line number	Diff line number	Diff line change
`@@ -74,7 +74,7 @@ public void DoesNotThrowParseExceptionForBool()`
`74`	`74`	`{`
`75`	`75`	`SmtContext ctx = new();`
`76`	`76`	`Assert.True(ctx.TryGetFunctionDeclaration(new("true"), out var truefn));`
`77`		`- Assert.True(truefn!.TryResolveRank(out var rank, default));`
	`77`	`+ Assert.True(truefn!.TryResolveRank(ctx, out var rank, default));`
`78`	`78`
`79`	`79`	`SemgusToken testToken = new SymbolToken("test", default);`
`80`	`80`	`SmtTerm testTerm = new SmtFunctionApplication(truefn, rank!, new List<SmtTerm>());`