mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fixes for #6577

Browse source 
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
This commit is contained in:
Nikolaj Bjorner 2023-02-11 09:32:53 -08:00
parent d22e4aa525
commit 46c8d78ece
3 changed files with 16 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_goal.cpp
View file

@ -198,7 +198,7 @@ extern "C" {
RESET_ERROR_CODE();
std::ostringstream buffer;
if (!to_goal_ref(g)->is_cnf()) {
SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf");
SET_ERROR_CODE(Z3_INVALID_ARG, "Goal is not converted into CNF. Preprocess by optional bit-blasting and applying tseitin-cnf");
RETURN_Z3(nullptr);
}
to_goal_ref(g)->display_dimacs(buffer, include_names);

8
src/ast/display_dimacs.cpp
View file

@ -47,6 +47,8 @@ struct dimacs_pp {
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m.is_false(l))
continue;
if (m.is_not(l))
l = to_app(l)->get_arg(0);
if (!is_uninterp_const(l))
@ -101,6 +103,12 @@ struct dimacs_pp {
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m.is_false(l))
continue;
if (m.is_true(l)) {
out << "1 -1 ";
continue;
}
if (m.is_not(l)) {
out << "-";
l = to_app(l)->get_arg(0);

19
src/tactic/goal.cpp
View file

@ -692,28 +692,23 @@ bool goal::is_cnf() const {
for (unsigned i = 0; i < size(); i++) {
expr * f = form(i);
if (m_manager.is_or(f)) {
for (expr* lit : *to_app(f)) {
if (!is_literal(lit)) {
for (expr* lit : *to_app(f))
if (!is_literal(lit))
return false;
}
}
return true;
}
if (!is_literal(f)) {
if (!is_literal(f))
return false;
}
}
return true;
}
bool goal::is_literal(expr* f) const {
m_manager.is_not(f, f);
if (!is_app(f)) return false;
if (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) {
if (!is_app(f))
return false;
if (to_app(f)->get_family_id() == m_manager.get_basic_family_id())
for (expr* arg : *to_app(f))
if (m_manager.is_bool(arg)) {
if (m_manager.is_bool(arg))
return false;
}
}
return true;
}