Merge pull request #111 from Shoooooon/main

Support parametric sorts in the JSON format (and initial ArraysEx support)

IntegrationTests/data/array.sem

@@ -0,0 +1,37 @@
+(declare-term-types
+((E 0) (Start 0))
+((($IBVVary )
+($bvsub E E)
+($bvadd E E)
+($IBVVarx ))
+(($bv=x E))))
+
+
+
+(define-funs-rec
+((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (rv (Array Int Int)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)
+(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (rq (Array Int Int)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool))
+
+((match E_term_0
+  (($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 y))))
+(($bvsub E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32)) (rb (Array Int Int))) (and (= r__0 (bvadd r__1 (bvneg r__2)))
+  (E.Sem E_term_1 r__1 rb x y)
+  (E.Sem E_term_2 r__2 rb x y))))
+(($bvadd E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32)) (rb (Array Int Int))) (and (= r__0 (bvadd r__1 r__2))
+  (E.Sem E_term_1 r__1 rb x y)
+  (E.Sem E_term_2 r__2 rb x y))))
+($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1)
+  (= r__1 x))))))
+(match Start_term_0
+  ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32)) (rb (Array Int Int))) (and (and (= x_r0 r__1)
+  (and (= rb rb) (= y y_r0)))
+  (E.Sem E_term_1 r__1 rb x y))))))))
+
+
+(synth-fun BVtest_ADD_01() Start)
+
+
+(constraint (exists ((rq (Array Int Int)) (y (_ BitVec 32))) (Start.Sem BVtest_ADD_01 #x00000004 #x00000004 rq #x00000003 y)))
+
+(check-synth)

IntegrationTests/tests/test-json-array.rsp

@@ -0,0 +1,6 @@
+--format
+json
+--mode
+batch
+--
+data/array.sem

README.md

@@ -31,6 +31,7 @@ This project is under active development and does not yet support all SMT-LIB2 f
 * Strings (with partial support for regular expressions)
 * Bit vectors (partial support; only theory functions supported for now)
 * Datatypes (non-parametric only)
+* Arrays (partial support)
 
 Other features:
 * Converting SyGuS problems to CHCs on the fly (beta)
@@ -42,14 +43,12 @@ New additions:
 * Arbitrary `match` expressions
 
 Unsupported SMT-LIB2 features include:
-* Parametric sorts
 * Theory functions annotated with `:left-assoc`, `:right-assoc`, `:chainable`, and `:pairwise`. Certain Core functions are implemented, so post an issue if others are needed.
 * Some terms, including `let`
 * Uninterpreted sorts (`declare-sort`) and sort aliases (`define-sort`)
 
 The roadmap for next-up features includes:
 * Arbitrary `let` terms
-* Parameteric sorts
 
 If there is an unsupported feature that you would like added, drop us a line by submitting an issue (or commenting on an existing one).
 This will help us prioritize what to put on our roadmap.

Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs

@@ -16,6 +16,7 @@ public static class SmtCommonIdentifiers
         public static SmtIdentifier StringsTheoryId { get; } = new("Strings");
         public static SmtIdentifier BitVectorsTheoryId { get; } = new("BitVectors");
         public static SmtIdentifier BitVectorsExtensionId { get; } = new("BitVectors", "extension");
+        public static SmtIdentifier ArraysExTheoryId { get; } = new("ArraysEx");
 
         public static SmtSortIdentifier BoolSortId { get; } = new("Bool");
         public static SmtSortIdentifier IntSortId { get; } = new("Int");
@@ -32,6 +33,7 @@ public SmtSortIdentifier this[int size]
                                              new SmtIdentifier.Index(size)));
             }
         }
+        public static SmtIdentifier ArraySortPrimaryId { get; } = new("Array");
 
         public static SmtIdentifier AndFunctionId { get; } = new("and");
         public static SmtIdentifier OrFunctionId { get; } = new("or");

Semgus-Lib/Model/Smt/SmtContext.cs

