CVCHOL is a proof translator that translates CVC3 theorems into HOL Light theorems. It is implemented in OCaml as an extension of HOL Light. Given a proof from CVC3, it constructs a corresponding proof in HOL Light. As of October 2008, it can translate proofs by CVC3 for most cases in the AUFLIA category of SMT-LIB .
CVCHOL can be used as a proof checker for CVC3. CVCHOL provides a HOL Light command: "cvc_prove_file". The command accepts a string containing a file name and invokes CVC3 on the file through its C API. If CVC3 reports that the formula in the file is valid, the proof is then translated into HOL Light. If the translation is successful, the result of translation is a theorem in HOL Light, which can be interpreted as a certificate that the result reported by CVC3 is correct.
Another way to look at CVCHOL is as a trusted external decision procedure for HOL Light. CVCHOL provides a HOL Light command: "cvc_prove". "cvc_prove" accepts a HOL term "t" and returns a HOL Light theorem "|- t" if CVC3 is able to prove that this term is valid and the proof translation back to HOL Light is successful.
CVCHOL works with HOL Light. CVC3 and HOL Light are connected through the C interface of OCaml. To use CVCHOL, a new OCaml toplevel that combines CVC3 has to be built.
As of October 2008, the translator works with the latest development version of CVC3. Before building a new OCaml toplevel, please check CVC3 and HOL Light have been properly installed.
Find the location of CVC3's static library file "libcvc3.a" and the c_interface header file "c_interface.h" (for instance, they may be in /usr/local/lib and /usr/local/include respectively). If you built CVC3 as a dynamic library, then you will need to find "libcvc3.so" instead.
1. Copy the CVCHOL tar file into the directory where HOL Light resides. Unpack the source tar file. e.g.
tar -vxf cvchol.tar
cd cvchol
2. Call "make" to build a new OCaml toplevel and specify values for "CVC_INCLUDE_DIR" and "CVC_LIB". e.g.
make "CVC_LIB=/usr/local/lib/libcvc3.a" "CVC_INCLUDE_DIR=/usr/local/include"
An alternative is to call "make" specifying only "CVC_DIR" for a
local CVC3 source installation, e.g.
make "CVC_DIR=/home/user/tools/cvc3"
A new OCaml toplevel named "cvc_hol" should be created.
3. Copy "cvc_hol" into the HOL Light directory. e.g.
cp cvc_hol ../
4. Copy "cvchol.ml" into the HOL Light directory. e.g.
cp cvchol.ml ../
To run CVCHOL
1. Go to the HOL Light directory
2. Run the new OCaml toplevel "cvc_hol". e.g.
./cvc_hol
3. Launch HOL Light. e.g.
#use"hol.ml";;
4. Load CVCHOL with the following command:
#use"cvchol/cvchol.ml";;
CVCHOL provides two HOL Light commands:
cvc_prove : term -> thm = <fun>
cvc_prove_file : string -> thm = <fun>
1. Errors when building the new OCaml toplevel.
Please check your installation of OCaml, HOL Light,
and CVC3. Make sure all the required files are there and that their locations
can be found by the Makefile.
2. Segmentation fault while running.
This usually means there is a bug in the translator.
Please contact someone in the list of CONTACTS below and send a brief bug report.
3. Unsupported proof rules.
As of October 2008, CVCHOL should be able to handle
most proof rules for arithmetic and arrays. Please contact us if you run into
trouble with unsupported proof rules in CVC3.
Yeting Ge
Clark Barrett
The translator is developed under the leadership of Clark Barrett. Sean McLaughlin wrote the first version. Yeting Ge has been the developer since 2005. John Harrison gave much helpful advice on HOL Light.