Skip to content

Commit 01c2d33

Browse files
kjcjohnsonkjcjohnson
authored
Merge pull request #114 from SemGuS-git/kjcjohnson/intrinsics
Support "intrinsic" declarations
2 parents 6739757 + 40c24b5 commit 01c2d33

8 files changed

Lines changed: 133 additions & 1 deletion

File tree

‎IntegrationTests/data/intrinsics.sem‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
;;;;
2+
;;;; Checks that intrinsics commands are handled properly
3+
;;;;
4+
(declare-intrinsic-sort Real2)
5+
(declare-intrinsic-const real2.tau Real2)
6+
(declare-intrinsic-fun real2.sin (Real2) Real2)
7+
(declare-intrinsic-fun real2.atan2 (Real2 Real2) Real2)
8+
(declare-intrinsic-fun real2.+ (Int Real2) Real2)
9+
10+
(constraint (forall ((x Real2) (y Real2))
11+
(exists ((z Int))
12+
(= (real2.sin (real2.+ z real2.tau)) (real2.atan2 x y)))))
13+
14+
(check-synth)

‎IntegrationTests/tests/test-intrinsics-json.rsp‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
--format
2+
json
3+
--
4+
data/intrinsics.sem
5+
6+

‎IntegrationTests/tests/test-intrinsics-json.txt‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
{"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"}
2+
{"$event":"check-synth","$type":"semgus"}
3+
{"$type":"meta","$event":"end-of-stream"}

‎IntegrationTests/tests/test-intrinsics-sexpr.rsp‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
--format
2+
sexpr
3+
--
4+
data/intrinsics.sem
5+
6+

‎IntegrationTests/tests/test-intrinsics-sexpr.txt‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
2+
(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")))))))
3+
(check-synth)

‎ParserLibrary/Commands/IntrinsicCommands.cs‎

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
using Microsoft.Extensions.Logging;
2+
3+
using Semgus.Model.Smt;
4+
using Semgus.Parser.Reader;
5+
6+
using System;
7+
using System.Collections.Generic;
8+
using System.Linq;
9+
using System.Text;
10+
using System.Threading.Tasks;
11+
12+
namespace Semgus.Parser.Commands
13+
{
14+
/// <summary>
15+
/// Intrinsic commands. These are an extension to declare "intrinsic" functions,
16+
/// constants, and sorts. These only are added to the SMT context for parsing, but
17+
/// are not emitted as a part of the problem file. They are assumed to be handled by
18+
/// another tool down the line, for example, theory extensions in an SMT solver.
19+
/// </summary>
20+
internal class IntrinsicCommands
21+
{
22+
private readonly ISmtContextProvider _smtCtxProvider;
23+
private readonly ISourceMap _sourceMap;
24+
private readonly ISourceContextProvider _sourceContextProvider;
25+
private readonly ILogger<IntrinsicCommands> _logger;
26+
27+
/// <summary>
28+
/// Creates a new IntrinsicCommands instance
29+
/// </summary>
30+
/// <param name="smtCtxProvider">The SMT context provider</param>
31+
/// <param name="sourceMap">The source map</param>
32+
/// <param name="sourceContextProvider">The source context provider</param>
33+
/// <param name="handler">Not used, but required for DI</param>
34+
/// <param name="logger">The logger</param>
35+
public IntrinsicCommands(ISmtContextProvider smtCtxProvider,
36+
ISourceMap sourceMap,
37+
ISourceContextProvider sourceContextProvider,
38+
ISemgusProblemHandler handler,
39+
ILogger<IntrinsicCommands> logger)
40+
{
41+
_smtCtxProvider = smtCtxProvider;
42+
_sourceMap = sourceMap;
43+
_sourceContextProvider = sourceContextProvider;
44+
_logger = logger;
45+
}
46+
47+
/// <summary>
48+
/// Declares an "intrinsic" constant
49+
/// </summary>
50+
/// <param name="name">Function name</param>
51+
/// <param name="argIds">Function argument sorts</param>
52+
/// <param name="returnSortId">Function return sort</param>
53+
[Command("declare-intrinsic-fun")]
54+
public void DeclareIntrinsicFun(SmtIdentifier name, IList<SmtSortIdentifier> argIds, SmtSortIdentifier returnSortId)
55+
{
56+
using var logScope = _logger.BeginScope($"while processing `declare-intrinsic-fun` for {name}:");
57+
58+
var returnSort = _smtCtxProvider.Context.GetSortOrDie(returnSortId, _sourceMap, _logger);
59+
var args = argIds.Select(argId => _smtCtxProvider.Context.GetSortOrDie(argId, _sourceMap, _logger));
60+
var rank = new SmtFunctionRank(returnSort, args.ToArray());
61+
var decl = new SmtFunction(name, _sourceContextProvider.CurrentSmtSource, rank);
62+
63+
_smtCtxProvider.Context.AddFunctionDeclaration(decl);
64+
}
65+
66+
/// <summary>
67+
/// Declares an "intrinsic" constant
68+
/// </summary>
69+
/// <param name="name">Constant name</param>
70+
/// <param name="returnSortId">Sort of constant</param>
71+
[Command("declare-intrinsic-const")]
72+
public void DeclareIntrinsicConst(SmtIdentifier name, SmtSortIdentifier returnSortId)
73+
{
74+
using var logScope = _logger.BeginScope($"while processing `declare-intrinsic-const` for {name}:");
75+
76+
var returnSort = _smtCtxProvider.Context.GetSortOrDie(returnSortId, _sourceMap, _logger);
77+
var rank = new SmtFunctionRank(returnSort, Array.Empty<SmtSort>());
78+
var decl = new SmtFunction(name, _sourceContextProvider.CurrentSmtSource, rank);
79+
80+
_smtCtxProvider.Context.AddFunctionDeclaration(decl);
81+
}
82+
83+
/// <summary>
84+
/// Declares an "intrinsic" sort
85+
/// </summary>
86+
/// <param name="name">Sort name to declare</param>
87+
[Command("declare-intrinsic-sort")]
88+
public void DeclareIntrinsicSort(SmtSortIdentifier name)
89+
{
90+
using var logScope = _logger.BeginScope($"while processing `declare-intrinsic-sort` for {name}:");
91+
92+
var sort = new SmtSort.GenericSort(name);
93+
94+
_smtCtxProvider.Context.AddSortDeclaration(sort);
95+
}
96+
}
97+
}

‎ParserLibrary/SemgusParser.cs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,9 @@ void procClass(Type t)
117117
procClass(typeof(SetLogicCommand));
118118
procClass(typeof(DeclareVarCommand));
119119

120+
// Parser extensions
121+
procClass(typeof(IntrinsicCommands));
122+
120123
ServiceCollection services = new ServiceCollection();
121124
services.AddSingleton<ISmtConverter, Reader.Converters.SmtConverter>();
122125
services.AddSingleton<DestructuringHelper>();

‎Semgus-Lib/Model/Smt/SmtSort.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ public virtual void UpdateForResolvedParameters(IList<SmtSort> resolved) { }
5555
/// <summary>
5656
/// An arbitrary generic sort
5757
/// </summary>
58-
internal class GenericSort : SmtSort
58+
public class GenericSort : SmtSort
5959
{
6060
/// <summary>
6161
/// Constructs a new generic sort

0 commit comments

Comments
 (0)