を使用しZ3_ast fs = Z3_parse_smtlib2_file(ctx,arg[1],0,0,0,0,0,0)てファイルを読み取りました。
expr F = to_expr(ctx,fs)さらに、と を使用してソルバーに追加しs.add(F)ます。
私の質問は、各インスタンスの合計制約数を取得するにはどうすればよいですか?
も試しましたF.num_args()が、場合によっては間違ったサイズが表示されます。
総制約を計算する方法はありますか?
質問する
116 次