From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sat, 27 Oct 2018 20:08:44 +0200 Subject: Adding support for lemmas in the command verit --- src/smtlib2/smtlib2_genConstr.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'src/smtlib2/smtlib2_genConstr.ml') diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index 27ac8d3..76dde25 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -93,7 +93,7 @@ let declare_fun rt ro sym arg cod = let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in - let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in + let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) None in VeritSyntax.add_fun s op; op @@ -147,35 +147,35 @@ let make_root ra rf t = | Atom a', Atom b' -> (match Atom.type_of a' with | Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|]))) - | ty -> Atom (Atom.mk_eq ra ty a' b')) + | ty -> Atom (Atom.mk_eq ra true ty a' b')) | _, _ -> assert false) | "<", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_lt ra true a' b') | _, _ -> assert false) | "<=", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_le ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_le ra true a' b') | _, _ -> assert false) | ">", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_gt ra true a' b') | _, _ -> assert false) | ">=", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_ge ra true a' b') | _, _ -> assert false) | "+", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_plus ra true a' b') | _, _ -> assert false) | "-", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_minus ra true a' b') | _, _ -> assert false) | "*", [a;b] -> (match make_root_term a, make_root_term b with - | Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b') + | Atom a', Atom b' -> Atom (Atom.mk_mult ra true a' b') | _, _ -> assert false) | "-", [a] -> (match make_root_term a with -- cgit