Merge pull request #118 from SemGuS-git/kjcjohnson/sexpr-term-annotations

Add option for term annotations in s-expression format

Author: kjcjohnson

IntegrationTests/tests/test-sexpr-annotations.rsp

@@ -0,0 +1,5 @@
+--format
+sexpr
+--term-annotations
+--
+data/perfect-prop-3a.sem

IntegrationTests/tests/test-sexpr-annotations.txt

@@ -44,6 +44,11 @@ private HandlerFlags(InvocationContext ctx, HandlerFlagsFactory fac)
         /// </summary>
         public bool LegacySymbols => _fac.LegacySymbols.GetFlag(_ctx);
 
+        /// <summary>
+        /// Whether or not the S-expression format should include term annotations
+        /// </summary>
+        public bool TermAnnotations => _fac.TermAnnotations.GetFlag(_ctx);
+
         /// <summary>
         /// Class for configuring and creating handler flags
         /// </summary>
@@ -59,6 +64,11 @@ public class HandlerFlagsFactory
             /// </summary>
             public readonly CommandFlag LegacySymbols = new("legacy-symbols", defaultValue: true, isHidden: true);
 
+            /// <summary>
+            /// Whether or not to output term annotations for the S-expression output
+            /// </summary>
+            public readonly CommandFlag TermAnnotations = new("term-annotations", defaultValue: false, isHidden: true);
+
             /// <summary>
             /// Creates a new HandlerFlagsFactory and configures it for the given command
             /// </summary>
@@ -67,6 +77,7 @@ public HandlerFlagsFactory(Command command)
             {
                 command.AddFlag(FunctionEvents);
                 command.AddFlag(LegacySymbols);
+                command.AddFlag(TermAnnotations);
             }
 
             /// <summary>

SemgusParser/HandlerFlags.cs

@@ -228,7 +228,7 @@ private static SemgusParser GetParser(string input, bool test, out string friend
                     break;
 
                 case OutputFormat.Sexpr:
-                    handler = new SexprHandler(writer);
+                    handler = new SexprHandler(writer, hf);
                     break;
 
                 default:

SemgusParser/Program.cs

@@ -17,9 +17,20 @@ internal class SexprHandler : ISemgusProblemHandler
     {
         private readonly ISexprWriter _sw;
 
-        public SexprHandler(TextWriter writer)
+        /// <summary>
+        /// Flags for the processing
+        /// </summary>
+        private readonly HandlerFlags _flags;
+
+        /// <summary>
+        /// Creates a new S-expression handler for the given writer and options
+        /// </summary>
+        /// <param name="writer">Underlying s-expression writer</param>
+        /// <param name="flags">Processing flags</param>
+        public SexprHandler(TextWriter writer, HandlerFlags flags)
         {
             _sw = new SexprWriter(writer);
+            _flags = flags;
         }
 
         public void OnCheckSynth(SmtContext smtCtx, SemgusContext semgusCtx)
@@ -53,7 +64,7 @@ public void OnCheckSynth(SmtContext smtCtx, SemgusContext semgusCtx)
                     _sw.WriteKeyword("symbols");
                     _sw.Write(chc.Symbols);
                     _sw.WriteKeyword("constraint");
-                    _sw.Write(chc.Constraint);
+                    _sw.Write(chc.Constraint, _flags.TermAnnotations);
                     _sw.WriteKeyword("constructor");
                     _sw.WriteConstructor(chc.Binder);
                 });
@@ -69,7 +80,7 @@ public void OnCheckSynth(SmtContext smtCtx, SemgusContext semgusCtx)
                 _sw.WriteList(() =>
                 {
                     _sw.WriteSymbol("constraint");
-                    _sw.Write(constraint);
+                    _sw.Write(constraint, _flags.TermAnnotations);
                 });
             }
 
@@ -145,7 +156,7 @@ public void OnFunctionDefinition(SmtContext ctx, SmtFunction function, SmtFuncti
                 _sw.WriteKeyword("rank");
                 _sw.Write(rank);
                 _sw.WriteKeyword("definition");
-                _sw.Write(lambda);
+                _sw.Write(lambda, _flags.TermAnnotations);
             });
         }
 

SemgusParser/Sexpr/SexprHandler.cs

