diff --git a/IntegrationTests/data/sequences.sem b/IntegrationTests/data/sequences.sem index 887f049..6170fb3 100644 --- a/IntegrationTests/data/sequences.sem +++ b/IntegrationTests/data/sequences.sem @@ -2,6 +2,8 @@ ((Start 0)) ((($main)))) +(declare-const X (Seq Int)) + (define-funs-rec ((Start.Sem ((Start_term_0 Start) (rq (Seq Int)) (x (_ BitVec 32))) Bool)) @@ -11,7 +13,17 @@ (and (= "Test" (seq.nth rb 7)) (= rb (seq.++ ra (seq.unit "a"))) (= rb (as seq.empty (Seq String))) - (= rq (seq.rev rq))))))))) + (= rq (seq.rev rq)) + (= (seq.len ra) (seq.nth rq 1)) + (= (seq.update ra 7 rb) rb) + (= ra (seq.extract rb 3 5)) + (= (seq.at rb 4) (seq.at ra 3)) + (seq.contains ra rb) + (= 12 (seq.indexof ra rb 7)) + (= ra (seq.replace ra ra rb)) + (= (seq.replace_all ra ra rb) rb) + (seq.prefixof ra rb) + (seq.suffixof rb ra)))))))) (synth-fun MyFunc () Start) diff --git a/IntegrationTests/tests/test-json-sequences.txt b/IntegrationTests/tests/test-json-sequences.txt index 3081f7e..ca79608 100644 --- a/IntegrationTests/tests/test-json-sequences.txt +++ b/IntegrationTests/tests/test-json-sequences.txt @@ -1,9 +1,10 @@ [ {"name":"Start","$event":"declare-term-type","$type":"semgus"}, {"name":"Start","constructors":[{"name":"$main","children":[]}],"$event":"define-term-type","$type":"semgus"}, +{"name":"X","rank":{"argumentSorts":[],"returnSort":{"kind":"Seq","params":["Int"]}},"$event":"declare-function","$type":"smt"}, {"name":"Start.Sem","rank":{"argumentSorts":["Start",{"kind":"Seq","params":["Int"]},["BitVec",32]],"returnSort":"Bool"},"$event":"declare-function","$type":"smt"}, -{"name":"Start.Sem","rank":{"argumentSorts":["Start",{"kind":"Seq","params":["Int"]},["BitVec",32]],"returnSort":"Bool"},"definition":{"arguments":["Start_term_0","rq","x"],"body":{"term":{"name":"Start_term_0","sort":"Start","$termType":"variable"},"binders":[{"operator":"$main","arguments":[],"child":{"bindings":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["String","String"],"arguments":["Test",{"name":"seq.nth","returnSort":"String","argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.++","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.unit","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":["String"],"arguments":["a"],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.empty","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["Int"]},{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},{"name":"seq.rev","returnSort":{"kind":"Seq","params":["Int"]},"argumentSorts":[{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"}],"$termType":"match"},"$termType":"lambda"},"$event":"define-function","$type":"smt"}, -{"id":"_CHC-$main-1","head":{"name":"Start.Sem","signature":["Start",{"kind":"Seq","params":["Int"]},["BitVec",32]],"arguments":["Start_term_0","rq","x"]},"bodyRelations":[],"inputVariables":null,"outputVariables":null,"variables":["Start_term_0","rq","x","rb","ra"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["String","String"],"arguments":["Test",{"name":"seq.nth","returnSort":"String","argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.++","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.unit","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":["String"],"arguments":["a"],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.empty","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["Int"]},{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},{"name":"seq.rev","returnSort":{"kind":"Seq","params":["Int"]},"argumentSorts":[{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$main","arguments":[],"argumentSorts":[],"returnSort":"Start"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"Start_term_0","sort":"Start","index":0},"unclassified":[{"id":"rq","sort":{"kind":"Seq","params":["Int"]},"index":1},{"id":"x","sort":["BitVec",32],"index":2}],"auxiliary":[{"id":"rb","sort":{"kind":"Seq","params":["String"]},"index":null},{"id":"ra","sort":{"kind":"Seq","params":["String"]},"index":null}],"children":[]},"$event":"chc","$type":"semgus"}, +{"name":"Start.Sem","rank":{"argumentSorts":["Start",{"kind":"Seq","params":["Int"]},["BitVec",32]],"returnSort":"Bool"},"definition":{"arguments":["Start_term_0","rq","x"],"body":{"term":{"name":"Start_term_0","sort":"Start","$termType":"variable"},"binders":[{"operator":"$main","arguments":[],"child":{"bindings":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["String","String"],"arguments":["Test",{"name":"seq.nth","returnSort":"String","argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.++","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.unit","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":["String"],"arguments":["a"],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.empty","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["Int"]},{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},{"name":"seq.rev","returnSort":{"kind":"Seq","params":["Int"]},"argumentSorts":[{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"seq.len","returnSort":"Int","argumentSorts":[{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"seq.nth","returnSort":"Int","argumentSorts":[{"kind":"Seq","params":["Int"]},"Int"],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},1],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"seq.update","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int",{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7,{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.extract","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int","Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},3,5],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"seq.at","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},4],"$termType":"application"},{"name":"seq.at","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},3],"$termType":"application"}],"$termType":"application"},{"name":"seq.contains","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[12,{"name":"seq.indexof","returnSort":"Int","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.replace","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"seq.replace_all","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"seq.prefixof","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"seq.suffixof","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"}],"$termType":"match"},"$termType":"lambda"},"$event":"define-function","$type":"smt"}, +{"id":"_CHC-$main-1","head":{"name":"Start.Sem","signature":["Start",{"kind":"Seq","params":["Int"]},["BitVec",32]],"arguments":["Start_term_0","rq","x"]},"bodyRelations":[],"inputVariables":null,"outputVariables":null,"variables":["Start_term_0","rq","x","rb","ra"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":["String","String"],"arguments":["Test",{"name":"seq.nth","returnSort":"String","argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.++","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.unit","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":["String"],"arguments":["a"],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.empty","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[],"arguments":[],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["Int"]},{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},{"name":"seq.rev","returnSort":{"kind":"Seq","params":["Int"]},"argumentSorts":[{"kind":"Seq","params":["Int"]}],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"seq.len","returnSort":"Int","argumentSorts":[{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"seq.nth","returnSort":"Int","argumentSorts":[{"kind":"Seq","params":["Int"]},"Int"],"arguments":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},1],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"seq.update","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int",{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7,{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.extract","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int","Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},3,5],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"seq.at","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},4],"$termType":"application"},{"name":"seq.at","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},3],"$termType":"application"}],"$termType":"application"},{"name":"seq.contains","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[12,{"name":"seq.indexof","returnSort":"Int","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]},"Int"],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},7],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"seq.replace","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"seq.replace_all","returnSort":{"kind":"Seq","params":["String"]},"argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"seq.prefixof","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"},{"name":"seq.suffixof","returnSort":"Bool","argumentSorts":[{"kind":"Seq","params":["String"]},{"kind":"Seq","params":["String"]}],"arguments":[{"name":"rb","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"},{"name":"ra","sort":{"kind":"Seq","params":["String"]},"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$main","arguments":[],"argumentSorts":[],"returnSort":"Start"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"Start_term_0","sort":"Start","index":0},"unclassified":[{"id":"rq","sort":{"kind":"Seq","params":["Int"]},"index":1},{"id":"x","sort":["BitVec",32],"index":2}],"auxiliary":[{"id":"rb","sort":{"kind":"Seq","params":["String"]},"index":null},{"id":"ra","sort":{"kind":"Seq","params":["String"]},"index":null}],"children":[]},"$event":"chc","$type":"semgus"}, {"name":"MyFunc","termType":"Start","grammar":{"nonTerminals":[{"name":"@Start__agtt","termType":"Start"}],"productions":[{"instance":"@Start__agtt","operator":"$main","occurrences":[]}]},"$event":"synth-fun","$type":"semgus"}, {"constraint":{"bindings":[{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"child":{"name":"Start.Sem","returnSort":"Bool","argumentSorts":["Start",{"kind":"Seq","params":["Int"]},["BitVec",32]],"arguments":[{"name":"MyFunc","returnSort":"Start","argumentSorts":[],"arguments":[],"$termType":"application"},{"name":"rq","sort":{"kind":"Seq","params":["Int"]},"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},"$termType":"exists"},"$event":"constraint","$type":"semgus"}, {"$event":"check-synth","$type":"semgus"}, diff --git a/IntegrationTests/tests/test-sexpr-sequences.txt b/IntegrationTests/tests/test-sexpr-sequences.txt index f3cac93..8655eb2 100644 --- a/IntegrationTests/tests/test-sexpr-sequences.txt +++ b/IntegrationTests/tests/test-sexpr-sequences.txt @@ -1,9 +1,10 @@ (declare-term-types (sort (identifier "Start"))) (add-constructor (sort (identifier "Start")) :operator (identifier "$main") :children (list)) +(declare-function (identifier "X") :rank (rank :argument-sorts (list) :return-sort (sort (identifier "Seq") (sort (identifier "Int"))))) (declare-function (identifier "Start.Sem") :rank (rank :argument-sorts (list (sort (identifier "Start")) (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :return-sort (sort (identifier "Bool")))) -(define-function (identifier "Start.Sem") :rank (rank :argument-sorts (list (sort (identifier "Start")) (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :return-sort (sort (identifier "Bool"))) :definition (term (lambda :arguments (list (identifier "Start_term_0") (identifier "rq") (identifier "x")) :body (match :term (variable (identifier "Start_term_0") :sort (sort (identifier "Start"))) :binders (list (binder :operator (identifier "$main") :arguments (list) :child (exists :bindings (list (identifier "rb") (identifier "ra")) :binding-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :child (application (identifier "and") :argument-sorts (list (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool"))) :arguments (list (application (identifier "=") :argument-sorts (list (sort (identifier "String")) (sort (identifier "String"))) :arguments (list "Test" (application (identifier "seq.nth") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7) :return-sort (sort (identifier "String")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.++") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.unit") :argument-sorts (list (sort (identifier "String"))) :arguments (list "a") :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.empty") :argument-sorts (list) :arguments (list) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) (application (identifier "seq.rev") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Bool")))) :return-sort (sort (identifier "Bool")))))))))) -(chc :id (identifier "_CHC-$main-1") :head (relation (identifier "Start.Sem") :signature (list (sort (identifier "Start")) (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :arguments (list (identifier "Start_term_0") (identifier "rq") (identifier "x"))) :body (list) :variables (list (identifier "Start_term_0") (identifier "rq") (identifier "x") (identifier "rb") (identifier "ra")) :symbols (symbol-table :term (symbol-entry (identifier "Start_term_0") :sort (sort (identifier "Start")) :index 0) :inputs (list) :outputs (list) :auxiliary (list (symbol-entry (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (symbol-entry (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :children (list) :unclassified (list (symbol-entry (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int"))) :index 1) (symbol-entry (identifier "x") :sort (sort (identifier "BitVec" 32)) :index 2))) :constraint (term (application (identifier "and") :argument-sorts (list (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool"))) :arguments (list (application (identifier "=") :argument-sorts (list (sort (identifier "String")) (sort (identifier "String"))) :arguments (list "Test" (application (identifier "seq.nth") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7) :return-sort (sort (identifier "String")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.++") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.unit") :argument-sorts (list (sort (identifier "String"))) :arguments (list "a") :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.empty") :argument-sorts (list) :arguments (list) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) (application (identifier "seq.rev") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Bool")))) :return-sort (sort (identifier "Bool")))) :constructor (constructor (identifier "$main") :arguments (list) :argument-sorts (list) :return-sort (sort (identifier "Start")))) +(define-function (identifier "Start.Sem") :rank (rank :argument-sorts (list (sort (identifier "Start")) (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :return-sort (sort (identifier "Bool"))) :definition (term (lambda :arguments (list (identifier "Start_term_0") (identifier "rq") (identifier "x")) :body (match :term (variable (identifier "Start_term_0") :sort (sort (identifier "Start"))) :binders (list (binder :operator (identifier "$main") :arguments (list) :child (exists :bindings (list (identifier "rb") (identifier "ra")) :binding-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :child (application (identifier "and") :argument-sorts (list (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool"))) :arguments (list (application (identifier "=") :argument-sorts (list (sort (identifier "String")) (sort (identifier "String"))) :arguments (list "Test" (application (identifier "seq.nth") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7) :return-sort (sort (identifier "String")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.++") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.unit") :argument-sorts (list (sort (identifier "String"))) :arguments (list "a") :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.empty") :argument-sorts (list) :arguments (list) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) (application (identifier "seq.rev") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Int")) (sort (identifier "Int"))) :arguments (list (application (identifier "seq.len") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Int"))) (application (identifier "seq.nth") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) 1) :return-sort (sort (identifier "Int")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (application (identifier "seq.update") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int")) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7 (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.extract") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int")) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 3 5) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (application (identifier "seq.at") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 4) :return-sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.at") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) 3) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "seq.contains") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Int")) (sort (identifier "Int"))) :arguments (list 12 (application (identifier "seq.indexof") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7) :return-sort (sort (identifier "Int")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.replace") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (application (identifier "seq.replace_all") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "seq.prefixof") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "seq.suffixof") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool")))) :return-sort (sort (identifier "Bool")))))))))) +(chc :id (identifier "_CHC-$main-1") :head (relation (identifier "Start.Sem") :signature (list (sort (identifier "Start")) (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :arguments (list (identifier "Start_term_0") (identifier "rq") (identifier "x"))) :body (list) :variables (list (identifier "Start_term_0") (identifier "rq") (identifier "x") (identifier "rb") (identifier "ra")) :symbols (symbol-table :term (symbol-entry (identifier "Start_term_0") :sort (sort (identifier "Start")) :index 0) :inputs (list) :outputs (list) :auxiliary (list (symbol-entry (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (symbol-entry (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :children (list) :unclassified (list (symbol-entry (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int"))) :index 1) (symbol-entry (identifier "x") :sort (sort (identifier "BitVec" 32)) :index 2))) :constraint (term (application (identifier "and") :argument-sorts (list (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool")) (sort (identifier "Bool"))) :arguments (list (application (identifier "=") :argument-sorts (list (sort (identifier "String")) (sort (identifier "String"))) :arguments (list "Test" (application (identifier "seq.nth") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7) :return-sort (sort (identifier "String")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.++") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.unit") :argument-sorts (list (sort (identifier "String"))) :arguments (list "a") :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.empty") :argument-sorts (list) :arguments (list) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) (application (identifier "seq.rev") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int")))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Seq") (sort (identifier "Int"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Int")) (sort (identifier "Int"))) :arguments (list (application (identifier "seq.len") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Int"))) (application (identifier "seq.nth") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) 1) :return-sort (sort (identifier "Int")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (application (identifier "seq.update") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int")) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7 (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.extract") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int")) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 3 5) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (application (identifier "seq.at") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 4) :return-sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.at") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) 3) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "seq.contains") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Int")) (sort (identifier "Int"))) :arguments (list 12 (application (identifier "seq.indexof") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Int"))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) 7) :return-sort (sort (identifier "Int")))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (application (identifier "seq.replace") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "=") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (application (identifier "seq.replace_all") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "seq.prefixof") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool"))) (application (identifier "seq.suffixof") :argument-sorts (list (sort (identifier "Seq") (sort (identifier "String"))) (sort (identifier "Seq") (sort (identifier "String")))) :arguments (list (variable (identifier "rb") :sort (sort (identifier "Seq") (sort (identifier "String")))) (variable (identifier "ra") :sort (sort (identifier "Seq") (sort (identifier "String"))))) :return-sort (sort (identifier "Bool")))) :return-sort (sort (identifier "Bool")))) :constructor (constructor (identifier "$main") :arguments (list) :argument-sorts (list) :return-sort (sort (identifier "Start")))) (synth-fun (identifier "MyFunc") :term-type (sort (identifier "Start")) :grammar (grammar :non-terminals (list (identifier "@Start__agtt")) :non-terminal-types (list (sort (identifier "Start"))) :productions (list (production :instance (identifier "@Start__agtt") :occurrences (list) :operator (identifier "$main"))))) (constraint (term (exists :bindings (list (identifier "rq") (identifier "y")) :binding-sorts (list (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :child (application (identifier "Start.Sem") :argument-sorts (list (sort (identifier "Start")) (sort (identifier "Seq") (sort (identifier "Int"))) (sort (identifier "BitVec" 32))) :arguments (list (application (identifier "MyFunc") :argument-sorts (list) :arguments (list) :return-sort (sort (identifier "Start"))) (variable (identifier "rq") :sort (sort (identifier "Seq") (sort (identifier "Int")))) (variable (identifier "y") :sort (sort (identifier "BitVec" 32)))) :return-sort (sort (identifier "Bool")))))) (check-synth) \ No newline at end of file