SyGuS language 2.0 support

[adaminsky]

• Removes declare_primed_var, and declare_fun.
• Negative constants must now be written with unary negation: -1 is (- 1).
• let terms are written in the SMT-LIB compliant way.

[SaswatPadhi]

I left a few more comments, but I think this PR is almost ready to be merged.

I think you should run the SyGuS 2.0 files that I sent and make sure we still pass those benchmarks.

[adaminsky]

I ran it against the SyGuS 2.0 files and it passes all of them except for 2 which don't finish running. For some reason the bash script says "unknown flag -t" and doesn't let me set a time limit.

[SaswatPadhi]

Great, thanks! I am not sure about the "-t" issue -- I'll try it locally and let you know.

This PR is ready to merge, but I will merge it after #11 since that's a much larger PR and would need some changes to benchmarks if this is merged first.

[Kakadu]

Does this pull request supports whole SyGuS language 2.0?
It tried to run example 2 from the spec but got an parsing error

$ ./loopinvgen.sh ~/syn1.sygus                           
Uncaught exception:          
  
  LoopInvGen.Exceptions.Parse_Exn("Unknown command: (declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))")

The contents of syn1.sygus:

(set-logic  DTLIA)
(declare-datatypes ((List  0)) ((( nil) (cons (head  Int) (tail  List )))))
(synth-fun f ((x List)) Int
  ((I Int) (L List) (B Bool))
  ((I Int (0 1
           (head L)
           (+ I I)
           (ite B I I)))
   (L List (nil x (cons I L) (tail L)))
   (B Bool  (((_ is nil) L)
             ((_ is cons) L)
             (= I I)
             (>= I I)))))

(constraint  (= (f (cons 4 nil)) 5))
(constraint  (= (f (cons 0 nil)) 1))
(constraint  (= (f nil) 0))
(check-synth)

[SaswatPadhi]

Hello @Kakadu,

No, LoopInvGen currently does not support user-defined data types.

It fully supports Boolean and integer data types, provides minimal support for arrays (we are working on extending it) and we are currently adding bitvector support (PR #13). There is an old branch that adds support for string type, but it's stalled because of parsing issues with Jane streets sexpression library.