Sequence functions (mostly tested)

IntegrationTests/data/sequences.sem

@@ -0,0 +1,22 @@
+(declare-term-types
+ ((Start 0))
+ ((($main))))
+
+(define-funs-rec
+    ((Start.Sem ((Start_term_0 Start) (rq (Seq Int)) (x (_ BitVec 32))) Bool))
+
+    ((match Start_term_0
+            ((($main)
+              (exists ((rb (Seq String)) (ra (Seq String)))
+                      (and (= "Test" (seq.nth rb 7))
+                           (= rb (seq.++ ra (seq.unit "a")))
+                           (= rb (as seq.empty (Seq String)))
+                           (= rq (seq.rev rq)))))))))
+
+
+(synth-fun MyFunc () Start)
+
+
+(constraint (exists ((rq (Seq Int)) (y (_ BitVec 32))) (Start.Sem MyFunc rq y)))
+
+(check-synth)

IntegrationTests/tests/test-json-sequences.rsp

@@ -0,0 +1,6 @@
+--format
+json
+--mode
+batch
+--
+data/sequences.sem

IntegrationTests/tests/test-json-sequences.txt

@@ -0,0 +1,11 @@
+[
+{"name":"Start","$event":"declare-term-type","$type":"semgus"},
+{"name":"Start","constructors":[{"name":"$main","children":[]}],"$event":"define-term-type","$type":"semgus"},
+{"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":"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"},
+{"$type":"meta","$event":"end-of-stream"}
+]

IntegrationTests/tests/test-sexpr-sequences.rsp

@@ -0,0 +1,4 @@
+--format
+sexpr
+--
+data/sequences.sem

IntegrationTests/tests/test-sexpr-sequences.txt

@@ -0,0 +1,9 @@
+
+(declare-term-types (sort (identifier "Start"))) 
+(add-constructor (sort (identifier "Start")) :operator (identifier "$main") :children (list)) 
+(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")))) 
+(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)

Semgus-Lib/Model/Smt/Theories/SmtSequencesTheory.cs

@@ -20,7 +20,7 @@ internal class SmtSequencesTheory : ISmtTheory
         /// <summary>
         /// A singleton theory instance
         /// </summary>
-        public static SmtSequencesTheory Instance { get; } = new();
+        public static SmtSequencesTheory Instance { get; } = new(SmtCoreTheory.Instance, SmtIntsTheory.Instance);
 
         /// <summary>
         /// Underlying sequence sort
@@ -127,12 +127,30 @@ public override void UpdateForResolvedParameters(IList<SmtSort> resolved)
         /// Constructs an instance of the theory of sequences
         /// </summary>
         /// <param name="core">Reference to the core theory</param>
-        private SmtSequencesTheory()
+        private SmtSequencesTheory(SmtCoreTheory core, SmtIntsTheory ints)
         {
+            SmtSort b = core.Sorts[BoolSortId.Name];
+            SmtSort i = ints.Sorts[IntSortId.Name];
+
             SmtSourceBuilder sb = new(this);
             var usf = new SmtSort.UniqueSortFactory();
             var elementSort = usf.Next();
             var seqSort = new SeqSort(elementSort);
+            sb.AddFn("seq.empty", seqSort);
+            sb.AddFn("seq.unit", seqSort, elementSort);
+            sb.AddFn("seq.len", i, seqSort);
+            sb.AddFn("seq.nth", elementSort, seqSort, i);
+            sb.AddFn("seq.update", seqSort, seqSort, i, seqSort);
+            sb.AddFn("seq.extract", seqSort, seqSort, i, i);
+            sb.AddFn("seq.++", seqSort, seqSort, seqSort);
+            sb.AddFn("seq.at", seqSort, seqSort, i);
+            sb.AddFn("seq.contains", b, seqSort, seqSort);
+            sb.AddFn("seq.indexof", i, seqSort, seqSort, i);
+            sb.AddFn("seq.replace", seqSort, seqSort, seqSort, seqSort);
+            sb.AddFn("seq.replace_all", seqSort, seqSort, seqSort, seqSort);
+            sb.AddFn("seq.rev", seqSort, seqSort);
+            sb.AddFn("seq.prefixof", b, seqSort, seqSort);
+            sb.AddFn("seq.suffixof", b, seqSort, seqSort);
 
             Functions = sb.Functions;
             PrimaryFunctionSymbols = sb.PrimaryFunctionSymbols;