Skip to content

Commit

Permalink
Merge branch 'master' into version_bump
Browse files Browse the repository at this point in the history
  • Loading branch information
marcoeilers committed Jul 26, 2020
2 parents 8b5b693 + 90ee117 commit f8bc593
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 12 deletions.
5 changes: 5 additions & 0 deletions src/nagini_translation/lib/constants.py
Original file line number Diff line number Diff line change
Expand Up @@ -120,13 +120,18 @@
COMBINED_NAME_ACCESSOR,
COMBINED_PREFIX_ACCESSOR,
SINGLE_NAME,
'_is_single',
'_is_combined',
'm', # the following are used in various
'X', # places in the resources/... files.
'Y',
'id',
't',
'g',
'x',
'n',
'n1',
'n2',
'Low',
'key',
'guard',
Expand Down
3 changes: 3 additions & 0 deletions src/nagini_translation/lib/viper_ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -277,6 +277,9 @@ def InhaleExhaleExp(self, inhale, exhale, position, info):
return self.ast.InhaleExhaleExp(inhale, exhale, position, info, self.NoTrafos)

def Assert(self, expr, position, info):
# Avoid generating "assert true" since this will trigger an expensive state consolidation in Silicon.
if isinstance(expr, self.ast.TrueLit):
return self.Seqn([], position, info)
return self.ast.Assert(expr, position, info, self.NoTrafos)

def FullPerm(self, position, info):
Expand Down
39 changes: 27 additions & 12 deletions src/nagini_translation/resources/name_domain.sil
Original file line number Diff line number Diff line change
Expand Up @@ -17,30 +17,45 @@ domain _Name {
function _get_combined_prefix(n: _Name): _Name
function _get_combined_name(n: _Name): _Name
function _get_value(n: _Name): Int

function _name_type(n: _Name): Bool

function _is_single(n: _Name): Bool
function _is_combined(n: _Name): Bool

axiom all_single_or_combined {
forall n: _Name :: n == _single(_get_value(n)) || n == _combine(_get_combined_prefix(n), _get_combined_name(n))
axiom decompose_single {
forall i: Int :: {_single(i)} _get_value(_single(i)) == i
}

axiom single_is_single {
forall i: Int :: {_single(i)} _is_single(_single(i))
axiom compose_single {
forall n: _Name :: { _get_value(n) } _is_single(n) ==> n == _single(_get_value(n))
}

axiom combined_is_not_single {
forall n1: _Name, n2: _Name :: {_combine(n1, n2)} !_is_single(_combine(n1, n2))
axiom type_of_single {
forall i: Int :: {_single(i)} _name_type(_single(i))
}

axiom decompose_single {
forall i: Int :: {_single(i)} _get_value(_single(i)) == i
axiom decompose_combined {
forall n1: _Name, n2: _Name :: {_combine(n1, n2)}
_get_combined_prefix(_combine(n1, n2)) == n1
&&
_get_combined_name(_combine(n1, n2)) == n2
}

axiom compose_combined {
forall n: _Name :: { _get_combined_prefix(n) } { _get_combined_name(n) }
_is_combined(n) ==> n == _combine(_get_combined_prefix(n), _get_combined_name(n))
}

axiom decompose_combined_prefix {
forall n1: _Name, n2: _Name :: {_combine(n1, n2)} _get_combined_prefix(_combine(n1, n2)) == n1
axiom type_of_composed {
forall n1: _Name, n2: _Name :: { _combine(n1, n2) } !_name_type(_combine(n1, n2))
}

axiom decompose_combined_name {
forall n1: _Name, n2: _Name :: {_combine(n1, n2)} _get_combined_name(_combine(n1, n2)) == n2
axiom type_is_single {
forall n: _Name :: { _name_type(n) } _name_type(n) <==> _is_single(n)
}

axiom type_is_combined {
forall n: _Name :: { _name_type(n) } !_name_type(n) <==> _is_combined(n)
}
}

0 comments on commit f8bc593

Please sign in to comment.