NEWS
changeset 57212 f25dad3d6144
parent 57112 70395c65c0e3
child 57237 bc51864c2ac4
equal deleted inserted replaced
57211:cc59d49bdf64 57212:f25dad3d6144
   380   "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
   380   "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
   381 
   381 
   382 * SMT module:
   382 * SMT module:
   383   * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
   383   * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
   384     and supports recent versions of Z3 (e.g., 4.3). The new proof method is
   384     and supports recent versions of Z3 (e.g., 4.3). The new proof method is
   385     called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and
   385     called "smt2".
   386     elsewhere.
       
   387 
   386 
   388 * Sledgehammer:
   387 * Sledgehammer:
   389   - New prover "z3_new" with support for Isar proofs
   388   - New prover "z3_new" with support for Isar proofs
   390   - MaSh overhaul:
   389   - MaSh overhaul:
   391       - New SML-based learning engines eliminate the dependency on Python
   390       - New SML-based learning engines eliminate the dependency on Python