Using Z3.jl

Specific Domains Optimization (Mathematical)
1

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

# 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

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 which does

Create an at-most Pseudo-Boolean k constraint.

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

and the C++

    // 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!

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
2

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

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)))