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
/*
* 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 Substitution.hpp
* Defines class Substitution.
*
* @since 08/07/2007 Manchester, flight Manchester-Cork
* @since 30/12/2007 Manchester, reimplemented from scratch using a skip list like structure
* @since 28/05/2025 Southampton, simplify, inline methods, conform to interfaces
*/
#ifndef __Substitution__
#define __Substitution__
#include "Lib/Allocator.hpp"
#include "Lib/DHMap.hpp"
#include "Term.hpp"
namespace Kernel {
/**
* The class Substitution implementing substitutions.
* @since 30/12/2007 Manchester
*
* This is a simple map from variables to terms.
* If you want something with 'banks' to implement renaming variables apart, you probably want RobSubstitution.
*/
class Substitution
{
public:
USE_ALLOCATOR(Substitution)
/**
* Bind `v` to `t`.
* Succeeds and returns true if `v` is either not bound or already bound to `t`.
* Returns false otherwise, leaving the substitution untouched.
*/
bool bind(unsigned v, TermList t) { return _map.findOrInsert(v, t) == t; }
bool bind(unsigned v, Term *t) { return bind(v, TermList(t)); }
/**
* Bind `v` to `t`: `v` must not be bound to anything.
*/
void bindUnbound(unsigned v, TermList t) { ALWAYS(_map.insert(v, t)); }
void bindUnbound(unsigned int v, Term *t) { bindUnbound(v, TermList(t)); }
/**
* Bind `v` to `t`, regardless of what was there before (if anything).
*/
void rebind(unsigned v, TermList t) { _map.set(v,t); }
void rebind(unsigned v, Term *t) { rebind(v, TermList(t)); }
/**
* If @c var is bound, assign binding into @c res and return true.
* Otherwise return false and do nothing.
*/
bool findBinding(unsigned v, TermList &out) const { return _map.find(v, out); }
// variable/term pairs
auto items() { return _map.items(); }
/**
* Return result of application of the substitution to variable @c var
*
* This function is to allow use of the @c Substitution class in the
* methods of the @c SubstHelper class for applying substitutions.
*/
TermList apply(unsigned var) const {
TermList res(var, false);
findBinding(var, res);
return res;
}
void specVar(unsigned var, TermList term) { ASSERTION_VIOLATION; }
void reset() { _map.reset(); }
bool isEmpty() const { return _map.isEmpty(); }
unsigned size() const { return _map.size(); }
friend std::ostream& operator<<(std::ostream& out, Substitution const &self) {
out << '[';
auto items = self._map.items();
bool first = true;
for(auto [x, t] : iterTraits(self._map.items())) {
if(!first)
out << ",";
first = false;
out << x << " -> " << t;
}
return out << ']';
}
private:
DHMap<unsigned,TermList> _map;
}; // class Substitution
} // namespace Kernel
#endif // __Substitution__