diff --git a/IntegrationTests/data/array.sem b/IntegrationTests/data/array.sem new file mode 100644 index 0000000..a55bd1e --- /dev/null +++ b/IntegrationTests/data/array.sem @@ -0,0 +1,37 @@ +(declare-term-types +((E 0) (Start 0)) +((($IBVVary ) +($bvsub E E) +($bvadd E E) +($IBVVarx )) +(($bv=x E)))) + + + +(define-funs-rec +((E.Sem ((E_term_0 E) (r__0 (_ BitVec 32)) (rv (Array Int Int)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool) +(Start.Sem ((Start_term_0 Start) (x_r0 (_ BitVec 32)) (y_r0 (_ BitVec 32)) (rq (Array Int Int)) (x (_ BitVec 32)) (y (_ BitVec 32))) Bool)) + +((match E_term_0 + (($IBVVary (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1) + (= r__1 y)))) +(($bvsub E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32)) (rb (Array Int Int))) (and (= r__0 (bvadd r__1 (bvneg r__2))) + (E.Sem E_term_1 r__1 rb x y) + (E.Sem E_term_2 r__2 rb x y)))) +(($bvadd E_term_1 E_term_2) (exists ((r__1 (_ BitVec 32)) (r__2 (_ BitVec 32)) (rb (Array Int Int))) (and (= r__0 (bvadd r__1 r__2)) + (E.Sem E_term_1 r__1 rb x y) + (E.Sem E_term_2 r__2 rb x y)))) +($IBVVarx (exists ((r__1 (_ BitVec 32))) (and (= r__0 r__1) + (= r__1 x)))))) +(match Start_term_0 + ((($bv=x E_term_1) (exists ((r__1 (_ BitVec 32)) (rb (Array Int Int))) (and (and (= x_r0 r__1) + (and (= rb rb) (= y y_r0))) + (E.Sem E_term_1 r__1 rb x y)))))))) + + +(synth-fun BVtest_ADD_01() Start) + + +(constraint (exists ((rq (Array Int Int)) (y (_ BitVec 32))) (Start.Sem BVtest_ADD_01 #x00000004 #x00000004 rq #x00000003 y))) + +(check-synth) diff --git a/IntegrationTests/tests/test-json-array.rsp b/IntegrationTests/tests/test-json-array.rsp new file mode 100644 index 0000000..3c04809 --- /dev/null +++ b/IntegrationTests/tests/test-json-array.rsp @@ -0,0 +1,6 @@ +--format +json +--mode +batch +-- +data/array.sem \ No newline at end of file diff --git a/IntegrationTests/tests/test-json-array.txt b/IntegrationTests/tests/test-json-array.txt new file mode 100644 index 0000000..3cc3d91 --- /dev/null +++ b/IntegrationTests/tests/test-json-array.txt @@ -0,0 +1,19 @@ +[ +{"name":"E","$event":"declare-term-type","$type":"semgus"}, +{"name":"Start","$event":"declare-term-type","$type":"semgus"}, +{"name":"E","constructors":[{"name":"$IBVVary","children":[]},{"name":"$bvsub","children":["E","E"]},{"name":"$bvadd","children":["E","E"]},{"name":"$IBVVarx","children":[]}],"$event":"define-term-type","$type":"semgus"}, +{"name":"Start","constructors":[{"name":"$bv=x","children":["E"]}],"$event":"define-term-type","$type":"semgus"}, +{"name":"E.Sem","rank":{"argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"returnSort":"Bool"},"$event":"declare-function","$type":"smt"}, +{"name":"Start.Sem","rank":{"argumentSorts":["Start",["BitVec",32],["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"returnSort":"Bool"},"$event":"declare-function","$type":"smt"}, +{"name":"E.Sem","rank":{"argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"returnSort":"Bool"},"definition":{"arguments":["E_term_0","r__0","rv","x","y"],"body":{"term":{"name":"E_term_0","sort":"E","$termType":"variable"},"binders":[{"operator":"$IBVVary","arguments":[],"child":{"bindings":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$bvsub","arguments":["E_term_1","E_term_2"],"child":{"bindings":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"r__2","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"bvadd","returnSort":["BitVec",32],"argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"bvneg","returnSort":["BitVec",32],"argumentSorts":[["BitVec",32]],"arguments":[{"name":"r__2","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":[{"name":"E_term_1","sort":"E","$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":[{"name":"E_term_2","sort":"E","$termType":"variable"},{"name":"r__2","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$bvadd","arguments":["E_term_1","E_term_2"],"child":{"bindings":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"r__2","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"bvadd","returnSort":["BitVec",32],"argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"r__2","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":[{"name":"E_term_1","sort":"E","$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":[{"name":"E_term_2","sort":"E","$termType":"variable"},{"name":"r__2","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"},{"operator":"$IBVVarx","arguments":[],"child":{"bindings":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"}],"$termType":"match"},"$termType":"lambda"},"$event":"define-function","$type":"smt"}, +{"name":"Start.Sem","rank":{"argumentSorts":["Start",["BitVec",32],["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"returnSort":"Bool"},"definition":{"arguments":["Start_term_0","x_r0","y_r0","rq","x","y"],"body":{"term":{"name":"Start_term_0","sort":"Start","$termType":"variable"},"binders":[{"operator":"$bv=x","arguments":["E_term_1"],"child":{"bindings":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"}],"child":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"x_r0","sort":["BitVec",32],"$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Array","params":["Int","Int"]},{"kind":"Array","params":["Int","Int"]}],"arguments":[{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"y","sort":["BitVec",32],"$termType":"variable"},{"name":"y_r0","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},{"name":"E.Sem","returnSort":"Bool","argumentSorts":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":[{"name":"E_term_1","sort":"E","$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"$termType":"exists"},"$termType":"binder"}],"$termType":"match"},"$termType":"lambda"},"$event":"define-function","$type":"smt"}, +{"id":"_CHC-$IBVVary-1","head":{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_0","r__0","rv","x","y"]},"bodyRelations":[],"inputVariables":null,"outputVariables":null,"variables":["E_term_0","r__0","rv","x","y","r__1"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$IBVVary","arguments":[],"argumentSorts":[],"returnSort":"E"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"E_term_0","sort":"E","index":0},"unclassified":[{"id":"r__0","sort":["BitVec",32],"index":1},{"id":"rv","sort":{"kind":"Array","params":["Int","Int"]},"index":2},{"id":"x","sort":["BitVec",32],"index":3},{"id":"y","sort":["BitVec",32],"index":4}],"auxiliary":[{"id":"r__1","sort":["BitVec",32],"index":null}],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$bvsub-2","head":{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_0","r__0","rv","x","y"]},"bodyRelations":[{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_1","r__1","rb","x","y"]},{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_2","r__2","rb","x","y"]}],"inputVariables":null,"outputVariables":null,"variables":["E_term_0","r__0","rv","x","y","r__1","r__2","rb"],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"bvadd","returnSort":["BitVec",32],"argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"bvneg","returnSort":["BitVec",32],"argumentSorts":[["BitVec",32]],"arguments":[{"name":"r__2","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$bvsub","arguments":["E_term_1","E_term_2"],"argumentSorts":["E","E"],"returnSort":"E"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"E_term_0","sort":"E","index":0},"unclassified":[{"id":"r__0","sort":["BitVec",32],"index":1},{"id":"rv","sort":{"kind":"Array","params":["Int","Int"]},"index":2},{"id":"x","sort":["BitVec",32],"index":3},{"id":"y","sort":["BitVec",32],"index":4}],"auxiliary":[{"id":"r__1","sort":["BitVec",32],"index":null},{"id":"r__2","sort":["BitVec",32],"index":null},{"id":"rb","sort":{"kind":"Array","params":["Int","Int"]},"index":null}],"children":[{"id":"E_term_1","sort":"E","index":0},{"id":"E_term_2","sort":"E","index":1}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$bvadd-3","head":{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_0","r__0","rv","x","y"]},"bodyRelations":[{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_1","r__1","rb","x","y"]},{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_2","r__2","rb","x","y"]}],"inputVariables":null,"outputVariables":null,"variables":["E_term_0","r__0","rv","x","y","r__1","r__2","rb"],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"bvadd","returnSort":["BitVec",32],"argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"r__2","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$bvadd","arguments":["E_term_1","E_term_2"],"argumentSorts":["E","E"],"returnSort":"E"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"E_term_0","sort":"E","index":0},"unclassified":[{"id":"r__0","sort":["BitVec",32],"index":1},{"id":"rv","sort":{"kind":"Array","params":["Int","Int"]},"index":2},{"id":"x","sort":["BitVec",32],"index":3},{"id":"y","sort":["BitVec",32],"index":4}],"auxiliary":[{"id":"r__1","sort":["BitVec",32],"index":null},{"id":"r__2","sort":["BitVec",32],"index":null},{"id":"rb","sort":{"kind":"Array","params":["Int","Int"]},"index":null}],"children":[{"id":"E_term_1","sort":"E","index":0},{"id":"E_term_2","sort":"E","index":1}]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$IBVVarx-4","head":{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_0","r__0","rv","x","y"]},"bodyRelations":[],"inputVariables":null,"outputVariables":null,"variables":["E_term_0","r__0","rv","x","y","r__1"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__0","sort":["BitVec",32],"$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"r__1","sort":["BitVec",32],"$termType":"variable"},{"name":"x","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$IBVVarx","arguments":[],"argumentSorts":[],"returnSort":"E"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"E_term_0","sort":"E","index":0},"unclassified":[{"id":"r__0","sort":["BitVec",32],"index":1},{"id":"rv","sort":{"kind":"Array","params":["Int","Int"]},"index":2},{"id":"x","sort":["BitVec",32],"index":3},{"id":"y","sort":["BitVec",32],"index":4}],"auxiliary":[{"id":"r__1","sort":["BitVec",32],"index":null}],"children":[]},"$event":"chc","$type":"semgus"}, +{"id":"_CHC-$bv=x-5","head":{"name":"Start.Sem","signature":["Start",["BitVec",32],["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["Start_term_0","x_r0","y_r0","rq","x","y"]},"bodyRelations":[{"name":"E.Sem","signature":["E",["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":["E_term_1","r__1","rb","x","y"]}],"inputVariables":null,"outputVariables":null,"variables":["Start_term_0","x_r0","y_r0","rq","x","y","r__1","rb"],"constraint":{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"x_r0","sort":["BitVec",32],"$termType":"variable"},{"name":"r__1","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},{"name":"and","returnSort":"Bool","argumentSorts":["Bool","Bool"],"arguments":[{"name":"=","returnSort":"Bool","argumentSorts":[{"kind":"Array","params":["Int","Int"]},{"kind":"Array","params":["Int","Int"]}],"arguments":[{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"rb","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"}],"$termType":"application"},{"name":"=","returnSort":"Bool","argumentSorts":[["BitVec",32],["BitVec",32]],"arguments":[{"name":"y","sort":["BitVec",32],"$termType":"variable"},{"name":"y_r0","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"}],"$termType":"application"}],"$termType":"application"},"constructor":{"name":"$bv=x","arguments":["E_term_1"],"argumentSorts":["E"],"returnSort":"Start"},"symbols":{"inputs":[],"outputs":[],"term":{"id":"Start_term_0","sort":"Start","index":0},"unclassified":[{"id":"x_r0","sort":["BitVec",32],"index":1},{"id":"y_r0","sort":["BitVec",32],"index":2},{"id":"rq","sort":{"kind":"Array","params":["Int","Int"]},"index":3},{"id":"x","sort":["BitVec",32],"index":4},{"id":"y","sort":["BitVec",32],"index":5}],"auxiliary":[{"id":"r__1","sort":["BitVec",32],"index":null},{"id":"rb","sort":{"kind":"Array","params":["Int","Int"]},"index":null}],"children":[{"id":"E_term_1","sort":"E","index":0}]},"$event":"chc","$type":"semgus"}, +{"name":"BVtest_ADD_01","termType":"Start","grammar":{"nonTerminals":[{"name":"@Start__agtt","termType":"Start"},{"name":"@E__agtt","termType":"E"}],"productions":[{"instance":"@Start__agtt","operator":"$bv=x","occurrences":["@E__agtt"]},{"instance":"@E__agtt","operator":"$IBVVary","occurrences":[]},{"instance":"@E__agtt","operator":"$bvsub","occurrences":["@E__agtt","@E__agtt"]},{"instance":"@E__agtt","operator":"$bvadd","occurrences":["@E__agtt","@E__agtt"]},{"instance":"@E__agtt","operator":"$IBVVarx","occurrences":[]}]},"$event":"synth-fun","$type":"semgus"}, +{"constraint":{"bindings":[{"name":"rq","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"child":{"name":"Start.Sem","returnSort":"Bool","argumentSorts":["Start",["BitVec",32],["BitVec",32],{"kind":"Array","params":["Int","Int"]},["BitVec",32],["BitVec",32]],"arguments":[{"name":"BVtest_ADD_01","returnSort":"Start","argumentSorts":[],"arguments":[],"$termType":"application"},{"size":32,"value":"0x0004","$termType":"bitvector"},{"size":32,"value":"0x0004","$termType":"bitvector"},{"name":"rq","sort":{"kind":"Array","params":["Int","Int"]},"$termType":"variable"},{"size":32,"value":"0x0003","$termType":"bitvector"},{"name":"y","sort":["BitVec",32],"$termType":"variable"}],"$termType":"application"},"$termType":"exists"},"$event":"constraint","$type":"semgus"}, +{"$event":"check-synth","$type":"semgus"}, +{"$type":"meta","$event":"end-of-stream"} +] diff --git a/README.md b/README.md index 4040c77..f5d9fdf 100644 --- a/README.md +++ b/README.md @@ -31,6 +31,7 @@ This project is under active development and does not yet support all SMT-LIB2 f * Strings (with partial support for regular expressions) * Bit vectors (partial support; only theory functions supported for now) * Datatypes (non-parametric only) +* Arrays (partial support) Other features: * Converting SyGuS problems to CHCs on the fly (beta) @@ -42,14 +43,12 @@ New additions: * Arbitrary `match` expressions Unsupported SMT-LIB2 features include: -* Parametric sorts * Theory functions annotated with `:left-assoc`, `:right-assoc`, `:chainable`, and `:pairwise`. Certain Core functions are implemented, so post an issue if others are needed. * Some terms, including `let` * Uninterpreted sorts (`declare-sort`) and sort aliases (`define-sort`) The roadmap for next-up features includes: * Arbitrary `let` terms -* Parameteric sorts If there is an unsupported feature that you would like added, drop us a line by submitting an issue (or commenting on an existing one). This will help us prioritize what to put on our roadmap. diff --git a/Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs b/Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs index 2a27453..30bd3c7 100644 --- a/Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs +++ b/Semgus-Lib/Model/Smt/SmtCommonIdentifiers.cs @@ -16,6 +16,7 @@ public static class SmtCommonIdentifiers public static SmtIdentifier StringsTheoryId { get; } = new("Strings"); public static SmtIdentifier BitVectorsTheoryId { get; } = new("BitVectors"); public static SmtIdentifier BitVectorsExtensionId { get; } = new("BitVectors", "extension"); + public static SmtIdentifier ArraysExTheoryId { get; } = new("ArraysEx"); public static SmtSortIdentifier BoolSortId { get; } = new("Bool"); public static SmtSortIdentifier IntSortId { get; } = new("Int"); @@ -32,6 +33,7 @@ public SmtSortIdentifier this[int size] new SmtIdentifier.Index(size))); } } + public static SmtIdentifier ArraySortPrimaryId { get; } = new("Array"); public static SmtIdentifier AndFunctionId { get; } = new("and"); public static SmtIdentifier OrFunctionId { get; } = new("or"); diff --git a/Semgus-Lib/Model/Smt/SmtContext.cs b/Semgus-Lib/Model/Smt/SmtContext.cs index 192ca57..ac52a97 100644 --- a/Semgus-Lib/Model/Smt/SmtContext.cs +++ b/Semgus-Lib/Model/Smt/SmtContext.cs @@ -64,7 +64,8 @@ public SmtContext() SmtCoreTheory.Instance, SmtIntsTheory.Instance, SmtStringsTheory.Instance, - SmtBitVectorsTheory.Instance + SmtBitVectorsTheory.Instance, + SmtArraysExTheory.Instance }; _extensions = new HashSet() @@ -249,7 +250,7 @@ private bool TryResolveSortParameters(SmtSortIdentifier id, SmtSort candidate, [ return false; } - if (candidate.Arity == 0) + if (candidate.Arity == 0 || !candidate.IsParametric) { resolved = candidate; error = default; @@ -266,13 +267,16 @@ private bool TryResolveSortParameters(SmtSortIdentifier id, SmtSort candidate, [ else { resolved = default; + error = $"Unable to resolve sort parameter {child.Name} in parametric sort {id.Name}: {error}"; return false; } } - resolved = default; - error = "Not finished being implemented"; - return false; + candidate.UpdateForResolvedParameters(resolvedSubsorts); + + resolved = candidate; + error = ""; + return true; } public void Push() diff --git a/Semgus-Lib/Model/Smt/SmtSort.cs b/Semgus-Lib/Model/Smt/SmtSort.cs index ee0085b..6b76c47 100644 --- a/Semgus-Lib/Model/Smt/SmtSort.cs +++ b/Semgus-Lib/Model/Smt/SmtSort.cs @@ -27,7 +27,7 @@ public SmtSort(SmtSortIdentifier name) public SmtSortIdentifier Name { get; } /// - /// Does this sort have parameters? + /// Does this sort have parameters that need to be resolved? /// public bool IsParametric { get; protected set; } = false; @@ -41,6 +41,12 @@ public SmtSort(SmtSortIdentifier name) /// public int Arity { get; protected set; } = 0; + /// + /// Updates this sort for resolved parameters + /// + /// Resolved parameters. Should have same length as arity + public virtual void UpdateForResolvedParameters(IList resolved) { } + /// /// An arbitrary generic sort /// @@ -54,6 +60,28 @@ public GenericSort(SmtSortIdentifier name) : base(name) { } } + /// + /// A sort parameter that needs to be resolved to a real sort + /// + internal class UnresolvedParameterSort : SmtSort + { + /// + /// Identifier that needs to be resolved + /// + public SmtSortIdentifier Identifier { get; } + + /// + /// Creates a new unresolved sort. This is a placeholder for sort parameters to be resolved. + /// + /// Sort identifier to resolve + public UnresolvedParameterSort(SmtSortIdentifier identifier) : base(identifier) + { + Identifier = identifier; + IsSortParameter = true; + Arity = identifier.Arity; + } + } + /// /// A sort containing wildcard parameters. Useful in rank templates. /// Indices in the sort name may be '*', which will match anything. diff --git a/Semgus-Lib/Model/Smt/Theories/SmtArraysExTheory.cs b/Semgus-Lib/Model/Smt/Theories/SmtArraysExTheory.cs new file mode 100644 index 0000000..9b8d401 --- /dev/null +++ b/Semgus-Lib/Model/Smt/Theories/SmtArraysExTheory.cs @@ -0,0 +1,156 @@ +using Semgus.Model.Smt.Terms; + +using System; +using System.Collections.Generic; +using System.Diagnostics.CodeAnalysis; +using System.Linq; +using System.Text; +using System.Threading.Tasks; + +using static Semgus.Model.Smt.SmtCommonIdentifiers; + +namespace Semgus.Model.Smt.Theories +{ + /// + /// The theory of arrays with extensions + /// + internal class SmtArraysExTheory : ISmtTheory + { + /// + /// A singleton theory instance + /// + public static SmtArraysExTheory Instance { get; } = new(); + + /// + /// Underlying array sort + /// + internal sealed class ArraySort : SmtSort + { + /// + /// Cache of instantiated sorts. We need this since sorts are compared by reference + /// + private static readonly IDictionary<(SmtSortIdentifier, SmtSortIdentifier), ArraySort> _sortCache + = new Dictionary<(SmtSortIdentifier, SmtSortIdentifier), ArraySort>(); + + /// + /// The sort used for indexing the array + /// + public SmtSort IndexSort { get; private set; } + + /// + /// The sort used for the array element values + /// + public SmtSort ValueSort { get; private set; } + + /// + /// Constructs a new array sort with the given parameters + /// + /// Size of bit vectors in this sort + private ArraySort(SmtSortIdentifier indexSort, SmtSortIdentifier valueSort) : + base(new(new SmtIdentifier(ArraySortPrimaryId.Symbol), indexSort, valueSort)) + { + IndexSort = new UnresolvedParameterSort(indexSort); + ValueSort = new UnresolvedParameterSort(valueSort); + IsParametric = true; + Arity = 2; + } + + /// + /// Gets the array sort for the given index and value sorts + /// + /// The index sort to use + /// The value sort to use + /// The array sort for the given index and value sorts + public static ArraySort GetSort(SmtSortIdentifier index, SmtSortIdentifier value) + { + if (_sortCache.TryGetValue((index, value), out ArraySort? sort)) + { + return sort; + } + else + { + sort = new ArraySort(index, value); + _sortCache.Add((index, value), sort); + return sort; + } + } + + /// + /// Updates this sort with the resolved parameteric sorts + /// + /// Resolved parameters. Must have arity 2 + public override void UpdateForResolvedParameters(IList resolved) + { + if (resolved.Count != 2) + { + throw new InvalidOperationException("Got list of resolved sorts not of length 2!"); + } + + IndexSort = resolved[0]; + ValueSort = resolved[1]; + } + } + + /// + /// This theory's name + /// + public SmtIdentifier Name { get; } = ArraysExTheoryId; + + #region Deprecated + public IReadOnlyDictionary Functions { get; } + #endregion + + /// + /// The primary (i.e., non-indexed) sort symbols (e.g., "Array") + /// + public IReadOnlySet PrimarySortSymbols { get; } + + /// + /// The primary (i.e., non-indexed) function symbols + /// + public IReadOnlySet PrimaryFunctionSymbols { get; } + + /// + /// Constructs an instance of the theory of arrays + /// + /// Reference to the core theory + private SmtArraysExTheory() + { + SmtSourceBuilder sb = new(this); + sb.AddOnTheFlyFn("select"); + sb.AddOnTheFlyFn("store"); + + Functions = sb.Functions; + PrimaryFunctionSymbols = sb.PrimaryFunctionSymbols; + PrimarySortSymbols = new HashSet() { ArraySortPrimaryId }; + } + + /// + /// Looks up a sort symbol in this theory + /// + /// The sort ID + /// The resolved sort + /// True if successfully gotten + public bool TryGetSort(SmtSortIdentifier sortId, [NotNullWhen(true)] out SmtSort? resolvedSort) + { + if (sortId.Arity == 2 && sortId.Name == ArraySortPrimaryId) + { + resolvedSort = ArraySort.GetSort(sortId.Parameters[0], sortId.Parameters[1]); + return true; + } + resolvedSort = default; + return false; + } + + /// + /// Looks up a function in this theory + /// + /// The function ID to look up + /// The resolved function + /// True if successfully gotten + public bool TryGetFunction(SmtIdentifier functionId, [NotNullWhen(true)] out IApplicable? resolvedFunction) + { + return Functions.TryGetValue(functionId, out resolvedFunction); + } + } +} diff --git a/SemgusParser/Json/Converters/SmtSortIdentifierConverter.cs b/SemgusParser/Json/Converters/SmtSortIdentifierConverter.cs index 2691539..e2861ad 100644 --- a/SemgusParser/Json/Converters/SmtSortIdentifierConverter.cs +++ b/SemgusParser/Json/Converters/SmtSortIdentifierConverter.cs @@ -31,7 +31,17 @@ public override void WriteJson(JsonWriter writer, object? value, JsonSerializer if (id.Parameters.Length > 0) { - throw new InvalidOperationException("Parameterized sorts not yet supported by the JSON serializer."); + writer.WriteStartObject(); + writer.WritePropertyName("kind"); + serializer.Serialize(writer, id.Name); + writer.WritePropertyName("params"); + writer.WriteStartArray(); + foreach (var sort in id.Parameters) + { + serializer.Serialize(writer, sort); + } + writer.WriteEndArray(); + writer.WriteEndObject(); } else {