From 240b76807340e59bb85b35e3ebbb807792459912 Mon Sep 17 00:00:00 2001 From: ckeller Date: Tue, 23 Feb 2021 17:06:51 +0100 Subject: 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 --- src/verit/veritSyntax.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/verit/veritSyntax.mli') diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli index 7a325a6..bd98ba6 100644 --- a/src/verit/veritSyntax.mli +++ b/src/verit/veritSyntax.mli @@ -52,8 +52,8 @@ val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCerti val ra : SmtAtom.Atom.reify_tbl val rf : SmtAtom.Form.reify -val ra' : SmtAtom.Atom.reify_tbl -val rf' : SmtAtom.Form.reify +val ra_quant : SmtAtom.Atom.reify_tbl +val rf_quant : SmtAtom.Form.reify val hlets : (string, Form.atom_form_lit) Hashtbl.t -- cgit