How to use Z3 C++ API to prove a theory based on input parameter?

Question

I am trying to use the Z3 C++ API to achieve the following:

(set-option :produce-proofs true)

(declare-const Weight Int)
(declare-const WeightLimit Int)
(declare-const P1 Bool)

(assert (= WeightLimit 10))

(assert (= P1 (>= Weight WeightLimit)))
(assert (= P1 true))

;Facts - Input
(assert (= Weight 100))

(check-sat)

And I ended up to the following function:

void test() {
    try {        
        context ctx;        
        Z3_string str = "(declare-const Weight Int) (declare-const WeightLimit Int) (declare-const P1 Bool) (assert (= WeightLimit 10)) (assert (= P1 (>= Weight WeightLimit))) (assert (= P1 true)) (assert (= Weight 100)) (check-sat)"; //Generated by some other function
        expr fs(ctx, Z3_parse_smtlib2_string(Z3_context(ctx), str, 0, 0, 0, 0, 0, 0));

        solver s(ctx);
        s.add(fs);

        switch (s.check()) {
            case unsat:   std::cout << "not satisfied\n"; break;
            case sat:     std::cout << "satisfied\n"; break;
            case unknown: std::cout << "unknown\n"; break;
        } 

        model m = s.get_model();
        std::cout << m << "\n";

    }
    catch (z3::exception e) {
        std::cout << e.msg() << std::endl;
    }
}

Is there any way to pass the Weight value as input parameter to the function instead of having it hard-coded?

Furthermore, how can I set-option by using the Z3 C++ API? And what is the impact if I don't set the option?

Answer 1

Well, this needs to be handled by the function that generates that string as its output, the one you commented as "//Generated by some other function"

You'd simply pass the Weight as a parameter to that function, which should use the correct value in generating the string.

If that function is not available to you for whatever reason, you'll have to do some string-processing; but of course that would be extremely brittle and error-prone.

The other alternative would be to not pass a string, but rather use the API to actually assert facts one at a time; but from your description it seems that's probably not a choice for you either.