search

bmstu-iu9 / SMT-to-REF

Чтение модели в строковом языке из SMT-форматов и перекодировка в программу-предикат на Рефале.
0 stars 0 forks source link

translateToCNF падает #13

Open TonitaN opened 3 years ago

TonitaN commented 3 years ago

Прилагаю тест:

(set-logic QF_SLIA)
(set-option :strings-exp true)

(declare-fun xx () String)
(declare-fun xxx () String)
(declare-fun x () String)

(assert (or (and (str.contains xxx "A") (not (str.contains x "A"))) (and (str.contains x "A") (str.contains xx "A"))))

(check-sat)
(get-model)
TonitaN commented 3 years ago

@ylyxa , теперь на этом тесте падает кодген.

ylyxa commented 3 years ago

Проблема все еще на стороне @StepanBog, в процессе перевода к КНФ в одном из or-блоков 'exprs' заменяется на пустой список. image

ylyxa commented 3 years ago

Хотя нет, оно не "заменяется", там какая-то другая проблема. Но эта проблема все равно где-то в переводе к КНФ, на выходе collapse_asserts все нормально.