diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/smtlib2/smtlib2_genConstr.ml | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/smtlib2/smtlib2_genConstr.ml')
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml | 18 |
1 files changed, 9 insertions, 9 deletions
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 |