@@ -64,7 +64,8 @@ public SmtContext()
                 SmtCoreTheory.Instance,
                 SmtIntsTheory.Instance,
                 SmtStringsTheory.Instance,
-                SmtBitVectorsTheory.Instance
+                SmtBitVectorsTheory.Instance,
+                SmtArraysExTheory.Instance
             };
 
             _extensions = new HashSet<ISmtExtension>()
@@ -249,7 +250,7 @@ private bool TryResolveSortParameters(SmtSortIdentifier id, SmtSort candidate, [
                 return false;
             }
 
-            if (candidate.Arity == 0)
+            if (candidate.Arity == 0 || !candidate.IsParametric)
             {
                 resolved = candidate;
                 error = default;
@@ -266,13 +267,16 @@ private bool TryResolveSortParameters(SmtSortIdentifier id, SmtSort candidate, [
                 else
                 {
                     resolved = default;
+                    error = $"Unable to resolve sort parameter {child.Name} in parametric sort {id.Name}: {error}";
                     return false;
                 }
             }
 
-            resolved = default;
-            error = "Not finished being implemented";
-            return false;
+            candidate.UpdateForResolvedParameters(resolvedSubsorts);
+
+            resolved = candidate;
+            error = "";
+            return true;
         }
 
         public void Push()

Semgus-Lib/Model/Smt/SmtSort.cs

@@ -27,7 +27,7 @@ public SmtSort(SmtSortIdentifier name)
         public SmtSortIdentifier Name { get; }
 
         /// <summary>
-        /// Does this sort have parameters?
+        /// Does this sort have parameters that need to be resolved?
         /// </summary>
         public bool IsParametric { get; protected set; } = false;
 
@@ -41,6 +41,12 @@ public SmtSort(SmtSortIdentifier name)
         /// </summary>
         public int Arity { get; protected set; } = 0;
 
+        /// <summary>
+        /// Updates this sort for resolved parameters
+        /// </summary>
+        /// <param name="resolved">Resolved parameters. Should have same length as arity</param>
+        public virtual void UpdateForResolvedParameters(IList<SmtSort> resolved) { }
+
         /// <summary>
         /// An arbitrary generic sort
         /// </summary>
@@ -54,6 +60,28 @@ public GenericSort(SmtSortIdentifier name) : base(name)
             { }
         }
 
+        /// <summary>
+        /// A sort parameter that needs to be resolved to a real sort
+        /// </summary>
+        internal class UnresolvedParameterSort : SmtSort
+        {
+            /// <summary>
+            /// Identifier that needs to be resolved
+            /// </summary>
+            public SmtSortIdentifier Identifier { get; }
+
+            /// <summary>
+            /// Creates a new unresolved sort. This is a placeholder for sort parameters to be resolved.
+            /// </summary>
+            /// <param name="identifier">Sort identifier to resolve</param>
+            public UnresolvedParameterSort(SmtSortIdentifier identifier) : base(identifier)
+            {
+                Identifier = identifier;
+                IsSortParameter = true;
+                Arity = identifier.Arity;
+            }
+        }
+
         /// <summary>
         /// A sort containing wildcard parameters. Useful in rank templates.
         /// Indices in the sort name may be '*', which will match anything.

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

@@ -0,0 +1,156 @@
+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 theory of arrays with extensions
+    /// </summary>
+    internal class SmtArraysExTheory : ISmtTheory
+    {
+        /// <summary>
+        /// A singleton theory instance
+        /// </summary>
+        public static SmtArraysExTheory Instance { get; } = new();
+
+        /// <summary>
+        /// Underlying array sort
+        /// </summary>
+        internal sealed class ArraySort : SmtSort
+        {
+            /// <summary>
+            /// Cache of instantiated sorts. We need this since sorts are compared by reference
+            /// </summary>
+            private static readonly IDictionary<(SmtSortIdentifier, SmtSortIdentifier), ArraySort> _sortCache
+                = new Dictionary<(SmtSortIdentifier, SmtSortIdentifier), ArraySort>();
+
+            /// <summary>
+            /// The sort used for indexing the array
+            /// </summary>
+            public SmtSort IndexSort { get; private set; }
+
+            /// <summary>
+            /// The sort used for the array element values
+            /// </summary>
+            public SmtSort ValueSort { get; private set; }
+
+            /// <summary>
+            /// Constructs a new array sort with the given parameters
+            /// </summary>
+            /// <param name="size">Size of bit vectors in this sort</param>
+            private ArraySort(SmtSortIdentifier indexSort, SmtSortIdentifier valueSort) :
+                base(new(new SmtIdentifier(ArraySortPrimaryId.Symbol), indexSort, valueSort))
+            {
+                IndexSort = new UnresolvedParameterSort(indexSort);
+                ValueSort = new UnresolvedParameterSort(valueSort);
+                IsParametric = true;
+                Arity = 2;
+            }
+
+            /// <summary>
+            /// Gets the array sort for the given index and value sorts
+            /// </summary>
+            /// <param name="index">The index sort to use</param>
+            /// <param name="value">The value sort to use</param>
+            /// <returns>The array sort for the given index and value sorts</returns>
+            public static ArraySort GetSort(SmtSortIdentifier index, SmtSortIdentifier value)
+            {
+                if (_sortCache.TryGetValue((index, value), out ArraySort? sort))
+                {
+                    return sort;
+                }
+                else
+                {
+                    sort = new ArraySort(index, value);
+                    _sortCache.Add((index, value), sort);
+                    return sort;
+                }
+            }
+
+            /// <summary>
+            /// Updates this sort with the resolved parameteric sorts
+            /// </summary>
+            /// <param name="resolved">Resolved parameters. Must have arity 2</param>
+            public override void UpdateForResolvedParameters(IList<SmtSort> resolved)
+            {
+                if (resolved.Count != 2)
+                {
+                    throw new InvalidOperationException("Got list of resolved sorts not of length 2!");
+                }
+
+                IndexSort = resolved[0];
+                ValueSort = resolved[1];
+            }
+        }
+
+        /// <summary>
+        /// This theory's name
+        /// </summary>
+        public SmtIdentifier Name { get; } = ArraysExTheoryId;
+
+        #region Deprecated
+        public IReadOnlyDictionary<SmtIdentifier, IApplicable> Functions { get; }
+        #endregion
+
+        /// <summary>
+        /// The primary (i.e., non-indexed) sort symbols (e.g., "Array")
+        /// </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 arrays
+        /// </summary>
+        /// <param name="core">Reference to the core theory</param>
+        private SmtArraysExTheory()
+        {
+            SmtSourceBuilder sb = new(this);
+            sb.AddOnTheFlyFn("select");
+            sb.AddOnTheFlyFn("store");
+
+            Functions = sb.Functions;
+            PrimaryFunctionSymbols = sb.PrimaryFunctionSymbols;
+            PrimarySortSymbols = new HashSet<SmtIdentifier>() { ArraySortPrimaryId };
+        }
+
+        /// <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 == 2 && sortId.Name == ArraySortPrimaryId)
+            {
+                resolvedSort = ArraySort.GetSort(sortId.Parameters[0], sortId.Parameters[1]);
+                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);
+        }
+    }
+}

SemgusParser/Json/Converters/SmtSortIdentifierConverter.cs

@@ -31,7 +31,17 @@ public override void WriteJson(JsonWriter writer, object? value, JsonSerializer
 
             if (id.Parameters.Length > 0)
             {
-                throw new InvalidOperationException("Parameterized sorts not yet supported by the JSON serializer.");
+                writer.WriteStartObject();
+                writer.WritePropertyName("kind");
+                serializer.Serialize(writer, id.Name);
+                writer.WritePropertyName("params");
+                writer.WriteStartArray();
+                foreach (var sort in id.Parameters)
+                {
+                    serializer.Serialize(writer, sort);
+                }
+                writer.WriteEndArray();
+                writer.WriteEndObject();
             }
             else
             {