Блог

Я учусь запускать аналогичные коды в соответствующем случае, который предназначен для сопоставления грузовиков для транспортировки (https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf ) в JAVA API. Существует код для определения функции max:

 (define-fun imax ((a Int) (b Int)) Int (if (> a b) a b))
  

Я перевожу это на Java:

      public static ArithExpr maxFunc(ArithExpr a, ArithExpr b)
     {
         Context ctx = new Context();
         ArithExpr result = (ArithExpr) ctx.mkITE(ctx.mkGe(a, b), a, b);
         return resu<
     }
  

И попробуйте использовать ее таким же образом (ниже приведена только демонстрация)

         ArithExpr per1 = maxFunc(X0101, maxFunc(X0201, maxFunc(X0301, maxFunc(X0401, X0501))));
        BoolExpr minPer1 = ctx.mkEq(per1, constant0);
        o.AssertSoft(minPer1,1 , "a");
  

Для приведенных выше кодов есть ошибки:

 Exception in thread "main" com.microsoft.z3.Z3Exception: Context mismatch
  

Ошибка относится к телу функции:

 ArithExpr result = (ArithExpr) ctx.mkITE(ctx.mkGe(a, b), a, b);
  

У меня определенно есть сомнения в построении функции z3 на JAVA. Существует ли специальная форма функции для Z3 Java API? Как исправить функцию?

«Несоответствие контекста» означает, что вы пытаетесь использовать выражения из нескольких контекстов вместе, что не поддерживается. Вместо Context ctx = new Context(); убедитесь, что вы используете тот же контекст, что и в остальной части вашей программы.