Merge pull request #114 from SemGuS-git/kjcjohnson/intrinsics

Support "intrinsic" declarations

IntegrationTests/data/intrinsics.sem

@@ -0,0 +1,14 @@
+;;;;
+;;;; Checks that intrinsics commands are handled properly
+;;;;
+(declare-intrinsic-sort Real2)
+(declare-intrinsic-const real2.tau Real2)
+(declare-intrinsic-fun real2.sin (Real2) Real2)
+(declare-intrinsic-fun real2.atan2 (Real2 Real2) Real2)
+(declare-intrinsic-fun real2.+ (Int Real2) Real2)
+
+(constraint (forall ((x Real2) (y Real2))
+              (exists ((z Int))
+                (= (real2.sin (real2.+ z real2.tau)) (real2.atan2 x y)))))
+
+(check-synth)

IntegrationTests/tests/test-intrinsics-json.rsp

@@ -0,0 +1,6 @@
+--format
+json
+--
+data/intrinsics.sem
+
+

IntegrationTests/tests/test-intrinsics-json.txt

@@ -0,0 +1,3 @@
+{"constraint":{"bindings":[{"name":"x","sort":"Real2","$termType":"variable"},{"name":"y","sort":"Real2","$termType":"variable"}],"child":{"bindings":[{"name":"z","sort":"Int","$termType":"variable"}],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Real2","Real2"],"arguments":[{"name":"real2.sin","returnSort":"Real2","argumentSorts":["Real2"],"arguments":[{"name":"real2.+","returnSort":"Real2","argumentSorts":["Int","Real2"],"arguments":[{"name":"z","sort":"Int","$termType":"variable"},{"name":"real2.tau","returnSort":"Real2","argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"real2.atan2","returnSort":"Real2","argumentSorts":["Real2","Real2"],"arguments":[{"name":"x","sort":"Real2","$termType":"variable"},{"name":"y","sort":"Real2","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"forall"},"$event":"constraint","$type":"semgus"}
+{"$event":"check-synth","$type":"semgus"}
+{"$type":"meta","$event":"end-of-stream"}

IntegrationTests/tests/test-intrinsics-sexpr.rsp

@@ -0,0 +1,6 @@
+--format
+sexpr
+--
+data/intrinsics.sem
+
+

IntegrationTests/tests/test-intrinsics-sexpr.txt

@@ -0,0 +1,3 @@
+
+(constraint (term (forall :bindings (list (identifier "x") (identifier "y")) :binding-sorts (list (sort (identifier "Real2")) (sort (identifier "Real2"))) :child (exists :bindings (list (identifier "z")) :binding-sorts (list (sort (identifier "Int"))) :child (application (identifier "=") :argument-sorts (list (sort (identifier "Real2")) (sort (identifier "Real2"))) :arguments (list (application (identifier "real2.sin") :argument-sorts (list (sort (identifier "Real2"))) :arguments (list (application (identifier "real2.+") :argument-sorts (list (sort (identifier "Int")) (sort (identifier "Real2"))) :arguments (list (variable (identifier "z") :sort (sort (identifier "Int"))) (application (identifier "real2.tau") :argument-sorts (list) :arguments (list) :return-sort (sort (identifier "Real2")))) :return-sort (sort (identifier "Real2")))) :return-sort (sort (identifier "Real2"))) (application (identifier "real2.atan2") :argument-sorts (list (sort (identifier "Real2")) (sort (identifier "Real2"))) :arguments (list (variable (identifier "x") :sort (sort (identifier "Real2"))) (variable (identifier "y") :sort (sort (identifier "Real2")))) :return-sort (sort (identifier "Real2")))) :return-sort (sort (identifier "Bool"))))))) 
+(check-synth)

ParserLibrary/Commands/IntrinsicCommands.cs

@@ -0,0 +1,97 @@
+using Microsoft.Extensions.Logging;
+
+using Semgus.Model.Smt;
+using Semgus.Parser.Reader;
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+
+namespace Semgus.Parser.Commands
+{
+    /// <summary>
+    /// Intrinsic commands. These are an extension to declare "intrinsic" functions,
+    /// constants, and sorts. These only are added to the SMT context for parsing, but
+    /// are not emitted as a part of the problem file. They are assumed to be handled by
+    /// another tool down the line, for example, theory extensions in an SMT solver.
+    /// </summary>
+    internal class IntrinsicCommands
+    {
+        private readonly ISmtContextProvider _smtCtxProvider;
+        private readonly ISourceMap _sourceMap;
+        private readonly ISourceContextProvider _sourceContextProvider;
+        private readonly ILogger<IntrinsicCommands> _logger;
+
+        /// <summary>
+        /// Creates a new IntrinsicCommands instance
+        /// </summary>
+        /// <param name="smtCtxProvider">The SMT context provider</param>
+        /// <param name="sourceMap">The source map</param>
+        /// <param name="sourceContextProvider">The source context provider</param>
+        /// <param name="handler">Not used, but required for DI</param>
+        /// <param name="logger">The logger</param>
+        public IntrinsicCommands(ISmtContextProvider smtCtxProvider,
+                                 ISourceMap sourceMap,
+                                 ISourceContextProvider sourceContextProvider,
+                                 ISemgusProblemHandler handler,
+                                 ILogger<IntrinsicCommands> logger)
+        {
+            _smtCtxProvider = smtCtxProvider;
+            _sourceMap = sourceMap;
+            _sourceContextProvider = sourceContextProvider;
+            _logger = logger;
+        }
+
+        /// <summary>
+        /// Declares an "intrinsic" constant
+        /// </summary>
+        /// <param name="name">Function name</param>
+        /// <param name="argIds">Function argument sorts</param>
+        /// <param name="returnSortId">Function return sort</param>
+        [Command("declare-intrinsic-fun")]
+        public void DeclareIntrinsicFun(SmtIdentifier name, IList<SmtSortIdentifier> argIds, SmtSortIdentifier returnSortId)
+        {
+            using var logScope = _logger.BeginScope($"while processing `declare-intrinsic-fun` for {name}:");
+
+            var returnSort = _smtCtxProvider.Context.GetSortOrDie(returnSortId, _sourceMap, _logger);
+            var args = argIds.Select(argId => _smtCtxProvider.Context.GetSortOrDie(argId, _sourceMap, _logger));
+            var rank = new SmtFunctionRank(returnSort, args.ToArray());
+            var decl = new SmtFunction(name, _sourceContextProvider.CurrentSmtSource, rank);
+
+            _smtCtxProvider.Context.AddFunctionDeclaration(decl);
+        }
+
+        /// <summary>
+        /// Declares an "intrinsic" constant
+        /// </summary>
+        /// <param name="name">Constant name</param>
+        /// <param name="returnSortId">Sort of constant</param>
+        [Command("declare-intrinsic-const")]
+        public void DeclareIntrinsicConst(SmtIdentifier name, SmtSortIdentifier returnSortId)
+        {
+            using var logScope = _logger.BeginScope($"while processing `declare-intrinsic-const` for {name}:");
+
+            var returnSort = _smtCtxProvider.Context.GetSortOrDie(returnSortId, _sourceMap, _logger);
+            var rank = new SmtFunctionRank(returnSort, Array.Empty<SmtSort>());
+            var decl = new SmtFunction(name, _sourceContextProvider.CurrentSmtSource, rank);
+
+            _smtCtxProvider.Context.AddFunctionDeclaration(decl);
+        }
+
+        /// <summary>
+        /// Declares an "intrinsic" sort
+        /// </summary>
+        /// <param name="name">Sort name to declare</param>
+        [Command("declare-intrinsic-sort")]
+        public void DeclareIntrinsicSort(SmtSortIdentifier name)
+        {
+            using var logScope = _logger.BeginScope($"while processing `declare-intrinsic-sort` for {name}:");
+
+            var sort = new SmtSort.GenericSort(name);
+
+            _smtCtxProvider.Context.AddSortDeclaration(sort);
+        }
+    }
+}

ParserLibrary/SemgusParser.cs

@@ -117,6 +117,9 @@ void procClass(Type t)
             procClass(typeof(SetLogicCommand));
             procClass(typeof(DeclareVarCommand));
 
+            // Parser extensions
+            procClass(typeof(IntrinsicCommands));
+
             ServiceCollection services = new ServiceCollection();
             services.AddSingleton<ISmtConverter, Reader.Converters.SmtConverter>();
             services.AddSingleton<DestructuringHelper>();

Semgus-Lib/Model/Smt/SmtSort.cs

@@ -55,7 +55,7 @@ public virtual void UpdateForResolvedParameters(IList<SmtSort> resolved) { }
         /// <summary>
         /// An arbitrary generic sort
         /// </summary>
-        internal class GenericSort : SmtSort
+        public class GenericSort : SmtSort
         {
             /// <summary>
             /// Constructs a new generic sort