GitLab

corrected bug in tptp parser (associativity)

Since there is no install target in the makefile, and people can
prefer to use why-cpulimit of why2. We must add the bin directory of
why3 in our $Path when we use why3 in order to get this new
why-cpulimit. (Perhaps it can be backported to why2?)

and solvers called by why (with tptp2why output)

tptp2why accepts stdin as a problem

If some goals are specified they are treated in the order of
apparition on the command line. If no goals are specified on the
command line, they are treated in the same order than they appear in
the theory.

Ajout d'un exemple contenant polymorphisme, predicats, inductifs qui
est prouvé instantanément par simplify mais bcp plus long avec les
autres. Peut-on simplifier le but pour améliorer cela?

as an axiom, and then add false as the unique goal

It is very likely to yield errors or to confuse provers.
The tptp driver now accepts a bit more outputs from provers

small fix for neq pretty-printing bug

code is still quite ugly, and more testing is required

simplify_trivial_quantifier va moins sous les triggers (il peut encore remplacer dessous mais pas y trouver d'égalité)

use of why AST in progress for tptp2why, but building a theory still does not work

It should build without problems

(exists x. x=t and F) -> F[t/x]
(forall x. x<>t or F) -> F[t/x]

Cette transformation n'élimine pas les quantifications qui ont des
triggers mais s'applique sous ces derniers. Le but est de pouvoir
éliminer les quantifications inutilement ajoutées lors de eliminate
inductive.

No commit message

why AST and pretty-printing facilities
implementation not yet complete