Skip to content

vampireHO-sledgehammerScheds
Compare
Choose a tag to compare
@quickbeam123 quickbeam123 released this 13 Sep 16:21
· 964 commits to master since this release
v4.8HO4Sledgahammer
93e8903

This is the higher-order branch of vampire 4.8 (not in master yet) updated after CASC 2023 by a few bug fixes and by adding a final schedule adapted to work well for problems coming from Sledgehammer. All of TFX/TFF, TH0 and TH1 exports are supported.

To access the new schedule(s), one should use

  • --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_slh
    Vampire will automatically dispatch to the corresponding sub-schedule, based on the input dialect: first-order / higher-order, polymorphic / monomorphic.

The compile is only compatible with cmake and it does not make sense to link against z3 here. Use
cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_BUILD_HOL=ON -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON
after cd-ing to your fresh build folder.

Assets 3