search

SemGuS-git / Semgus-Parser

Library and tool for parsing SemGuS specifications
MIT License
4 stars 1 forks source link

Stack dump when function in SyGuS grammar doesn't exist #100

Open kjcjohnson opened 1 year ago

kjcjohnson commented 1 year ago

Just got a gross error message when trying to parse a SyGuS problem. Benchmark:

(set-logic SLIA)

(synth-fun f ((name String)) String
    ((Start String) (ntString String) (ntInt Int) (ntBool Bool))
    ((Start String (ntString))
    (ntString String (name " " "." "Dr." (str.++ ntString ntString) (str.replace ntString ntString ntString) (str.at ntString ntInt) (int.to.str ntInt) (str.substr ntString ntInt ntInt)))
    (ntInt Int (0 1 2 (+ ntInt ntInt) (- ntInt ntInt) (str.len ntString) (str.to.int ntString) (str.indexof ntString ntString ntInt)))
    (ntBool Bool (true false (str.prefixof ntString ntString) (str.suffixof ntString ntString) (str.contains ntString ntString)))))

(declare-var name String)
(constraint (= (f "Nancy FreeHafer") "Dr. Nancy"))
(constraint (= (f "Andrew Cencici") "Dr. Andrew"))
(constraint (= (f "Jan Kotas") "Dr. Jan"))
(constraint (= (f "Mariya Sergienko") "Dr. Mariya"))

(check-synth)

Note the int.to.str function in the grammar; this is not a real string function. But, instead of getting something useful, we get the following stack trace:

Unhandled exception: System.Reflection.TargetInvocationException: Exception has been thrown by the target of an invocation.
 ---> System.InvalidOperationException: Unable to resolve function: int.to.str
   at Semgus.Model.Smt.Terms.SmtTermBuilder.<>c.<.cctor>b__14_0(Object thing, String msg) in /home/runner/work/Semgus-Parser/Semgus-Parser/Semgus-Lib/Model/Smt/Terms/SmtTermBuilder.cs:line 18
   at Semgus.Model.Smt.Terms.SmtTermBuilder.Apply(SmtContext ctx, Action`2 onError, SmtIdentifier id, SmtTerm[] args) in /home/runner/work/Semgus-Parser/Semgus-Parser/Semgus-Lib/Model/Smt/Terms/SmtTermBuilder.cs:line 73
   at Semgus.Parser.Commands.GrammarBlockHelper.ConvertSygusGrammar[T](GrammarForm grammar, IList`1 args, SmtContext ctx, ISmtConverter converter, ISourceMap sourceMap, ISourceContextProvider sourceContextProvider, ILogger`1 logger) in /home/runner/work/Semgus-Parser/Semgus-Parser/ParserLibrary/Commands/GrammarBlockHelper.cs:line 265
   at Semgus.Parser.Commands.SynthFunCommand.SynthFun(SmtIdentifier name, IList`1 args, SmtSortIdentifier retId, SemgusToken grammarPredecl, SemgusToken grammarBlock) in /home/runner/work/Semgus-Parser/Semgus-Parser/ParserLibrary/Commands/SynthFunCommand.cs:line 54
   --- End of inner exception stack trace ---
   at System.RuntimeMethodHandle.InvokeMethod(Object target, Span`1& arguments, Signature sig, Boolean constructor, Boolean wrapExceptions)
   at System.Reflection.RuntimeMethodInfo.Invoke(Object obj, BindingFlags invokeAttr, Binder binder, Object[] parameters, CultureInfo culture)
   at System.Reflection.MethodBase.Invoke(Object obj, Object[] parameters)
   at Semgus.Parser.Reader.DestructuringHelper.TryDestructureAndInvoke(MethodInfo method, IConsOrNil form, Object instance) in /home/runner/work/Semgus-Parser/Semgus-Parser/ParserLibrary/Reader/DestructuringHelper.cs:line 32
   at Semgus.Parser.SemgusParser.TryParse(ISemgusProblemHandler handler, Int32& errCount, TextWriter errorStream) in /home/runner/work/Semgus-Parser/Semgus-Parser/ParserLibrary/SemgusParser.cs:line 219
   at Semgus.Parser.Program.Execute(ProcessingMode mode, OutputFormat format, Boolean test, String output, HandlerFlags hf, IEnumerable`1 inputs) in /home/runner/work/Semgus-Parser/Semgus-Parser/SemgusParser/Program.cs:line 132
   at Semgus.Parser.Program.<>c__DisplayClass2_0.<Main>b__4(ProcessingMode mode, OutputFormat format, Boolean test, String output, String[] inputs, InvocationContext ctx) in /home/runner/work/Semgus-Parser/Semgus-Parser/SemgusParser/Program.cs:line 95
   at System.CommandLine.Handler.<>c__DisplayClass6_0`6.<SetHandler>b__0(InvocationContext context)
   at System.CommandLine.Invocation.AnonymousCommandHandler.<>c__DisplayClass2_0.<.ctor>g__Handle|0(InvocationContext context)
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass18_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass13_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass20_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__19_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__6_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass9_0.<<UseExceptionHandler>b__0>d.MoveNext()