Hide sexpr annotations behind a flag

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,11 +11,25 @@ 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>
@@ -25,7 +39,7 @@ public SmtTermWriter(ISexprWriter sw)
         /// <param name="inner">Action to call for writing the term</param>
         private void MaybeWriteAnnotations(SmtTerm term, Action inner)
         {
-            if (term.Annotations != null && term.Annotations.Count > 0)
+            if (_includeTermAnnotations && term.Annotations != null && term.Annotations.Count > 0)
             {
                 _sw.WriteList(() =>
                 {