Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>One way to do this for the integers is with <code>is_int</code> and <code>is_int_value</code>:</p> <pre><code>x = Int('x') print "x types" print is_int(x) # true, is of sort int print is_int_value(x) # false, not a "value" x_ = IntVal(7) print "x_ types" print is_int(x_) # true, is also of sort int print is_int_value(x_) # true, is a value </code></pre> <p>For reals, you can do this using <code>is_real</code> to check the variable sort, and use (the disjunction of) <code>is_algebraic_value</code> and <code>is_rational_value</code> for the values (I didn't see a function like <code>is_real_value</code> in the API, but I think this disjunct will do it). For bitvectors, you can use <code>is_bv_value</code> for values, and <code>is_bv</code> to check the variable sort.</p> <p>The .NET API has <code>Expr.IsNumeral</code>, and you can see how these are implemented in the API here (e.g., <code>Expr.IsIntNum</code> [the equivalent of the Python <code>is_int_value</code>] checks if both <code>Expr.IsNumeral</code> and <code>Expr.IsInt</code> are true): <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/_expr_8cs_source.html" rel="nofollow">http://research.microsoft.com/en-us/um/redmond/projects/z3/_expr_8cs_source.html</a></p> <p>I did not immediately see a way to do this for custom-defined enumeration sorts. As one alternative, you could encode your enum using bitvectors and compare variables / values using <code>is_bv_value</code>. As a better workaround though, you appear to need to use the more general algebraic datatypes and their automatically created "recognizers". The Python API does not seem to properly create the recognizers if you declare them as enum sorts. Here's one way to do it for what's effectively an enum sort (but declared as the more general datatype).</p> <p>Z3Py encoding of the following: <a href="http://rise4fun.com/Z3Py/ELtn" rel="nofollow">http://rise4fun.com/Z3Py/ELtn</a></p> <pre><code>ColorVal = Datatype('ColorVal') ColorVal.declare('white') ColorVal.declare('black') ColorVal = ColorVal.create() mycolor = Const("mycolor", ColorVal) print ColorVal.recognizer(0) # is_white print ColorVal.recognizer(1) # is_black print simplify(ColorVal.is_white(mycolor)) # returns is_white(mycolor) print simplify(ColorVal.is_black(mycolor)) # returns is_black(mycolor) mycolorVal = ColorVal.white # set to value white print simplify(ColorVal.is_white(mycolorVal)) # true print simplify(ColorVal.is_black(mycolorVal)) # false # compare "variable" versus "value" with return of is_white, is_black, etc.: if it gives a boolean value, it's a value, if not, it's a variable print "var vs. value" x = simplify(ColorVal.is_white(mycolor)) print is_true(x) or is_false(x) # returns false, since x is is_white(mycolor) y = simplify(ColorVal.is_white(mycolorVal)) print is_true(y) or is_false(y) # true ColorValEnum, (whiteEnum,blackEnum) = EnumSort("ColorValEnum",["whiteEnum","blackEnum"]) mycolorEnum = Const("mycolorEnum",ColorValEnum) print ColorValEnum.recognizer(0) # is_whiteEnum print ColorValEnum.recognizer(1) # is_blackEnum # it appears that declaring an enum does not properly create the recognizers in the Python API: #print simplify(ColorValEnum.is_whiteEnum(mycolorEnum)) # error: gives DatatypeSortRef instance has no attribute 'is_whiteEnum' #print simplify(ColorValEnum.is_blackEnum(mycolorEnum)) # error: gives DatatypeSortRef instance has no attribute 'is_blackEnum' </code></pre>
    singulars
    1. This table or related slice is empty.
    1. POhow to check if a const in z3 is a variable or a value?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USTaylor
    1. USTaylor
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POhow to check if a const in z3 is a variable or a value?
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    1. COright, for real, ints etc I can use those but not for custom type.
      singulars
      1. PO
      1. USVu Nguyen
    2. COI added way to do this for enums, so long as you declare them as a custom datatype, instead of using EnumSort. It looks like the Python API does not properly create recognizers for the datatype values if you declare them using EnumSort; there's an example of this at the bottom of the new script
      singulars
      1. PO
      1. USTaylor
    3. COhi, thanks, I understand what you did and it would work. But this seems too complicated and probably takes lots of time to do all those checking, i.e. checking if mycolorVal is Colorval.v1 or v2 or v3 .... . I thought z3 would provide a simple way to check if something is a value or variable.
      singulars
      1. PO
      1. USVu Nguyen
 

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.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload