GitHub

Vampire 5.1.0

The new Vampire version includes full higher-order reasoning and compliance with GDV (commit 503a7971f569d7a291a22269ab8aa5ad64453240). More details below.

What's Changed

New Contributors

Full Changelog: v5.0.1...v5.1.0

Vampire 5.0.1

Merge pull request #802 from kazarmy/5.0.1-bump
Bump version number to 5.0.1

Vampire 5.0.0

This is very similar to the version that competed in CASC-30.

Pre-built Binaries

We offer pre-built binaries (including Z3) for common platforms below. These are new this release, so please tell us if they don't work for you. A source build is of course still possible - please use the provided tarballs rather than the GitHub sources. The pre-built binaries:

  • are static for Linux systems
  • dynamically link to the C++ runtime on Mac
  • dynamically link to the C++ runtime and to Cygwin on Windows - we provide the Cygwin DLL we linked against, but others may work

Semantic Versioning

This is a major release mostly to coincide with The Vampire Diary (CAV 2025), but we intend to stick to semantic versioning in a very restricted sense from now on:

  • The only supported interface is the default mode and the portfolio mode, --mode portfolio.
  • Supported portfolio schedules are casc and casc_sat, e.g. --schedule casc: this list might be extended to other schedules in the future.
  • The TPTP and SMT-LIB input formats are supported via --input_syntax tptp and --input_syntax smtlib2.
  • The default output and the output flags -p tptp or -om smtcomp or -om ucore are supported.
  • Runtime can be limited (with some margin of error) using -t <seconds>, where <seconds> is a positive integer.
  • Vampire uses one CPU core in its default mode.
  • All other options may break without warning.
  • We do not guarantee solving any particular problem or returning any particular output, only that the above-enumerated ways of calling Vampire remain valid.

Most of our releases will be minor releases because we do not break the above, but may change, add or remove other functionality. Occasional point releases may occur in the event of disaster.

Vampire 4.9

This Vampire is very similar to the version that competed in CASC-J12.

Linked against Z3 4.12.3, commit 79bbbf76d0c123481c8ca05cd3a98939270074d3.

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

Read the original on github.com ↗