Как получить реальные значения из модели в виде десятичных (двойных) в Z3 (Java)? - PullRequest
Новая
       9

Как получить реальные значения из модели в виде десятичных (двойных) в Z3 (Java)?

0 голосов
/ 27 февраля 2019

Я пытаюсь получить реальные значения из Model, вычисленного по Solver.Однако, хотя я установил для pp.decimal значение true (как в файле SMT2, так и с использованием Global.setParameter), это выполняется только при печати самой модели.

Когда я пытаюсь получить значения с помощьюmodel.getConstInterp сверх значений model.getConstDecls, все они отображают дроби (что делает мое хакерское решение использовать Double.parseDouble неосуществимым).

Мне было интересно, есть ли какой-нибудь удобный способ получить значения постоянных функций в пределахмодель, не заставляя меня писать анализатор (либо для модели, либо для создаваемых ею арифметических выражений).

Любая помощь будет принята с благодарностью.

РЕДАКТИРОВАТЬ, чтобы включить пример: 

BoolExpr[] assertions = ctx.parseSMTLIB2String(smt, null, null, null, null);

// get solver from context (modelled upon assertions)
Solver solver = ctx.mkSolver();
solver.add(assertions);

switch (solver.check()) {
    case SATISFIABLE: {
        // fetch our model
        Model model = solver.getModel();
        System.out.println(model);

        for(FuncDecl constant : model.getConstDecls()) {
            // get the interpretation
            Expr value = model.getConstInterp(constant);
            System.out.println(value.toString());

Вывод: 

(define-fun b () Real
  (- 1.0))
(define-fun w2 () Real
  0.5)
(define-fun w1 () Real
  0.5)
-1
1/2
1/2

Я хочу каким-то образом извлечь результаты этих константных функций в Java double s.Я мог бы просто разобрать значения Expr s 'toString(), если бы они оба соблюдали pp.decimal.

1 Ответ

0 голосов
/ 27 февраля 2019

После легкого копания (за рамками рассмотрения предложений по автозаполнению) я решил, что вы можете просто проверить, является ли Expr у вас RatNum.Оттуда вы можете повышать до RatNum и использовать getNumerator и getDenominator() и получать double от деления таким образом. 

Expr value = model.getConstInterp(constant);
if(value.isRatNum()) {
    RatNum rational = (RatNum) value;
    IntNum num = rational.getNumerator(), den = rational.getDenominator();
    System.out.println("Value = " + ((double) num.getInt() / den.getInt()));
}

Это имеет смысл сейчас.

...