vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */
/**
 * @file TermIndex.hpp
 * Defines class TermIndex.
 */


#ifndef __TermIndex__
#define __TermIndex__

#include "Index.hpp"
#include "TermIndexingStructure.hpp"

namespace Indexing {

template<class Data>
class TermIndex
: public Index
{
public:
  ~TermIndex() override {}

  VirtualIterator<QueryRes<AbstractingUnifier*, Data>> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration)
  { return _is->getUwa(t, uwa, fixedPointIteration); }

  VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getUnifications(TypedTermList t, bool retrieveSubstitutions = true)
  { return _is->getUnifications(t, retrieveSubstitutions); }

  VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true)
  { return _is->getGeneralizations(t, retrieveSubstitutions); }

  VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getInstances(TypedTermList t, bool retrieveSubstitutions = true)
  { return _is->getInstances(t, retrieveSubstitutions); }

  friend std::ostream& operator<<(std::ostream& out, TermIndex const& self)
  { return out << *self._is; }
protected:
  TermIndex(TermIndexingStructure<Data>* is) : _is(is) {}

  std::unique_ptr<TermIndexingStructure<Data>> _is;
};

class SuperpositionSubtermIndex
: public TermIndex<TermLiteralClause>
{
public:
  SuperpositionSubtermIndex(SaturationAlgorithm& salg);
protected:
  void handleClause(Clause* c, bool adding) override;
private:
  Ordering& _ord;
};

class SuperpositionLHSIndex
: public TermIndex<TermLiteralClause>
{
public:
  SuperpositionLHSIndex(SaturationAlgorithm& salg);
protected:
  void handleClause(Clause* c, bool adding) override;
private:
  Ordering& _ord;
  const Options& _opt;
};

/**
 * Term index for backward demodulation
 */
class DemodulationSubtermIndex
: public TermIndex<TermLiteralClause>
{
public:
  DemodulationSubtermIndex(SaturationAlgorithm& salg);
protected:
  void handleClause(Clause* c, bool adding) override;
private:
  const bool _skipNonequationalLiterals;
};

/**
 * Term index for forward demodulation
 */
class DemodulationLHSIndex
: public TermIndex<DemodulatorData>
{
public:
  DemodulationLHSIndex(SaturationAlgorithm& salg);
protected:
  void handleClause(Clause* c, bool adding) override;
private:
  Ordering& _ord;
  const bool _preordered;
};

/**
 * Term index for induction
 */
class InductionTermIndex
: public TermIndex<TermLiteralClause>
{
public:
  InductionTermIndex(SaturationAlgorithm& salg);
protected:
  void handleClause(Clause* c, bool adding) override;
private:
  const bool _inductionGroundOnly;
};

/**
 * Term index for structural induction
 */
class StructInductionTermIndex
: public TermIndex<TermLiteralClause>
{
public:
  StructInductionTermIndex(SaturationAlgorithm& salg);
protected:
  void handleClause(Clause* c, bool adding) override;
private:
  const bool _inductionGroundOnly;
};

class SkolemisingFormulaIndex
: public TermIndex<TermWithValue<TermList>>
{
public:
  SkolemisingFormulaIndex(SaturationAlgorithm&);
  void insertFormula(TermList formula, TermList skolem);
};

} // namespace Indexing
#endif /* __TermIndex__ */