NameDateSize

..25-Jul-201970

COPYRIGHTH A D25-Jul-20191.5 KiB

HolmakefileH A D25-Jul-2019200

HolSmtLib.sigH A D25-Jul-2019352

HolSmtLib.smlH A D25-Jul-20192.3 KiB

HolSmtScript.smlH A D25-Jul-201927 KiB

Library.smlH A D25-Jul-201911 KiB

READMEH A D25-Jul-20191.4 KiB

selftest.smlH A D25-Jul-201946.1 KiB

SmtLib.smlH A D25-Jul-201923.4 KiB

SmtLib_Logics.smlH A D25-Jul-20199 KiB

SmtLib_Parser.smlH A D25-Jul-201920 KiB

SmtLib_Theories.smlH A D25-Jul-201911.2 KiB

SolverSpec.smlH A D25-Jul-20194.2 KiB

Yices.smlH A D25-Jul-201936.5 KiB

Z3.smlH A D25-Jul-20194.7 KiB

Z3_ProformaThms.smlH A D25-Jul-20193.3 KiB

Z3_Proof.smlH A D25-Jul-20193.1 KiB

Z3_ProofParser.smlH A D25-Jul-201916.6 KiB

Z3_ProofReplay.smlH A D25-Jul-201941.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