mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

mbqi support

Browse source
This commit is contained in:
nilsbecker 2019-01-05 14:44:06 +01:00
parent 6d2cf4f464
commit 58def55796
2 changed files with 45 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.cpp
View file

@ -28,6 +28,7 @@ Revision History:
#include "ast/ast_smt2_pp.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_translation.h"
#include "util/z3_version.h"
// -----------------------------------
@ -1364,6 +1365,7 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
if (trace_file) {
m_trace_stream = alloc(std::fstream, trace_file, std::ios_base::out);
m_trace_stream_owner = true;
*m_trace_stream << "[tool-version] Z3 " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\n";
}
if (!is_format_manager)
@ -2346,7 +2348,7 @@ var * ast_manager::mk_var(unsigned idx, sort * s) {
var * r = register_node(new_node);
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-var] #" << r->get_id() << "\n";
*m_trace_stream << "[mk-var] #" << r->get_id() << " " << idx << "\n";
}
return r;
}

12
src/smt/smt_quantifier.cpp
View file

@ -210,7 +210,14 @@ namespace smt {
get_stat(q)->update_max_generation(max_generation);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
if (f) {
if (has_trace_stream() && pat != nullptr) {
if (has_trace_stream()) {
if (pat == nullptr) {
trace_stream() << "[mbqi-triggered] " << static_cast<void*>(f) << " #" << q->get_id();
for (unsigned i = 0; i < num_bindings; ++i) {
trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id();
}
trace_stream() << "\n";
} else {
std::ostream & out = trace_stream();
obj_hashtable<enode> already_visited;
@ -235,7 +242,7 @@ namespace smt {
for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing.
// This nasty side-effect may change the behavior of Z3.
out << " #" << bindings[i]->get_owner_id();
out << " #" << bindings[num_bindings - i - 1]->get_owner_id();
}
out << " ;";
for (auto n : used_enodes) {
@ -249,6 +256,7 @@ namespace smt {
}
out << "\n";
}
}
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
m_num_instances++;
}