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

Merge pull request #2264 from Nils-Becker/master

Browse source 
Logging Support for Nested Quantifiers
This commit is contained in:
Nikolaj Bjorner 2019-05-09 12:02:40 +02:00 • committed by GitHub
commit 4d05a11144
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -2443,7 +2443,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
static void trace_quant(std::ostream& strm, quantifier* q) { static void trace_quant(std::ostream& strm, quantifier* q) {
strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]") strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
<< " #" << q->get_id() << " " << q->get_qid(); << " #" << q->get_id() << " " << q->get_qid() << " " << q->get_num_decls();
for (unsigned i = 0; i < q->get_num_patterns(); ++i) { for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
strm << " #" << q->get_pattern(i)->get_id(); strm << " #" << q->get_pattern(i)->get_id();
} }

10
src/ast/datatype_decl_plugin.cpp
View file

@ -461,6 +461,8 @@ namespace datatype {
func_decl_ref f = c->instantiate(new_sort); func_decl_ref f = c->instantiate(new_sort);
const unsigned num_args = f->get_arity(); const unsigned num_args = f->get_arity();
if (num_args == 0) continue; if (num_args == 0) continue;
// log constructor with quantified variables as arguments
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
++m_id_counter; ++m_id_counter;
@ -472,6 +474,8 @@ namespace datatype {
} }
out << "\n"; out << "\n";
++m_id_counter; ++m_id_counter;
// axioms for all accessors are generated when a constructor is applied => use constructor as pattern
out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
++m_id_counter; ++m_id_counter;
m_axiom_bases.insert(f->get_name(), constructor_id + 4); m_axiom_bases.insert(f->get_name(), constructor_id + 4);
@ -480,6 +484,8 @@ namespace datatype {
var_sorts << " (;" << a->range()->get_name() << ")"; var_sorts << " (;" << a->range()->get_name() << ")";
} }
std::string var_description = var_sorts.str(); std::string var_description = var_sorts.str();
// create axioms: the ith accessor returns the ith argument of the constructor
unsigned i = 0; unsigned i = 0;
for (accessor const* a : *c) { for (accessor const* a : *c) {
func_decl_ref acc = a->instantiate(new_sort); func_decl_ref acc = a->instantiate(new_sort);
@ -488,8 +494,8 @@ namespace datatype {
out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i
<< " " << family_name << "#" << m_id_counter - 1 << "\n"; << " " << family_name << "#" << m_id_counter - 1 << "\n";
++m_id_counter; ++m_id_counter;
out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << num_args << " " << family_name
<< " " << family_name << "#" << m_id_counter - 1 << "\n"; << "#" << constructor_id + 1 << " " << family_name << "#" << m_id_counter - 1 << "\n";
out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
++m_id_counter; ++m_id_counter;
++i; ++i;

4
src/smt/qi_queue.cpp
View file

@ -216,8 +216,10 @@ namespace smt {
if (m_manager.is_true(s_instance)) { if (m_manager.is_true(s_instance)) {
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
if (m_manager.has_trace_stream()) if (m_manager.has_trace_stream()) {
display_instance_profile(f, q, num_bindings, bindings, pr->get_id(), generation);
m_manager.trace_stream() << "[end-of-instance]\n"; m_manager.trace_stream() << "[end-of-instance]\n";
}
return; return;
} }