# Detailed use of SMTCoq Examples are given in the file examples/Example.v. They are meant to be easily re-usable for your own usage. ## Overview After installation, the SMTCoq module can be used in Coq files via the `Require Import SMTCoq.SMTCoq.` command. For each supported solver, it provides: - a vernacular command to check answers: `XXX_Checker "problem_file" "witness_file"` returns `true` only if `witness_file` contains a proof of the unsatisfiability of the problem stated in `problem_file`; - a vernacular command to safely import theorems: `XXX_Theorem theo "problem_file" "witness_file"` produces a Coq term `theo` whose type is the theorem stated in `problem_file` if `witness_file` is a proof of the unsatisfiability of it, and fails otherwise. - safe tactics to try to solve a Coq goal using the chosen solver (or a combination of solvers). We now give more details for each solver. ## zChaff Compile and install zChaff as explained in the installation instructions. In the following, we consider that the command `zchaff` is in your `PATH` environment variable. ### Checking zChaff answers of unsatisfiability and importing theorems To check the result given by zChaff on an unsatisfiable dimacs file `file.cnf`: - Produce a zChaff proof witness: `zchaff file.cnf`. This command produces a proof witness file named `resolve_trace`. - In a Coq file `file.v`, put: ```coq Require Import SMTCoq.SMTCoq. Zchaff_Checker "file.cnf" "resolve_trace". ``` - Compile `file.v`: `coqc file.v`. If it returns `true` then zChaff indeed proved that the problem was unsatisfiable. - You can also produce Coq theorems from zChaff proof witnesses: the commands ```coq Require Import SMTCoq.SMTCoq. Zchaff_Theorem theo "file.cnf" "resolve_trace". ``` will produce a Coq term `theo` whose type is the theorem stated in `file.cnf`. ### zChaff as a Coq decision procedure The `zchaff` tactic can be used to solve any goal of the form: ```coq forall l, b1 = b2 ``` where `l` is a quantifier-free list of terms and `b1` and `b2` are expressions of type `bool`. A more efficient version of this tactic, called `zchaff_no_check`, performs only the check at `Qed`. (Thus it is safe, but a proof may fail at `Qed` even if everything went through during proof elaboration.) ## veriT Compile and install veriT as explained in the installation instructions. In the following, we consider that the command `veriT` is in your `PATH` environment variable. ### Checking veriT answers of unsatisfiability and importing theorems To check the result given by veriT on an unsatisfiable SMT-LIB2 file `file.smt2`: - Produce a veriT proof witness: ```coq veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-e --disable-ackermann --input=smtlib2 --proof=file.log file.smt2 ``` This command produces a proof witness file named `file.log`. - In a Coq file `file.v`, put: ```coq Require Import SMTCoq.SMTCoq. Section File. Verit_Checker "file.smt2" "file.log". End File. ``` - Compile `file.v`: `coqc file.v`. If it returns `true` then veriT indeed proved that the problem was unsatisfiable. - You can also produce Coq theorems from veriT proof witnesses: the commands ```coq Require Import SMTCoq.SMTCoq. Section File. Verit_Theorem theo "file.smt2" "file.log". End File. ``` will produce a Coq term `theo` whose type is the theorem stated in `file.smt2`. The theories that are currently supported by these commands are `QF_UF` (theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL` (integer difference logic), and their combinations. ### veriT as a Coq decision procedure The `verit_bool [h1 ...]` tactic can be used to solve any goal of the form: ```coq forall l, b1 = b2 ``` where `l` is a quantifier-free list of terms and `b1` and `b2` are expressions of type `bool`. This tactic **supports quantifiers**: it takes optional arguments which are names of universally quantified lemmas/hypotheses that can be used to solve the goal. These lemmas can also be given once and for all using the `Add_lemmas` command (see [examples/Example.v](https://github.com/smtcoq/smtcoq/blob/master/examples/Example.v) for details). In addition, the `verit` tactic applies to Coq goals of sort `Prop`: it first converts the goal into a term of type `bool` (thanks to the `reflect` predicate of `SSReflect`), and then calls the previous tactic `verit_bool`. The theories that are currently supported by these tactics are `QF_UF` (theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL` (integer difference logic), and their combinations. A more efficient version of this tactic, called `verit_no_check`, performs only the check at `Qed`. (Thus it is safe, but a proof may fail at `Qed` even if everything went through during proof elaboration.) ## CVC4 Compile and install `CVC4` as explained in the installation instructions. In the following, we consider that the command `cvc4` is in your `PATH` environment variable. ### Checking CVC4 answers of unsatisfiability and importing theorems To check the result given by CVC4 on an unsatisfiable SMT-LIB2 file `name.smt2`: - Produce a CVC4 proof witness: ```bash cvc4 --dump-proof --no-simplification --fewer-preprocessing-holes --no-bv-eq --no-bv-ineq --no-bv-algebraic name.smt2 > name.lfsc ``` This set of commands produces a proof witness file named `name.lfsc`. - In a Coq file `name.v`, put: ```coq Require Import SMTCoq.SMTCoq Bool List. Import ListNotations BVList.BITVECTOR_LIST FArray. Local Open Scope list_scope. Local Open Scope farray_scope. Local Open Scope bv_scope. Section File. Lfsc_Checker "name.smt2" "name.lfsc". End File. ``` - Compile `name.v`: `coqc name.v`. If it returns `true` then the problem is indeed unsatisfiable. NB: Use `cvc4tocoq` script in `src/lfsc/tests` to automatize the above steps. - Ex: `./cvc4tocoq name.smt2` returns `true` only if the problem `name.smt2` has been proved unsatisfiable by CVC4. The theories that are currently supported by these commands are `QF_UF` (theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL` (integer difference logic), `QF_BV` (theory of fixed-size bit vectors), `QF_A` (theory of arrays), and their combinations. ### CVC4 as a Coq decision procedure The `cvc4_bool` tactic can be used to solve any goal of the form: ```coq forall l, b1 = b2 ``` where `l` is a quantifier-free list of terms and `b1` and `b2` are expressions of type `bool`. In addition, the `cvc4` tactic applies to Coq goals of sort `Prop`: it first converts the goal into a term of type `bool` (thanks to the `reflect` predicate of `SSReflect`), it then calls the previous tactic `cvc4_bool`, and it finally converts any unsolved subgoals returned by CVC4 back to `Prop`, thus offering to the user the possibility to solve these (usually simpler) subgoals. The theories that are currently supported by these tactics are `QF_UF` (theory of equality), `QF_LIA` (linear integer arithmetic), `QF_IDL` (integer difference logic), `QF_BV` (theory of fixed-size bit vectors), `QF_A` (theory of arrays), and their combinations. A more efficient version of this tactic, called `cvc4_no_check`, performs only the check at `Qed`. (Thus it is safe, but a proof may fail at `Qed` even if everything went through during proof elaboration.) ## The smt tactic The more powerful tactic `smt` combines all the previous tactics: it first converts the goal to a term of type `bool` (thanks to the `reflect` predicate of `SSReflect`), it then calls a combination of the `cvc4_bool` and `verit_bool` tactics, and it finally converts any unsolved subgoals back to `Prop`, thus offering to the user the possibility to solve these (usually simpler) subgoals. A more efficient version of this tactic, called `smt_no_check`, performs only the check at `Qed`. (Thus it is safe, but a proof may fail at `Qed` even if everything went through during proof elaboration.) ## Conversion tactics SMTCoq provides conversion tactics, to inject various integer types into the type Z supported by SMTCoq. They can be called before the other SMTCoq tactics. These tactics are named `nat_convert`, `N_convert` and `pos_convert`. They can be combined.