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
|
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];
}
void setValue( uint32_t index, Term&& val );
UnificationContext& flip()
{
swap( m_currentLHSNamespaceIndex, m_currentRHSNamespaceIndex );
return *this;
}
uint32_t numUnknownValues() const { return m_numUnknownValues; }
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 >();
};
}
#endif
|
|
|
>
>
>
>
|
>
>
>
<
<
<
|
<
|
|
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].first;
}
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;
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 >;
using HoleDict = unordered_map< HoleName, uint32_t >;
ptr< HoleDict > m_pHoleDict = make_shared< HoleDict >();
};
}
#endif
|