equal
deleted
inserted
replaced
33 -- "ATPs will be interrupted after this time (in seconds)" |
33 -- "ATPs will be interrupted after this time (in seconds)" |
34 |
34 |
35 public option z3_non_commercial : string = "unknown" |
35 public option z3_non_commercial : string = "unknown" |
36 -- "status of Z3 activation for non-commercial use (yes, no, unknown)" |
36 -- "status of Z3 activation for non-commercial use (yes, no, unknown)" |
37 |
37 |
38 public option MaSh : string = "none" |
38 public option MaSh : string = "sml" |
39 -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)" |
39 -- "machine learning engine to use by Sledgehammer (sml, sml_knn, sml_nb, py, none)" |