mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-22 11:07:51 +00:00
Code Activity

print validation num_check

Browse source
This commit is contained in:
Jakob Rath 2024-05-11 14:23:54 +02:00
parent c3ffbf05db
commit 2494ffacaf
1 changed files with 40 additions and 57 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -214,14 +214,52 @@ namespace intblast {
original_es.append(es); original_es.append(es);
static unsigned num_check = 0;
num_check += 1;
lbool r; lbool r;
if (false) { if (false) {
r = m_solver->check_sat(es); r = m_solver->check_sat(es);
} }
else { else {
#if 0
std::string name_esc;
if (name) {
name_esc = name;
for (char& c : name_esc)
if (c == '|')
c = '!';
}
else
name_esc = "<none>";
namespace fs = std::filesystem;
{
fs::path filename = std::string("validation/bv-") + std::to_string(num_check) + ".smt2";
fs::create_directories(filename.parent_path());
IF_VERBOSE(1, verbose_stream() << "validation check written to file " << filename << "\n");
std::ofstream file(filename);
file << "(set-logic ALL)\n";
file << "(set-info :source |\n";
file << " Name: " << name_esc << "\n";
// file << original_es << "\n";
file << "|)\n";
m_solver->push();
m_solver->assert_expr(original_es);
m_solver->display(file) << "(check-sat)\n";
m_solver->pop(1);
file.close();
}
r = l_false;
#else
translate(es); translate(es);
for (auto e : m_vars) { for (auto e : m_vars) {
auto v = translated(e); auto v = translated(e);
auto b = rational::power_of_two(bv.get_bv_size(e)); auto b = rational::power_of_two(bv.get_bv_size(e));
@ -235,62 +273,6 @@ namespace intblast {
es[i] = tmp; es[i] = tmp;
} }
#if 0
std::string name_esc;
if (name) {
name_esc = name;
for (char& c : name_esc)
if (c == '|')
c = '!';
}
else
name_esc = "<none>";
namespace fs = std::filesystem;
static unsigned num_check = 0;
num_check += 1;
{
fs::path filename = std::string("validation/int-") + std::to_string(num_check) + ".smt2";
fs::create_directories(filename.parent_path());
IF_VERBOSE(1, verbose_stream() << "validation check written to file " << filename << "\n");
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(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();
r = l_false;
#else
IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n"); IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n");
IF_VERBOSE(2, IF_VERBOSE(2,
@ -310,6 +292,7 @@ namespace intblast {
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
if (r == l_true) { if (r == l_true) {
verbose_stream() << "validation failed: " << name << "\n"; verbose_stream() << "validation failed: " << name << "\n";
verbose_stream() << "validation num_check: " << num_check << "\n";
IF_VERBOSE(0, IF_VERBOSE(0,
model_ref mdl; model_ref mdl;
m_solver->get_model(mdl); m_solver->get_model(mdl);