• Andrei Paskevich's avatar
    change default polymorphism encoding methods · 036c6ce5
    Andrei Paskevich authored
    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.
    036c6ce5
iprover.drv 121 Bytes