vampireHO-sledgehammerScheds

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.

Vampire 4.8

This is the 4.8 version submitted to CASC in 2023.

NOTE: This release has only been optimized for the Starexec cluster and does not represent the full capabilities of Vampire. It will be followed up by a full-fledged version in the near future.

There were new schedules developed for FOF, TFA, and UEQ accessible under --mode casc and one new schedule for FNT under --mode casc_sat.

Linked with z3 6ed071b44407cf6623b8d3c0dceb2a8fb7040cee z3-4.9.1

vampireHO-casc2023

This is the higher-order branch of vampire 4.8 (not in master yet) which competed in CASC 2023.

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.

The interesting modes of operation are:

• --cores 8 --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_tptp_hol used in the Higher-order Theorems division of CASC
• --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_slh used in the SLedgeHammer Theorems division there

There is also a likely quite a bit more powerful schedule for sledgehammer schedule under --schedule snake_slh2 that got only fine-tuned after the competition.

SnakeForV4.7+

This is the 4.7 version of Vampire enhanced with randomization.

It includes (an improved version) of the snake schedules which participated at CASC 2022.

Linked with z3 f03d756e086f81f2596157241e0decfb1c982299.

Version 4.7

This is the 4.7 version submitted to SMTCOMP and CASC in 2022.

No major differences to the competition schedules compared to 2021.

Linked with z3 f03d756e086f81f2596157241e0decfb1c982299.

Version 4.6.1 - Sledgehammer Eval

Few fixes and extensions on top of 4.6.1 motivated by a Sledgehammer evaluation on https://martin.desharnais.me/17-provers/2021-11-18/problem-examples.tar.lz
On top of master (106b95b), we also include two experimental schedules sh_hydra_fol and sh_hydra_tf0.

Version 4.6.1

A slight extension of version 4.6 including finished developments since CASC / SMTCOMP 2021 and excluding competition-specific additions to the competition portfolios (available in 4.6).

Version 4.6

This is the 4.6 version submitted to SMTCOMP and CASC in 2021.

For the competitions, we slightly modified the schedules from master taking advantage of new options. This extension of the schedules will probably not propagate to the upcoming 4.6.1, which will represent a stable snapshot of the current master development.

Finally, please note that for compiling with z3 we have currently tested with commit 517d907567f4283ad8b48ff9c2a3f6dce838569e.

Version 4.5.1

This is a slight extension of the 4.5 versions submitted to SMTCOMP and CASC in 2020. Both of those submissions (which differed slightly) had issues that have been fixed.

The SMTCOMP submission had unsoundness issues with Datatypes and in an edge case for some integer reasoning. It should not be used.

The CASC submission had some minor issues in applying some inferences that should not impact proof search that much. But more importantly, it had a significant issue in portfolio mode that caused it to give up before the time limit. It is safe to use that version but it is preferred to use 4.5.1.

Finally, please note that for compiling with z3 we have currently tested with commit 5a1003f6ed10fc65a1cbcd2554f183714c413c7c.

Version 4.5-poly-hol for higher-order and polymorphic problems

This version of Vampire supports FOL with rank-1 polymorphism and (TPTP's TF1) and higher-order logic (THF).

It has diverged somewhat from the main Vampire branch. You should not use this version if you are not interested in TF1 or THF problems e.g. if you want to run on just first-order problems or SMTLIB problems then use the main 4.5.1 release.

This release contains a few minor bug fixes implemented since CASC