@@ -130,12 +130,12 @@ public static void WriteConstructor(this ISexprWriter writer, SmtMatchBinder bin
         /// </summary>
         /// <param name="writer">Writer to write to</param>
         /// <param name="term">Term to write</param>
-        public static void Write(this ISexprWriter writer, SmtTerm term)
+        public static void Write(this ISexprWriter writer, SmtTerm term, bool includeTermAnnotations)
         {
             writer.WriteList(() =>
             {
                 writer.WriteSymbol("term");
-                term.Accept(new SmtTermWriter(writer));
+                term.Accept(new SmtTermWriter(writer, includeTermAnnotations));
             });
         }
 
@@ -284,7 +284,7 @@ public static void Write(this ISexprWriter sw, SmtAttributeValue attrval)
                     sw.WriteKeyword(attrval.KeywordValue!.Name);
                     break;
                 case SmtAttributeValue.AttributeType.Literal:
-                    sw.Write(attrval.LiteralValue!);
+                    sw.Write(attrval.LiteralValue!, includeTermAnnotations: false);
                     break;
                 case SmtAttributeValue.AttributeType.List:
                     sw.WriteList(attrval.ListValue!, se => sw.Write(se));

SemgusParser/Sexpr/SexprWriterExtensions.cs

@@ -11,80 +11,138 @@ namespace Semgus.Parser.Sexpr
 {
     internal class SmtTermWriter : ISmtTermVisitor<ISexprWriter>
     {
+        /// <summary>
+        /// The writer to write with
+        /// </summary>
         private readonly ISexprWriter _sw;
 
-        public SmtTermWriter(ISexprWriter sw)
+        /// <summary>
+        /// Whether or not to include term annotations
+        /// </summary>
+        private readonly bool _includeTermAnnotations;
+
+        /// <summary>
+        /// Creates a new SmtTermWriter
+        /// </summary>
+        /// <param name="sw">The underlying S-expression writer</param>
+        /// <param name="includeTermAnnotations">Whether or not annotations should be included on terms</param>
+        public SmtTermWriter(ISexprWriter sw, bool includeTermAnnotations)
         {
             _sw = sw;
+            _includeTermAnnotations = includeTermAnnotations;
+        }
+
+        /// <summary>
+        /// Wraps an annotation block around the current term, if necessary
+        /// </summary>
+        /// <param name="term">Term to write annotations for, if any</param>
+        /// <param name="inner">Action to call for writing the term</param>
+        private void MaybeWriteAnnotations(SmtTerm term, Action inner)
+        {
+            if (_includeTermAnnotations && term.Annotations != null && term.Annotations.Count > 0)
+            {
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("annotated");
+                    inner();
+                    foreach (var ann in term.Annotations)
+                    {
+                        _sw.WriteString(ann.Keyword.Name);
+                        _sw.Write(ann.Value);
+                    }
+                });
+            }
+            else
+            {
+                inner();
+            }
         }
 
         public ISexprWriter VisitBitVectorLiteral(SmtBitVectorLiteral bitVectorLiteral)
         {
-            _sw.WriteBitVector(bitVectorLiteral.Value);
+            MaybeWriteAnnotations(bitVectorLiteral, () =>
+            {
+                _sw.WriteBitVector(bitVectorLiteral.Value);
+            });
             return _sw;
         }
 
         public ISexprWriter VisitDecimalLiteral(SmtDecimalLiteral decimalLiteral)
         {
-            _sw.WriteDecimal(decimalLiteral.Value);
+            MaybeWriteAnnotations(decimalLiteral, () =>
+            {
+                _sw.WriteDecimal(decimalLiteral.Value);
+            });
             return _sw;
         }
 
         public ISexprWriter VisitExistsBinder(SmtExistsBinder existsBinder)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(existsBinder, () =>
             {
-                _sw.WriteSymbol("exists");
-                _sw.WriteKeyword("bindings");
-                _sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
-                _sw.WriteKeyword("binding-sorts");
-                _sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
-                _sw.WriteKeyword("child");
-                existsBinder.Child.Accept(this);
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("exists");
+                    _sw.WriteKeyword("bindings");
+                    _sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
+                    _sw.WriteKeyword("binding-sorts");
+                    _sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
+                    _sw.WriteKeyword("child");
+                    existsBinder.Child.Accept(this);
+                });
             });
             return _sw;
         }
 
         public ISexprWriter VisitForallBinder(SmtForallBinder forallBinder)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(forallBinder, () =>
             {
-                _sw.WriteSymbol("forall");
-                _sw.WriteKeyword("bindings");
-                _sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
-                _sw.WriteKeyword("binding-sorts");
-                _sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
-                _sw.WriteKeyword("child");
-                forallBinder.Child.Accept(this);
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("forall");
+                    _sw.WriteKeyword("bindings");
+                    _sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
+                    _sw.WriteKeyword("binding-sorts");
+                    _sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
+                    _sw.WriteKeyword("child");
+                    forallBinder.Child.Accept(this);
+                });
             });
             return _sw;
         }
 
         public ISexprWriter VisitFunctionApplication(SmtFunctionApplication functionApplication)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(functionApplication, () =>
             {
-                _sw.WriteSymbol("application");
-                _sw.Write(functionApplication.Definition.Name);
-                _sw.WriteKeyword("argument-sorts");
-                _sw.WriteList(functionApplication.Rank.ArgumentSorts, s => _sw.Write(s.Name));
-                _sw.WriteKeyword("arguments");
-                _sw.WriteList(functionApplication.Arguments, a => a.Accept(this));
-                _sw.WriteKeyword("return-sort");
-                _sw.Write(functionApplication.Rank.ReturnSort.Name);
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("application");
+                    _sw.Write(functionApplication.Definition.Name);
+                    _sw.WriteKeyword("argument-sorts");
+                    _sw.WriteList(functionApplication.Rank.ArgumentSorts, s => _sw.Write(s.Name));
+                    _sw.WriteKeyword("arguments");
+                    _sw.WriteList(functionApplication.Arguments, a => a.Accept(this));
+                    _sw.WriteKeyword("return-sort");
+                    _sw.Write(functionApplication.Rank.ReturnSort.Name);
+                });
             });
             return _sw;
         }
 
         public ISexprWriter VisitLambdaBinder(SmtLambdaBinder lambdaBinder)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(lambdaBinder, () =>
             {
-                _sw.WriteSymbol("lambda");
-                _sw.WriteKeyword("arguments");
-                _sw.WriteList(lambdaBinder.ArgumentNames, an => _sw.Write(an));
-                _sw.WriteKeyword("body");
-                lambdaBinder.Child.Accept(this);
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("lambda");
+                    _sw.WriteKeyword("arguments");
+                    _sw.WriteList(lambdaBinder.ArgumentNames, an => _sw.Write(an));
+                    _sw.WriteKeyword("body");
+                    lambdaBinder.Child.Accept(this);
+                });
             });
             return _sw;
         }
