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
141
/*
* 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 ResultSubstitution.hpp
* Defines class ResultSubstitution.
*/
#ifndef __ResultSubstitution__
#define __ResultSubstitution__
#include "Forwards.hpp"
#include "Kernel/Term.hpp"
#include "Kernel/Renaming.hpp"
namespace Indexing {
using namespace Kernel;
/**
* Represents a substitution, that has been retrieved from an
* indexing structure.
*
* It distinguishes two classes of terms/literals --
* query and result ones. Variables in query
* terms/literals have the same meaning as variables in query
* that was the indexing structure asked, and variables in
* result terms/literals have the meaning of variables in the
* term/literal that was retrieved from the index.
*/
class ResultSubstitution
{
public:
virtual ~ResultSubstitution() {}
virtual TermList applyToQuery(TermList t) { NOT_IMPLEMENTED; }
virtual Literal* applyToQuery(Literal* l) { NOT_IMPLEMENTED; }
virtual TypedTermList applyToQuery(TypedTermList t) { return TypedTermList(applyToQuery(TermList(t)), applyToQuery(t.sort())); }
virtual TermList applyToResult(TermList t) { NOT_IMPLEMENTED; }
virtual Literal* applyToResult(Literal* l) { NOT_IMPLEMENTED; }
virtual TypedTermList applyToResult(TypedTermList t) { return TypedTermList(applyToResult(TermList(t)), applyToResult(t.sort())); }
virtual TermList applyTo(TermList t, unsigned index) { ASSERTION_VIOLATION; }
virtual Literal* applyTo(Literal* l, unsigned index) { NOT_IMPLEMENTED; }
/** if implementation cannot easily give result for this, zero is returned */
virtual size_t getQueryApplicationWeight(TermList t) { return 0; }
/** if implementation cannot easily give result for this, zero is returned */
virtual size_t getQueryApplicationWeight(Literal* l) { return 0; }
/** if implementation cannot easily give result for this, zero is returned */
virtual size_t getResultApplicationWeight(TermList t) { return 0; }
/** if implementation cannot easily give result for this, zero is returned */
virtual size_t getResultApplicationWeight(Literal* l) { return 0; }
template<typename T>
T apply(T t, bool result)
{
if(result) {
return applyToResult(t);
} else {
return applyToQuery(t);
}
}
bool isRenamingOn(TermList t, bool result);
/** if implementation cannot easily give result for this, zero is returned */
template<typename T>
size_t getApplicationWeight(T t, bool result)
{
if(result) {
return getResultApplicationWeight(t);
} else {
return getQueryApplicationWeight(t);
}
}
virtual TermList applyToBoundResult(unsigned v)
{ return applyToResult(TermList::var(v)); }
/**
* Apply substitution to result term that fulfills the condition,
* that all its variables are bound to some term of the query.
*
* Applying this substitution makes sense, when
* @b isIdentityOnQueryWhenResultBound() method returns true,
* as then there's no need to apply the substitution to any
* query terms.
*/
virtual TermList applyToBoundResult(TermList t)
{ return applyToResult(t); }
/**
* Same as @b applyToBoundResult(TermList) with @b Literal argument.
*/
virtual Literal* applyToBoundResult(Literal* lit)
{ return applyToResult(lit); }
/**
* Return true if, when the substitution is applied to a result
* term through the @b applyToBoundResult function, the corresponding
* substitution for query terms is identity.
*/
virtual bool isIdentityOnQueryWhenResultBound() {return false;}
/**
* Apply substitution to query term that fulfills the condition,
* that all its variables are bound to some term of the result.
*
* Applying this substitution makes sense, when
* @b isIdentityOnResultWhenQueryBound() method returns true,
* as then there is no need to apply the substitution to any
* result terms.
*/
virtual TermList applyToBoundQuery(TermList t)
{ return applyToQuery(t); }
/**
* Return true if, when the substitution is applied to a query
* term through the @b applyToBoundQuery function, the corresponding
* substitution for query terms is identity.
*/
virtual bool isIdentityOnResultWhenQueryBound() {return false;}
static ResultSubstitutionSP fromSubstitution(RobSubstitution* s, int queryBank, int resultBank);
virtual void output(std::ostream& ) const = 0;
friend std::ostream& operator<<(std::ostream& out, ResultSubstitution const& self)
{ self.output(out); return out; }
};
}; // namespace Indexing
#endif /* __ResultSubstitution__ */