MetiTarski release 2.3 2014-03-03
* User-defined functions (abbreviations introduced using axioms) should be expanded
properly now. This has been achieved via changes to the term ordering (KBO).
* Autoconf is now used to automatically configure builds on a variety of UNIX environments.
* The --time option, for setting the runtime limit, now accepts decimals, for example 0.1.
* The parser now tolerates superfluous parentheses.
* Improved treatment of errors and warnings.
MetiTarski release 2.2 2013-06-17
* Compatibility with latest version of Z3 - 'pi' renamed automatically in interactions with Z3 to prevent errors, also the removal of underscores from variable names is automatically done prior to passing problems to Mathematica or Z3.
* consistency of the use of 'arc' rather than 'a' in inverse trigonometric functions arcsin, arccos and arctan. (This mainly affects axiom files.)
* free variables no longer permitted in first-order-formulae (fofs): all variables must be explicitly quantified.
* Sinh, ArcCos and CubeRoot added to functions passed to Mathematica (if the --allowSF option is used).
* an error message is now generated if the RCF procedure encounters an error leading to an error in MetiTarski (previously only the final broken pipe operating system error was reported).
* the Makefile now has separate targets to 'make build' and 'make install' as alternatives to the existing 'make'.
* various additional problem files and minor bug fixes.
MetiTarski release 2.1 2013-02-04
* option to optimise proofs by rerunning decisions to minimise the number of algebraic clauses (premises) required. This is turned on with the option --optProof. NB this may require quite a bit more time to run than the original proof took. Also, in some rare cases the decision procedure may fail on the reduced clause lists used in the optimising process causing the problem to time out. Proof size reduction can be as much as 80%, or as little as 0%.
* SMTLIB v2.0 support added. This is at a basic level with the following commands recognized:
assert, define-fun
Additionally include files may be listed in using set-option in the form
(set-option :includes (Élist of file namesÉ))
Note the use of the colon before the word includes to make it a keyword.
Functions/constants must all be of type (or sort) Real.
Variables can be of type Int or type Rat or of type Real.
All functions recognized by MetiTarski (i.e. sin() cos() etc) are built-in to the SMTLIB parser so for use with MetiTarski define-fun statements are not required.
The first command beginning "(assert (not" is taken to be the negated conjecture (NB this differs from the TPTP file format where the conjecture is not negated in the file). Only one such conjecture is allowed. Other assert commands are taken to be axioms.
Unrecognized SMTLIB commands are simply ignored.
A new flag, --writeSMTLIB has been added which, if set, will generate an SMTLIB version of an input TPTP file. The tptp file should only have one conjecture. The logic set in the file is AUFNIRA which is a superset of what is required as it contains arrays which MetiTarski does not deal with.
* Allowing special functions in RCF decision procedures.
Options have been added to allow special functions (sin, cos, tan, ln, exp, etc) in the calls to the decision procedure (normally only algebraic expressions are passed).
Currently this only works with Mathematica and selecting the options will select Mathematica as the decision procedure. Within the overall option of allowing special functions there are three choices, one is to allow special functions both in the given clause and in the environment of algebraic clauses, a second alternative is to allow the special functions only within the given clause and exclude them from the environment of algebraic clauses. Thirdly, for either of the other two options there is the option to only allow special functions that are not themselves contained as arguments of special functions (i.e. no nesting of special functions).
The option flags are as follows :
--allowSF_in_GC .................... Allow special functions in algebraic literals in the Given Clause only (Mathematica only)
--allowUSF_in_GC ................... Allow only un-nested special functions in algebraic literals in the Given Clause only (Mathematica only)
--allowSF .......................... Allow special functions in algebraic literals as well as the Given Clause (Mathematica only)
--allowUSF ......................... Allow un-nested special functions in algebraic literals as well as the Given Clause (Mathematica only)
Note, that allowing special functions will also cause the exact value of pi to be used. That is "pi" will be passed symbolically to Mathematica as "Pi".
* Restricting the RCF decision procedure time per call
An option has been added to allow RCF calls to be time restricted. This applies to Mathematica or to Z3. It should be noted that there is a bug within Z3 such that when it is running under OSX and it is time restricted it occasionally switches to a very low priority mode and will take a lot of time to reach a given cpu limit. This is not a problem under Linux.
RCF time limit is set using
--RCFtime time_in_millisecs
where time_in_millisecs is an integer giving the time limit in millisecs for any single RCF decision procedure call.
Restricting the RCFtime may greatly speed up some proof searches whilst causing others to fail by giving up or in some cases the search may even be extended.
Note that for Z3 strategies, setting RCFtime will override the strategy time.
MetiTarski release 2.0 2012-05-17
* Mathematica and Z3 can be used as external algebraic decision methods!
* Model sharing and other specialised heuristics for Z3
* Automatic inclusion of axioms, using the options --autoInclude, --autoIncludeExtended, --autoIncludeSuperExtended
* Visual feedback of CPU usage. (This is now the default meaning of --verbose 1. Other
"verbosity levels" are one higher than before.)
* function "log" (common logarithms) and axiom file log.ax
* Notation for intervals. t : (a,b), t : (=a,b=), etc.
* Problems with non-disjoint free and bound variables are rejected
(as probably missing parentheses after a quantifier).
* New option --rerun on/off (Reruns unsuccessful proofs with more liberal search settings)
* New parser (built using ML-YACC) with greatly improved error recovery. However, the syntax of cnf is now strictly enforced, so existing problems may need some additional parentheses.
* Additional problems (including PolyPaver benchmarks), and revisions to problems
* Stricter control on processor time used by the RCF decision procedure
* Numerous general internal improvements
MetiTarski release 1.9 2011-08-05
* Correction of a soundness bug involving decision procedure calls and labels.
(Only one false theorem was proved as a result of this bug, namely X2-tan.tptp.)
* Case-splitting with backtracking.
* Heuristic improvements, e.g. SOS weighting, the --maxalg and --proj_ord switches
* Syntactic changes
- in CNF, negative literals may appear as ~ ( ATOM ) and not just ~ ATOM
- decimal numbers may start with a decimal point: .1
* Slightly improved documentation in the README file.
* Refinement and corrections to the internal QEPCAD interface.
* The addaxioms script now works with Windows line breaks and spaces at the start of lines.
* Additional problems.
MetiTarski release 1.8 2011-01-18
* Constant folding, to ensure that 1.01, 1 + 10^-2 and 101/100 produce identical terms.
* Experimental case-splitting Òwithout backtracking". It is ON by default.
* Significant new heuristics, various small bugfixes and other refinements.
* Complicated new exp, sine and cosine problems.
* Removal of the axiom arctan(0) = 0 and similar axioms for tan, arcsin, cosh, sinh, tanh.
They were never used in proofs (empirically) but could slow down the search.
* Removal of the constant pi from the axioms for arctan.
MetiTarski release 1.7 2010-11-01
* Corrected a serious parsing bug, ensuring that -X^2 is parsed as -(X^2) and not as (-X)^2!
* Corrected a serious error in the file atan-extended.ax, where the axiom atan_upper_bound_case_41
did not hold when X=0!
* Added the functions cbrt (cube roots), arcsin and arccos.
* New option --time to limit the processor time used in the proof attempt.
* New option --tstp to generate standard TSTP output with no infixes or minus signs.
* New option --full to include variable instantiations in proofs.
* New bounds for sqrt, using scaling to improve accuracy near zero and for large arguments.
The old fourth-order bounds have been moved to sqrt-extended.ax.
* Improved bounds for tan, with more problems.
* Corrected the Nichols plot problems (using Maple) and used scaled axioms for sqrt
to solve some of them.
* Added parallelism to the script runmetit.pl, via the option --threads.
* Many more new problems.
MetiTarski release 1.6 2010-09-09
* Corrected a serious error in the file ln-extended.ax: the lower bounds were identical to
the upper bounds!
* Introduced a cache for QEPCAD calls, eliminating duplicates and improving performance.
* Many more new problems.
MetiTarski release 1.5 2010-07-23
* Modifications to heuristics, e.g., now all new clauses receive arithmetic simplification.
* Efficiency improvements, in particular, direct support for rational numbers as constants.
* Faster set and map data structures, supplied by Joe Hurd.
* Corrected the log error analysis problems (using Maple). Added a few other problems.
MetiTarski release 1.4 26-05-2010
* Experimental and limited support for problems involving existential quantifiers.
* Direct upper/lower bounds for the functions tan, sinh, cosh (which previously expanded to expressions involving other functions).
* Support for the hyperbolic function tanh, with some problems.
* Reports status GaveUp rather than CounterSatisfiable when the search fails, because the algorithms are incomplete.
* The "include" directive now allows absolute path names, which begin with a "/".
* Incorporated some code from Metis 2.2 (release 20100524).
MetiTarski release 1.3 25-02-2010
* Fixed a bug that caused MetiTarski to hang by sending formulas to QEPCAD
containing the logical constants TRUE or FALSE.
* Fixed a bug that caused MetiTarski to die if the supplied clauses included arithmetic tautologies.
(Both bugs reported by Geoff Sutcliffe.)
* Nine new problems from various sources.
MetiTarski release 1.2 11-08-2009
* Support for the TPTP "include" directive. Also in the accompanying Perl scripts.
* Many new problems on analogue circuit verification, etc., from Concordia University.
* Now detects whether the supplied problem is immediately inconsistent in the theory of real closed fields (useful for problems that, after simplification, no longer contain occurrences of functions).
* New axiom file: trans.ax.
* Improved documentation.
MetiTarski release 1.1 14-01-2009
* Tuning and heuristic improvements, with significantly faster performance.
* The parser now indicates the approximate location of syntax errors. (Thanks to Joe Hurd!)
* Corrected the problem two_variable_problem_6, which needed a quantifier over Y.
MetiTarski release 1.0 02-12-2008
* Corrected serious errors in the exp upper bound definitions.
* Moved the most accurate approximations to separate files of extended bounds in order to improve performance for the harder problems, many of which do not require accuracy at all.
* Refinements to heuristics, particularly concerning case splitting on signs.
* Simplification of some problems, using a maximum of three significant digits for control and hybrid systems.
* Numerous minor adjustments to the axioms, particularly for exponentials.
* Now all problems are in first-order format!
MetiTarski release 0.9 12-09-2008
* Fixed a soundness bug concerning the normalisation of quotients.
* Corrected serious errors in the atan upper bound definitions.
* Improved bounds for the atan and log functions using continued fractions.
* Improved reasoning about rational numbers (they are smaller than Skolem constants in KBO).
* Eliminated the axiom file division.ax, combining it with general.ax.
* Added Nichols Plot problems.
* More of the problems have been converted to first-order format.
MetiTarski release 0.8 22-08-2008
* More of the problems have been converted to first-order format.
* Introduction of decimal notation: a decimal such as 1.23 abbreviates the fraction 123/100.
* Many of the problems have been converted into first-order format, with decimal notation.
* Improved bounds for the atan (arctangent) function, based on continued fractions. Many thanks to Annie Cuyt!
* Improved simplification so that quotients whose operands are complicated numerical expressions are guaranteed to be evaluated.
MetiTarski release 0.7 29-07-2008
* First public release.