mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
036c6ce5b8
in a series of tests on available examples, lightweight polymorphism encoding techniques combined with a more agressive generation of monomorphic instances (via Discriminate) show better results than our earlier defaults. In the same commit: - remove Encoding_explicit (unsound), Encoding_decoexp (too naive), and Encoding_instantiate (subsumed by Discriminate) - rename Encoding_decorate to Encoding_tags_full and Encoding_guard to Encoding_guards_full - move Encoding_guards_full specific functions from Libencoding to Encoding_guards_full - do not apply type protection in "encoding_tptp" and remove Protect_finite which is not needed anymore.
7 lines
121 B
Plaintext
7 lines
121 B
Plaintext
(* Why driver for first-order tptp provers *)
|
|
|
|
timeout "Time Out Virtual"
|
|
|
|
import "tptp.gen"
|
|
import "discrimination.gen"
|