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
/*
* 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 TermAlgebraReasoning.hpp
*
* Inference rules allowing efficient reasoning in the theory of term
* algebras. These rules concerns (dis)equalities between terms of
* sorts marked as term algebra sorts.
*/
#ifndef __TermAlgebraReasoning__
#define __TermAlgebraReasoning__
#include "Forwards.hpp"
#include "Indexing/AcyclicityIndex.hpp"
#include "Inferences/InferenceEngine.hpp"
#include "Kernel/Clause.hpp"
#include "Saturation/SaturationAlgorithm.hpp"
namespace Inferences {
/*
Simplification rule:
f(...) = g(...) \/ A
--------------------
A
Tautology deletion:
f(...) ~= g(...) \/ A
where f and g are different term algebra constructors
*/
class DistinctnessISE
: public ImmediateSimplificationEngine
{
public:
Kernel::Clause* simplify(Kernel::Clause* c) override;
};
/*
Generating rule:
f(s1 ... sn) = f(t1 ... tn) \/ A
--------------------------------
s1 = t1 \/ A
...
sn = tn \/ A
where f is a term algebra constructor of arity n > 1
*/
class InjectivityGIE
: public GeneratingInferenceEngine {
public:
Kernel::ClauseIterator generateClauses(Kernel::Clause* c) override;
private:
struct SubtermIterator;
struct SubtermEqualityFn;
};
/*
Simplification rule:
f(s) = f(t) \/ A
----------------
s = t \/ A
where f is a term algebra constructor of arity 1
*/
class InjectivityISE
: public ImmediateSimplificationEngine
{
public:
Kernel::Clause* simplify(Kernel::Clause* c) override;
};
class NegativeInjectivityISE
: public ImmediateSimplificationEngine
{
public:
Kernel::Clause* simplify(Kernel::Clause* c) override;
private:
bool litCondition(Clause* c, unsigned i);
};
class AcyclicityGIE
: public GeneratingInferenceEngine {
public:
void attach(Saturation::SaturationAlgorithm* salg) override;
void detach() override;
Kernel::ClauseIterator generateClauses(Kernel::Clause *c) override;
private:
struct AcyclicityGenIterator;
struct AcyclicityGenFn;
std::shared_ptr<Indexing::AcyclicityIndex> _acyclIndex;
};
class AcyclicityGIE1
: public GeneratingInferenceEngine {
public:
Kernel::ClauseIterator generateClauses(Kernel::Clause* c) override;
private:
struct SubtermDisequalityFn;
struct LiteralIterator;
struct SubtermDisequalityIterator;
};
};
#endif