Problem with setting the bound variable for a quantified formula #6264
Unanswered
daneshvar-amrollahi
asked this question in
Q&A
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Hi,
I am trying to implement a quantified expression using Z3's C API in KLEE.
Here is the Z3_ast representing the body of my quantifier:
which is basically this:
({a3[fqv1[3:0]+3], a3[fqv1[3:0]+2], a3[fqv1[3:0]+1], a3[fqv1[3:0]+0]} = {b4[fqv1[3:0]+3], b4[fqv1[3:0]+2], b4[fqv1[3:0]+1], b4[fqv1[3:0]+0]})
where{x1, ..., xn}
is my self-made notation for the concatenation of x1, ..., xn.It is saying that the concatenation of 4 bytes at index fqv1 in arrays a3 and b4 should be equal.
My question is, how am I supposed to set the bound variable correctly? As far as I understood, we can create quantified formulas using Z3's C API with
Z3_mk_forall
andZ3_mk_forall_const
. Both of these require me to set asort
for my bound variable.Is this the correct way of doing this?
The forall expression created by Z3 using the above method is:
The
fqv
as the bound variable, does not seem to be the same asfqv1
in the body. Am I understanding this correctly?How can I make this happen? Can I force
fqv
to be equal tofqv1
by adding an equality constraint?The point is that KLEE creates this complicated representation for the body involving concatenations (Even for single integers where we don't have arrays), and I am forced to set the bound variable to something suitable to match the variable in the created body.
Can I somehow extract the
fqv1
from the body and set it as the bound variable?I am sorry if this question is a bit complicated or naive. Please let me know if you need any other info on this.
Beta Was this translation helpful? Give feedback.
All reactions