<commit_before>(*  Title:      HOL/SMT.thy
    Author:     <NAME>, <NAME>
*)

header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}

theory SMT
imports Record
uses
  "Tools/SMT/smt_utils.ML"
  "Tools/SMT/smt_failure.ML"
  "Tools/SMT/smt_config.ML"
  ("Tools/SMT/smt_monomorph.ML")
  ("Tools/SMT/smt_builtin.ML")
  ("Tools/SMT/smt_datatypes.ML")
  ("Tools/SMT/smt_normalize.ML")
  ("Tools/SMT/smt_translate.ML")
  ("Tools/SMT/smt_solver.ML")
  ("Tools/SMT/smtlib_interface.ML")
  ("Tools/SMT/z3_interface.ML")
  ("Tools/SMT/z3_proof_parser.ML")
  ("Tools/SMT/z3_proof_tools.ML")
  ("Tools/SMT/z3_proof_literals.ML")
  ("Tools/SMT/z3_proof_methods.ML")
  ("Tools/SMT/z3_proof_reconstruction.ML")
  ("Tools/SMT/z3_model.ML")
  ("Tools/SMT/smt_setup_solvers.ML")
begin



subsection {* Triggers for quantifier instantiation *}

text {*
Some SMT solvers support patterns as a quantifier instantiation
heuristics.  Patterns may either be positive terms (tagged by "pat")
triggering quantifier instantiations -- when the solver finds a
term matching a positive pattern, it instantiates the corresponding
quantifier accordingly -- or negative terms (tagged by "nopat")
inhibiting quantifier instantiations.  A list of patterns
of the same kind is called a multipattern, and all patterns in a
multipattern are considered conjunctively for quantifier instantiation.
A list of multipatterns is called a trigger, and their multipatterns
act disjunctively during quantifier instantiation.  Each multipattern
should mention at least all quantified variables of the preceding
quantifier block.
*}

datatype pattern = Pattern

definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"

definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
where "trigger _ P = P"



subsection {* Quantifier weights *}

text {*
Weight annotations to quantifiers influence the priority of quantifier
instantiations.  They should be handled with care for solvers, which support
them, because incorrect choices of weights might render a problem unsolvable.
*}

definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"

text {*
Weights must be non-negative.  The value @{text 0} is equivalent to providing
no weight at all.

Weights should only be used at quantifiers and only inside triggers (if the
quantifier has triggers).  Valid usages of weights are as follows:

\begin{itemize}
\item
@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
\item
@{term "\<forall>x. weight 3 (P x)"}
\end{itemize}
*}



subsection {* Higher-order encoding *}

text {*
Application is made explicit for constants occurring with varying
numbers of arguments.  This is achieved by the introduction of the
following constant.
*}

definition fun_app where "fun_app f = f"

text {*
Some solvers support a theory of arrays which can be used to encode
higher-order functions.  The following set of lemmas specifies the
properties of such (extensional) arrays.
*}

lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
  fun_upd_upd fun_app_def



subsection {* First-order logic *}

text {*
Some SMT solvers only accept problems in first-order logic, i.e.,
where formulas and terms are syntactically separated. When
translating higher-order into first-order problems, all
uninterpreted constants (those not built-in in the target solver)
are treated as function symbols in the first-order sense.  Their
occurrences as head symbols in atoms (i.e., as predicate symbols) are
turned into terms by logically equating such atoms with @{term True}.
For technical reasons, @{term True} and @{term False} occurring inside
terms are replaced by the following constants.
*}

definition term_true where "term_true = True"
definition term_false where "term_false = False"



subsection {* Integer division and modulo for Z3 *}

definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
  "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"

definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
  "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"



subsection {* Setup *}

use "Tools/SMT/smt_monomorph.ML"
use "Tools/SMT/smt_builtin.ML"
use "Tools/SMT/smt_datatypes.ML"
use "Tools/SMT/smt_normalize.ML"
use "Tools/SMT/smt_translate.ML"
use "Tools/SMT/smt_solver.ML"
use "Tools/SMT/smtlib_interface.ML"
use "Tools/SMT/z3_interface.ML"
use "Tools/SMT/z3_proof_parser.ML"
use "Tools/SMT/z3_proof_tools.ML"
use "Tools/SMT/z3_proof_literals.ML"
use "Tools/SMT/z3_proof_methods.ML"
use "Tools/SMT/z3_proof_reconstruction.ML"
use "Tools/SMT/z3_model.ML"
use "Tools/SMT/smt_setup_solvers.ML"

setup {*
  SMT_Config.setup #>
  SMT_Normalize.setup #>
  SMT_Solver.setup #>
  SMTLIB_Interface.setup #>
  Z3_Interface.setup #>
  Z3_Proof_Reconstruction.setup #>
  SMT_Setup_Solvers.setup
*}



subsection {* Configuration *}

text {*
The current configuration can be printed by the command
@{text smt_status}, which shows the values of most options.
*}



subsection {* General configuration options *}

text {*
The option @{text smt_solver} can be used to change the target SMT
solver.  The possible values can be obtained from the @{text smt_status}
command.
*}
<commit_msg>added hints about licensing restrictions and how to enable Z3<commit_after>(*  Title:      HOL/SMT.thy
    Author:     <NAME>, <NAME>
*)

header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}

