Zugriff auf Variable `exists` Umfang in Z3

Question

Ich versuche, das folgende Problem mit Z3 zu lösen:

Nachdem Satz von vier Operatoren (+, -, *, /), entscheiden die Betreiber in die ersetzt werden könnte folgender Ausdruck um es wahr zu machen:

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

Ich muss alle gültigen Antworten drucken. Hier ist ein Beispielprogramm in Z3 Sprache:

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

Es ist nicht alle Lösungen nicht gedruckt werden. Ich verstehe, dass, um alle Lösungen zu drucken ich Constraints dem Solver nach jeder Iteration like that answer recommends hinzufügen muss, aber ich kann nicht, wie man es mit C# macht.

Hier ist meine aktuellen Code (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 
    } 

Ich habe Probleme Variablen aus dem exists Umfang Zugriff auf: es scheint, dass model.Eval(b1, true) Rendite einen gewissen Wert, aber nicht der Wert Löser zu verwenden haben beschlossen die aktuelle Iteration. Und auch die Werte dieser Konstanten fragen weiter den Solver Umfang verpestet (zB ich diese Konstanten in der Modell-Ausgabe den ganzen Weg sehen können):

(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 

Wie behebe ich mein Programm zu Einschränkungen für die richtigen Werte hinzufügen und Verschmutzen Sie nicht den Umfang?

Answer 1

Leider habe ich keinen Zugriff auf C#, um dies auszuprobieren, aber ich bin neugierig, warum Sie einen Anruf an mkExist überhaupt benötigen? Da haben Sie bereits die Variablen b1 .. b6 über Anrufe zu MkConst erstellt, sollten Sie sie einfach auf beide verwenden, um Ihren Zwang durchsetzen und dann die Modelle widerlegen, wie Sie die „all-sat“ do-Schleife, ohne Anrufe zu mkExist und auch ohne Aufruf new innerhalb Ihrer Schleife, um neue zu erstellen.