は、私がZ3と次のような問題を解決しようとしていますZ3

Question

で `exists`スコープの変数へのアクセス：

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 

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

Answer 1

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