Quelle smtlib_interface.ML Sprache: SML

(*  Title:      HOL/Tools/SMT/smtlib_interface.ML
    Author:     Sascha Boehme, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen

Interface to SMT solvers based on the SMT-LIB 2 format.
*)

signature SMTLIB_INTERFACE =
sig
  val smtlibC: SMT_Util.class
  val hosmtlibC: SMT_Util.class
  val bvsmlibC: SMT_Util.class
  val realsmlibC: SMT_Util.class
  val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
  val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic

  type dtype_decls = (string * (string * (string * string) list) list) list
  type func_decl = string * (string list * string)
  val serialize: (BNF_Util.fp_kind * dtype_decls -> Buffer.T -> Buffer.T) -> (string * string) list -> string list ->
    {dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
     funcs: func_decl list, logic: string, sorts: string list} ->
    (SMT_Util.role * SMT_Translate.sterm) list -> string

  val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
  val assert_name_of_role_and_index: SMT_Util.role -> int -> string
  val role_and_index_of_assert_name: string -> SMT_Util.role * int
end;

structure SMTLIB_Interface: SMTLIB_INTERFACE =
struct

val hoC = ["ho"]

val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
val bvsmlibC = smtlibC @ ["BV"] (* if BV are supported *)
val realsmlibC = ["Real"]

(* builtins *)

local
  fun int_num _ i = SOME (string_of_int i)

  fun is_linear [t] = SMT_Util.is_number t
    | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
    | is_linear _ = false

  fun times _ _ ts =
    let val mk = Term.list_comb o pair \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>
    in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
in

