mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix #2076, add option to handle .cnf files into dimacs parser
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b63a0e31d3
commit
9c318ed304
|
@ -181,7 +181,7 @@ extern "C" {
|
|||
if (!is) {
|
||||
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
|
||||
}
|
||||
else if (ext && std::string("dimacs") == ext) {
|
||||
else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
|
||||
ast_manager& m = to_solver_ref(s)->get_manager();
|
||||
std::stringstream err;
|
||||
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
|
||||
|
|
|
@ -1197,8 +1197,11 @@ namespace smt {
|
|||
literal_vector& lits = get_unhelpful_literals(c, true);
|
||||
lits.push_back(c.lit());
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
|
||||
add_assign(c, lits, c.lit(i));
|
||||
literal lit = c.lit(i);
|
||||
if (ctx.get_assignment(lit) == l_undef) {
|
||||
DEBUG_CODE(validate_assign(c, lits, lit););
|
||||
add_assign(c, lits, c.lit(i));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue