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
/*
* 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 PartialOrdering.hpp
*/
#ifndef __PartialOrdering__
#define __PartialOrdering__
#include <cstdint>
#include <string>
#include <vector>
namespace Kernel {
/** This corresponds to the values we can handle between two elements.
* Note that incomparability is also possible, namely ≱ (NGEQ),
* ≰ (NLEQ) and their conjunction (INCOMPARABLE). */
enum class PoComp : std::uint8_t {
UNKNOWN,
GREATER,
EQUAL,
LESS,
NGEQ,
NLEQ,
INCOMPARABLE,
};
bool checkCompatibility(PoComp old, PoComp curr, PoComp& res);
std::string pocompToInfix(PoComp c);
/**
* Partial ordering between elements of some set.
*
* We initially have an empty relation, and we extend this by
* maintaining a triangular array where each entry is a @b PoComp
* value. After each extension we compute the transitive closure
* of the current relation. Assuming this was done for the previous
* relation, it is enough to compute what has become "connected"
* through the newly added value. In certain cases, this extension
* fails as the new relation would be contradictory. This state
* is represented by a null partial ordering.
*
* The set elements are denoted by IDs inside the class, which is
* given by order of appearance, as explained below. The set
* elements are abstracted via these IDs to increase sharing among
* partial ordering objects. Hence, operations modifying the
* objects are performed through static methods, and we get shared
* heap-allocated objects, or null if the operation fails.
*/
class PartialOrdering
{
public:
/** Get relation between two elements with IDs @b x and @b y. */
PoComp get(size_t x, size_t y) const;
bool isGround() const { return _isGround; }
/** Get empty partial ordering. */
static const PartialOrdering* getEmpty();
/** Add new element to partial ordering. The ID of this
* element is set to @b _size-1 of the new partial ordering. */
static const PartialOrdering* extend(const PartialOrdering* po);
/** Tries to set relation between two elements with IDs @b x and @b y,
* and performs transitive closure over the entire set so far.
* If this fails, returns null, otherwise returns a non-null object. */
static const PartialOrdering* set(const PartialOrdering* po, size_t x, size_t y, PoComp v);
/** Reset static caches (for library use when running multiple proofs) */
static void resetStaticCaches();
friend std::ostream& operator<<(std::ostream& str, const PartialOrdering& po);
private:
PartialOrdering() = default;
~PartialOrdering() = default;
PartialOrdering(const PartialOrdering&) = default;
PartialOrdering& operator=(const PartialOrdering&) = delete;
void extend();
PoComp getUnsafe(size_t x, size_t y) const;
bool setRel(size_t x, size_t y, PoComp v, bool& changed);
bool setRelSafe(size_t x, size_t y, PoComp v, bool& changed);
bool setInferred(size_t x, size_t y, PoComp result);
bool setInferredHelper(size_t x, size_t y, PoComp rel);
bool setInferredHelperInc(size_t x, size_t y, PoComp wkn);
bool setInferredHelperEq(size_t x, size_t y);
size_t _size = 0;
std::vector<PoComp> _array;
bool _isGround = true;
};
};
#endif /* __PartialOrdering__ */