Outline of theory of sequences

Author: kjcjohnson

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");

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>()

Semgus-Lib/Model/Smt/Theories/SmtSequencesTheory.cs

@@ -0,0 +1,170 @@
+using Semgus.Model.Smt.Terms;
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.CodeAnalysis;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+
+using static Semgus.Model.Smt.SmtCommonIdentifiers;
+
+namespace Semgus.Model.Smt.Theories
+{
+    /// <summary>
+    /// The (non-standard) theory of sequences
+    /// https://cvc5.github.io/docs-ci/docs-main/theories/sequences.html
+    /// </summary>
+    internal class SmtSequencesTheory : ISmtTheory
+    {
+        /// <summary>
+        /// A singleton theory instance
+        /// </summary>
+        public static SmtSequencesTheory Instance { get; } = new();
+
+        /// <summary>
+        /// Underlying sequence sort
+        /// </summary>
+        internal sealed class SeqSort : SmtSort
+        {
+            /// <summary>
+            /// Cache of instantiated sorts. We need this since sorts are compared by reference
+            /// </summary>
+            private static readonly IDictionary<SmtSortIdentifier, SeqSort> _sortCache
+                = new Dictionary<SmtSortIdentifier, SeqSort>();
+
+            /// <summary>
+            /// The sort used for the sequence element values
+            /// </summary>
+            public SmtSort ElementSort { get; private set; }
+
+            /// <summary>
+            /// This sort's parameters
+            /// </summary>
+            public override IEnumerable<SmtSort> Parameters
+            {
+                get => new SmtSort[] { ElementSort };
+            }
+
+            /// <summary>
+            /// Constructs a new seq sort with the given element type
+            /// </summary>
+            /// <param name="elementSort">Sort for sequence elements</param>
+            private SeqSort(SmtSortIdentifier elementSort) :
+                base(new(new SmtIdentifier(SeqSortPrimaryId.Symbol), elementSort))
+            {
+                ElementSort = new UnresolvedParameterSort(elementSort);
+                IsParametric = true;
+                Arity = 1;
+            }
+
+            /// <summary>
+            /// Constructs a new seq sort with the given (possibly concrete) element type
+            /// </summary>
+            /// <param name="elementSort">Sort for sequence elements</param>
+            internal SeqSort(SmtSort elementSort)
+                : base(new(SeqSortPrimaryId, elementSort.Name))
+            {
+                ElementSort = elementSort;
+                IsSortParameter = elementSort.IsSortParameter;
+                Arity = 1;
+            }
+
+            /// <summary>
+            /// Gets the seq sort for the given element sort
+            /// </summary>
+            /// <param name="element">The id of the element sort</param>
+            /// <returns>The seq sort for the given element sort</returns>
+            public static SeqSort GetSort(SmtSortIdentifier element)
+            {
+                if (_sortCache.TryGetValue(element, out SeqSort? sort))
+                {
+                    return sort;
+                }
+                else
+                {
+                    sort = new SeqSort(element);
+                    _sortCache.Add(element, sort);
+                    return sort;
+                }
+            }
+
+            /// <summary>
+            /// Updates this sort with the resolved parameteric sorts
+            /// </summary>
+            /// <param name="resolved">Resolved parameters. Must have arity 1</param>
+            public override void UpdateForResolvedParameters(IList<SmtSort> resolved)
+            {
+                if (resolved.Count != 1)
+                {
+                    throw new InvalidOperationException("Got list of resolved sorts not of length 1!");
+                }
+
+                ElementSort = resolved[0];
+            }
+        }
+
+        /// <summary>
+        /// This theory's name
+        /// </summary>
+        public SmtIdentifier Name { get; } = SequencesTheoryId;
+
+        #region Deprecated
+        public IReadOnlyDictionary<SmtIdentifier, IApplicable> Functions { get; }
+        #endregion
+
+        /// <summary>
+        /// The primary (i.e., non-indexed) sort symbols (e.g., "Seq")
+        /// </summary>
+        public IReadOnlySet<SmtIdentifier> PrimarySortSymbols { get; }
+
+        /// <summary>
+        /// The primary (i.e., non-indexed) function symbols
+        /// </summary>
+        public IReadOnlySet<SmtIdentifier> PrimaryFunctionSymbols { get; }
+
+        /// <summary>
+        /// Constructs an instance of the theory of sequences
+        /// </summary>
+        /// <param name="core">Reference to the core theory</param>
+        private SmtSequencesTheory()
+        {
+            SmtSourceBuilder sb = new(this);
+            var usf = new SmtSort.UniqueSortFactory();
+            var elementSort = usf.Next();
+            var seqSort = new SeqSort(elementSort);
+
+            Functions = sb.Functions;
+            PrimaryFunctionSymbols = sb.PrimaryFunctionSymbols;
+            PrimarySortSymbols = new HashSet<SmtIdentifier>() { SeqSortPrimaryId };
+        }
+
+        /// <summary>
+        /// Looks up a sort symbol in this theory
+        /// </summary>
+        /// <param name="sortId">The sort ID</param>
+        /// <param name="resolvedSort">The resolved sort</param>
+        /// <returns>True if successfully gotten</returns>
+        public bool TryGetSort(SmtSortIdentifier sortId, [NotNullWhen(true)] out SmtSort? resolvedSort)
+        {
+            if (sortId.Arity == 1 && sortId.Name == SeqSortPrimaryId)
+            {
+                resolvedSort = SeqSort.GetSort(sortId.Parameters[0]);
+                return true;
+            }
+            resolvedSort = default;
+            return false;
+        }
+
+        /// <summary>
+        /// Looks up a function in this theory
+        /// </summary>
+        /// <param name="functionId">The function ID to look up</param>
+        /// <param name="resolvedFunction">The resolved function</param>
+        /// <returns>True if successfully gotten</returns>
+        public bool TryGetFunction(SmtIdentifier functionId, [NotNullWhen(true)] out IApplicable? resolvedFunction)
+        {
+            return Functions.TryGetValue(functionId, out resolvedFunction);
+        }
+    }
+}