Когда я должен усвоить выражение? - PullRequest
Новая
       16

Когда я должен усвоить выражение?

0 голосов
/ 10 апреля 2019

Я пытаюсь написать собственную теорию струн для z3. Одна проблема, с которой я столкнулся, - это концепция интернализации в z3.

Если я не усваиваю выражение (или литерал) перед тем, как добавить его в качестве аксиомы, иногда я получаю исключение, а иногда нет.

Например, в следующем коде из theory_seq.cpp 

    VERIFY(m_util.str.is_index(i, t, s) ||
           m_util.str.is_index(i, t, s, offset));
    expr_ref minus_one(m_autil.mk_int(-1), m);

    literal cnt = mk_literal(m_util.str.mk_contains(t, s));
    literal i_eq_m1 = mk_eq(i, minus_one, false);
    add_axiom(cnt,  i_eq_m1);

Он не усваивает i_eq_m1 и, кажется, работает нормально.

Но если я не усваиваю какое-либо выражение (например, удаляю все вызовы ctx.internalize (e, false)), я получу некоторое исключение.

Есть ли какой-то принцип, которому я должен следовать, когда создаю новое выражение из существующих?

...