#
6a81a039 |
|
21-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from src Will also make selftest to check that they aren't introduced
|
#
0df98768 |
|
01-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More changes to get basis2002 changes working properly in both poly + mosml.
|
#
ea7bf382 |
|
01-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement more of Basis2002 for Moscow ML (adding Vector, Array, ArraySlice and VectorSlice), simplifying what Poly/ML has to emulate. Haven't done full rebuild test, but have got as far as integerTheory and Omega, which makes heavy uses of Vector etc.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
8915325f |
|
13-Dec-2008 |
Hasan Amjad <ha227@cam.ac.uk> |
Fix for conflicting behaviour of Moscow ML and PolyML on FileSys.tmpName. Thanks to Scott Owens for spotting and diagnosing the problem, and providing a temporary patch.
|
#
a41da662 |
|
10-Dec-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
This was causing hundreds of empty temporary files to be generated during the build on PolyML. This quick fix val tmp = FileSys.tmpName() - val cnfname = if isSome fname then (valOf fname) else tmp^".cnf"; + val cnfname = if isSome fname then (valOf fname) else tmp; isn't ideal, but fixed the bulk of the problem for now. On PolyML, the call to tmpName() actually creates the file (as per the ML basis standars), and by adding the suffix, the original file is never removed. There are still obvious potential cases where the temporary file is created but not used or removed, but I don't immediately see how to fix them (or indeed what this code does).
|
#
e07db070 |
|
08-Aug-2007 |
Hasan Amjad <ha227@cam.ac.uk> |
Summary: tautLib upgraded to use HolSatLib engine. Details: * tautLib signature (and behaviour hopefully!) is unchanged. Internally, TAUT_CHECK_CONV now uses HolSatLib. * HolSatLib can now handle Boolean-valued conditionals. This was forced because tautLib handled them. * We now have full drop-in support for zChaff, via a proof translator. * HolSatLib now deletes temporary files. * Legacy HolSatLib interface dropped in favour of simpler interface with single entry-point, plus some convenience wrappers. * examples/miller/m renamed to selftest.exe; now works with build -selftest * build-sequence changes: src/compute and src/HolSat/* moved above src/taut; examples/miller stuff condensed into one entry * build.sml patched to handle zChaff proof translator (in C++). * New windows binaries for MiniSat and zChaff proof translator. * Changes/additions to HolSatLib interface rippled to affected files. * Documentation updated. In particular, HolSatLib section in Description had to be almost completely rewritten. * HOL builds to selftest level 1 on standard kernel, and level 2 on experimental kernel. Level 2 failures on standard are non-critical and authors have been informed.
|
#
d8cf5be0 |
|
30-Oct-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
* Implicit definitional CNF (from HOL Light code due to John Harrison), modified to exploit primitive CONJUNCT* rules in HOL4. * Optimisations to above for the case where problem is already CNF. This is handy for SATLIB problems. * Fallback to SML DPLL prover extended to the case where MiniSat binary cannot be found or cannot be executed. * SML DPLL prover modified to use implicit def CNF, and to produce countermodels in the same format as SAT_TAUT_PROVE. * Explicit definitional CNF and normalFormsTest files removed, so we can move HolSatLib up the build-sequence, to follow src/taut.
|
#
0c840916 |
|
29-Sep-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
Some technical improvements: * HOL-side - All is now tail recursive and most uses less RAM - Undocumented feature allows skipping CNF conversion (still WIP) - General refactoring preparatory to adding proof replay for ZChaff * Solver-side - Proof log now indexes root clauses, and writes sign info for pivots - Proof::compress has been implemented - Folded in miscellaneous upstream deltas PS: None of the above applies to defCNF stuff. Still a black box to me.
|
#
cde2941e |
|
19-Mar-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
HolSatLib refactoring and additions. * MiniSat-p v1.14 added as a "built-in" SAT-solver * A new function SAT_TAUT_PROVE uses MiniSat to prove propositional tautologies within HOL * HolSatLib refactored into satTools and dimacsTools * Local documentation removed; it was folded into the Description some time ago. * The HolSatLib interface remains the same, save for the addition of SAT_TAUT_PROVE. * Two minor additions to defCNF: a global ref for the variable name prefix used by DEF_CNF_VECTOR_CONV (defaulting to the current setting), and a global ref for the number of new vars introduced by definitional CNF.
|