• 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
Name
Last commit
Last update
..
alt_ergo.drv Loading commit data...
alt_ergo_0.92.drv Loading commit data...
alt_ergo_0.93.drv Loading commit data...
alt_ergo_0.94.drv Loading commit data...
alt_ergo_bare.drv Loading commit data...
alt_ergo_model.drv Loading commit data...
alt_ergo_smt2.drv Loading commit data...
beagle.drv Loading commit data...
coq-common.gen Loading commit data...
coq-realize.drv Loading commit data...
coq.drv Loading commit data...
coq_8_4.drv Loading commit data...
cvc3.drv Loading commit data...
cvc3_bare.drv Loading commit data...
cvc4.drv Loading commit data...
cvc4_bare.drv Loading commit data...
discrimination.gen Loading commit data...
eprover.drv Loading commit data...
gappa.drv Loading commit data...
iprover.drv Loading commit data...
mathematica.drv Loading commit data...
mathsat.drv Loading commit data...
ocaml.drv Loading commit data...
princess.drv Loading commit data...
pvs-common.gen Loading commit data...
pvs-realize.drv Loading commit data...
pvs.drv Loading commit data...
simplify.drv Loading commit data...
spass.drv Loading commit data...
spass_types.drv Loading commit data...
tptp-tff.drv Loading commit data...
tptp.gen Loading commit data...
vampire.drv Loading commit data...
verit.drv Loading commit data...
why3.drv Loading commit data...
why3_smt.drv Loading commit data...
why3_tptp.drv Loading commit data...
yices.drv Loading commit data...
yices_bare.drv Loading commit data...
z3.drv Loading commit data...
z3_bare.drv Loading commit data...
z3_smtv1.drv Loading commit data...
zenon.drv Loading commit data...