2017-07-09 35 views
3

で `exists`スコープの変数へのアクセス:は、私がZ3と次のような問題を解決しようとしていますZ3

4つの演算子(+-*/)の設定した、で置換することができた事業者を決めますそれを真にするための式に従う:

(((((1 <op1> 2) <op2> 3) <op3> 4) <op4> 5) <op5> 6) = 35 

すべての有効な回答を印刷する必要があります。ここではサンプルプログラムは、Z3言語である:

(declare-datatypes() ((operator (Plus) (Minus) (Mult) (Divid)))) 
(define-fun myf ((x Int) (z operator) (y Int)) Int 
     (ite (= z Plus) (+ x y) 
     (ite (= z Minus) (- x y) 
      (ite (= z Mult) (* x y) 
       (div x y))))) 
(assert 
    (exists ((b1 operator) (b2 operator) (b3 operator) (b4 operator) (b5 operator)) 
    (= (myf(myf(myf(myf(myf 1 b1 2) b2 3) b3 4) b4 5) b5 6) 35) 
) 
) 

(check-sat) 
(get-model) 
(exit) 

http://rise4fun.com/Z3/8usN

それは、ソリューションのすべてを印刷しません。私はすべての解を印刷するために、反復のたびにソルバに制約を追加する必要があることを理解していますが、C#でそれを行う方法はわかりません。

ここに私の現在のコード(C#7)です:

using (var context = new Context()) 
{ 
    var @operator = context.MkEnumSort("operator", "Plus", "Minus", "Mult", "Div"); 
    var plus = @operator.Consts[0]; 
    var minus = @operator.Consts[1]; 
    var mult = @operator.Consts[2]; 

    IntExpr myf(IntExpr x, Expr z, IntExpr y) => 
     (IntExpr)context.MkITE(context.MkEq(z, plus), context.MkAdd(x, y), 
      context.MkITE(context.MkEq(z, minus), context.MkSub(x, y), 
       context.MkITE(context.MkEq(z, mult), context.MkMul(x, y), 
        context.MkDiv(x, y)))); 

    var solver = context.MkSolver(); 

    var b1 = context.MkConst("b1", @operator); 
    var b2 = context.MkConst("b2", @operator); 
    var b3 = context.MkConst("b3", @operator); 
    var b4 = context.MkConst("b4", @operator); 
    var b5 = context.MkConst("b5", @operator); 

    solver.Assert(
     context.MkExists(
      new[] { b1, b2, b3, b4, b5 }, 
      context.MkEq(
       myf(
        myf(
         myf(
          myf(
           myf(
            context.MkInt(1), 
            b1, 
            context.MkInt(2)), 
           b2, 
           context.MkInt(3)), 
          b3, 
          context.MkInt(4)), 
         b4, 
         context.MkInt(5)), 
        b5, 
        context.MkInt(6)), 
       context.MkInt(35)))); 

    while (Status.SATISFIABLE == solver.Check()) 
    { 
     var operators = new[] { b1, b2, b3, b4, b5 }; 
     var model = solver.Model; 
     var values = operators.Select(o => model.Eval(o, true)); // That doesn't return the right values 

     Console.WriteLine(model); 
     Console.WriteLine(string.Join(" ", values)); 

     solver.Add(context.MkOr(
      operators.Select(o => context.MkNot(context.MkEq(o, model.Eval(o, true)))))); // That's supposed to work, but it doesn't 
    } 

私はexists範囲から変数へのアクセスに問題があります:model.Eval(b1, true)戻っていくつかの値が、ない値ソルバは上使用することを決定したようです現在の反復。そして、さらにソルバーのスコープを汚染(例えば、私はモデル出力にすべての方法をこれらの定数を参照することができます)これらの定数の値を求めて:

(define-fun b3!2() operator 
    Mult) 
(define-fun b2!3() operator 
    Mult) 
(define-fun b5!0() operator 
    Minus) 
(define-fun b1!4() operator 
    Plus) 
(define-fun b4!1() operator 
    Plus) 
#^^^^ these seems like the proper values 
(define-fun b1() operator 
    Minus) 
(define-fun b2() operator 
    Minus) 
(define-fun b3() operator 
    Minus) 
(define-fun b4() operator 
    Minus) 
(define-fun b5() operator 
    Minus) 
#^^^^ and I don't know why it prints these 

私は適切な値に制約を追加するために私のプログラムを修正するにはどうすればよいと範囲を汚染しないでください。

答えて

4

残念ながら私はこれを試してみるためにC#にアクセスすることはできませんが、なぜmkExistへの呼び出しが必要なのか不思議です。変数b1 .. b6は既にMkConstへの呼び出しを介して作成されているので、制約をアサートしてからモデルを拒否するだけで、なしでmkExistまた、がなく、新しいループを作成するためにループ内にと呼びます。

+0

これは私の質問には答えませんが、それはもっと効率的な方法で私の仕事を解決します。どうもありがとう! – ForNeVeR

+1

一般的に、SMTLibの量子にバインドされた変数にアクセスする手段はありません。もちろん、C#インターフェイスを使用しています。そのためにはZ3固有の方法があるかもしれませんが、get-modelなどの呼び出しではトップレベルの変数だけが一般的に表示されます。https://stackoverflow.com/あなたの質問にかなり関連している質問/ 7179777/z3-extracted-existential-model-values/7181987#7181987 –

関連する問題