mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
41 lines
1.2 KiB
Plaintext
41 lines
1.2 KiB
Plaintext
(* Why driver for first-order tptp provers *)
|
|
|
|
printer "tptp-fof"
|
|
filename "%f-%t-%g.p"
|
|
|
|
valid "PROOF-FOUND"
|
|
timeout "Zenon error: could not find a proof within the time limit"
|
|
outofmemory "Zenon error: could not find a proof within the memory size limit"
|
|
unknown "NO-PROOF" "no proof found"
|
|
time "why3cpulimit time : %s s"
|
|
|
|
(* to be improved *)
|
|
|
|
(* Performed introductions depending on whether counterexamples are
|
|
requested, as said by the meta "get_counterexmp". When this meta
|
|
set, this transformation introduces the model variables that are
|
|
still embedded in the goal. When it is not set, it removes all
|
|
these unused-ce-related variables, even in the context. *)
|
|
transformation "counterexamples_dependent_intros"
|
|
|
|
transformation "inline_trivial"
|
|
|
|
transformation "eliminate_builtin"
|
|
transformation "eliminate_definition"
|
|
transformation "eliminate_inductive"
|
|
transformation "eliminate_if"
|
|
transformation "eliminate_epsilon"
|
|
transformation "eliminate_algebraic"
|
|
transformation "eliminate_literal"
|
|
transformation "eliminate_let"
|
|
|
|
transformation "discriminate"
|
|
transformation "encoding_tptp"
|
|
|
|
theory BuiltIn
|
|
syntax predicate (=) "(%1 = %2)"
|
|
meta "eliminate_algebraic" "no_index"
|
|
end
|
|
|
|
import "discrimination.gen"
|