CODEWITHSUNDEEP
z3z3pytheorem-proving
tridu33
tridu33

Reputation: 11

How can I get constants and specific instances of Uninterpreted sort under Z3 Solver/theorem prover?

x_instance = IntVal('3')
x_uninterpred_const1 = Const("x",IntSort())
x_uninterpred_const2 = Int("x")# syntax sugar for the former line above

In Z3, we use the term "variable" for universal and existential variables. Quantifier-free formulas do not contain variables, only constants. But at least we can get an int_instance with the value three at the same time.

Then when I use Z3 for Blockworld, I have found this:

BlockType, (block1,block2) = EnumSort('Block', ('block1','block2'))
x, y, z, w = Consts('x y z w', BlockType)

I think this means, constants "x, y, z, w" can be either block1 or block2, it depends on what constraint we set for the next Solver().add(), but now I want constants "x, y, z, w" to be countless blocks even I have not "Enum" all possible block instance like "A, B, C, D,..." yet.

But now I just have two specific block instance name "block1,block2". How can I get this in Z3 solver? (Just like the IntVal("3") and IntSort constant above)

I wrote the code below, but I don't think it is right:

BlockType = DeclareSort('Block type')#Uninterpreted or free Sorts"BlockType", 
block1, block2 = Consts('blockinstance1 blockinstance2',BlockType) #this seems wrong but I do not know how to write. #I do not how to get this: I want two specific block but not constants(a.k.a variables of BlockType)
x, y, z, w = Consts('x y z w', BlockType) # constants(a.k.a variables of BlockType)

Upvotes: 0

Views: 273

Answers (1)

alias
alias

Reputation: 30460

It's not quite clear to me what exactly you're asking, but it appears you want to have an enum constant that's always fixed at one value? (Akin to what IntVal does for integers.)

To do so, simply assert the equality in the solver:

from z3 import *

BlockType, (block1,block2) = EnumSort('Block', ('block1', 'block2'))

s = Solver()
x = Const('x', BlockType)
s.add(x == block1)
print(s.check())
print(s.model())

This prints:

sat
[x = block1]

Upvotes: 1

Related Questions