Add handling (just skip) for ! in forall

[moratorium08]

I modified the parser so that it can handle !.

Detail

In order to handle smt2 files preprocessed by z3, we have to handle annotations specified by !.
Annotations are used for specifying additional information such as :weight 0, and in a semantical sense, we can just ignore them (as specified in Section 3.6.5, The SMT-LIB Standard: Version 2.6).

One example that contains ! is as follows (generated by z3)

(declare-fun id (Bool Bool Bool Int Int) Bool)
(assert (forall ((A Int) (B Int)) (! (id true true true A B) :weight 0)))
(assert (forall ((A Int) (B Int)) (! (id false true true A B) :weight 0)))
(assert (forall ((A Int) (B Int)) (! (id false false false A B) :weight 0)))
(assert (forall ((A Int)
                 (B Int)
                 (C Int)
                 (D Bool)
                 (E Int)
                 (F Bool)
                 (G Bool)
                 (H Int)
                 (I Int)
                 (J Int))
          (! (let ((a!1 (and (id D false false A B)
                             (or (not F) (= H 0) (not G))
                             (or (not F) (= J 0) (not G))
                             (or (not F) (not G) (= I H))
                             (or (not D) (= C (+ 1 B)))
                             (or (not D) (= E C))
                             (or (not D) (= A (+ (- 1) J)))
                             (or (not D) (= I E))
                             (or (not D) (and F D))
                             (or D (and F G))
                             (or F (not G))
                             (or (not F) (not D) (not (= J 0))))))
               (=> a!1 (id true false false J I)))
             :weight 0)))
(assert (forall ((A Int)) (! (=> (id true false false A 1000) false) :weight 0)))
(check-sat)

[KenSakayori]

Merged on behalf of @moratorium08