StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
primarykey
Id
12324518
data
AcceptedAnswerId
0
AnswerCount
0
ClosedDate
CommentCount
0
CommunityOwnedDate
CreationDate
2012-09-07T19:52:08.383
FavoriteCount
0
LastActivityDate
2015-12-15T16:51:11.020
LastEditDate
2015-12-15T16:51:11.020
LastEditorUserId
815653
OwnerUserId
841416
ParentId
12253088
PostTypeId
2
Score
3
ViewCount
0
LastEditorDisplayName
text
Body
What you call variables are (technically) called uninterpreted constants in Z3. Values (such as <code>1</code>, <code>true</code>, <code>#x01</code>) are called interpreted constants. So, in principle, a fast way to check whether <code>a</code> is a "variable" can be done using the following piece of code: <pre><code>is_const(a) and a.decl().kind() == Z3_OP_UNINTERPRETED </code></pre> This piece of code works for everything, but datatypes. After trying your example, I realized that Z3 is incorrectly returning <code>Z3_OP_UNINTERPRETED</code> for datatype constructors. I fixed that for Z3 4.2. In the meantime, you can use the following workaround where the function <code>is_datatype_const_value(a)</code> returns <code>True</code> is <code>a</code> is a constant constructor. <pre><code>def is_datatype_sort(s): return s.kind() == Z3_DATATYPE_SORT def is_datatype_constructor(x): s = x.sort() if is_datatype_sort(s): n = s.num_constructors() f = x.decl() for i in range(n): c = s.constructor(i) if eq(c, f): return True return False # Return True if x is a constant constructor, that is, a constructor without arguments. def is_datatype_const_value(x): return is_const(x) and is_datatype_constructor(x) </code></pre> Then, the following code catches all uninterpreted constants: <pre><code> is_const(a) and a.decl().kind() == Z3_OP_UNINTERPRETED and not is_datatype_const_value(a) </code></pre> The following link contains a complete example. <a href="http://rise4fun.com/Z3Py/vjb" rel="nofollow">http://rise4fun.com/Z3Py/vjb</a>
Tags
Title
singulars
PostAcceptedAnswerId
1. This table or related slice is empty.
PostParentId
1. POhow to check if a const in z3 is a variable or a value?
 singulars
 PostTypePostTypeId
 PTQuestion
PostTypePostTypeId
1. PTAnswer
UserLastEditorUserId
1. USzell
UserOwnerUserId
1. USLeonardo de Moura
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. This table or related slice is empty.
PostsParentIdCreationDate
1. This table or related slice is empty.
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
CommentsPostId
1. This table or related slice is empty.

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.