# Using Z3.jl

**URL:** <https://discourse.julialang.org/t/using-z3-jl/48006>\
**Category:** Optimization (Mathematical)\
**Tags:** z3\
**Created:** [October 8, 2020, 9:22pm UTC](https://discourse.julialang.org/t/using-z3-jl/48006 "2020-10-08T21:22:42Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Nosferican](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/nosferican/32/9275_2.png) [@Nosferican](https://discourse.julialang.org/u/Nosferican)\
**Post date:** [October 8, 2020, 9:22pm UTC](https://discourse.julialang.org/t/using-z3-jl/48006/1 "2020-10-08T21:22:42Z")

</div>

I am trying to use `atleast` and `atmost` to set up constraints but not sure how these work (type of the first argument). The method signature is

```julia
# 1 method for generic function "atleast":
  [1] atleast(arg1::Union{CxxWrap.CxxWrapCore.ConstCxxRef{var"#s36"} where var"#s36"<:Z3.AstVectorTpl{Z3.Expr}, CxxWrap.CxxWrapCore.CxxRef{var"#s35"} where var"#s35"<:Z3.AstVectorTpl{Z3.Expr}, Union{CxxWrap.CxxWrapCore.SmartPointer{T2}, T2} where T2<:Z3.AstVectorTpl{Z3.Expr}}, arg2::Integer) in Z3 at ~/.julia/packages/CxxWrap/94t40/src/CxxWrap.jl:590

```

I have tried something like

```julia
using Z3
ctx = Context()
constraints = bool_const.(Ref(ctx), string.("c", 1:3))
s = Solver(ctx, "QF_NRA")
x = atleast(constrains, 2)

```

which prompts the method error.  
CC: @ahumenberger, @XVilka  
From the examples, I have been able to look at I am missing some way of declaring the vector expression. Here is the Python [API](https://z3prover.github.io/api/html/namespacez3py.html#a8575bdeb9d1b8feac119aa162b5acfa6) which does

```julia
Create an at-most Pseudo-Boolean k constraint.

>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)

```

and the C++

```julia
    // each row contains a digit at most once
    for (unsigned i = 0; i < 9; ++i) {
        expr_vector t(c);
        for (unsigned j = 0; j < 9; ++j)
            t.push_back(x[i * 9 + j]);
        s.add(distinct(t));
    }

```

Thanks!

This worked!

```julia
ctx = Context()
constraints = bool_const.(Ref(ctx), string.("c", 1:3))
s = Solver(ctx, "QF_FD")
add(s, atleast(ExprVector(ctx, constraints), 2))
res = check(s)
m = get_model(s)
for (k, v) in consts(m)
    println("$k = $v")
end

```

---

<div class="post-metadata">

**Author:** ![Nosferican](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/nosferican/32/9275_2.png) [@Nosferican](https://discourse.julialang.org/u/Nosferican)\
**Post date:** [October 8, 2020, 10:25pm UTC](https://discourse.julialang.org/t/using-z3-jl/48006/2 "2020-10-08T22:25:13Z")

</div>

Another question I have relates to obtaining the results. For example,

```julia
ctx = Context()
constraints = bool_const.(Ref(ctx), string.("c", 1:3))
s = Solver(ctx, "QF_NRA")
add(s, constraints[1])
add(s, not(constraints[3]))
res = check(s)
m = get_model(s)
for (k, v) in consts(m)
    println("$k = $v")
end
parse(Bool, convert(String, string(first(values(consts(m))).second)))

```