Z3 C++ APIを使用して入力パラメータに基づく理論を証明するにはどうすればよいですか？

Question

I以下を達成するためにZ3 C++ APIを使用しようとしています：

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

そして、私は次の関数になってしまった：

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; 
    } 
} 

は、入力として重み値を渡す方法はありますパラメータをハードコーディングする代わりに関数に渡しますか？

さらに、Z3 C++ APIを使用してset-optionを設定するにはどうすればよいですか？オプションを設定しないと、どのような影響がありますか？

Answer 1

まあ、これは「//他のいくつかの関数によって生成された」あなたはとしてコメント1、その出力として、その文字列を生成する関数によって処理されるように

を必要とするあなたは、単にとしてWeightを渡したいですその関数のパラメータ。文字列を生成する際に正しい値を使用する必要があります。

何らかの理由でこの機能がでない場合は、をご利用いただけます。文字列処理を行う必要があります。もちろん、それは非常に脆く、エラーを起こしやすいでしょう。

もう1つの方法はではなく、では文字列を渡しますが、実際には一度に1つのファクトを実際にアサートするためにAPIを使用します。あなたの説明からはおそらくどちらかの選択肢ではないようです。