mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

test

Browse source
This commit is contained in:
Jakob Rath 2022-12-01 16:16:22 +01:00
parent 91c6582bf7
commit 2704626a5d
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/test/polysat.cpp
View file

@ -241,7 +241,10 @@ namespace polysat {
public: public:
scoped_solver(std::string name): solver(lim), m_name(name) { scoped_solver(std::string name): solver(lim), m_name(name) {
if (!collect_test_records) { if (collect_test_records) {
std::cout << m_name << ":";
std::cout.flush();
} else {
std::cout << std::string(78, '#') << "\n\n"; std::cout << std::string(78, '#') << "\n\n";
std::cout << "START: " << m_name << "\n"; std::cout << "START: " << m_name << "\n";
} }
@ -252,6 +255,8 @@ namespace polysat {
~scoped_solver() { ~scoped_solver() {
test_records.end_batch(); test_records.end_batch();
if (collect_test_records)
std::cout << "\n";
} }
void set_max_conflicts(unsigned c) { void set_max_conflicts(unsigned c) {
@ -261,6 +266,10 @@ namespace polysat {
} }
void check() { void check() {
if (collect_test_records) {
std::cout << " ...";
std::cout.flush();
}
auto* rec = test_records.active_or_new_record(); auto* rec = test_records.active_or_new_record();
m_last_finished = nullptr; m_last_finished = nullptr;
SASSERT(rec->m_answer == l_undef); SASSERT(rec->m_answer == l_undef);
@ -277,6 +286,9 @@ namespace polysat {
} }
rec->m_finished = true; rec->m_finished = true;
m_last_finished = rec; m_last_finished = rec;
if (collect_test_records)
std::cout << " " << m_last_result;
else
std::cout << "DONE: " << m_name << ": " << m_last_result << "\n"; std::cout << "DONE: " << m_name << ": " << m_last_result << "\n";
statistics st; statistics st;
collect_statistics(st); collect_statistics(st);