@@ -96,59 +154,68 @@ public ISexprWriter VisitLetBinder(SmtLetBinder letBinder)
 
         public ISexprWriter VisitMatchBinder(SmtMatchBinder matchBinder)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(matchBinder, () =>
             {
-                _sw.WriteSymbol("binder");
-                _sw.WriteKeyword("operator");
-                if (matchBinder.Constructor is null)
-                {
-                    _sw.WriteNil();
-                }
-                else
+                _sw.WriteList(() =>
                 {
-                    _sw.Write(matchBinder.Constructor.Name);
-                }
-                _sw.WriteKeyword("arguments");
-                _sw.WriteList(matchBinder.Bindings, b => _sw.Write(b.Binding.Id));
-                _sw.WriteKeyword("child");
-                matchBinder.Child.Accept(this);
+                    _sw.WriteSymbol("binder");
+                    _sw.WriteKeyword("operator");
+                    if (matchBinder.Constructor is null)
+                    {
+                        _sw.WriteNil();
+                    }
+                    else
+                    {
+                        _sw.Write(matchBinder.Constructor.Name);
+                    }
+                    _sw.WriteKeyword("arguments");
+                    _sw.WriteList(matchBinder.Bindings, b => _sw.Write(b.Binding.Id));
+                    _sw.WriteKeyword("child");
+                    matchBinder.Child.Accept(this);
+                });
             });
             return _sw;
         }
 
         public ISexprWriter VisitMatchGrouper(SmtMatchGrouper matchGrouper)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(matchGrouper, () =>
             {
-                _sw.WriteSymbol("match");
-                _sw.WriteKeyword("term");
-                matchGrouper.Term.Accept(this);
-                _sw.WriteKeyword("binders");
-                _sw.WriteList(matchGrouper.Binders, b => b.Accept(this));
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("match");
+                    _sw.WriteKeyword("term");
+                    matchGrouper.Term.Accept(this);
+                    _sw.WriteKeyword("binders");
+                    _sw.WriteList(matchGrouper.Binders, b => b.Accept(this));
+                });
             });
             return _sw;
         }
 
         public ISexprWriter VisitNumeralLiteral(SmtNumeralLiteral numeralLiteral)
         {
-            _sw.WriteNumeral(numeralLiteral.Value);
+            MaybeWriteAnnotations(numeralLiteral, () => { _sw.WriteNumeral(numeralLiteral.Value); });
             return _sw;
         }
 
         public ISexprWriter VisitStringLiteral(SmtStringLiteral stringLiteral)
         {
-            _sw.WriteString(stringLiteral.Value);
+            MaybeWriteAnnotations(stringLiteral, () => { _sw.WriteString(stringLiteral.Value); });
             return _sw;
         }
 
         public ISexprWriter VisitVariable(SmtVariable variable)
         {
-            _sw.WriteList(() =>
+            MaybeWriteAnnotations(variable, () =>
             {
-                _sw.WriteSymbol("variable");
-                _sw.Write(variable.Name);
-                _sw.WriteKeyword("sort");
-                _sw.Write(variable.Sort.Name);
+                _sw.WriteList(() =>
+                {
+                    _sw.WriteSymbol("variable");
+                    _sw.Write(variable.Name);
+                    _sw.WriteKeyword("sort");
+                    _sw.Write(variable.Sort.Name);
+                });
             });
             return _sw;
         }