Skip to content

Commit 25f6d51

Browse files
kjcjohnsonkjcjohnson
authored
Add IDs to CHCs (#104)
* Add CHC IDs to output events
1 parent 6739a59 commit 25f6d51

15 files changed

Lines changed: 220 additions & 154 deletions

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

Lines changed: 12 additions & 12 deletions
Large diffs are not rendered by default.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
{"name":"BV.Sem","rank":{"argumentSorts":["BV",["BitVec",8]],"returnSort":"Bool"},"definition":{"arguments":["term","x1"],"body":{"term":{"name":"term","sort":"BV","$termType":"variable"},"binders":[{"operator":"$bv","arguments":[],"child":{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"},"$termType":"binder"}],"$termType":"match"},"$termType":"lambda"},"$event":"define-function","$type":"smt"}
55
{"name":"bvxor","rank":{"argumentSorts":[["BitVec",8],["BitVec",8]],"returnSort":["BitVec",8]},"$event":"declare-function","$type":"smt"}
66
{"name":"bvxor","rank":{"argumentSorts":[["BitVec",8],["BitVec",8]],"returnSort":["BitVec",8]},"definition":{"arguments":["a1","a2"],"body":{"name":"bvor","returnSort":["BitVec",8],"argumentSorts":[["BitVec",8],["BitVec",8]],"arguments":[{"name":"bvand","returnSort":["BitVec",8],"argumentSorts":[["BitVec",8],["BitVec",8]],"arguments":[{"name":"a1","sort":["BitVec",8],"$termType":"variable"},{"name":"bvnot","returnSort":["BitVec",8],"argumentSorts":[["BitVec",8]],"arguments":[{"name":"a2","sort":["BitVec",8],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"bvand","returnSort":["BitVec",8],"argumentSorts":[["BitVec",8],["BitVec",8]],"arguments":[{"name":"bvnot","returnSort":["BitVec",8],"argumentSorts":[["BitVec",8]],"arguments":[{"name":"a1","sort":["BitVec",8],"$termType":"variable"}],"$termType":"application"},{"name":"a2","sort":["BitVec",8],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"lambda"},"$event":"define-function","$type":"smt"}
7-
{"head":{"name":"BV.Sem","signature":["BV",["BitVec",8]],"arguments":["term","x1"]},"bodyRelations":[],"inputVariables":null,"outputVariables":null,"variables":["term","x1"],"constraint":{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"},"constructor":{"name":"$bv","arguments":[],"argumentSorts":[],"returnSort":"BV"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"term","sort":"BV","index":0},"unclassified":[{"id":"x1","sort":["BitVec",8],"index":1}],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}
7+
{"id":"_CHC-$bv-1","head":{"name":"BV.Sem","signature":["BV",["BitVec",8]],"arguments":["term","x1"]},"bodyRelations":[],"inputVariables":null,"outputVariables":null,"variables":["term","x1"],"constraint":{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"},"constructor":{"name":"$bv","arguments":[],"argumentSorts":[],"returnSort":"BV"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"term","sort":"BV","index":0},"unclassified":[{"id":"x1","sort":["BitVec",8],"index":1}],"auxiliary":[],"children":[]},"$event":"chc","$type":"semgus"}
88
{"name":"fn","termType":"BV","grammar":{"nonTerminals":[{"name":"@BV__agtt","termType":"BV"}],"productions":[{"instance":"@BV__agtt","operator":"$bv","occurrences":[]}]},"$event":"synth-fun","$type":"semgus"}
99
{"constraint":{"name":"BV.Sem","returnSort":"Bool","argumentSorts":["BV",["BitVec",8]],"arguments":[{"name":"fn","returnSort":"BV","argumentSorts":[],"arguments":[],"$termType":"application"},{"name":"concat","returnSort":["BitVec",8],"argumentSorts":[["BitVec",4],["BitVec",4]],"arguments":[{"size":4,"value":"0x0","$termType":"bitvector"},{"size":4,"value":"0xF","$termType":"bitvector"}],"$termType":"application"}],"$termType":"application"},"$event":"constraint","$type":"semgus"}
1010
{"constraint":{"name":"BV.Sem","returnSort":"Bool","argumentSorts":["BV",["BitVec",8]],"arguments":[{"name":"fn","returnSort":"BV","argumentSorts":[],"arguments":[],"$termType":"application"},{"name":"concat","returnSort":["BitVec",8],"argumentSorts":[["BitVec",1],["BitVec",7]],"arguments":[{"size":1,"value":"0x1","$termType":"bitvector"},{"size":7,"value":"0x18","$termType":"bitvector"}],"$termType":"application"}],"$termType":"application"},"$event":"constraint","$type":"semgus"}

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

Lines changed: 10 additions & 10 deletions
Large diffs are not rendered by default.

‎IntegrationTests/tests/test-json-no-functions.txt‎

Lines changed: 12 additions & 12 deletions
Large diffs are not rendered by default.

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

Lines changed: 12 additions & 12 deletions
Large diffs are not rendered by default.

‎IntegrationTests/tests/test-json-sygus-dr-name.txt‎

Lines changed: 31 additions & 31 deletions
Large diffs are not rendered by default.

‎IntegrationTests/tests/test-semantic-sugar.txt‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@
22
{"name":"E","constructors":[{"name":"$a","children":[]},{"name":"$b","children":[]},{"name":"$c","children":[]},{"name":"$d","children":[]},{"name":"$e","children":[]}],"$event":"define-term-type","$type":"semgus"}
33
{"name":"E.Sem","rank":{"argumentSorts":["E","Int","Int","Int"],"returnSort":"Bool"},"$event":"declare-function","$type":"smt"}
44
{"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":"$a","arguments":[],"child":{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"},{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"},"$termType":"binder"},{"operator":"$b","arguments":[],"child":{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[0,{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},"$termType":"binder"},{"operator":"$c","arguments":[],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[0,{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},0],"$termType":"application"}],"$termType":"application"},"$termType":"binder"},{"operator":"$d","arguments":[],"child":{"name":"or","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et","sort":"E","$termType":"variable"},{"name":"x","sort":"Int","$termType":"variable"},0,12],"$termType":"application"},{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},3],"$termType":"application"}],"$termType":"application"},"$termType":"binder"},{"operator":"$e","arguments":[],"child":{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"et","sort":"E","$termType":"variable"},{"name":"+","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"-","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[12,{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"},89],"$termType":"application"},"$termType":"binder"}],"$termType":"match","annotations":[{"keyword":{"name":"input"},"value":["x","y"]},{"keyword":{"name":"output"},"value":["r"]}]},"$termType":"lambda"},"$event":"define-function","$type":"smt"}
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":["et","x","y","r"]}],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"},"constructor":{"name":"$a","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"}
6-
{"head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[0,{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},"constructor":{"name":"$b","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"}
7-
{"head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[0,{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},0],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$c","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"}
8-
{"head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x",["_CHC_VAR",1],["_CHC_VAR",2]]}],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r",["_CHC_VAR",1],["_CHC_VAR",2]],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",1],"sort":"Int","$termType":"variable"},0],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",2],"sort":"Int","$termType":"variable"},12],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$d","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":[{"id":["_CHC_VAR",1],"sort":"Int","index":null},{"id":["_CHC_VAR",2],"sort":"Int","index":null}],"children":[]},"$event":"chc","$type":"semgus"}
9-
{"head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},3],"$termType":"application"},"constructor":{"name":"$d","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"}
10-
{"head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et",["_CHC_VAR",3],["_CHC_VAR",4],["_CHC_VAR",5]]}],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r",["_CHC_VAR",3],["_CHC_VAR",4],["_CHC_VAR",5]],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",3],"sort":"Int","$termType":"variable"},{"name":"+","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",4],"sort":"Int","$termType":"variable"},{"name":"-","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[12,{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",5],"sort":"Int","$termType":"variable"},89],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$e","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":[{"id":["_CHC_VAR",3],"sort":"Int","index":null},{"id":["_CHC_VAR",4],"sort":"Int","index":null},{"id":["_CHC_VAR",5],"sort":"Int","index":null}],"children":[]},"$event":"chc","$type":"semgus"}
5+
{"id":"_CHC-$a-1","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]}],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":"true","returnSort":"Bool","argumentSorts":[],"arguments":[],"$termType":"application"},"constructor":{"name":"$a","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"}
6+
{"id":"_CHC-$b-2","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[0,{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},"constructor":{"name":"$b","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"}
7+
{"id":"_CHC-$c-3","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[0,{"name":"x","sort":"Int","$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},0],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$c","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"}
8+
{"id":"_CHC-$d-6","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x",["_CHC_VAR",4],["_CHC_VAR",5]]}],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r",["_CHC_VAR",4],["_CHC_VAR",5]],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",4],"sort":"Int","$termType":"variable"},0],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",5],"sort":"Int","$termType":"variable"},12],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$d","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":[{"id":["_CHC_VAR",4],"sort":"Int","index":null},{"id":["_CHC_VAR",5],"sort":"Int","index":null}],"children":[]},"$event":"chc","$type":"semgus"}
9+
{"id":"_CHC-$d-7","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":">","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},3],"$termType":"application"},"constructor":{"name":"$d","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"}
10+
{"id":"_CHC-$e-11","head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et",["_CHC_VAR",8],["_CHC_VAR",9],["_CHC_VAR",10]]}],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r",["_CHC_VAR",8],["_CHC_VAR",9],["_CHC_VAR",10]],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",8],"sort":"Int","$termType":"variable"},{"name":"+","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[{"name":"x","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",9],"sort":"Int","$termType":"variable"},{"name":"-","returnSort":"Int","argumentSorts":["Int","Int"],"arguments":[12,{"name":"r","sort":"Int","$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":["_CHC_VAR",10],"sort":"Int","$termType":"variable"},89],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$e","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":[{"id":["_CHC_VAR",8],"sort":"Int","index":null},{"id":["_CHC_VAR",9],"sort":"Int","index":null},{"id":["_CHC_VAR",10],"sort":"Int","index":null}],"children":[]},"$event":"chc","$type":"semgus"}
1111
{"name":"f","termType":"E","grammar":{"nonTerminals":[{"name":"@E__agtt","termType":"E"}],"productions":[{"instance":"@E__agtt","operator":"$a","occurrences":[]},{"instance":"@E__agtt","operator":"$b","occurrences":[]},{"instance":"@E__agtt","operator":"$c","occurrences":[]},{"instance":"@E__agtt","operator":"$d","occurrences":[]},{"instance":"@E__agtt","operator":"$e","occurrences":[]}]},"$event":"synth-fun","$type":"semgus"}
1212
{"constraint":{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E","Int","Int","Int"],"arguments":[{"name":"f","returnSort":"E","argumentSorts":[],"arguments":[],"$termType":"application"},1,2,0],"$termType":"application"},"$event":"constraint","$type":"semgus"}
1313
{"$event":"check-synth","$type":"semgus"}

0 commit comments

Comments
 (0)