some question about sum(list) on c++

[1214465750]

question 1:
on python if I want to get a list about some bool val I can

s=Optimize()
a=[Bool(str(i) for i in range(10)]
s.add(sum(a)==5)

so how can I make this on c++

question 2:
context c;
optimize s(c);
expr x = c.bool_const("x");
expr y = c.bool_const("y");
s.check();
model m = s.get_model();

so how can I get x by it's name "x" and how can I get it's value (because in a big item it have a lot of vars)

question 3:
speed between z3 on c++ and python
is z3 on c++ several times faster than z3 on python?

[1214465750]

I test

import time
from z3 import *
def zero_one_knapsack(weights, values, cap):
    solver = Optimize()
    # the decision variables
    flags = [Int(f"x_{i}") for i in range(len(weights))]
    for flag in flags:
        solver.add(Or(flag == 0, flag == 1))

    weight_arr = []
    i = 0
    for w in weights:
        weight_arr.append(w * flags[i])
        i += 1
    # add weight constraint
    solver.add(sum(weight_arr) <= cap)
    value_arr = []
    i = 0
    for v in values:
        value_arr.append(v * flags[i])
        i += 1
    solver.maximize(sum(value_arr))

    start = time.time()
    # calculate
    result = solver.check()
    print(f"use {time.time() - start}s to calculate")
    if result == sat:
        model = solver.model()
        print("\n".join([f"Index: {index}, weight: {weights[index]}, value: {values[index]}"
                            for index, flag in enumerate(flags) if model[flag] == 1]))
    else:
        print("empty")

if __name__ == '__main__':
    C = 300
    W = [71,34,82,23,1,88,12,57,10,68,5,33,37,69,98,24,26,83,16,26,18,43,52,71,22,65,68,8,40,40,24,72,16,34,10,19,28,13,34,98]
    V = [26,59,30,19,66,85,94,8,3,44,5,1,41,82,76,1,12,81,73,32,74,54,62,41,19,10,65,53,56,53,70,66,58,22,72,33,96,88,68,45]
    zero_one_knapsack(W, V, C)

and

#include <iostream>
#include <typeinfo>
#include <string>
#include <z3++.h>
#include <vector>
#include <ctime>

using namespace z3;
using std::cout;
using std::cin;
using std::endl;
using std::string;
using std::vector;

void knapsack(const vector<int> &weights, const vector<int> &values, int cap) 
{
    context c;
    optimize opt(c);
    vector<expr> flags;
    for (decltype(weights.size()) i = 0; i < weights.size(); ++i) {
        flags.push_back(c.int_const( ("x" + std::to_string(i)).c_str() ));
    }
    for (auto &flag : flags) {
        opt.add(flag == 0 || flag == 1);
    }
    expr tmp = c.int_const("tmp");
    tmp = c.int_val(0);
    for (decltype(weights.size()) i = 0; i < weights.size(); ++i) {
        tmp = tmp + weights[i] * flags[i];
    }
    opt.add(tmp <= cap);
    tmp = c.int_val(0);
    for (decltype(values.size()) i = 0; i < values.size(); ++i) {
        tmp = tmp + values[i] * flags[i];
    }
    opt.maximize(tmp);
    //cout << opt << endl;

    clock_t begin = clock();
    auto result = opt.check();
    clock_t end = clock();
    
    if (result == sat) {
        model m = opt.get_model();
        //cout << m << endl;
        for (unsigned i = 0; i < flags.size(); ++i) {
            auto item = flags[i];
            if (m.eval(item).get_numeral_int() == 0) continue;
            cout << i << ":\t"  << weights[i] << "\t" << values[i] << endl;
        }
    } else {
        cout << "no solution" << endl;
    }
    
    cout << "cost time:" << static_cast<double>(end - begin) / CLOCKS_PER_SEC << "s" << endl;
}


void work()
{
    vector<int> W,V;
    int C,n,w,v;
    cin >> C >> n;
    while (n--) {
        cin >> w >> v;
        W.push_back(w);
        V.push_back(v);
    }
    knapsack(W, V, C);
}

int main()
{
    std::ios::sync_with_stdio(false);
    work();
    return 0;
}

the time on c++ and python are the same