src/HOL/Tools/SMT2/smtlib2_interface.ML
2014-07-30 fleury 2014-07-30 Basic support for the SMT prover veriT.
2014-07-15 blanchet 2014-07-15 don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
2014-06-12 blanchet 2014-06-12 don't ask proof-disabled solvers to do proofs
2014-06-12 blanchet 2014-06-12 tuning
2014-06-12 blanchet 2014-06-12 tuning
2014-06-10 blanchet 2014-06-10 generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
2014-06-03 blanchet 2014-06-03 removed SMT weights -- their impact was very inconclusive anyway
2014-03-13 blanchet 2014-03-13 simplified solution parsing
2014-03-13 blanchet 2014-03-13 adapted to renamed ML files
2014-03-13 blanchet 2014-03-13 reintroduced old model reconstruction code -- still needs to be ported
2014-03-13 blanchet 2014-03-13 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle