Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Harco Kuppens
z3gi
Commits
462be62d
Commit
462be62d
authored
Jun 25, 2020
by
Harco Kuppens
Browse files
remove unchecked code from master
parent
f2bde74a
Changes
1
Hide whitespace changes
Inline
Side-by-side
constraints.py
deleted
100644 → 0
View file @
f2bde74a
# "def axioms" and "def observations" are contained in encode module
def
axioms
(
self
,
ra
:
RegisterAutomaton
,
mapper
:
Mapper
):
l
=
z3
.
Const
(
'l'
,
ra
.
Label
)
q
,
qp
=
z3
.
Consts
(
'q qp'
,
ra
.
Location
)
r
,
rp
=
z3
.
Consts
(
'r rp'
,
ra
.
Register
)
# Z3 cannot handle higher order concepts
# Given any guard, we may replace the
# first occurrence of a variable by $v_1$, the second by $v_2$, etc. We callthe result a \emph{guard pattern}.
# For instance, the guard $v_3 < v_4\wedge v_4 \geq v_5$ has guard pattern $v_1 < v_2 \wedge v_3 \geq v_4$.
# Each guard pattern has an arity, which is the number of variables occurring in it.
# Now each guard can be represented by a pair of its guard pattern and an array of variables of length its arity.
# For instance, the above guard is represented by the pair $(v_1 < v_2 \wedge v_3 \geq v_4 , [v_3, v_4, v_4, v_5])$.
# Now in our Z3 encoding we postulate an uninterpreted set ofguard patterns GP,
# we represent variable vi just by the number i.
# we postulate a function arity : GP $\rightarrow \mathbb{N}$, and represent guards as pairs of a guard pattern P
# and an array of length $arity(P)$.
I
=
IntSort
()
L_1
=
Array
(
'L_1'
,
I
,
I
)
L_2
=
Array
(
'L_2'
,
I
,
I
)
i
=
Int
(
'i'
)
axioms
=
[
z3
.
Implies
(
\
map_r
(
w
,
L_1
[
i
])
=
\
map_r
(
w
,
L_2
[
i
]),
L_1
[
i
]
==
L_2
[
i
]
),
z3
.
Implies
(
\
map_t
(
w_1
a_1
G_1
)
==
\
map_t
(
w_2
a_2
G_2
),
\
map_l
(
w_1
)
=
\
map_l
(
w_2
)
),
z3
.
Implies
(
\
map_t
(
w_1
a_1
G_1
)
==
\
map_t
(
w_2
a_2
G_2
),
(
a_1
==
a_2
)
),
z3
.
Implies
(
z3
.
Or
(
z3
.
Implies
(
L_1
(
i
)
==
length
(
w_1
),
L_2
(
i
)
==
length
(
w_2
)
),
\
map_r
(
w_1
,
L_1
(
i
))
==
\
map_r
(
w_2
,
L_2
(
i
)
),
P_1
==
P_2
),
Z3
.
Implies
(
\
map_t
(
w_1
)
==
\
map_t
(
w_2
),
\
map_l
(
w_1
)
==
\
map_l
(
w_2
)
),
z3
.
Implies
(
z3
.
And
(
\
map_t
(
w_1
)
==
\
map_t
(
w_2
),
\
map_r
(
w_1
,
length
(
w_1
))
==
\
map_r
(
w_1
,
length
(
w_1
))
),
\
map_r
(
w_1
,
length
(
w_2
))
==
\
map_r
(
w_2
,
length
(
w_1
))
),
z3
.
Implies
(
z3
.
And
(
\
map_t
(
u_1
)
==
\
map_t
(
u_2
),
u_1
==
w_1a_1P_1L_1
,
u_2
==
w_2a_2P_2L_2
,
\
map_r
(
w_1
,
L_1
[
i
])
==
\
map_r
(
w_2
,
L_2
[
i
]),
\
map_r
(
u_1
,
L_1
[
i
])
==
\
map_r
(
u_1
,
L_1
[
i
])
),
\
map_r
(
u_1
,
L_1
[
i
])
==
\
map_r
(
u_2
,
L_2
[
i
])
),
z3
.
Implies
(
z3
.
And
(
\
map_t
(
u_1
)
==
\
map_t
(
u_2
),
u_1
==
w_1a_1P_1L_1
,
u_2
==
w_2a_2P_2L_2
,
\
map_r
(
u_1
,
L_1
[
i
])
==
\
map_r
(
u_2
,
L_2
[
i
]),
L_1
[
i
]
!=
length
(
u_2
)
),
\
map_r
(
w_1
,
L_1
[
i
])
==
\
map_r
(
w_2
,
L_2
[
i
])
),
z3
.
Implies
(
z3
.
And
(
\
map_l
(
w_1
)
=
\
map_l
(
w_2
),
\
lambda
(
\
map_l
(
w_1a_1
P_1
L_1
))
==
true
,
# it may need to change
L_1
[
i
]
!=
length
(
w_1a_1
P_1
L_1
)
),
\
map_r
(
w_1
,
L_1
[
i
])
=
\
map_r
(
w_2
,
L_2
[
i
])
),
]
return
axioms
def
observations
(
self
,
ra
:
RegisterAutomaton
,
mapper
:
Mapper
):
constraints
=
[
dfa
.
start
==
mapper
.
map_l
(
mapper
.
start
)]
# following three statements are depending on the representation of the observation tree - it may need to change
for
node
,
label
in
self
.
tree
.
transitions
():
x
=
mapper
.
element
(
node
.
id
)
l
=
dfa
.
labels
[
label
]
observations
=
[
z3
.
Forall
(
[
xl
,
x
'l],
z3.Implies(
\map_l(x) = \map_l(x'
),
\
map_l
(
xl
)
=
\
map_l
(
x
' l)
)
),
z3.Forall(
[x, x'
],
z3
.
Implies
(
\
map
(
x
)
=
\
map
(
x
'),
x \in S^+ \Leftrightarrow x'
\
in
S
^+
)
# How to conver this statement into python?
)
)
]
return
observations
# control goes to ""define module"" from ""build method"" of encode module and returns
#into ""ra"" and "mapper".
# following class is from encode module
class
RAEncoder
(
Encoder
):
def
build
(
self
,
num_locations
,
num_registers
)
->
(
RegisterAutomaton
,
z3
.
ExprRef
):
ra
=
RegisterAutomaton
(
list
(
self
.
labels
),
self
.
param_size
,
num_locations
,
num_registers
)
# Goes to encode module and returns "ra".
mapper
=
Mapper
(
ra
)
# Goes to encode module and returns "mapper".
constraints
=
self
.
axioms
(
ra
,
mapper
)
+
\
self
.
observation_constraints
(
ra
,
mapper
)
+
\
# self.size_constraints(ra, mapper)
return
ra
,
constraints
class
RegisterAutomaton
(
RegisterMachine
):
def
__init__
(
self
,
labels
,
param_size
,
num_locations
,
num_registers
):
super
().
__init__
(
num_locations
,
num_registers
,
param_size
)
self
.
Label
,
elements
=
dt_enum
(
'Label'
,
labels
)
self
.
labels
=
{
labels
[
i
]:
elements
[
i
]
for
i
in
range
(
len
(
labels
))}
self
.
start
=
self
.
locations
[
0
]
# self.fresh = self.registers[-1]
self
.
observation
=
z3
.
Function
(
'observation'
,
self
.
State
,
self
.
Label
,
self
.
State
)
class
Mapper
(
object
):
# control comes from encode file and returns into ""mapper""
def
__init__
(
self
,
ra
):
self
.
Value
=
z3
.
DeclareSort
(
'Value'
)
self
.
Element
=
z3
.
DeclareSort
(
'Element'
)
self
.
start
=
self
.
element
(
0
)
self
.
init
=
self
.
value
(
"_"
)
self
.
map_l
=
z3
.
Function
(
'map_l'
,
self
.
Element
,
ra
.
Location
)
# paper : $\map_l : Q^T \rightarrow Q^A$
self
.
map_t
=
z3
.
Function
(
'map_t'
,
self
.
Element
,
ra
.
transition
)
# paper : \map_t : Q^T \setminus \{ \epsilon \} \rightarrow \Gamma^A$
self
.
map_r
=
z3
.
Function
(
'map_r'
,
self
.
Location
,
?
,
?
)
# paper : $\map_r : Q^T \times \mathbb{N} \rightarrow \V$
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment