Как использовать разделенные на z3 предложения неснятых ядер & amp; попытаться снова найти ядро
Не могли бы вы рассказать, как разбить предложения несостоявшихся ядер?
И вот вопрос 2 касательно обнаруженных несоответствующих ядер, я попытаюсь искать снова.
Хотите рассказать, как это сделать?
Большое спасибо.
Как разделить пункты, как показано ниже
`and` (`or` (`<=_int` 1002 x1) (`<=_int` 1000 x1)) (`and` (`or` (`<=_int` 0 (`+_int` x2 (`*_int` -1003 x1))) (`<=_int` 0 (`+_int` x2 (`*_int` -1230 x1)))) (`and` (`or` (`<=_int` 0 (`+_int` x3 (`*_int` -1999 x2)))
Что касается вопроса 2,
cout<<s.check(3,assumptions)<<endl;
expr_vector core = s.unsat_core();
................
expr assumptions2[2] = {p1,p3};
cout<<"check next"<<s.check(2,assumptions2)<<endl;
expr_vector core1 = s.unsat_core();
for(unsigned int k=0;k<core1.size();++k){
cout<<"New core size "<<k<<endl;
cout<<"New unsat core "<<core1[k]<<endl;
}
Вызов функции ядра unsat снова, она не может снова выдать ядра unsat.
Большое спасибо.
Решение
Я не уверен, что понял ваш вопрос. Кажется, у вас есть утверждение формы (and c1 (and c2 c3))и вы хотите отслеживать c1, c2 а также c3 индивидуально.
В Z3 мы используем ответные литералы для отслеживания утверждений. Ответный литерал, по сути, является новым логическим значением, которое используется для отслеживания утверждения. То есть, было ли утверждение использовано (Z3), чтобы показать неудовлетворенность всего набора утверждений или нет. Например, если мы хотим отслеживать утверждение Fмы создаем свежую логическую переменную p и утверждать p implies F, Затем мы предоставляем p в качестве аргумента для метода проверки.
Если F является большим соединением, и мы хотим отслеживать его элементы индивидуально, мы должны извлечь его элементы и создать ответный литерал для каждого из них. Вот полный пример, который делает свое дело. Вы можете проверить это, включив его в example.cpp файл, включенный в дистрибутив Z3. Обратите внимание, что вы должны включить #include<vector>,
/**
\brief Unsat core example 2
*/
void unsat_core_example2() {
std::cout << "unsat core example 2\n";
context c;
// The answer literal mechanism, described in the previous example,
// tracks assertions. An assertion can be a complicated
// formula containing containing the conjunction of many subformulas.
expr p1 = c.bool_const("p1");
expr x = c.int_const("x");
expr y = c.int_const("y");
solver s(c);
expr F = x > 10 && y > x && y < 5 && y > 0;
s.add(implies(p1, F));
expr assumptions[1] = { p1 };
std::cout << s.check(1, assumptions) << "\n";
expr_vector core = s.unsat_core();
std::cout << core << "\n";
std::cout << "size: " << core.size() << "\n";
for (unsigned i = 0; i < core.size(); i++) {
std::cout << core[i] << "\n";
}
// The core is not very informative, since p1 is tracking the formula F
// that is a conjunction of subformulas.
// Now, we use the following piece of code to break this conjunction
// into individual subformulas. First, we flat the conjunctions by
// using the method simplify.
std::vector<expr> qs; // auxiliary vector used to store new answer literals.
assert(F.is_app()); // I'm assuming F is an application.
if (F.decl().decl_kind() == Z3_OP_AND) {
// F is a conjunction
std::cout << "F num. args (before simplify): " << F.num_args() << "\n";
F = F.simplify();
std::cout << "F num. args (after simplify): " << F.num_args() << "\n";
for (unsigned i = 0; i < F.num_args(); i++) {
std::cout << "Creating answer literal q" << i << " for " << F.arg(i) << "\n";
std::stringstream qname; qname << "q" << i;
expr qi = c.bool_const(qname.str().c_str()); // create a new answer literal
s.add(implies(qi, F.arg(i)));
qs.push_back(qi);
}
}
// The solver s already contains p1 => F
// To disable F, we add (not p1) as an additional assumption
qs.push_back(!p1);
std::cout << s.check(qs.size(), &qs[0]) << "\n";
expr_vector core2 = s.unsat_core();
std::cout << core2 << "\n";
std::cout << "size: " << core2.size() << "\n";
for (unsigned i = 0; i < core2.size(); i++) {
std::cout << core2[i] << "\n";
}
}
Другие решения
Других решений пока нет …