3

C / C++APIを介して線形整数算術式の数量詞を削除するためにZ3を使用したいと思います。簡単な例を考えてみましょう：Exists（x）（x <= y＆y <= 2 * x）。同じモデルの数量詞なしの式はy>=0です。

私はそれをこのようにしようとしました：

   context ctx;
   ctx.set("ELIM_QUANTIFIERS", "true");
   expr x = ctx.int_const("x"); 
   expr y = ctx.int_const("y"); 
   expr sub_expr = (x <= y)  && (y <= 2*x);

   Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                                  0, {}, // patterns don't seem to make sense here.
                                  sub_expr); //No C++ API for quantifiers :(
   qf = Z3_simplify(ctx, qf);
   cout << Z3_ast_to_string(ctx, qf);

私が得るものは

（exists（（x Int）（and（<= xy）（<= y（* 2 x））））

一方、私は次のようなものを取得したいのですが

（<= 0年）

Z3で入手できる可能性はありますか？よろしくお願いします。

4

2 に答える 2

4

Nikolaj はすでに、タクティクスを使用して量指定子の削除を実行できることを指摘しました。この投稿では、C++ と C API を安全に混在させる方法を強調したいと思います。Z3 C++ API は、参照カウントを使用してメモリを管理します。expr基本的に、参照カウンターを自動的に管理する「スマートポインター」です。この問題については、次の投稿で説明しました: C++ API を使用した配列の選択と格納。

したがって、Z3_ast を返す C API を呼び出すときは、関数to_expr、to_sortまたはを使用して結果をラップする必要がありto_func_declます。の署名to_exprは次のとおりです。

inline expr to_expr(context & c, Z3_ast a);

この関数を使用することで、メモリ リークとクラッシュ (Z3 によってガベージ コレクションされたオブジェクトにアクセスする場合) を回避します。を使用した完全な例を次に示しto_expr()ます。Z3ディストリビューションexample.cppのフォルダー内のファイルにこの関数をコピーすることでテストできます。c++

void tst_quantifier() {
    context ctx;
    expr x = ctx.int_const("x"); 
    expr y = ctx.int_const("y"); 
    expr sub_expr = (x <= y) && (y <= 2*x);
    Z3_app vars[] = {(Z3_app) x};

    expr qf = to_expr(ctx, Z3_mk_exists_const(ctx, 0, 1, vars,
                                              0, 0, // patterns don't seem to make sense here.
                                              sub_expr)); //No C++ API for quantifiers :(
    tactic qe(ctx, "qe");
    goal g(ctx);
    g.add(qf);
    std::cout << qe.apply(g);
}
于 2012-10-26T03:34:56.373 に答える
3

単純化子は、量指定子の削除手順を呼び出さなくなりました。量指定子の削除やその他の多くの特別な目的の単純化の書き直しは、タクティック上で利用できます。

C++ ラッパー z3++.h は、戦術オブジェクトを作成するためのメソッドを公開します。「qe」タクティック用のタクティック オブジェクトを作成する必要があります。Z3 ディストリビューションには、z3++.h API からの戦術を使用するためのサンプルがいくつか付属しています。例えば：

void tactic_example1() {
/*
  Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic
  reasoning steps are represented as functions known as tactics, and tactics are composed
  using combinators known as tacticals. Tactics process sets of formulas called Goals.

  When a tactic is applied to some goal G, four different outcomes are possible. The tactic succeeds
  in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); 
  produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, 
  we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.

  In this example, we create a goal g consisting of three formulas, and a tactic t composed of two built-in tactics: 
  simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. 
  The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted 
  only to linear arithmetic. It can also eliminate arbitrary variables. 
  Then, sequential composition combinator & applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. 
  In this example, only one subgoal is produced.
*/
std::cout << "tactic example 1\n";
context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
goal g(c);
g.add(x > 0);
g.add(y > 0);
g.add(x == y + 2);
std::cout << g << "\n";
tactic t1(c, "simplify");
tactic t2(c, "solve-eqs");
tactic t = t1 & t2;
apply_result r = t(g);
std::cout << r << "\n";

}

あなたの場合、次のようなものが必要になります。

context ctx;
expr x = ctx.int_const("x"); 
expr y = ctx.int_const("y"); 
expr sub_expr = (x <= y)  && (y <= 2*x);

Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                              0, {}, // patterns don't seem to make sense here.
                              sub_expr); //No C++ API for quantifiers :(
tactic qe(ctx, "qe");
goal g(ctx);
g.add(qf);
cout << qe.apply(g);
于 2012-10-26T00:21:21.820 に答える