mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

comments for log_axiom_definitions

Browse source
This commit is contained in:
Nils Becker 2019-04-09 16:54:54 +02:00
parent e79f7ca1fd
commit 7ead159b2d
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/datatype_decl_plugin.cpp
View file

@ -459,6 +459,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) {
m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
++m_id_counter; ++m_id_counter;
@ -470,6 +472,8 @@ namespace datatype {
} }
m_manager->trace_stream() << "\n"; m_manager->trace_stream() << "\n";
++m_id_counter; ++m_id_counter;
// axioms for all accessors are generated when a constructor is applied => use constructor as pattern
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; m_manager->trace_stream() << "[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);
@ -478,6 +482,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);