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
|
return *this;
}
void incComplexity( uint32_t n = 1 ) { m_complexity += n; }
uint32_t numUnknownValues() const { return m_numUnknownValues; }
uint32_t complexity() const { return m_complexity; }
auto score() const { return UnificationScore( m_complexity, m_pCow->holeDict.size() ); }
// Used to detect and reject recursive hole nesting.
bool isHoleLocked( uint32_t index ) const;
void lockHole( uint32_t index );
void unlockHole( uint32_t index );
private:
Context m_context;
using StoredValue = pair< optional< Term >, uint32_t >;
immer::vector< StoredValue > m_values;
uint32_t m_currentLHSNamespaceIndex = 1;
uint32_t m_currentRHSNamespaceIndex = 2;
uint32_t m_numUnknownValues = 0;
uint32_t m_complexity = 0;
using HoleName = pair< StringId, uint32_t >;
struct Cow
{
unordered_map< HoleName, uint32_t > holeDict;
unordered_set< uint32_t > lockedHoles;
|
|
>
>
|
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
|
return *this;
}
void incComplexity( uint32_t n = 1 ) { m_complexity += n; }
uint32_t numUnknownValues() const { return m_numUnknownValues; }
uint32_t complexity() const { return m_complexity; }
auto score() const { return UnificationScore( m_complexity, m_pCow->holeDict.size() + m_numAnonymousHoles ); }
// Used to detect and reject recursive hole nesting.
bool isHoleLocked( uint32_t index ) const;
void lockHole( uint32_t index );
void unlockHole( uint32_t index );
private:
Context m_context;
using StoredValue = pair< optional< Term >, uint32_t >;
immer::vector< StoredValue > m_values;
uint32_t m_currentLHSNamespaceIndex = 1;
uint32_t m_currentRHSNamespaceIndex = 2;
uint32_t m_numUnknownValues = 0;
uint32_t m_complexity = 0;
uint32_t m_numAnonymousHoles = 0;
using HoleName = pair< StringId, uint32_t >;
struct Cow
{
unordered_map< HoleName, uint32_t > holeDict;
unordered_set< uint32_t > lockedHoles;
|