674 |
674 |
675 text \<open> |
675 text \<open> |
676 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT |
676 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT |
677 solvers are fully trusted without additional checks. The following |
677 solvers are fully trusted without additional checks. The following |
678 option can cause the SMT solver to run in proof-producing mode, giving |
678 option can cause the SMT solver to run in proof-producing mode, giving |
679 a checkable certificate. This is currently only implemented for Z3. |
679 a checkable certificate. This is currently implemented only for veriT and |
|
680 Z3. |
680 \<close> |
681 \<close> |
681 |
682 |
682 declare [[smt_oracle = false]] |
683 declare [[smt_oracle = false]] |
683 |
684 |
684 text \<open> |
685 text \<open> |
685 Each SMT solver provides several commandline options to tweak its |
686 Each SMT solver provides several command-line options to tweak its |
686 behaviour. They can be passed to the solver by setting the following |
687 behaviour. They can be passed to the solver by setting the following |
687 options. |
688 options. |
688 \<close> |
689 \<close> |
689 |
690 |
690 declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] |
691 declare [[cvc4_options = ""]] |
691 declare [[verit_options = ""]] |
692 declare [[verit_options = ""]] |
692 declare [[z3_options = ""]] |
693 declare [[z3_options = ""]] |
693 |
694 |
694 text \<open> |
695 text \<open> |
695 The SMT method provides an inference mechanism to detect simple triggers |
696 The SMT method provides an inference mechanism to detect simple triggers |