diff options
Diffstat (limited to 'src/verit/veritParser.mly')
| -rw-r--r-- | src/verit/veritParser.mly | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly index 08c5cb3..c46b7c3 100644 --- a/src/verit/veritParser.mly +++ b/src/verit/veritParser.mly @@ -272,7 +272,7 @@ term: /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean i | VAR args { let f = $1 in let a = $2 in match find_opt_qvar f with | Some bt -> let op = dummy_indexed_op (Rel_name f) [||] bt in false, Form.Atom (Atom.get ~declare:false ra (Aapp (op, Array.of_list (snd (list_dec a))))) | None -> let dl, l = list_dec $2 in dl, Form.Atom (Atom.get ra ~declare:dl (Aapp (SmtMaps.get_fun f, Array.of_list l))) } /* Both */ - | EQ name_term name_term { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Form.Atom h1), (decl2, Form.Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Form.Atom (Atom.mk_eq ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); Form.lit_of_atom_form_lit rf (decl2, t2)|])) } + | EQ name_term name_term { let t1 = $2 in let t2 = $3 in match t1,t2 with | (decl1, Form.Atom h1), (decl2, Form.Atom h2) when (match Atom.type_of h1 with | SmtBtype.Tbool -> false | _ -> true) -> let decl = decl1 && decl2 in decl, Form.Atom (Atom.mk_eq_sym ra ~declare:decl (Atom.type_of h1) h1 h2) | (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); Form.lit_of_atom_form_lit rf (decl2, t2)|])) } | EQ nlit lit { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|t1; t2|])) } | EQ name_term nlit { match $2, $3 with (decl1, t1), (decl2, t2) -> decl1 && decl2, Form.Form (Fapp (Fiff, [|Form.lit_of_atom_form_lit rf (decl1, t1); t2|])) } | LET LPAR bindlist RPAR name_term { $3; $5 } |