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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
/*
* 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 MLMatcher.hpp
* Defines class MLMatcher with methods
* supporting multiliteral matching.
*/
#ifndef __MLMatcher__
#define __MLMatcher__
#include "Forwards.hpp"
#include "Clause.hpp"
#include <unordered_map>
namespace Kernel {
using namespace Lib;
struct MLMatchStats
{
uint64_t numDecisions = 0;
// int numDecisionsAdjusted = 0; // adjusted to "smt-like decisions"
bool result = false; // true iff match was found
};
inline std::ostream& operator<<(std::ostream& os, MLMatchStats const& stats)
{
os << "{ \"numDecisions\": " << stats.numDecisions
<< ", \"result\": " << stats.result
<< " }";
return os;
}
/**
* MLMatcher implements a solver for the multi-literal match problem.
*
* Input: two clauses, a base clause C and an instance clause D.
* Question: Does a substitution θ exist such that Cθ is a subset (or submultiset) of D?
*/
class MLMatcher
{
private:
/**
* Initializes the matcher to the given match problem.
* The matcher will be in a valid (but unmatched) state.
*
* Preconditions:
* - baseLits must have length baseLen
* - alts must have length baseLen (for 0 <= bi < baseLen, the literal baseLits[bi] will be matched against the alternatives in the list alts[bi])
* - All literals in 'alts' must appear in 'instance'.
* - If resolvedLit is not null, multiset must be false. (Hypothesis; not 100% sure if the matching algorithm breaks in that case)
* - No duplicates in baseLits[]
*/
void init(Literal** baseLits,
unsigned baseLen,
Clause* instance,
LiteralList const* const *alts,
Literal* resolvedLit,
bool multiset);
public:
/**
* Constructs an MLMatcher and puts it in an invalid state.
*/
MLMatcher();
void init(Literal** baseLits, unsigned baseLen, Clause* instance, LiteralList const* const *alts, bool multiset = false)
{
init(baseLits, baseLen, instance, alts, nullptr, multiset);
}
void init(Clause* base, Clause* instance, LiteralList const* const *alts, bool multiset = false)
{
init(base->literals(), base->length(), instance, alts, multiset);
}
void init(Literal** baseLits, unsigned baseLen, Clause* instance, LiteralList const* const *alts, Literal* resolvedLit)
{
// NOTE: we need multiset matching for subsumption, but for subsumption resolution it is not necessary
init(baseLits, baseLen, instance, alts, resolvedLit, resolvedLit == nullptr);
}
void init(Clause* base, Clause* instance, LiteralList const* const *alts, Literal* resolvedLit)
{
init(base->literals(), base->length(), instance, alts, resolvedLit);
}
~MLMatcher();
/**
* Finds the next match.
* May only be called if the matcher is in a valid state.
* Return value:
* - True if a match was found. The matcher is now in a valid and matched state.
* - False if no more matches are possible. The matcher is now in an invalid state.
*/
bool nextMatch();
/**
* Returns a bitmap that indicates which alts are currently matched by some base literal.
* May only be called in a matched state (i.e., after nextMatch() has returned true).
* May only be called if the matcher was initialized with resolvedLit == nullptr.
*
* After the function returns:
* outMatchedBitmap[i] == true iff instance[i] is matched by some literal of base
*
* The given vector will be cleared before operating on it.
*/
void getMatchedAltsBitmap(std::vector<bool>& outMatchedBitmap) const;
/**
* Returns the variable bindings due to the current match.
* May only be called in a matched state (i.e., after nextMatch() has returned true).
*/
void getBindings(std::unordered_map<unsigned, TermList>& outBindings) const;
MLMatchStats getStats() const;
// Disallow copy because the internal implementation still uses pointers to the underlying storage and it seems hard to untangle that.
MLMatcher(MLMatcher const&) = delete;
MLMatcher& operator=(MLMatcher const&) = delete;
// Moving works by moving the pointer m_impl
MLMatcher(MLMatcher&&) = default;
MLMatcher& operator=(MLMatcher&&) = default;
private:
class Impl;
std::unique_ptr<Impl> m_impl;
public:
/// Helper function for compatibility to previous code. It uses a shared static instance of MLMatcher::Impl.
static bool canBeMatched(Literal** baseLits, unsigned baseLen, Clause* instance, LiteralList const* const *alts, Literal* resolvedLit, bool multiset);
/// Helper function for compatibility to previous code. It uses a shared static instance of MLMatcher::Impl.
static bool canBeMatched(Clause* base, Clause* instance, LiteralList const* const *alts, Literal* resolvedLit)
{
return canBeMatched(base->literals(), base->length(), instance, alts, resolvedLit, resolvedLit == nullptr);
}
static MLMatchStats getStaticStats();
};
};
#endif /* __MLMatcher__ */