diff options
author | ckeller <ckeller@users.noreply.github.com> | 2021-02-23 17:06:51 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-23 17:06:51 +0100 |
commit | 240b76807340e59bb85b35e3ebbb807792459912 (patch) | |
tree | 22d60d5c8db5034bdd9045e8579df14406ac69bc /src/verit/veritParser.mly | |
parent | 74558c622de91801e3e188bdf690eb9a665f965b (diff) | |
download | smtcoq-240b76807340e59bb85b35e3ebbb807792459912.tar.gz smtcoq-240b76807340e59bb85b35e3ebbb807792459912.zip |
Link equality on uninterpreted sorts with SMT equality (#86)
Equality is now treated from uninterpreted sorts, which makes them usable with tactics!
Closes #17
Closes #78
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 } |