mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 10:10:21 +00:00
Code Activity

write validation in bv format too

Browse source
This commit is contained in:
Jakob Rath 2024-03-12 16:18:39 +01:00
parent 37bf5fefca
commit 58c14ba2f9
1 changed files with 46 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/sat/smt/intblast_solver.cpp
View file

@ -251,19 +251,47 @@ namespace intblast {
else else
name_esc = "<none>"; name_esc = "<none>";
file << "(set-logic ALL)\n"; namespace fs = std::filesystem;
file << "(set-info :source |\n"; static unsigned num_check = 0;
file << " Name: " << name_esc << "\n"; num_check += 1;
file << original_es << "\n|)\n";
m_solver->push(); {
m_solver->assert_expr(es); fs::path filename = std::string("validation/int-") + std::to_string(num_check) + ".smt2";
m_solver->display(file) << "(check-sat)\n"; fs::create_directories(filename.parent_path());
m_solver->pop(1); IF_VERBOSE(1, verbose_stream() << "validation check written to file " << filename << "\n");
std::ofstream file(filename);
file.close(); file << "(set-logic ALL)\n";
file << "(set-info :source |\n";
file << " Name: " << name_esc << "\n";
file << original_es << "\n|)\n";
// if (num_check == 68) m_solver->push();
m_solver->assert_expr(es);
m_solver->display(file) << "(check-sat)\n";
m_solver->pop(1);
file.close();
}
{
fs::path filename = std::string("validation/bv-") + std::to_string(num_check) + ".smt2";
std::ofstream file(filename);
file << "(set-logic ALL)\n";
file << "(set-info :source |\n";
file << " Name: " << name_esc << "\n";
file << original_es << "\n|)\n";
m_solver->push();
m_solver->assert_expr(original_es);
m_solver->display(file) << "(check-sat)\n";
m_solver->pop(1);
file.close();
}
// if (num_check == 62)
// std::abort(); // std::abort();
r = l_false; r = l_false;
@ -469,10 +497,10 @@ namespace intblast {
continue; continue;
if (sib->get_arg(0)->get_root() == r1) if (sib->get_arg(0)->get_root() == r1)
continue; continue;
auto a = eq_internalize(n, sib); auto a = eq_internalize(n, sib);
auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
ctx.mark_relevant(a); ctx.mark_relevant(a);
ctx.mark_relevant(b); ctx.mark_relevant(b);
add_clause(~a, b, nullptr); add_clause(~a, b, nullptr);
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
@ -490,10 +518,10 @@ namespace intblast {
auto nBv2int = ctx.get_enode(bv2int); auto nBv2int = ctx.get_enode(bv2int);
auto nxModN = ctx.get_enode(xModN); auto nxModN = ctx.get_enode(xModN);
if (nBv2int->get_root() != nxModN->get_root()) { if (nBv2int->get_root() != nxModN->get_root()) {
auto a = eq_internalize(nBv2int, nxModN); auto a = eq_internalize(nBv2int, nxModN);
ctx.mark_relevant(a); ctx.mark_relevant(a);
add_unit(a); add_unit(a);
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
} }
return sat::check_result::CR_DONE; return sat::check_result::CR_DONE;