repository·master·Indexed 19 days ago
https://github.com/vprover/vampireAn advanced tool for automated reasoning and theorem proving that accepts problems in TPTP format. It utilizes various strategies, SAT/SMT solvers, and portfolio modes such as Cascading (`--mode casc`) and Satisfiable-focused Cascading (`--mode casc_sat`) to find proofs or determine satisfiability. The tool includes an indexing API allowing for custom Index implementations via the `Indexing::Index` class and `LeafData` types.
You can obtain Vampire in two ways:
Vampire supports different execution modes that act as shortcuts for complex strategy combinations. Using portfolio modes often yields better performance than the default mode.
--mode casc): Tries many different strategies. This is a shortcut for --mode portfolio --schedule casc --proof tptp.--mode casc_sat): Uses a set of strategies specifically suited for problems that are satisfiable.# Try many different strategies
$ vampire --mode casc problem.p
# Use strategies suited for satisfiable problems
$ vampire --mode casc_sat problem.pTo run Vampire on a problem file, ensure your problem is saved in TPTP format. Running the command without specific mode flags will execute Vampire in its default mode with a 60-second time limit.
$ vampire problem.pIndices in Vampire are parameterized by a LeafData type. For a type to be used as LeafData, it must satisfy the following requirements:
Key const& key() const method.Literal* or a TypedTermList.<=, <, >=, >, !=, and ==.Commonly used leaf data structures provided in the API include:
LiteralClause: Maps a Literal* to a Clause*.TermWithValue<Value>: Maps a TypedTermList to an arbitrary Value.TermLiteralClause: Maps a TypedTermList to a Literal* and a Clause*.DemodulatorData: A specialized structure for forward demodulation containing the term, RHS, clause, and ordering information.To see the complete list of available command-line options and flags, use the --show_options on flag.
$ vampire --show_options onThe Indexing::TermWithValue<Value> template allows you to associate a TypedTermList with any user-defined value. This is useful when you want to index terms and retrieve associated metadata during a query.
TermWithoutValue is a convenience alias for TermWithValue<std::tuple<>> used when you only need to index the term itself without extra data.
struct MyMetadata { int id; };
// Create a mapping from TypedTermList to MyMetadata
Indexing::TermWithValue<MyMetadata> entry(someTypedTermList, MyMetadata{42});
// Access the key (the term)
const auto& term = entry.key();
// Access the value
const auto& meta = entry.term.value;To create a custom index, inherit from the Indexing::Index class and implement the protected virtual method handleClause(Clause* c, bool adding).
The Index class provides hooks for managing clause lifecycle via a ClauseContainer. When a clause is added to or removed from the container, the index is notified through onAddedToContainer and onRemovedFromContainer, which in turn call your implementation of handleClause.
c: The pointer to the Clause being processed.adding: A boolean indicating whether the clause is being added (true) or removed (false) from the container.class MyCustomIndex : public Indexing::Index {
protected:
void handleClause(Clause* c, bool adding) override {
if (adding) {
// Logic to add clause c to your index
} else {
// Logic to remove clause c from your index
}
}
};
// Usage:
MyCustomIndex myIndex;
ClauseContainer container;
myIndex.attachContainer(&container);
// Now, adding clauses to 'container' will trigger 'handleClause' in 'myIndex'When performing queries against an index, results are returned as a Indexing::QueryRes<Unifier, Data> object. This object encapsulates both the data found in the index and the unifier required to apply the match.
unifier: The Unifier object representing the substitution found.data: A pointer to the Data (the LeafData) found in the index.// Example of what a query result looks like
// QueryRes<MyUnifier, MyLeafData> result = ...;
if (result.data != nullptr) {
// Use the unifier and the data
auto myData = *(result.data);
apply(result.unifier, myData);
}The following structures are provided for common indexing tasks. They all implement the necessary comparison operators and key() methods required for use in an Index.
struct LiteralClause {
Literal* const& key() const;
Literal* literal;
Clause* clause;
};
template<class Value>
struct TermWithValue {
TypedTermList const& key() const;
TypedTermList term;
Value value;
};
struct TermLiteralClause {
TypedTermList const& key() const;
TypedTermList term;
Literal* literal;
Clause* clause;
};
struct DemodulatorData {
TypedTermList const& key() const;
TypedTermList term;
TermList rhs;
Clause* clause;
bool preordered;
TermOrderingDiagramUP tod;
};The starexec_run_casc script is a wrapper used to execute Vampire in casc mode. It automatically detects the input language from the provided file and selects the appropriate executable (vampire-ho for thf syntax or vampire for other TPTP syntaxes).
It uses the following fixed configuration:
--input_syntax tptp--output_axiom_names on--mode casc-m 16384 (Memory limit)--cores 7 (CPU cores)-t $STAREXEC_WALLCLOCK_LIMIT (Time limit, driven by the STAREXEC_WALLCLOCK_LIMIT environment variable)Usage:
./starexec_run_casc <input_file>#!/bin/sh
input_language=`egrep -om1 "^(thf|tff|tcf|fof|cnf)" $1`
if test "$input_language" = "thf"
then
exec ./vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t $STAREXEC_WALLCLOCK_LIMIT $1
else
exec ./vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t $STAREXEC_WALLCLOCK_LIMIT $1
fiThe starexec_run_casc_sat script is a wrapper for executing Vampire in cascaded SAT mode (--mode casc). It is designed to be used within an environment where the STAREXEC_WALLCLOCK_LIMIT environment variable is defined.
This command uses the following configuration:
--input_syntax tptp)--output_axiom_names on)--intent sat)-m 16384)--cores 7)$STAREXEC_WALLCLOCK_LIMIT environment variable.# Usage: ./starexec_run_casc_sat <input_file>
./starexec_run_casc_sat input.tptp