val setup_builtins =
  SMT_Builtin.add_builtin_typ hosmtlibC
    (\<^typ>\<open>'a => 'b\<close>, fn Type (\<^type_name>\<open>fun\<close>, Ts) => SOME ("->", Ts), K (K NONE)) #>
  fold (SMT_Builtin.add_builtin_typ smtlibC) [
    (\<^typ>\<open>bool\<close>, K (SOME ("Bool", [])), K (K NONE)),
    (\<^typ>\<open>int\<close>, K (SOME ("Int", [])), int_num)] #>
  fold (SMT_Builtin.add_builtin_fun' smtlibC) [
    (\<^Const>\<open>True\<close>, "true"),
    (\<^Const>\<open>False\<close>, "false"),
    (\<^Const>\<open>Not\<close>, "not"),
    (\<^Const>\<open>conj\<close>, "and"),
    (\<^Const>\<open>disj\<close>, "or"),
    (\<^Const>\<open>implies\<close>, "=>"),
    (\<^Const>\<open>HOL.eq \<^typ>\<open>'a\\, "="),
    (\<^Const>\<open>If \<^typ>\<open>'a\\, "ite"),
    (\<^Const>\<open>less \<^Type>\<open>int\<close>\<close>, "<"),
    (\<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, "<="),
    (\<^Const>\<open>uminus \<^Type>\<open>int\<close>\<close>, "-"),
    (\<^Const>\<open>plus \<^Type>\<open>int\<close>\<close>, "+"),
    (\<^Const>\<open>minus \<^Type>\<open>int\<close>\<close>, "-")] #>
  SMT_Builtin.add_builtin_fun smtlibC
    (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, times)

end

(* serialization *)

(** logic **)

fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)

structure Logics = Generic_Data
(
  type T = (int * (string -> term list -> string option)) list
  val empty = []
  fun merge data = Ord_List.merge fst_int_ord data
)

fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
fun del_logic pf = Logics.map (Ord_List.remove fst_int_ord pf)

fun choose_logic ctxt prover ts =
  let
    fun choose [] = "AUFLIA"
      | choose ((_, f) :: fs) = (case f prover ts of SOME s => s | NONE => choose fs)
  in
    (case choose (Logics.get (Context.Proof ctxt)) of
      "" => "" (* for default Z3 logic, a subset of everything *)
    | logic => "(set-logic " ^ logic ^ ")\n")
  end

(** serialization **)

fun var i = "?v" ^ string_of_int i

fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
  | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
      SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
  | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
  | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
      SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
  | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
      let
        val l' = l + length ss

        fun quant_name SMT_Translate.SForall = "forall"
          | quant_name SMT_Translate.SExists = "exists"

        fun gen_trees_of_pat keyword ps =
          [SMTLIB.Key keyword, SMTLIB.S (map (tree_of_sterm l') ps)]
        fun trees_of_pat (SMT_Translate.SPat ps) = gen_trees_of_pat "pattern" ps
          | trees_of_pat (SMT_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps
        fun tree_of_pats [] t = t
          | tree_of_pats pats t = SMTLIB.S (SMTLIB.Sym "!" :: t :: maps trees_of_pat pats)

        val vs = map_index (fn (i, ty) =>
          SMTLIB.S [SMTLIB.Sym (var (l + i)), SMTLIB.Sym ty]) ss

        val body = t
          |> tree_of_sterm l'
          |> tree_of_pats pats
      in
        SMTLIB.S [SMTLIB.Sym (quant_name q), SMTLIB.S vs, body]
      end

fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
fun sctr (name, args) = enclose "(" ")" (implode_space (name :: map sctrarg args))
fun sdatatype (name, ctrs) = enclose "(" ")" (implode_space (name :: map sctr ctrs))

fun string_of_fun (f, (ss, s)) = f ^ " (" ^ implode_space ss ^ ") " ^ s

fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s]

val conjecture_prefix = "conjecture" (* FUDGE *)
val hypothesis_prefix = "hypothesis" (* FUDGE *)
val axiom_prefix = "a" (* matching Alethe's convention *)

fun assert_prefix_of_role SMT_Util.Conjecture = conjecture_prefix
  | assert_prefix_of_role SMT_Util.Hypothesis = hypothesis_prefix
  | assert_prefix_of_role SMT_Util.Axiom = axiom_prefix

fun assert_name_of_role_and_index role i = assert_prefix_of_role role ^ string_of_int i

fun unprefix_axiom s =
  try (pair SMT_Util.Conjecture o unprefix conjecture_prefix) s
  |> curry merge_options (try (pair SMT_Util.Hypothesis o unprefix hypothesis_prefix) s)
  |> curry merge_options (try (pair SMT_Util.Axiom o unprefix axiom_prefix) s)
  |> the

fun role_and_index_of_assert_name s =
  apsnd (the_default ~1 o Int.fromString) (unprefix_axiom s)

type dtype_decls = (string * (string * (string * string) list) list) list

fun sdtyp (fp, dtyps : dtype_decls) =
  Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
    (space_implode "\n " (map sdatatype dtyps)))

type func_decl = string * (string list * string)

fun serialize (sdtyp : BNF_Util.fp_kind * dtype_decls -> Buffer.T -> Buffer.T) smt_options comments
      {logic, sorts, dtyps, funcs} ts =
  let
    val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
  in
    Buffer.empty
    |> fold (Buffer.add o enclose "; " "\n") comments
    |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options
    |> Buffer.add logic
    |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
    |> fold sdtyp (AList.coalesce (op =) dtyps)
    |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
        (sort (fast_string_ord o apply2 fst) funcs)
    |> fold (fn (i, (role, t)) => Buffer.add (enclose "(assert " ")\n"
        (SMTLIB.str_of (named_sterm (assert_name_of_role_and_index role i) (tree_of_sterm 0 t)))))
        (map_index I ts)
    |> Buffer.add "(check-sat)\n"
    |> Buffer.add (if unsat_core then "(get-unsat-core)\n" else "(get-proof)\n")
    |> Buffer.content
  end

(* interface *)

fun translate_config order ctxt = {
  order = order,
  logic = choose_logic ctxt,
  fp_kinds = [],
  serialize = serialize sdtyp}

val _ = Theory.setup (Context.theory_map
  (setup_builtins #>
   SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
   SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))

end;

quality99%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.