Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Tools/SMT/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 10 kB

Quelle cvc5_replay_methods.ML Sprache: SML

(*  Title:      HOL/Tools/SMT/cvc5_replay_methods.ML
    Author:     Mathias Fleury, JKU, Uni Freiburg
    Author:     Hanna Lachnitt, Stanford University

Proof method for replaying cvc5 proofs.
*)

signature CVC5_REPLAY_METHODS =
sig
  (*methods for verit proof rules*)
  val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table ->
     (string * term) list -> term -> thm

  val discharge: Proof.context -> thm list -> term -> thm
end;

structure CVC5_Replay_Methods: CVC5_REPLAY_METHODS =
struct

open Lethe_Replay_Methods

fun cvc5_rule_of "bind" = Bind
  | cvc5_rule_of "cong" = Cong
  | cvc5_rule_of "refl" = Refl
  | cvc5_rule_of "equiv1" = Equiv1
  | cvc5_rule_of "equiv2" = Equiv2
  | cvc5_rule_of "equiv_pos1" = Equiv_pos1
   (*Equiv_pos2 covered below*)
  | cvc5_rule_of "equiv_neg1" = Equiv_neg1
  | cvc5_rule_of "equiv_neg2" = Equiv_neg2
  | cvc5_rule_of "sko_forall" = Skolem_Forall
  | cvc5_rule_of "sko_ex" = Skolem_Ex
  | cvc5_rule_of "eq_reflexive" = Eq_Reflexive
  | cvc5_rule_of "forall_inst" = Forall_Inst
  | cvc5_rule_of "implies_pos" = Implies_Pos
  | cvc5_rule_of "or" = Or
  | cvc5_rule_of "not_or" = Not_Or
  | cvc5_rule_of "resolution" = Resolution
  | cvc5_rule_of "trans" = Trans
  | cvc5_rule_of "false" = False
  | cvc5_rule_of "ac_simp" = AC_Simp
  | cvc5_rule_of "and" = And
  | cvc5_rule_of "not_and" = Not_And
  | cvc5_rule_of "and_pos" = And_Pos
  | cvc5_rule_of "and_neg" = And_Neg
  | cvc5_rule_of "or_pos" = Or_Pos
  | cvc5_rule_of "or_neg" = Or_Neg
  | cvc5_rule_of "not_equiv1" = Not_Equiv1
  | cvc5_rule_of "not_equiv2" = Not_Equiv2
  | cvc5_rule_of "not_implies1" = Not_Implies1
  | cvc5_rule_of "not_implies2" = Not_Implies2
  | cvc5_rule_of "implies_neg1" = Implies_Neg1
  | cvc5_rule_of "implies_neg2" = Implies_Neg2
  | cvc5_rule_of "implies" = Implies
  | cvc5_rule_of "bfun_elim" = Bfun_Elim
  | cvc5_rule_of "ite1" = ITE1
  | cvc5_rule_of "ite2" = ITE2
  | cvc5_rule_of "not_ite1" = Not_ITE1
  | cvc5_rule_of "not_ite2" = Not_ITE2
  | cvc5_rule_of "ite_pos1" = ITE_Pos1
  | cvc5_rule_of "ite_pos2" = ITE_Pos2
  | cvc5_rule_of "ite_neg1" = ITE_Neg1
  | cvc5_rule_of "ite_neg2" = ITE_Neg2
  | cvc5_rule_of "la_disequality" = LA_Disequality
  | cvc5_rule_of "lia_generic" = LIA_Generic
  | cvc5_rule_of "la_generic" = LA_Generic
  | cvc5_rule_of "la_tautology" = LA_Tautology
  | cvc5_rule_of "la_totality" = LA_Totality
  | cvc5_rule_of "la_rw_eq"= LA_RW_Eq
  | cvc5_rule_of "nla_generic"= NLA_Generic
  | cvc5_rule_of "eq_transitive" = Eq_Transitive
  | cvc5_rule_of "qnt_rm_unused" = Qnt_Rm_Unused
  | cvc5_rule_of "onepoint" = Onepoint
  | cvc5_rule_of "qnt_join" = Qnt_Join
  | cvc5_rule_of "subproof" = Subproof
  | cvc5_rule_of "bool_simplify" = Bool_Simplify
  | cvc5_rule_of "or_simplify" = Or_Simplify
  | cvc5_rule_of "ite_simplify" = ITE_Simplify
  | cvc5_rule_of "and_simplify" = And_Simplify
  | cvc5_rule_of "not_simplify" = Not_Simplify
  | cvc5_rule_of "equiv_simplify" = Equiv_Simplify
  | cvc5_rule_of "eq_simplify" = Eq_Simplify
  | cvc5_rule_of "implies_simplify" = Implies_Simplify
  | cvc5_rule_of "connective_def" = Connective_Def
  | cvc5_rule_of "minus_simplify" = Minus_Simplify
  | cvc5_rule_of "sum_simplify" = Sum_Simplify
  | cvc5_rule_of "prod_simplify" = Prod_Simplify
  | cvc5_rule_of "comp_simplify" = Comp_Simplify
  | cvc5_rule_of "qnt_simplify" = Qnt_Simplify
  | cvc5_rule_of "tautology" = Tautological_Clause
  | cvc5_rule_of "qnt_cnf" = Qnt_CNF
  | cvc5_rule_of "symm" = Symm
  | cvc5_rule_of "not_symm" = Not_Symm
  | cvc5_rule_of "reordering" = Reordering
  | cvc5_rule_of "unary_minus_simplify" = Minus_Simplify
  | cvc5_rule_of "quantifier_simplify" = Tmp_Quantifier_Simplify (*TODO Remove*)
  | cvc5_rule_of r =
     if r = Lethe_Proof.normalized_input_rule then Normalized_Input
     else if r = Lethe_Proof.local_input_rule then Local_Input
     else if r = Lethe_Proof.lethe_def then Definition
     else if r = Lethe_Proof.not_not_rule then Not_Not
     else if r = Lethe_Proof.contract_rule orelse r = "duplicate_literals" then Duplicate_Literals
     else if r = Lethe_Proof.ite_intro_rule then ITE_Intro
     else if r = Lethe_Proof.eq_congruent_rule then Eq_Congruent
     else if r = Lethe_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
     else if r = Lethe_Proof.theory_resolution2_rule then Theory_Resolution2
     else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution
     else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2
     else if r = Lethe_Proof.hole orelse r = "undefined" then Hole
     else Other_Rule r

fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
let
    val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("normalized input t =",t))
    val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("normalized ipput prems =",prems))

in
  resolve_tac ctxt prems
    (*TODO: should only be used for lambda encoding*)
    ORELSE' Clasimp.force_tac ctxt
end)

fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
      K (Clasimp.auto_tac ctxt))

fun hole ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  K (print_tac ctxt "stuff")
    THEN' Method.insert_tac ctxt prems
    (*TODO: should only be used for lambda encoding*)
THEN' K (print_tac ctxt "stuff")
    THEN' Clasimp.force_tac ctxt
THEN' K (print_tac ctxt "stuff")
)

(*
Example:
lemma \<open>(\<forall>x y. P x = Q y) \<Longrightarrow> (\<forall> y z. Q y = R z) \<Longrightarrow> (\<forall>x z. P x = R z)\<close>
*)
fun trans ctxt prems t =
  SMT_Replay_Methods.prove ctxt t (fn _ =>
    Method.insert_tac ctxt prems
    THEN' (REPEAT_CHANGED (resolve_tac ctxt @{thms trans} THEN' assume_tac ctxt))
    THEN' (resolve_tac ctxt @{thms refl}))

(* Combining all together *)

fun unsupported rule ctxt thms _ _ _ = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule"
  rule thms

fun ignore_args  f ctxt thm _    _     _ t = f ctxt thm t
fun ignore_decls f ctxt thm args insts _ t = f ctxt thm args insts t
fun ignore_insts f ctxt thm args  _    _ t = f ctxt thm args t

fun choose _ And = ignore_args and_rule
  | choose _ And_Neg = ignore_args and_neg_rule
  | choose _ And_Pos = ignore_args and_pos
  | choose _ And_Simplify = ignore_args rewrite_and_simplify
  | choose _ Bind = ignore_insts bind
  | choose _ Bool_Simplify = ignore_args rewrite_bool_simplify
  | choose _ Comp_Simplify = ignore_args rewrite_comp_simplify
  | choose _ Cong = ignore_args (cong "cvc5")
  | choose _ Connective_Def = ignore_args rewrite_connective_def
  | choose _ Duplicate_Literals = ignore_args duplicate_literals
  | choose _ Eq_Congruent = ignore_args eq_congruent
  | choose _ Eq_Congruent_Pred = ignore_args eq_congruent_pred
  | choose _ Eq_Reflexive = ignore_args eq_reflexive
  | choose _ Eq_Simplify = ignore_args rewrite_eq_simplify
  | choose _ Eq_Transitive = ignore_args eq_transitive
  | choose _ Equiv1 = ignore_args equiv1
  | choose _ Equiv2 = ignore_args equiv2
  | choose _ Equiv_neg1 = ignore_args equiv_neg1
  | choose _ Equiv_neg2 = ignore_args equiv_neg2
  | choose _ Equiv_pos1 = ignore_args equiv_pos1
  | choose _ Equiv_pos2 = ignore_args equiv_pos2
  | choose _ Equiv_Simplify = ignore_args rewrite_equiv_simplify
  | choose _ False = ignore_args false_rule
  | choose _ Forall_Inst = ignore_decls forall_inst
  | choose _ Implies = ignore_args implies_rules
  | choose _ Implies_Neg1 = ignore_args implies_neg1
  | choose _ Implies_Neg2 = ignore_args implies_neg2
  | choose _ Implies_Pos = ignore_args implies_pos
  | choose _ Implies_Simplify = ignore_args rewrite_implies_simplify
  | choose _ ITE1 = ignore_args ite1
  | choose _ ITE2 = ignore_args ite2
  | choose _ ITE_Intro = ignore_args ite_intro
  | choose _ ITE_Neg1 = ignore_args ite_neg1
  | choose _ ITE_Neg2 = ignore_args ite_neg2
  | choose _ ITE_Pos1 = ignore_args ite_pos1
  | choose _ ITE_Pos2 = ignore_args ite_pos2
  | choose _ ITE_Simplify = ignore_args rewrite_ite_simplify
  | choose _ LA_Disequality = ignore_args la_disequality
  | choose _ LA_Generic = ignore_insts la_generic
  | choose _ LA_RW_Eq = ignore_args la_rw_eq
  | choose _ LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
  | choose _ LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
  | choose _ LIA_Generic = ignore_args lia_generic
  | choose _ Local_Input = ignore_args (refl "cvc5")
  | choose _ Minus_Simplify = ignore_args rewrite_minus_simplify
  | choose _ NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
  | choose _ Normalized_Input = ignore_args normalized_input
  | choose _ Not_And = ignore_args not_and_rule
  | choose _ Not_Equiv1 = ignore_args not_equiv1
  | choose _ Not_Equiv2 = ignore_args not_equiv2
  | choose _ Not_Implies1 = ignore_args not_implies1
  | choose _ Not_Implies2 = ignore_args not_implies2
  | choose _ Not_ITE1 = ignore_args not_ite1
  | choose _ Not_ITE2 = ignore_args not_ite2
  | choose _ Not_Not = ignore_args not_not
  | choose _ Not_Or = ignore_args not_or_rule
  | choose _ Not_Simplify = ignore_args rewrite_not_simplify
  | choose _ Or = ignore_args or
  | choose _ Or_Neg = ignore_args or_neg_rule
  | choose _ Or_Pos = ignore_args or_pos_rule
  | choose _ Or_Simplify = ignore_args rewrite_or_simplify
  | choose _ Theory_Resolution2 = ignore_args theory_resolution2
  | choose _ Prod_Simplify = ignore_args prod_simplify
  | choose _ Qnt_Join = ignore_args qnt_join
  | choose _ Qnt_Rm_Unused = ignore_args qnt_rm_unused
  | choose _ Onepoint = ignore_args onepoint
  | choose _ Qnt_Simplify = ignore_args qnt_simplify
  | choose _ Refl = ignore_args (refl "cvc5")
  | choose _ Resolution = ignore_args unit_res
  | choose _ Skolem_Ex = ignore_args skolem_ex
  | choose _ Skolem_Forall = ignore_args skolem_forall
  | choose _ Subproof = ignore_args subproof
  | choose _ Sum_Simplify = ignore_args sum_simplify
  | choose _ Tautological_Clause = ignore_args tautological_clause
  | choose _ Theory_Resolution = ignore_args unit_res
  | choose _ AC_Simp = ignore_args tmp_AC_rule
  | choose _ Bfun_Elim = ignore_args bfun_elim
  | choose _ Qnt_CNF = ignore_args qnt_cnf
  | choose _ Trans = ignore_args trans
  | choose _ Symm = ignore_args symm
  | choose _ Not_Symm = ignore_args not_symm
  | choose _ Reordering = ignore_args reordering
  | choose _ Tmp_Quantifier_Simplify = ignore_args qnt_simplify
  | choose ctxt (x as Other_Rule r) =
    (case get_alethe_tac r ctxt of
      NONE => unsupported (string_of_verit_rule x)
    | SOME a => ignore_insts a)
  | choose _ Hole = ignore_args hole
  | choose _ r = (@{print} ("unknown rule, using hole", r); ignore_args hole)
(*unsupported (string_of_verit_rule r)*)

type verit_method = Proof.context -> thm list -> term -> thm
type abs_context = int * term Termtab.table

fun with_tracing rule method ctxt thms args insts decls t =
  let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t
  in method ctxt thms args insts decls t end

fun method_for rule ctxt = with_tracing rule (choose (Context.Proof ctxt) (cvc5_rule_of rule)) ctxt

fun discharge ctxt [thm] t =
  SMT_Replay_Methods.prove ctxt t (fn _ =>
    resolve_tac ctxt [thm] THEN_ALL_NEW (resolve_tac ctxt @{thms refl}))

end;

quality100%

¤ 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.