From 7dc7f52760d9272a212e868ff13457655bb04d56 Mon Sep 17 00:00:00 2001 From: Keith Johnson Date: Mon, 18 Mar 2024 19:51:44 -0500 Subject: [PATCH] Add option to disable legacy symbols in CHC JSON events --- .../tests/test-json-no-legacy-symbols.rsp | 6 ++++ .../tests/test-json-no-legacy-symbols.txt | 31 +++++++++++++++++++ SemgusParser/HandlerFlags.cs | 11 +++++++ SemgusParser/Json/ChcEvent.cs | 11 ++++++- SemgusParser/Json/JsonHandler.cs | 2 +- 5 files changed, 59 insertions(+), 2 deletions(-) create mode 100644 IntegrationTests/tests/test-json-no-legacy-symbols.rsp create mode 100644 IntegrationTests/tests/test-json-no-legacy-symbols.txt diff --git a/IntegrationTests/tests/test-json-no-legacy-symbols.rsp b/IntegrationTests/tests/test-json-no-legacy-symbols.rsp new file mode 100644 index 0000000..5417393 --- /dev/null +++ b/IntegrationTests/tests/test-json-no-legacy-symbols.rsp @@ -0,0 +1,6 @@ +--test +--format +json +--mode +batch +--no-legacy-symbols diff --git a/IntegrationTests/tests/test-json-no-legacy-symbols.txt b/IntegrationTests/tests/test-json-no-legacy-symbols.txt new file mode 100644 index 0000000..bf06c9f --- /dev/null +++ b/IntegrationTests/tests/test-json-no-legacy-symbols.txt @@ -0,0 +1,31 @@ +[ +{"keyword":"format-version","value":"2.0.0","$event":"set-info","$type":"meta"}, +{"keyword":"author","value":["Jinwoo Kim","Keith Johnson"],"$event":"set-info","$type":"meta"}, +{"keyword":"realizable","value":"true","$event":"set-info","$type":"meta"}, +{"name":"E","$event":"declare-term-type","$type":"semgus"}, +{"name":"B","$event":"declare-term-type","$type":"semgus"}, +{"name":"E","constructors":[{"name":"$x","children":[]},{"name":"$y","children":[]},{"name":"$0","children":[]},{"name":"$1","children":[]},{"name":"$+","children":["E","E"]},{"name":"$ite","children":["B","E","E"]}],"$event":"define-term-type","$type":"semgus"}, +{"name":"B","constructors":[{"name":"$t","children":[]},{"name":"$f","children":[]},{"name":"$!","children":["B"]},{"name":"$and","children":["B","B"]},{"name":"$or","children":["B","B"]},{"name":"$<","children":["E","E"]}],"$event":"define-term-type","$type":"semgus"}, +{"name":"E.Sem","rank":{"argumentSorts":["E","Int","Int","Int"],"returnSort":"Bool"},"$event":"declare-function","$type":"smt"}, +{"name":"B.Sem","rank":{"argumentSorts":["B","Int","Int","Bool"],"returnSort":"Bool"},"$event":"declare-function","$type":"smt"}, +{"name":"E.Sem","rank":{"argumentSorts":["E","Int","Int","Int"],"returnSort":"Bool"},"definition":{"arguments":["et","x","y","r"],"body":{"term":{"name":"et","sort":"E","$termType":"variable"},"binders":[{"operator":"$x","arguments":[],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},"$termType":"binder"},{"operator":"$y","arguments":[],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"},"$termType":"binder"},{"operator":"$0","arguments":[],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},0],"$termType":"application"},"$termType":"binder"},{"operator":"$1","arguments":[],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},1],"$termType":"application"},"$termType":"binder"},{"operator":"$+","arguments":["et1","et2"],"child":{"bindings":[{"name":"r1","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et1","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r1","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et2","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"+","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[{"name":"r1","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$ite","arguments":["bt","etc","eta"],"child":{"bindings":[{"name":"rb","sort":"Bool","$termType":"variable"},{"name":"rc","sort":"Int","$termType":"variable"},{"name":"ra","sort":"Int","$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool","Bool"],"arguments":[{"name":"B.Sem","returnSort":"Bool","argumentSorts":["B","Int","Int","Bool"],"arguments":[{"name":"bt","sort":"B","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rb","sort":"Bool","$termType":"variable"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"etc","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rc","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"eta","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"ra","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"ite","returnSort":"Int","argumentSorts":["Bool","Int","Int"],"arguments":[{"name":"rb","sort":"Bool","$termType":"variable"},{"name":"rc","sort":"Int","$termType":"variable"},{"name":"ra","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"}],"$termType":"match","annotations":[{"keyword":{"name":"input"},"value":["x","y"]},{"keyword":{"name":"output"},"value":["r"]}]},"$termType":"lambda"},"$event":"define-function","$type":"smt"}, +{"name":"B.Sem","rank":{"argumentSorts":["B","Int","Int","Bool"],"returnSort":"Bool"},"definition":{"arguments":["bt","x","y","r"],"body":{"term":{"name":"bt","sort":"B","$termType":"variable"},"binders":[{"operator":"$t","arguments":[],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},"$termType":"binder"},{"operator":"$f","arguments":[],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"false","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},"$termType":"binder"},{"operator":"$!","arguments":["bt"],"child":{"bindings":[{"name":"rb","sort":"Bool","$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"B.Sem","returnSort":"Bool","argumentSorts":["B","Int","Int","Bool"],"arguments":[{"name":"bt","sort":"B","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rb","sort":"Bool","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"not","returnSort":"Bool","argumentSorts":["Bool"],"arguments":[{"name":"rb","sort":"Bool","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$and","arguments":["bt1","bt2"],"child":{"bindings":[{"name":"rb1","sort":"Bool","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"B.Sem","returnSort":"Bool","argumentSorts":["B","Int","Int","Bool"],"arguments":[{"name":"bt1","sort":"B","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rb1","sort":"Bool","$termType":"variable"}],"$termType":"application"},{"name":"B.Sem","returnSort":"Bool","argumentSorts":["B","Int","Int","Bool"],"arguments":[{"name":"bt2","sort":"B","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"rb1","sort":"Bool","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$or","arguments":["bt1","bt2"],"child":{"bindings":[{"name":"rb1","sort":"Bool","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"B.Sem","returnSort":"Bool","argumentSorts":["B","Int","Int","Bool"],"arguments":[{"name":"bt1","sort":"B","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rb1","sort":"Bool","$termType":"variable"}],"$termType":"application"},{"name":"B.Sem","returnSort":"Bool","argumentSorts":["B","Int","Int","Bool"],"arguments":[{"name":"bt2","sort":"B","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"or","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"rb1","sort":"Bool","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$<","arguments":["et1","et2"],"child":{"bindings":[{"name":"r1","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et1","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r1","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et2","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"<","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r1","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"}],"$termType":"match","annotations":[{"keyword":{"name":"input"},"value":["x","y"]},{"keyword":{"name":"output"},"value":["r"]}]},"$termType":"lambda"},"$event":"define-function","$type":"smt"}, +{"id":"_CHC-$x-1","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},"constructor":{"name":"$x","arguments":[],"argumentSorts":[],"returnSort":"E"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Int","index":3}],"term":{"id":"et","sort":"E","index":0},"unclassified":[],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$y-2","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"},"constructor":{"name":"$y","arguments":[],"argumentSorts":[],"returnSort":"E"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Int","index":3}],"term":{"id":"et","sort":"E","index":0},"unclassified":[],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$0-3","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},0],"$termType":"application"},"constructor":{"name":"$0","arguments":[],"argumentSorts":[],"returnSort":"E"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Int","index":3}],"term":{"id":"et","sort":"E","index":0},"unclassified":[],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$1-4","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},1],"$termType":"application"},"constructor":{"name":"$1","arguments":[],"argumentSorts":[],"returnSort":"E"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Int","index":3}],"term":{"id":"et","sort":"E","index":0},"unclassified":[],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$+-5","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et1","x","y","r1"]},{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et2","x","y","r2"]}],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"+","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[{"name":"r1","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$+","arguments":["et1","et2"],"argumentSorts":["E","E"],"returnSort":"E"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Int","index":3}],"term":{"id":"et","sort":"E","index":0},"unclassified":[],"auxiliary":[{"id":"r1","sort":"Int","index":null},{"id":"r2","sort":"Int","index":null}],"children":[{"id":"et1","sort":"E","index":0},{"id":"et2","sort":"E","index":1}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$ite-6","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","rb"]},{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["etc","x","y","rc"]},{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["eta","x","y","ra"]}],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"ite","returnSort":"Int","argumentSorts":["Bool","Int","Int"],"arguments":[{"name":"rb","sort":"Bool","$termType":"variable"},{"name":"rc","sort":"Int","$termType":"variable"},{"name":"ra","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$ite","arguments":["bt","etc","eta"],"argumentSorts":["B","E","E"],"returnSort":"E"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Int","index":3}],"term":{"id":"et","sort":"E","index":0},"unclassified":[],"auxiliary":[{"id":"rb","sort":"Bool","index":null},{"id":"rc","sort":"Int","index":null},{"id":"ra","sort":"Int","index":null}],"children":[{"id":"bt","sort":"B","index":0},{"id":"etc","sort":"E","index":1},{"id":"eta","sort":"E","index":2}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$t-7","head":{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","r"]},"bodyRelations":[],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$t","arguments":[],"argumentSorts":[],"returnSort":"B"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Bool","index":3}],"term":{"id":"bt","sort":"B","index":0},"unclassified":[],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$f-8","head":{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","r"]},"bodyRelations":[],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"false","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$f","arguments":[],"argumentSorts":[],"returnSort":"B"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Bool","index":3}],"term":{"id":"bt","sort":"B","index":0},"unclassified":[],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$!-9","head":{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","r"]},"bodyRelations":[{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","rb"]}],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"not","returnSort":"Bool","argumentSorts":["Bool"],"arguments":[{"name":"rb","sort":"Bool","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$!","arguments":["bt"],"argumentSorts":["B"],"returnSort":"B"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Bool","index":3}],"term":{"id":"bt","sort":"B","index":0},"unclassified":[],"auxiliary":[{"id":"rb","sort":"Bool","index":null}],"children":[{"id":"bt","sort":"B","index":0}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$and-10","head":{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","r"]},"bodyRelations":[{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt1","x","y","rb1"]},{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt2","x","y","rb2"]}],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"rb1","sort":"Bool","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$and","arguments":["bt1","bt2"],"argumentSorts":["B","B"],"returnSort":"B"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Bool","index":3}],"term":{"id":"bt","sort":"B","index":0},"unclassified":[],"auxiliary":[{"id":"rb1","sort":"Bool","index":null},{"id":"rb2","sort":"Bool","index":null}],"children":[{"id":"bt1","sort":"B","index":0},{"id":"bt2","sort":"B","index":1}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$or-11","head":{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","r"]},"bodyRelations":[{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt1","x","y","rb1"]},{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt2","x","y","rb2"]}],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"or","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"rb1","sort":"Bool","$termType":"variable"},{"name":"rb2","sort":"Bool","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$or","arguments":["bt1","bt2"],"argumentSorts":["B","B"],"returnSort":"B"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Bool","index":3}],"term":{"id":"bt","sort":"B","index":0},"unclassified":[],"auxiliary":[{"id":"rb1","sort":"Bool","index":null},{"id":"rb2","sort":"Bool","index":null}],"children":[{"id":"bt1","sort":"B","index":0},{"id":"bt2","sort":"B","index":1}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$<-12","head":{"name":"B.Sem","signature":["B","Int","Int","Bool"],"arguments":["bt","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et1","x","y","r1"]},{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et2","x","y","r2"]}],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"r","sort":"Bool","$termType":"variable"},{"name":"<","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r1","sort":"Int","$termType":"variable"},{"name":"r2","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$<","arguments":["et1","et2"],"argumentSorts":["E","E"],"returnSort":"B"},"symbols":{"inputs":[{"id":"x","sort":"Int","index":1},{"id":"y","sort":"Int","index":2}],"outputs":[{"id":"r","sort":"Bool","index":3}],"term":{"id":"bt","sort":"B","index":0},"unclassified":[],"auxiliary":[{"id":"r1","sort":"Int","index":null},{"id":"r2","sort":"Int","index":null}],"children":[{"id":"et1","sort":"E","index":0},{"id":"et2","sort":"E","index":1}]},"$event":"chc","$type":"semgus"}, +{"name":"max2","termType":"E","grammar":{"nonTerminals":[{"name":"@E__agtt","termType":"E"},{"name":"@B__agtt","termType":"B"}],"productions":[{"instance":"@E__agtt","operator":"$x","occurrences":[]},{"instance":"@E__agtt","operator":"$y","occurrences":[]},{"instance":"@E__agtt","operator":"$0","occurrences":[]},{"instance":"@E__agtt","operator":"$1","occurrences":[]},{"instance":"@E__agtt","operator":"$+","occurrences":["@E__agtt","@E__agtt"]},{"instance":"@E__agtt","operator":"$ite","occurrences":["@B__agtt","@E__agtt","@E__agtt"]},{"instance":"@B__agtt","operator":"$t","occurrences":[]},{"instance":"@B__agtt","operator":"$f","occurrences":[]},{"instance":"@B__agtt","operator":"$!","occurrences":["@B__agtt"]},{"instance":"@B__agtt","operator":"$and","occurrences":["@B__agtt","@B__agtt"]},{"instance":"@B__agtt","operator":"$or","occurrences":["@B__agtt","@B__agtt"]},{"instance":"@B__agtt","operator":"$<","occurrences":["@E__agtt","@E__agtt"]}]},"$event":"synth-fun","$type":"semgus"}, +{"constraint":{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"max2","returnSort":"E","argumentSorts":[],"arguments":[],"$termType":"application"},4,2,4],"$termType":"application"},"$event":"constraint","$type":"semgus"}, +{"constraint":{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"max2","returnSort":"E","argumentSorts":[],"arguments":[],"$termType":"application"},2,5,5],"$termType":"application"},"$event":"constraint","$type":"semgus"}, +{"constraint":{"bindings":[{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r","sort":"Int","$termType":"variable"}],"child":{"name":"=","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"max2","returnSort":"E","argumentSorts":[],"arguments":[],"$termType":"application"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"or","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"y","sort":"Int","$termType":"variable"},{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":">=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":">=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"forall"},"$event":"constraint","$type":"semgus"}, +{"$event":"check-synth","$type":"semgus"}, +{"$type":"meta","$event":"end-of-stream"} +] diff --git a/SemgusParser/HandlerFlags.cs b/SemgusParser/HandlerFlags.cs index f2609bc..477c966 100644 --- a/SemgusParser/HandlerFlags.cs +++ b/SemgusParser/HandlerFlags.cs @@ -39,6 +39,11 @@ private HandlerFlags(InvocationContext ctx, HandlerFlagsFactory fac) /// public bool FunctionEvents => _fac.FunctionEvents.GetFlag(_ctx); + /// + /// Whether or not to hide the legacy input/output/variables properties in CHCs in JSON + /// + public bool LegacySymbols => _fac.LegacySymbols.GetFlag(_ctx); + /// /// Class for configuring and creating handler flags /// @@ -49,6 +54,11 @@ public class HandlerFlagsFactory /// public readonly CommandFlag FunctionEvents = new("function-events", isHidden: true); + /// + /// Whether or not to hide the legacy input/output/variables properties in CHCs in JSON + /// + public readonly CommandFlag LegacySymbols = new("legacy-symbols", defaultValue: true, isHidden: true); + /// /// Creates a new HandlerFlagsFactory and configures it for the given command /// @@ -56,6 +66,7 @@ public class HandlerFlagsFactory public HandlerFlagsFactory(Command command) { command.AddFlag(FunctionEvents); + command.AddFlag(LegacySymbols); } /// diff --git a/SemgusParser/Json/ChcEvent.cs b/SemgusParser/Json/ChcEvent.cs index f1952d0..7cb729a 100644 --- a/SemgusParser/Json/ChcEvent.cs +++ b/SemgusParser/Json/ChcEvent.cs @@ -13,23 +13,32 @@ namespace Semgus.Parser.Json internal class ChcEvent : ParseEvent { private readonly SemgusChc _chc; + private readonly bool _includeLegacySymbols; public SmtIdentifier? Id => _chc.Id; public SemgusChc.SemanticRelation Head => _chc.Head; public IReadOnlyList BodyRelations => _chc.BodyRelations; + #region Deprecated variable properties public IReadOnlyCollection? InputVariables => _chc.InputVariables?.Select(v => v.Name).ToList(); public IReadOnlyCollection? OutputVariables => _chc.OutputVariables?.Select(v => v.Name).ToList(); public IReadOnlyCollection? Variables => _chc.VariableBindings.Select(b => b.Id).ToList(); + + public bool ShouldSerializeInputVariables() => _includeLegacySymbols; + public bool ShouldSerializeOutputVariables() => _includeLegacySymbols; + public bool ShouldSerializeVariables() => _includeLegacySymbols; + #endregion + public SmtTerm Constraint => _chc.Constraint; public ConstructorModel? Constructor { get; } public SemgusChc.SymbolTable Symbols => _chc.Symbols; - public ChcEvent(SemgusChc chc) : base("chc", "semgus") + public ChcEvent(SemgusChc chc, bool includeLegacySymbols) : base("chc", "semgus") { _chc = chc; + _includeLegacySymbols = includeLegacySymbols; if (_chc.Binder.Constructor != null) { Constructor = new(_chc.Binder.Constructor.Name, diff --git a/SemgusParser/Json/JsonHandler.cs b/SemgusParser/Json/JsonHandler.cs index e1f662f..5f2b875 100644 --- a/SemgusParser/Json/JsonHandler.cs +++ b/SemgusParser/Json/JsonHandler.cs @@ -68,7 +68,7 @@ public void OnCheckSynth(SmtContext smtCtx, SemgusContext semgusCtx) { foreach (var chc in semgusCtx.Chcs) { - _serializer.Serialize(_writer, new ChcEvent(chc)); + _serializer.Serialize(_writer, new ChcEvent(chc, includeLegacySymbols: _flags.LegacySymbols)); EndOfEvent(); }