| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
added timeout argument to TPTP tools
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 23:13:10 +0200 |
blanchet |
more standard SZS output
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 22:40:25 +0200 |
blanchet |
tuned SZS status output
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 22:40:25 +0200 |
blanchet |
added SZS status wrappers in TPTP mode
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 22:40:25 +0200 |
blanchet |
fixed Auto Nitpick's output
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 15:09:47 +0200 |
wenzelm |
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 18:25:36 +0100 |
blanchet |
updated message
|
file |
diff |
annotate
|
| Wed, 04 Jan 2012 12:09:53 +0100 |
blanchet |
remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
rationalized output (a bit)
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
more precise warning
|
file |
diff |
annotate
|
| Thu, 30 Jun 2011 13:21:41 +0200 |
wenzelm |
standardized use of Path operations;
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case gracefully in Nitpick
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
use \<emdash> rather than \<midarrow>
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 17:20:29 +0200 |
wenzelm |
direct use of Variable.is_fixed;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:04:58 +0200 |
blanchet |
use "Spec_Rules" for finding axioms -- more reliable and cleaner
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 11:43:28 +0100 |
blanchet |
optimize Kodkod bounds when "need" is specified
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 22:07:17 +0100 |
blanchet |
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 14:43:53 +0100 |
blanchet |
reword Nitpick's wording concerning potential counterexamples
|
file |
diff |
annotate
|
| Tue, 15 Mar 2011 15:49:42 +0100 |
blanchet |
support non-ground "need" values
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2011 10:25:29 +0100 |
blanchet |
perform no arity check in debug mode so that we get to see the Kodkod problem
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 14:25:15 +0100 |
blanchet |
don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
simplify "need" option's syntax
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
renamed "preconstr" option "need"
|
file |
diff |
annotate
|
| Wed, 02 Mar 2011 15:51:22 +0100 |
blanchet |
added missing spaces in output
|
file |
diff |
annotate
|
| Wed, 02 Mar 2011 14:50:16 +0100 |
blanchet |
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
|
file |
diff |
annotate
|
| Wed, 02 Mar 2011 13:09:57 +0100 |
blanchet |
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
|
file |
diff |
annotate
|
| Wed, 02 Mar 2011 13:09:57 +0100 |
blanchet |
make "preconstr" option more robust -- shouldn't throw exceptions
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 17:53:10 +0100 |
blanchet |
if "total_consts" is set, report cex's as quasi-genuine
|
file |
diff |
annotate
|
| Mon, 28 Feb 2011 17:53:10 +0100 |
blanchet |
added "total_consts" option
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 17:36:32 +0100 |
blanchet |
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 16:33:21 +0100 |
blanchet |
more work on "fix_datatype_vals"
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 15:45:44 +0100 |
blanchet |
first steps in implementing "fix_datatype_vals" optimization
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 11:50:31 +0100 |
blanchet |
tweaked Nitpick based on C++ memory model example
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:42:29 +0100 |
blanchet |
always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:29:13 +0100 |
blanchet |
don't distinguish between "fixes" and other free variables -- this confuses users
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 16:19:08 +0100 |
blanchet |
make Nitpick's timeout mechanism somewhat more reliable/friendly;
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 11:48:42 +0100 |
blanchet |
added a timestamp to Nitpick in verbose mode for debugging purposes;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:53 +0100 |
blanchet |
remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:01 +0100 |
blanchet |
give the inner timeout mechanism a chance, since it gives more precise information to the user
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:01 +0100 |
blanchet |
added a hint when the user obviously just forgot a colon after the lemma's name
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:33:09 +0100 |
blanchet |
removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 13:18:25 +0100 |
blanchet |
support 3 monotonicity calculi in one and fix soundness bug
|
file |
diff |
annotate
|
| Sun, 07 Nov 2010 13:29:59 +0100 |
blanchet |
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 19:47:20 +0100 |
wenzelm |
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 22:26:53 +0100 |
blanchet |
standardize on seconds for Nitpick and Sledgehammer timeouts
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 09:29:57 +0200 |
blanchet |
clear identification
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 14:12:18 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 13:24:18 +0200 |
blanchet |
remove "fast_descs" option from Nitpick;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 20:21:40 +0200 |
blanchet |
remove unreferenced identifiers
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 10:20:25 +0200 |
blanchet |
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|