summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

simplify selectors in code views

note correct induction schemes in 'primrec' (for N2M)

use right meson tactic for preplaying

simplify unused universally quantified variables in Z3 proofs

fixed Waldmeister endgame w.r.t. "Trueprop"

tuned structure name

added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')

renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish

added 'satx' proof method to Try0

make 'dpll_p' the default SAT solver, rather than the hard-to-get zChaff-with-proofs