Почему следующее выражение в z3 занимает много времени? - PullRequest
Новая
       9

Почему следующее выражение в z3 занимает много времени?

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

Что не так с этим выражением z3? 

(declare-const arg_1 Int)
(assert
  (and
     (not (= 0 (mod arg_1 10)))
     (= 0 (mod (+ 1 arg_1) 10))))
(check-sat)
(get-model)

Попытка оценить его с помощью z3 зависает навсегда.С другой стороны, если я попытаюсь выполнить одно из следующих действий, оно немедленно вернется.

Использование только первого выражения 

(declare-const arg_1 Int)
(assert (not (= 0 (mod arg_1 10))))
(check-sat)
(get-model)

=> sat
(model 
  (define-fun arg_1 () Int
 1)
)

Использование второго выражениятолько 

(declare-const arg_1 Int)
(assert (= 0 (mod (+ 1 arg_1) 10)))
(check-sat)
(get-model)

=> sat
(model
  (define-fun arg_1 () Int
    9)
)

Выдача их вместе в одном файле также немедленно возвращается. 

(declare-const arg_1 Int)
(declare-const arg_2 Int)
(assert (= 0 (mod (+ 1 arg_1) 10)))
(assert (not (= 0 (mod arg_2 10))))

;(assert (= arg_1 arg_2))
(check-sat)
(get-model)

=> sat
(model 
  (define-fun arg_2 () Int
    1)
  (define-fun arg_1 () Int
    9)
)

Однако, если я раскомментирую утверждение arg_1 = arg_2, оно будет зависать.

1 Ответ

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

Скорее всего, это ошибка z3.Если вы запускаете оригинал с z3 -v:3, вы получаете: 

$ z3 -v:3 a.smt2
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 1)
final-check OPTIMAL
final-check OPTIMAL
...

, и он продолжает печатать это.Я пытался с cvc4, yices и mathsat;и все они решают это немедленно.Вы должны сообщить об этом на https://github.com/Z3Prover/z3/issues, чтобы они могли взглянуть на это.

...