использование арифметики с плавающей точкой с API Z3 C ++ - PullRequest
Новая
       4

использование арифметики с плавающей точкой с API Z3 C ++

0 голосов
/ 29 мая 2018

Я пытаюсь решить проблему нелинейных действительных чисел, используя Z3.Мне нужен Z3 для генерации нескольких решений.В проблемной области точность не является критической проблемой;Мне нужно только одна или две десятичные цифры после десятичной точки.поэтому мне нужно установить Z3, чтобы не исследовать все пространство поиска действительных чисел, чтобы минимизировать время нахождения нескольких решений.

Я пытаюсь заменить действительные числа числами с плавающей запятой.Я прочитал пример fpa в файле c_api.c, но нашел его немного смущающим для меня. Например,

, позвольте мне предположить, что я хочу конвертировать реалы в следующем коде: 

config cfg;
cfg.set("auto_config", true);
context con(cfg);

expr x = con.real_const("x");
expr y = con.real_const("y");

solver sol(con);
sol.add(x*y > 10);
std::cout << sol.check() << "\n";
std::cout << sol.get_model() << "\n";

}

Я попробовал следующий код, но он не работал 

config cfg;
cfg.set("auto_config", true);
context con(cfg);

expr sign = con.bv_const("sig", 1);
expr exp = con.bv_const("exp", 10);
expr sig = con.bv_const("sig", 10);


expr x = to_expr(con, Z3_mk_fpa_fp(con, sign, exp, sig));
expr y = to_expr(con, Z3_mk_fpa_fp(con, sign, exp, sig));

solver sol(con);
sol.add(x*y > 10);

std::cout << sol.check() << "\n";

, и вывод: 

Assertion failed: false, file c:\users\rehab\downloads\z3-master\z3-master\src\a
pi\c++\z3++.h, line 1199

Мои вопросы:

  1. Есть ли подробные примеры или фрагменты кода об использовании fpa в C ++ API?мне не ясно, как преобразовать пример fpa в C API для C ++ API.
  2. Что не так в приведенном выше преобразовании кода?

1 Ответ

0 голосов
/ 29 мая 2018

Я не уверен, что использование поплавков - лучший способ решить вашу проблему.Но звучит так, как будто вы перепробовали все другие варианты, и нелинейность мешает вам.Обратите внимание, что даже если вы моделируете свою проблему с помощью чисел с плавающей запятой, арифметика с плавающей запятой довольно сложна, и решателю может быть трудно найти подходящие модели.Кроме того, решения могут быть далеки от реальных результатов из-за нестабильности чисел.

Использование C

Если оставить все это в стороне, правильный способ кодирования вашего запроса с использованием C api будет (если мыиспользовать 32-битные числа с плавающей запятой одинарной точности): 

#include <z3.h>

int main(void) {
    Z3_config  cfg = Z3_mk_config();
    Z3_context ctx = Z3_mk_context(cfg);
    Z3_solver  s   = Z3_mk_solver(ctx);

    Z3_solver_inc_ref(ctx, s);
    Z3_del_config(cfg);

    Z3_sort float_sort = Z3_mk_fpa_sort(ctx, 8, 24);

    Z3_symbol s_x = Z3_mk_string_symbol(ctx, "x");
    Z3_symbol s_y = Z3_mk_string_symbol(ctx, "y");
    Z3_ast      x = Z3_mk_const(ctx, s_x, float_sort);
    Z3_ast      y = Z3_mk_const(ctx, s_y, float_sort);

    Z3_symbol s_x_times_y = Z3_mk_string_symbol(ctx, "x_times_y");
    Z3_ast      x_times_y = Z3_mk_const(ctx, s_x_times_y, float_sort);

    Z3_ast c1 = Z3_mk_eq(ctx, x_times_y, Z3_mk_fpa_mul(ctx, Z3_mk_fpa_rne(ctx), x, y));

    Z3_ast c2 = Z3_mk_fpa_gt(ctx, x_times_y, Z3_mk_fpa_numeral_float(ctx, 10, float_sort));

    Z3_solver_assert(ctx, s, c1);
    Z3_solver_assert(ctx, s, c2);

    Z3_lbool result = Z3_solver_check(ctx, s);

    switch(result) {
        case Z3_L_FALSE: printf("unsat\n");
                         break;
        case Z3_L_UNDEF: printf("undef\n");
                         break;
        case Z3_L_TRUE:  { Z3_model m = Z3_solver_get_model(ctx, s);
                           if(m) Z3_model_inc_ref(ctx, m);
                           printf("sat\n%s\n", Z3_model_to_string(ctx, m));
                           break;
                         }
    }

    return 0;
}

При запуске выдает: 

sat
x_times_y -> (fp #b0 #xbe #b10110110110101010000010)
y -> (fp #b0 #xb5 #b00000000000000000000000)
x -> (fp #b0 #x88 #b10110110110101010000010)

Это числа с плавающей запятой одинарной точности;вы можете прочитать о них в википедии, например.В более традиционных обозначениях это: 

x_times_y -> 1.5810592e19
y         -> 1.8014399e16
x         -> 877.6642

Это довольно сложно использовать, но то, что вы спросили.

Использование Python

Я бы искренне рекомендовал использоватьPython API, чтобы хотя бы увидеть, на что способен решатель, прежде чем инвестировать в такой сложный код на Си.Вот как это будет выглядеть в Python: 

from z3 import *

x = FP('x', FPSort(8, 24))
y = FP('y', FPSort(8, 24))

s = Solver()
s.add(x*y > 10);
s.check()
print s.model()

При запуске это печатает: 

[y = 1.32167303562164306640625,
 x = 1.513233661651611328125*(2**121)]

Возможно, не то, что вы ожидали, но это действительно правильная модель.

Использование Haskell

Просто чтобы дать вам представление о простоте, вот как можно выразить ту же проблему, используя привязки Haskell (это всего лишь один вкладыш!) 

Prelude Data.SBV> sat $ \x y -> fpIsPoint x &&& fpIsPoint y &&& x * y .> (10::SFloat)
Satisfiable. Model:
  s0 = 5.1129496e28 :: Float
  s1 =  6.6554557e9 :: Float

Резюме

Обратите внимание, что с плавающей точкой также возникают проблемы, связанные со значениями NaN / Infinity, поэтому вам, возможно, придется избегать их явно.(Это то, что было сделано в выражении Haskell с использованием предиката isFPPoint. Кодирование его на Python или C потребовало бы большего количества кода, но, безусловно, выполнимо.)

Следует подчеркнуть, что буквально любая другая привязка к Z3(Python, Haskell, Scala, что у вас есть) даст вам лучший опыт, чем то, что вы получите с C / C ++ / Java.(Даже прямое кодирование в SMTLib было бы лучше.)

Итак, я от всей души рекомендую использовать какой-то высокоуровневый интерфейс (хороший Python: его легко освоить), и как только вы будете уверены в моделии как это работает, вы можете начать кодировать то же самое в C, если это необходимо.

...