diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-05-02 23:32:09 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-05-02 23:32:09 +0200 |
| commit | 7a17276943c42c7997389d4782e457f449bd102e (patch) | |
| tree | 433e1dd64dd2d685e8dcd9f85f42b7a5be80f667 /src/verit/veritParser.mly | |
| parent | d3f4ee8411a56f77ad47449be57e40c846b49cfd (diff) | |
| download | smtcoq-7a17276943c42c7997389d4782e457f449bd102e.tar.gz smtcoq-7a17276943c42c7997389d4782e457f449bd102e.zip | |
Correct parsing of <-> for veriT
Diffstat (limited to 'src/verit/veritParser.mly')
| -rw-r--r-- | src/verit/veritParser.mly | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly index 7bb4c8e..799c32d 100644 --- a/src/verit/veritParser.mly +++ b/src/verit/veritParser.mly @@ -181,6 +181,8 @@ term: /* returns a SmtAtom.Form.pform or a SmtAtom.hatom */ /* Both */ | EQ name_term name_term { let t1 = $2 in let t2 = $3 in match t1,t2 with | Atom h1, Atom h2 when (match Atom.type_of h1 with | Tbool -> false | _ -> true) -> Atom (Atom.mk_eq ra (Atom.type_of h1) h1 h2) | _, _ -> Form (Fapp (Fiff, [|lit_of_atom_form_lit rf t1; lit_of_atom_form_lit rf t2|])) } + /* This rule introduces lots of shift/reduce conflicts */ + | EQ lit lit { let t1 = $2 in let t2 = $3 in Form (Fapp (Fiff, [|t1; t2|])) } | LET LPAR bindlist RPAR name_term { $3; $5 } | BINDVAR { Hashtbl.find hlets $1 } ; |