Add Sequences as a new Suslik data type

[abhishekc-sharma]

Adding a new IntSequence type to SuSLik.

• Encoded to SMT using SMT Sequences
• Some SSL rules were explicitly modified to allow synthesis with operations besides append. (d185b4b)

[ilyasergey]

I didn't manage to get it past the parser phase:

./suslik src/test/resources/synthesis/sequences/llist/llist_insert_head.syn

resulted in

Synthesis failed:
Failed to parse the input:
[3.29] failure: '`;'' expected but `:' found

|  not (x == y)  => { s == v:s1 ; [x, 2] ** x :-> v ** (x + 1) :-> nxt ** lseg(nxt, y, s1) }

Please, supply the tests for features that work and mark those that don't as separate test files.

[abhishekc-sharma]

Whoops ! Sorry about that. Seems like some of the earlier test cases weren't updated after a minor syntax change. All the test cases under sequences should now either be marked or work.

[ilyasergey]

Thanks! Which are the tests (i.e., ScalaTest implementations) covering the examples from the sequences folder? I don't think they are in the suite.

[abhishekc-sharma]

Do you mean a file under src/test/scala/org/tygus/suslik/synthesis that runs those cases ? I always ended up testing it manually.. Although @aidandenlinger did generate the benchmark data for these sequence cases. Not sure if that required creating a test file in this directory. Either way will add in that file.

[nadia-polikarpova]

Also, in addition to making a Test file for all the sequence benchmarks, can you please put all the changes you made to BranchAbduction etc under a flag, so that we can still run other benchmarks like before? Thanks!

[abhishekc-sharma]

Sorry for the delayed response. I have added a --sequenceRules flag to enable the various changes made to the rules along with a test suite file that runs the sequence tests. Unfortunately I hadn't run the test suite in a long time and it seems like some of the existing benchmarks break even when the flag is disabled. I am trying to debug and fix these.