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
|
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
|
-
+
-
+
+
+
+
+
-
+
+
+
+
-
-
-
-
+
-
-
+
|
uint32_t createValue();
void setLHSHoleIndex( const StringId& name, uint32_t index );
void setRHSHoleIndex( const StringId& name, uint32_t index );
const optional< Term >& getValue( uint32_t index ) const
{
assert( m_values.size() > index );
return m_values[index];
return m_values[index].first;
}
void setValue( uint32_t index, Term&& val );
void setValue( uint32_t index, Term&& val, uint32_t complexity );
UnificationContext& flip()
{
swap( m_currentLHSNamespaceIndex, m_currentRHSNamespaceIndex );
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_pHoleDict->size() ); }
private:
ptr< UnificationRuleSet > m_rules;
immer::vector< optional< Term > > m_values;
struct cow
{
unordered_map< HoleName, uint32_t > m_holes;
};
ptr< cow > m_pCoW = make_shared< cow >();
ptr< HoleDict > m_pHoleDict = make_shared< HoleDict >();
};
}
#endif
|