mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix release build failure

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-10 14:53:05 -07:00
parent 5063a2cdb6
commit 1a4e8f89bd
2 changed files with 5 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/nlsat_smt/nl_purify_tactic.cpp
View file

@ -264,7 +264,7 @@ private:
void display_result(std::ostream& out, goal_ref_buffer const& result) { void display_result(std::ostream& out, goal_ref_buffer const& result) {
for (unsigned i = 0; i < result.size(); ++i) { for (unsigned i = 0; i < result.size(); ++i) {
result[i]->display(tout << "goal\n"); result[i]->display(out << "goal\n");
} }
} }

27
src/test/ddnf.cpp
View file

@ -21,15 +21,12 @@ void read_nums(std::istream& is, unsigned & x, unsigned& y) {
std::getline(is, line); std::getline(is, line);
} }
static bool g_verbose = false;
static char const* g_file = 0; static char const* g_file = 0;
void create_forwarding(char const* file, datalog::ddnf_core& ddnf, ptr_vector<tbv>& tbvs) { void create_forwarding(char const* file, datalog::ddnf_core& ddnf, ptr_vector<tbv>& tbvs) {
if (g_verbose) { IF_VERBOSE(1, verbose_stream() << "creating (and forgetting) forwarding index\n";);
std::cout << "creating (and forgetting) forwarding index\n";
}
std::ifstream is(file); std::ifstream is(file);
if (is.bad() || is.fail()) { if (is.bad() || is.fail()) {
std::cout << "could not load " << file << "\n"; std::cout << "could not load " << file << "\n";
@ -72,9 +69,7 @@ void create_forwarding(char const* file, datalog::ddnf_core& ddnf, ptr_vector<tb
datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) { datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
if (g_verbose) { IF_VERBOSE(1, verbose_stream() << "populate ddnf\n";);
std::cout << "populate ddnf\n";
}
std::ifstream is(file); std::ifstream is(file);
if (is.bad() || is.fail()) { if (is.bad() || is.fail()) {
@ -91,9 +86,7 @@ datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
for (unsigned r = 0; r < M; ++r) { for (unsigned r = 0; r < M; ++r) {
unsigned P, K; unsigned P, K;
read_nums(is, K, P); read_nums(is, K, P);
if (g_verbose) { IF_VERBOSE(1, verbose_stream() << K << " " << P << "\n";);
std::cout << K << " " << P << "\n";
}
unsigned p; unsigned p;
for (unsigned g = 0; g < K; ++g) { for (unsigned g = 0; g < K; ++g) {
is >> p; is >> p;
@ -123,15 +116,6 @@ static void read_args(char ** argv, int argc) {
return; return;
} }
for (int i = 2; i < argc; ++i) {
if (argv[i] == "v") {
g_verbose = true;
}
else {
g_file = argv[i];
}
}
if (!g_file) { if (!g_file) {
std::cout << "Need routing table file as argument. Arguments provided: "; std::cout << "Need routing table file as argument. Arguments provided: ";
for (int i = 0; i < argc; ++i) { for (int i = 0; i < argc; ++i) {
@ -150,10 +134,7 @@ void tst_ddnf(char ** argv, int argc, int& i) {
create_forwarding(g_file, *ddnf, tbvs); create_forwarding(g_file, *ddnf, tbvs);
std::cout << "resulting size: " << ddnf->size() << "\n"; std::cout << "resulting size: " << ddnf->size() << "\n";
ddnf->display_statistics(std::cout); ddnf->display_statistics(std::cout);
if (g_verbose) { IF_VERBOSE(1, ddnf->display(verbose_stream()););
ddnf->display(std::cout);
}
std::cout.flush();
tbv_manager& tbvm = ddnf->get_tbv_manager(); tbv_manager& tbvm = ddnf->get_tbv_manager();
for (unsigned i = 0; i < tbvs.size(); ++i) { for (unsigned i = 0; i < tbvs.size(); ++i) {