equal
deleted
inserted
replaced
349 |
349 |
350 * Theory reorganizations: |
350 * Theory reorganizations: |
351 * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy |
351 * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy |
352 |
352 |
353 * New internal SAT solver "dpll_p" that produces models and proof traces. |
353 * New internal SAT solver "dpll_p" that produces models and proof traces. |
|
354 This solver replaces the internal SAT solvers "enumerate" and "dpll". |
|
355 Applications that explicitly used one of these two SAT solvers should |
|
356 use "dpll_p" instead. Minor INCOMPATIBILITY. |
354 |
357 |
355 * SMT module: |
358 * SMT module: |
356 * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 |
359 * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 |
357 and supports recent versions of Z3 (e.g., 4.3). The new proof method is |
360 and supports recent versions of Z3 (e.g., 4.3). The new proof method is |
358 called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and |
361 called "smt2", and the new Z3 is called "z3_new" in Sledgehammer and |