theory SMT
imports Record
uses
  "Tools/SMT/smt_utils.ML"
  "Tools/SMT/smt_failure.ML"
  "Tools/SMT/smt_config.ML"
  ("Tools/SMT/smt_monomorph.ML")
  ("Tools/SMT/smt_builtin.ML")
  ("Tools/SMT/smt_datatypes.ML")
  ("Tools/SMT/smt_normalize.ML")
  ("Tools/SMT/smt_translate.ML")
  ("Tools/SMT/smt_solver.ML")
  ("Tools/SMT/smtlib_interface.ML")
  ("Tools/SMT/z3_interface.ML")
  ("Tools/SMT/z3_proof_parser.ML")
  ("Tools/SMT/z3_proof_tools.ML")
  ("Tools/SMT/z3_proof_literals.ML")
  ("Tools/SMT/z3_proof_methods.ML")
  ("Tools/SMT/z3_proof_reconstruction.ML")
  ("Tools/SMT/z3_model.ML")
  ("Tools/SMT/smt_setup_solvers.ML")
begin



subsection {* Triggers for quantifier instantiation *}

text {*
Some SMT solvers support patterns as a quantifier instantiation
heuristics.  Patterns may either be positive terms (tagged by "pat")
triggering quantifier instantiations -- when the solver finds a
term matching a positive pattern, it instantiates the corresponding
quantifier accordingly -- or negative terms (tagged by "nopat")
inhibiting quantifier instantiations.  A list of patterns
of the same kind is called a multipattern, and all patterns in a
multipattern are considered conjunctively for quantifier instantiation.
A list of multipatterns is called a trigger, and their multipatterns
act disjunctively during quantifier instantiation.  Each multipattern
should mention at least all quantified variables of the preceding
quantifier block.
*}

datatype pattern = Pattern

definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"

definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
where "trigger _ P = P"



subsection {* Quantifier weights *}

text {*
Weight annotations to quantifiers influence the priority of quantifier
instantiations.  They should be handled with care for solvers, which support
them, because incorrect choices of weights might render a problem unsolvable.
*}

definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"

text {*
Weights must be non-negative.  The value @{text 0} is equivalent to providing
no weight at all.

Weights should only be used at quantifiers and only inside triggers (if the
quantifier has triggers).  Valid usages of weights are as follows:

\begin{itemize}
\item
@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
\item
@{term "\<forall>x. weight 3 (P x)"}
\end{itemize}
*}



subsection {* Higher-order encoding *}

text {*
Application is made explicit for constants occurring with varying
numbers of arguments.  This is achieved by the introduction of the
following constant.
*}

definition fun_app where "fun_app f = f"

text {*
Some solvers support a theory of arrays which can be used to encode
higher-order functions.  The following set of lemmas specifies the
properties of such (extensional) arrays.
*}

lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
  fun_upd_upd fun_app_def



subsection {* First-order logic *}

text {*
Some SMT solvers only accept problems in first-order logic, i.e.,
where formulas and terms are syntactically separated. When
translating higher-order into first-order problems, all
uninterpreted constants (those not built-in in the target solver)
are treated as function symbols in the first-order sense.  Their
occurrences as head symbols in atoms (i.e., as predicate symbols) are
turned into terms by logically equating such atoms with @{term True}.
For technical reasons, @{term True} and @{term False} occurring inside
terms are replaced by the following constants.
*}

definition term_true where "term_true = True"
definition term_false where "term_false = False"



subsection {* Integer division and modulo for Z3 *}

definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
  "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"

definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
  "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"



subsection {* Setup *}

use "Tools/SMT/smt_monomorph.ML"
use "Tools/SMT/smt_builtin.ML"
use "Tools/SMT/smt_datatypes.ML"
use "Tools/SMT/smt_normalize.ML"
use "Tools/SMT/smt_translate.ML"
use "Tools/SMT/smt_solver.ML"
use "Tools/SMT/smtlib_interface.ML"
use "Tools/SMT/z3_interface.ML"
use "Tools/SMT/z3_proof_parser.ML"
use "Tools/SMT/z3_proof_tools.ML"
use "Tools/SMT/z3_proof_literals.ML"
use "Tools/SMT/z3_proof_methods.ML"
use "Tools/SMT/z3_proof_reconstruction.ML"
use "Tools/SMT/z3_model.ML"
use "Tools/SMT/smt_setup_solvers.ML"

setup {*
  SMT_Config.setup #>
  SMT_Normalize.setup #>
  SMT_Solver.setup #>
  SMTLIB_Interface.setup #>
  Z3_Interface.setup #>
  Z3_Proof_Reconstruction.setup #>
  SMT_Setup_Solvers.setup
*}



subsection {* Configuration *}

text {*
The current configuration can be printed by the command
@{text smt_status}, which shows the values of most options.
*}



subsection {* General configuration options *}

text {*
The option @{text smt_solver} can be used to change the target SMT
solver.  The possible values can be obtained from the @{text smt_status}
command.

Due to licensing restrictions, Yices and Z3 are not installed/enabled
by default.  Z3 is free for non-commercial applications and can be enabled
by simply setting the environment variable Z3_NON_COMMERCIAL to @{text yes}.
*}

{'fraction_non_alphanumeric': 0.09855923648710654, 'fraction_numerical': 0.005139029090575388, 'mean_word_length': 4.582991803278689, 'pattern_counts': {'":': 0, '<': 35, '<?xml version=': 0, '>': 47, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2830460', 'n_tokens_mistral': 3672, 'n_tokens_neox': 3538, 'n_words': 1221}