From daf73594accedc0b430bef1c2afe6a6ddccb4562 Mon Sep 17 00:00:00 2001 From: Keith Johnson Date: Mon, 11 Mar 2024 20:43:31 -0500 Subject: [PATCH 1/2] Make GenericSort public --- Semgus-Lib/Model/Smt/SmtSort.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Semgus-Lib/Model/Smt/SmtSort.cs b/Semgus-Lib/Model/Smt/SmtSort.cs index 8a6997d..1882202 100644 --- a/Semgus-Lib/Model/Smt/SmtSort.cs +++ b/Semgus-Lib/Model/Smt/SmtSort.cs @@ -55,7 +55,7 @@ public virtual void UpdateForResolvedParameters(IList resolved) { } /// /// An arbitrary generic sort /// - internal class GenericSort : SmtSort + public class GenericSort : SmtSort { /// /// Constructs a new generic sort From 40c24b594b8a8f10480c5ee85edc4ee5c79b321b Mon Sep 17 00:00:00 2001 From: Keith Johnson Date: Mon, 11 Mar 2024 20:43:56 -0500 Subject: [PATCH 2/2] Allow declaring intrinsics --- IntegrationTests/data/intrinsics.sem | 14 +++ .../tests/test-intrinsics-json.rsp | 6 ++ .../tests/test-intrinsics-json.txt | 3 + .../tests/test-intrinsics-sexpr.rsp | 6 ++ .../tests/test-intrinsics-sexpr.txt | 3 + ParserLibrary/Commands/IntrinsicCommands.cs | 97 +++++++++++++++++++ ParserLibrary/SemgusParser.cs | 3 + 7 files changed, 132 insertions(+) create mode 100644 IntegrationTests/data/intrinsics.sem create mode 100644 IntegrationTests/tests/test-intrinsics-json.rsp create mode 100644 IntegrationTests/tests/test-intrinsics-json.txt create mode 100644 IntegrationTests/tests/test-intrinsics-sexpr.rsp create mode 100644 IntegrationTests/tests/test-intrinsics-sexpr.txt create mode 100644 ParserLibrary/Commands/IntrinsicCommands.cs diff --git a/IntegrationTests/data/intrinsics.sem b/IntegrationTests/data/intrinsics.sem new file mode 100644 index 0000000..6a29179 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/IntegrationTests/tests/test-intrinsics-json.rsp b/IntegrationTests/tests/test-intrinsics-json.rsp new file mode 100644 index 0000000..ce8e30b --- /dev/null +++ b/IntegrationTests/tests/test-intrinsics-json.rsp @@ -0,0 +1,6 @@ +--format +json +-- +data/intrinsics.sem + + diff --git a/IntegrationTests/tests/test-intrinsics-json.txt b/IntegrationTests/tests/test-intrinsics-json.txt new file mode 100644 index 0000000..d965ec1 --- /dev/null +++ b/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"} diff --git a/IntegrationTests/tests/test-intrinsics-sexpr.rsp b/IntegrationTests/tests/test-intrinsics-sexpr.rsp new file mode 100644 index 0000000..f1b2d2e --- /dev/null +++ b/IntegrationTests/tests/test-intrinsics-sexpr.rsp @@ -0,0 +1,6 @@ +--format +sexpr +-- +data/intrinsics.sem + + diff --git a/IntegrationTests/tests/test-intrinsics-sexpr.txt b/IntegrationTests/tests/test-intrinsics-sexpr.txt new file mode 100644 index 0000000..401d4cd --- /dev/null +++ b/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) \ No newline at end of file diff --git a/ParserLibrary/Commands/IntrinsicCommands.cs b/ParserLibrary/Commands/IntrinsicCommands.cs new file mode 100644 index 0000000..e47f6ca --- /dev/null +++ b/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 +{ + /// + /// 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. + /// + internal class IntrinsicCommands + { + private readonly ISmtContextProvider _smtCtxProvider; + private readonly ISourceMap _sourceMap; + private readonly ISourceContextProvider _sourceContextProvider; + private readonly ILogger _logger; + + /// + /// Creates a new IntrinsicCommands instance + /// + /// The SMT context provider + /// The source map + /// The source context provider + /// Not used, but required for DI + /// The logger + public IntrinsicCommands(ISmtContextProvider smtCtxProvider, + ISourceMap sourceMap, + ISourceContextProvider sourceContextProvider, + ISemgusProblemHandler handler, + ILogger logger) + { + _smtCtxProvider = smtCtxProvider; + _sourceMap = sourceMap; + _sourceContextProvider = sourceContextProvider; + _logger = logger; + } + + /// + /// Declares an "intrinsic" constant + /// + /// Function name + /// Function argument sorts + /// Function return sort + [Command("declare-intrinsic-fun")] + public void DeclareIntrinsicFun(SmtIdentifier name, IList 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); + } + + /// + /// Declares an "intrinsic" constant + /// + /// Constant name + /// Sort of constant + [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()); + var decl = new SmtFunction(name, _sourceContextProvider.CurrentSmtSource, rank); + + _smtCtxProvider.Context.AddFunctionDeclaration(decl); + } + + /// + /// Declares an "intrinsic" sort + /// + /// Sort name to declare + [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); + } + } +} diff --git a/ParserLibrary/SemgusParser.cs b/ParserLibrary/SemgusParser.cs index 02d738e..a7bfdd4 100644 --- a/ParserLibrary/SemgusParser.cs +++ b/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(); services.AddSingleton();