Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 70 | ||
COPYRIGHT | H A D | 25-Jul-2019 | 1.5 KiB | |
Holmakefile | H A D | 25-Jul-2019 | 200 | |
HolSmtLib.sig | H A D | 25-Jul-2019 | 352 | |
HolSmtLib.sml | H A D | 25-Jul-2019 | 2.3 KiB | |
HolSmtScript.sml | H A D | 25-Jul-2019 | 27 KiB | |
Library.sml | H A D | 25-Jul-2019 | 11 KiB | |
README | H A D | 25-Jul-2019 | 1.4 KiB | |
selftest.sml | H A D | 25-Jul-2019 | 46.1 KiB | |
SmtLib.sml | H A D | 25-Jul-2019 | 23.4 KiB | |
SmtLib_Logics.sml | H A D | 25-Jul-2019 | 9 KiB | |
SmtLib_Parser.sml | H A D | 25-Jul-2019 | 20 KiB | |
SmtLib_Theories.sml | H A D | 25-Jul-2019 | 11.2 KiB | |
SolverSpec.sml | H A D | 25-Jul-2019 | 4.2 KiB | |
Yices.sml | H A D | 25-Jul-2019 | 36.5 KiB | |
Z3.sml | H A D | 25-Jul-2019 | 4.7 KiB | |
Z3_ProformaThms.sml | H A D | 25-Jul-2019 | 3.3 KiB | |
Z3_Proof.sml | H A D | 25-Jul-2019 | 3.1 KiB | |
Z3_ProofParser.sml | H A D | 25-Jul-2019 | 16.6 KiB | |
Z3_ProofReplay.sml | H A D | 25-Jul-2019 | 41.6 KiB |
README
1HolSmtLib is a library for integrating Satisfiability Modulo Theories (SMT) 2solvers with the HOL theorem prover. 3 4Files: 5 6COPYRIGHT Copyright notice, license and disclaimer. 7Holmakefile Makefile for Holmake (to build selftest.exe). 8HolSmtLib.{sig,sml} Entry point into HolSmtLib. Provides GENERIC_SMT_TAC 9 and derived tactics to call SMT solvers. 10HolSmtScript.sml Various theorems for HolSmtLib. 11Library.sml Common auxiliary functions, tracing. 12README This file. 13selftest.sml Unit tests for HolSmtLib. 14SmtLib_Logics.sml SMT-LIB 2 logics. 15SmtLib_Parser.sml Parsing of SMT-LIB 2 benchmarks. 16SmtLib_Theories.sml SMT-LIB 2 theories. 17SmtLib.sml Translation of HOL terms into SMT-LIB 2 format. 18SolverSpec.sml Definition of SMT solvers. 19Yices.sml Functions to invoke the Yices SMT solver. 20Z3.sml Functions to invoke the Z3 SMT solver. 21Z3_ProformaThms.sml Proforma theorems, used for Z3 proof reconstruction. 22Z3_Proof.sml Proof reconstruction for Z3: SML type of Z3 proofs. 23Z3_ProofParser.sml Proof reconstruction for Z3: parsing of Z3's proofs. 24Z3_ProofReplay.sml Proof reconstruction for Z3: replaying Z3's proofs in 25 HOL. 26 27Further documentation can be found in the HOL Description (in 28HOL/Manual/Description). 29