Как заменить старый z3 :: expr (Oldve c) на новый z3 :: expr (Ve c)? - PullRequest
Новая
       13

Как заменить старый z3 :: expr (Oldve c) на новый z3 :: expr (Ve c)?

0 голосов
/ 14 апреля 2020

Я хочу изменить Старый z3 :: expr (Oldve c) следующим образом: 

OldVec is:(and (= (= R4 0) true) (= (= R6 R7) true))

На новый z3 :: expr (Ve c) следующим образом: 

Vec is:(and (= (= R4 0) false) (= (= R6 R7) true))

Я попытался изменить строку на z3 :: expr следующим образом: 

void changeZ3(z3::expr &OldVec) {
    std::string s="(set-info :status unknown)\n"
                  "(declare-fun R4 () Int)\n"
                  "(declare-fun R7 () Int)\n"
                  "(declare-fun R6 () Int)\n"
                  "(assert\n"
                  " (= (= R4 0) false))\n"
                  "(assert\n"
                  " (= (= R6 R7) true))\n"
                  "(check-sat)";
    std::cout<<"OldVec is:"<<OldVec<<"\n";
    z3::expr Vec=C.parse_string(s.data());
    std::cout<<"Vec is:"<<Vec<<"\n";
    OldVec=Vec;
}

Я напечатал Oldve c и Ve c, они выглядят одинаково: 

OldVec is:(and (= (= R4 0) true) (= (= R6 R7) true))    
Vec is:(and (= (= R4 0) false) (= (= R6 R7) true))

После того, как changeZ3 вернулся, я сделал Solver.add(Vec) так: 

z3::expr Vec = Ctx.parse_file(FormulaFile); //FormulaFile save z3::expr which looked like "s" on the top|^    
changeZ3(Vec);
Solver.add(Vec);

и затем я получил исключение, когда я Solver.add(Vec) сделал так: 

terminate called after throwing an instance of 'z3::exception'

Почему это случилось? Есть ли другой способ изменить z3 :: expr?

1 Ответ

1 голос
/ 14 апреля 2020

Как правило, вызову parse_file необходимо сообщить, какие сортировки и объявления находятся в области видимости. То есть, пока вы успешно создали «выражение» в Vec, вам все равно нужно вставить в контекст сортировку Int и объявления для R4, R7 и R6.

Это распространенная ошибка в программировании на z3: вы должны иметь в виду, что Ctx должен быть соответствующим образом настроен для этих формул, чтобы «иметь смысл» при вызове Solver.add.

В общем Вы должны уклоняться от "разбора" таких строк и добавления их в решатель. Вместо этого вы должны работать в имеющемся контексте и напрямую создавать выражения, используя выражение AST.

...