Search code examples
z3smtz3py

simple z3 question - why x*x-1==0 does not return both roots

I'm just trying to study z3 and its .NET interface. I'm using PowerShell for that, to make it a bit more interactive. And my first hello world is below.

$ctx = [Microsoft.Z3.Context]::new()

$x = $ctx.MkConst("x", $ctx.MkIntSort())
$zero = $ctx.MkNumeral(0, $ctx.MkIntSort())
$one = $ctx.MkNumeral(1, $ctx.MkIntSort())

$s = $ctx.MkSolver()

$expr =  $x * $x - $one # x*x- 1
$assert = $s.Assert($ctx.MkEq( $expr, $zero)) # x*x - 1 = 0

$s.Check()
$m = $s.Model
$m.Decls | % { "$($_.Name) -> $($m.ConstInterp($_))" }

this, however, returns

SATISFIABLE
x -> -1

This is a bit confusing to me, as I'd expect it to return two roots, 1 and -1

The more confusing it becomes when I try this in python (in google colab)

x = Int('x')
solve(x*x-1==0)

it says

enter image description here

What do I do wrong in both cases?

Solution

  • z3 (and SMT solvers in general) will return only one model for each call to check. If you want to find out "all-solutions" then you have to enumerate them. There are several different ways of doing so, see this answer (Z3Py) checking all solutions for equation in the Python context; which can be translated to other API's as well.

    So, you're not doing anything wrong. You're just getting one possible model, as this is how the z3 API works.