From 607c758e0220d8ba91eaf0e9e96b5ea71c5c6fd2 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 2 Mar 2016 13:38:21 +0100 Subject: Separate verit input (smtlib2) from output --- src/smtlib2/smtlib2_genConstr.ml | 226 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 226 insertions(+) create mode 100644 src/smtlib2/smtlib2_genConstr.ml (limited to 'src/smtlib2/smtlib2_genConstr.ml') diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml new file mode 100644 index 0000000..f11d650 --- /dev/null +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -0,0 +1,226 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +open Smtlib2_ast +open SmtAtom +open SmtForm +open SmtMisc +open CoqTerms + + +(* For debugging *) + +let pp_symbol s = + let pp_position p = "{pos_fname = "^p.Lexing.pos_fname^"; pos_lnum = "^(string_of_int p.Lexing.pos_lnum)^"; pos_bol = "^(string_of_int p.Lexing.pos_bol)^"; pos_cnum = "^(string_of_int p.Lexing.pos_cnum)^"}" in + + let pp_loc (p1,p2) = "("^(pp_position p1)^", "^(pp_position p2)^")" in + + match s with + | Symbol (l,s) -> "Symbol ("^(pp_loc l)^", "^s^")" + | SymbolWithOr (l,s) -> "SymbolWithOr ("^(pp_loc l)^", "^s^")" + + +(* Main functions *) + +let string_of_symbol = function | Symbol (_,s) | SymbolWithOr (_,s) -> s + + +let identifier_of_qualidentifier = function + | QualIdentifierId (_,id) | QualIdentifierAs (_,id,_) -> id + + +let string_type s = match s with + | "Bool" -> Tbool + | "Int" -> TZ + | _ -> VeritSyntax.get_btype s + + +let sort_of_string s = (string_type s, []) + + +let sort_of_symbol s = sort_of_string (string_of_symbol s) + + +let string_of_identifier = function + | IdSymbol (_,s) -> (string_of_symbol s) + | IdUnderscoreSymNum (_,s,(_,l)) -> + List.fold_left (fun c c' -> c^"_"^c') (string_of_symbol s) l + + +let string_of_qualidentifier id = string_of_identifier (identifier_of_qualidentifier id) + + +let rec sort_of_sort = function + | SortIdentifier (_,id) -> sort_of_string (string_of_identifier id) + | SortIdSortMulti (_,id,(_,l)) -> + (string_type (string_of_identifier id), List.map sort_of_sort l) + + +let declare_sort rt sym = + let s = string_of_symbol sym in + let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in + let eq_t = declare_new_variable (Names.id_of_string ("eq_"^s)) (Term.mkArrow cons_t (Term.mkArrow cons_t (Lazy.force cbool))) in + let x = mkName "x" in + let y = mkName "y" in + let rx = Term.mkRel 2 in + let ry = Term.mkRel 1 in + let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in + let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in + let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in + let res = Btype.declare rt cons_t ce in + VeritSyntax.add_btype s res; + res + + +let declare_fun rt ro sym arg cod = + let s = string_of_symbol sym in + let tyl = List.map sort_of_sort arg in + let ty = sort_of_sort cod in + + let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.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 + VeritSyntax.add_fun s op; + op + + +let make_root_specconstant ra = function + | SpecConstsDec _ -> failwith "Smtlib2_genConstr.make_root_specconstant: decimals not implemented yet" + | SpecConstNum (_,s) -> + (try + let i = int_of_string s in + Atom.hatom_Z_of_int ra i + with + | Failure _ -> + let i = Big_int.big_int_of_string s in + Atom.hatom_Z_of_bigint ra i) + | SpecConstString _ -> failwith "Smtlib2_genConstr.make_root_specconstant: strings not implemented yet" + | SpecConstsHex _ -> failwith "Smtlib2_genConstr.make_root_specconstant: hexadecimals not implemented yet" + | SpecConstsBinary _ -> failwith "Smtlib2_genConstr.make_root_specconstant: binaries not implemented yet" + + +type atom_form = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t + + +let make_root ra rf t = + + let hlets = Hashtbl.create 17 in + + let rec make_root_term = function + | TermSpecConst (_,c) -> Atom (make_root_specconstant ra c) + | TermQualIdentifier (_,id) -> + let v = string_of_qualidentifier id in + (try Hashtbl.find hlets v with + | Not_found -> + make_root_app v []) + | TermQualIdTerm (_,id,(_,l)) -> + let v = string_of_qualidentifier id in + make_root_app v l + | TermLetTerm (_,(_,l),t) -> + List.iter (fun (VarBindingSymTerm (_, sym, u)) -> + let u' = make_root_term u in + let s' = string_of_symbol sym in + Hashtbl.add hlets s' u') l; + make_root_term t + | TermForAllTerm _ -> failwith "Smtlib2_genConstr.make_root_term: ForAll not implemented yet" + | TermExistsTerm _ -> failwith "Smtlib2_genConstr.make_root_term: Exists not implemented yet" + | TermExclimationPt (_,t,_) -> make_root_term t + + and make_root_app v l = + match (v,l) with + | "=", [a;b] -> + (match make_root_term a, make_root_term b with + | 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')) + | _, _ -> 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') + | _, _ -> 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') + | _, _ -> 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') + | _, _ -> 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') + | _, _ -> 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') + | _, _ -> 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') + | _, _ -> 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') + | _, _ -> assert false) + | "-", [a] -> + (match make_root_term a with + | Atom a' -> Atom (Atom.mk_opp ra a') + | _ -> assert false) + | "distinct", _ -> + let make_h h = + match make_root_term h with + | Atom h' -> h' + | _ -> assert false in + let a = Array.make (List.length l) (make_h (List.hd l)) in + let i = ref (-1) in + List.iter (fun h -> + incr i; + a.(!i) <- make_h h) l; + Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a) + | "true", _ -> Form (Form.get rf Form.pform_true) + | "false", _ -> Form (Form.get rf Form.pform_false) + | "and", _ -> + Form (Form.get rf (Fapp (Fand, Array.of_list (List.map make_root l)))) + | "or", _ -> + Form (Form.get rf (Fapp (For, Array.of_list (List.map make_root l)))) + | "xor", _ -> + Form (Form.get rf (Fapp (Fxor, Array.of_list (List.map make_root l)))) + | "=>", _ -> + Form (Form.get rf (Fapp (Fimp, Array.of_list (List.map make_root l)))) + | "ite", _ -> + Form (Form.get rf (Fapp (Fite, Array.of_list (List.map make_root l)))) + | "not", [a] -> Form (Form.neg (make_root a)) + | _, _ -> + let op = VeritSyntax.get_fun v in + let l' = List.map (fun t -> match make_root_term t with + | Atom h -> h | Form _ -> assert false) l in + Atom (Atom.get ra (Aapp (op, Array.of_list l'))) + + and make_root t = + match make_root_term t with + | Atom h -> Form.get rf (Fatom h) + | Form f -> f in + + make_root t + + +let declare_commands rt ro ra rf acc = function + | CDeclareSort (_,sym,_) -> let _ = declare_sort rt sym in acc + | CDeclareFun (_,sym, (_, arg), cod) -> + let _ = declare_fun rt ro sym arg cod in acc + | CAssert (_, t) -> (make_root ra rf t)::acc + | _ -> acc -- cgit