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

hide new datatype plugin

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-03 20:01:59 -07:00
parent 09386e43e3
commit a3dba5b2f9
24 changed files with 211 additions and 191 deletions
Download patch file Download diff file Expand all files Collapse all files

107
src/api/api_datatype.cpp
View file

@ -69,18 +69,13 @@ extern "C" {
// create constructor // create constructor
SASSERT(dt_util.is_datatype(tuple)); SASSERT(dt_util.is_datatype(tuple));
SASSERT(!dt_util.is_recursive(tuple)); SASSERT(!dt_util.is_recursive(tuple));
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(tuple);
func_decl* decl = (*decls)[0]; func_decl* decl = (decls)[0];
mk_c(c)->save_multiple_ast_trail(decl); mk_c(c)->save_multiple_ast_trail(decl);
*mk_tuple_decl = of_func_decl(decl); *mk_tuple_decl = of_func_decl(decl);
// Create projections // Create projections
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl); ptr_vector<func_decl> const & _accs = dt_util.get_constructor_accessors(decl);
if (!accs) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
ptr_vector<func_decl> const & _accs = *accs;
SASSERT(_accs.size() == num_fields); SASSERT(_accs.size() == num_fields);
for (unsigned i = 0; i < _accs.size(); i++) { for (unsigned i = 0; i < _accs.size(); i++) {
mk_c(c)->save_multiple_ast_trail(_accs[i]); mk_c(c)->save_multiple_ast_trail(_accs[i]);
@ -136,10 +131,10 @@ extern "C" {
// create constructor // create constructor
SASSERT(dt_util.is_datatype(e)); SASSERT(dt_util.is_datatype(e));
SASSERT(!dt_util.is_recursive(e)); SASSERT(!dt_util.is_recursive(e));
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(e); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(e);
SASSERT(decls && decls->size() == n); SASSERT(decls.size() == n);
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
func_decl* decl = (*decls)[i]; func_decl* decl = (decls)[i];
mk_c(c)->save_multiple_ast_trail(decl); mk_c(c)->save_multiple_ast_trail(decl);
enum_consts[i] = of_func_decl(decl); enum_consts[i] = of_func_decl(decl);
decl = dt_util.get_constructor_recognizer(decl); decl = dt_util.get_constructor_recognizer(decl);
@ -191,7 +186,7 @@ extern "C" {
sort * s = sorts.get(0); sort * s = sorts.get(0);
mk_c(c)->save_multiple_ast_trail(s); mk_c(c)->save_multiple_ast_trail(s);
ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s); ptr_vector<func_decl> const& cnstrs = data_util.get_datatype_constructors(s);
SASSERT(cnstrs.size() == 2); SASSERT(cnstrs.size() == 2);
func_decl* f; func_decl* f;
if (nil_decl) { if (nil_decl) {
@ -215,18 +210,16 @@ extern "C" {
*is_cons_decl = of_func_decl(f); *is_cons_decl = of_func_decl(f);
} }
if (head_decl) { if (head_decl) {
ptr_vector<func_decl> const* acc = data_util.get_constructor_accessors(cnstrs[1]); ptr_vector<func_decl> const& acc = data_util.get_constructor_accessors(cnstrs[1]);
SASSERT(acc); SASSERT(acc.size() == 2);
SASSERT(acc->size() == 2); f = (acc)[0];
f = (*acc)[0];
mk_c(c)->save_multiple_ast_trail(f); mk_c(c)->save_multiple_ast_trail(f);
*head_decl = of_func_decl(f); *head_decl = of_func_decl(f);
} }
if (tail_decl) { if (tail_decl) {
ptr_vector<func_decl> const* acc = data_util.get_constructor_accessors(cnstrs[1]); ptr_vector<func_decl> const& acc = data_util.get_constructor_accessors(cnstrs[1]);
SASSERT(acc); SASSERT(acc.size() == 2);
SASSERT(acc->size() == 2); f = (acc)[1];
f = (*acc)[1];
mk_c(c)->save_multiple_ast_trail(f); mk_c(c)->save_multiple_ast_trail(f);
*tail_decl = of_func_decl(f); *tail_decl = of_func_decl(f);
} }
@ -301,13 +294,9 @@ extern "C" {
*tester = of_func_decl(f2); *tester = of_func_decl(f2);
} }
ptr_vector<func_decl> const* accs = data_util.get_constructor_accessors(f); ptr_vector<func_decl> const& accs = data_util.get_constructor_accessors(f);
if (!accs && num_fields > 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return;
}
for (unsigned i = 0; i < num_fields; ++i) { for (unsigned i = 0; i < num_fields; ++i) {
func_decl* f2 = (*accs)[i]; func_decl* f2 = (accs)[i];
mk_c(c)->save_multiple_ast_trail(f2); mk_c(c)->save_multiple_ast_trail(f2);
accessors[i] = of_func_decl(f2); accessors[i] = of_func_decl(f2);
} }
@ -368,11 +357,11 @@ extern "C" {
sort * s = sorts.get(0); sort * s = sorts.get(0);
mk_c(c)->save_ast_trail(s); mk_c(c)->save_ast_trail(s);
ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s); ptr_vector<func_decl> const& cnstrs = data_util.get_datatype_constructors(s);
for (unsigned i = 0; i < num_constructors; ++i) { for (unsigned i = 0; i < num_constructors; ++i) {
constructor* cn = reinterpret_cast<constructor*>(constructors[i]); constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
cn->m_constructor = (*cnstrs)[i]; cn->m_constructor = cnstrs[i];
} }
RETURN_Z3_mk_datatype(of_sort(s)); RETURN_Z3_mk_datatype(of_sort(s));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -434,10 +423,10 @@ extern "C" {
mk_c(c)->save_multiple_ast_trail(s); mk_c(c)->save_multiple_ast_trail(s);
sorts[i] = of_sort(s); sorts[i] = of_sort(s);
constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]); constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
ptr_vector<func_decl> const* cnstrs = data_util.get_datatype_constructors(s); ptr_vector<func_decl> const& cnstrs = data_util.get_datatype_constructors(s);
for (unsigned j = 0; j < cl->size(); ++j) { for (unsigned j = 0; j < cl->size(); ++j) {
constructor* cn = (*cl)[j]; constructor* cn = (*cl)[j];
cn->m_constructor = (*cnstrs)[j]; cn->m_constructor = cnstrs[j];
} }
} }
RETURN_Z3_mk_datatypes; RETURN_Z3_mk_datatypes;
@ -456,12 +445,7 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); return dt_util.get_datatype_constructors(_t).size();
if (!decls) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return decls->size();
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -474,12 +458,12 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(_t);
if (!decls || idx >= decls->size()) { if (idx >= decls.size()) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
func_decl* decl = (*decls)[idx]; func_decl* decl = (decls)[idx];
mk_c(c)->save_ast_trail(decl); mk_c(c)->save_ast_trail(decl);
return of_func_decl(decl); return of_func_decl(decl);
} }
@ -504,12 +488,12 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(_t);
if (!decls || idx >= decls->size()) { if (idx >= decls.size()) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
func_decl* decl = (*decls)[idx]; func_decl* decl = (decls)[idx];
decl = dt_util.get_constructor_recognizer(decl); decl = dt_util.get_constructor_recognizer(decl);
mk_c(c)->save_ast_trail(decl); mk_c(c)->save_ast_trail(decl);
RETURN_Z3(of_func_decl(decl)); RETURN_Z3(of_func_decl(decl));
@ -527,23 +511,23 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(_t);
if (!decls || idx_c >= decls->size()) { if (idx_c >= decls.size()) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
func_decl* decl = (*decls)[idx_c]; func_decl* decl = (decls)[idx_c];
if (decl->get_arity() <= idx_a) { if (decl->get_arity() <= idx_a) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors(decl); ptr_vector<func_decl> const & accs = dt_util.get_constructor_accessors(decl);
SASSERT(accs && accs->size() == decl->get_arity()); SASSERT(accs.size() == decl->get_arity());
if (!accs || accs->size() <= idx_a) { if (accs.size() <= idx_a) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
decl = (*accs)[idx_a]; decl = (accs)[idx_a];
mk_c(c)->save_ast_trail(decl); mk_c(c)->save_ast_trail(decl);
RETURN_Z3(of_func_decl(decl)); RETURN_Z3(of_func_decl(decl));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -574,16 +558,13 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(tuple);
if (!decls || decls->size() != 1) { if (decls.size() != 1) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
return 0; return 0;
} }
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors((*decls)[0]); ptr_vector<func_decl> const & accs = dt_util.get_constructor_accessors(decls[0]);
if (!accs) { return accs.size();
return 0;
}
return accs->size();
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -597,21 +578,17 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(tuple); ptr_vector<func_decl> const & decls = dt_util.get_datatype_constructors(tuple);
if (!decls || decls->size() != 1) { if (decls.size() != 1) {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
ptr_vector<func_decl> const * accs = dt_util.get_constructor_accessors((*decls)[0]); ptr_vector<func_decl> const & accs = dt_util.get_constructor_accessors((decls)[0]);
if (!accs) { if (accs.size() <= i) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
if (accs->size() <= i) {
SET_ERROR_CODE(Z3_IOB); SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0); RETURN_Z3(0);
} }
func_decl* acc = (*accs)[i]; func_decl* acc = (accs)[i];
mk_c(c)->save_ast_trail(acc); mk_c(c)->save_ast_trail(acc);
RETURN_Z3(of_func_decl(acc)); RETURN_Z3(of_func_decl(acc));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);

17
src/ast/ast_smt_pp.cpp
View file

@ -907,7 +907,6 @@ public:
void pp_dt(ast_mark& mark, sort* s) { void pp_dt(ast_mark& mark, sort* s) {
SASSERT(s->is_sort_of(m_dt_fid, DATATYPE_SORT)); SASSERT(s->is_sort_of(m_dt_fid, DATATYPE_SORT));
datatype_util util(m_manager); datatype_util util(m_manager);
ptr_vector<func_decl> const* decls;
ptr_vector<sort> rec_sorts; ptr_vector<sort> rec_sorts;
rec_sorts.push_back(s); rec_sorts.push_back(s);
@ -916,10 +915,10 @@ public:
// collect siblings and sorts that have not already been printed. // collect siblings and sorts that have not already been printed.
for (unsigned h = 0; h < rec_sorts.size(); ++h) { for (unsigned h = 0; h < rec_sorts.size(); ++h) {
s = rec_sorts[h]; s = rec_sorts[h];
decls = util.get_datatype_constructors(s); ptr_vector<func_decl> const& decls = util.get_datatype_constructors(s);
for (unsigned i = 0; i < decls->size(); ++i) { for (unsigned i = 0; i < decls.size(); ++i) {
func_decl* f = (*decls)[i]; func_decl* f = decls[i];
for (unsigned j = 0; j < f->get_arity(); ++j) { for (unsigned j = 0; j < f->get_arity(); ++j) {
sort* s2 = f->get_domain(j); sort* s2 = f->get_domain(j);
if (!mark.is_marked(s2)) { if (!mark.is_marked(s2)) {
@ -955,11 +954,11 @@ public:
m_out << "("; m_out << "(";
m_out << m_renaming.get_symbol(s->get_name()); m_out << m_renaming.get_symbol(s->get_name());
m_out << " "; m_out << " ";
decls = util.get_datatype_constructors(s); ptr_vector<func_decl> const& decls = util.get_datatype_constructors(s);
for (unsigned i = 0; i < decls->size(); ++i) { for (unsigned i = 0; i < decls.size(); ++i) {
func_decl* f = (*decls)[i]; func_decl* f = decls[i];
ptr_vector<func_decl> const& accs = *util.get_constructor_accessors(f); ptr_vector<func_decl> const& accs = util.get_constructor_accessors(f);
if (m_is_smt2 || accs.size() > 0) { if (m_is_smt2 || accs.size() > 0) {
m_out << "("; m_out << "(";
} }
@ -976,7 +975,7 @@ public:
} }
if (m_is_smt2 || accs.size() > 0) { if (m_is_smt2 || accs.size() > 0) {
m_out << ")"; m_out << ")";
if (i + 1 < decls->size()) { if (i + 1 < decls.size()) {
m_out << " "; m_out << " ";
} }
} }

37
src/ast/datatype_decl_plugin.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "util/warning.h" #include "util/warning.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#ifndef DATATYPE_V2
/** /**
\brief Auxiliary class used to declare inductive datatypes. \brief Auxiliary class used to declare inductive datatypes.
@ -802,11 +803,11 @@ func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id) {
return d; return d;
} }
ptr_vector<func_decl> const * datatype_util::get_datatype_constructors(sort * ty) { ptr_vector<func_decl> const & datatype_util::get_datatype_constructors(sort * ty) {
SASSERT(is_datatype(ty)); SASSERT(is_datatype(ty));
ptr_vector<func_decl> * r = 0; ptr_vector<func_decl> * r = 0;
if (m_datatype2constructors.find(ty, r)) if (m_datatype2constructors.find(ty, r))
return r; return *r;
r = alloc(ptr_vector<func_decl>); r = alloc(ptr_vector<func_decl>);
m_asts.push_back(ty); m_asts.push_back(ty);
m_vectors.push_back(r); m_vectors.push_back(r);
@ -819,7 +820,7 @@ ptr_vector<func_decl> const * datatype_util::get_datatype_constructors(sort * ty
m_asts.push_back(c); m_asts.push_back(c);
r->push_back(c); r->push_back(c);
} }
return r; return *r;
} }
/** /**
@ -854,12 +855,12 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
// 1) T_i's are not recursive // 1) T_i's are not recursive
// If there is no such constructor, then we select one that // If there is no such constructor, then we select one that
// 2) each type T_i is not recursive or contains a constructor that does not depend on T // 2) each type T_i is not recursive or contains a constructor that does not depend on T
ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty); ptr_vector<func_decl> const & constructors = get_datatype_constructors(ty);
// step 1) // step 1)
unsigned sz = constructors->size(); unsigned sz = constructors.size();
++m_start; ++m_start;
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = (*constructors)[(j + m_start) % sz]; func_decl * c = constructors[(j + m_start) % sz];
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;
for (; i < num_args; i++) { for (; i < num_args; i++) {
@ -872,7 +873,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
} }
// step 2) // step 2)
for (unsigned j = 0; j < sz; ++j) { for (unsigned j = 0; j < sz; ++j) {
func_decl * c = (*constructors)[(j + m_start) % sz]; func_decl * c = constructors[(j + m_start) % sz];
TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";); TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
unsigned num_args = c->get_arity(); unsigned num_args = c->get_arity();
unsigned i = 0; unsigned i = 0;
@ -915,11 +916,11 @@ func_decl * datatype_util::get_constructor_recognizer(func_decl * constructor) {
return d; return d;
} }
ptr_vector<func_decl> const * datatype_util::get_constructor_accessors(func_decl * constructor) { ptr_vector<func_decl> const & datatype_util::get_constructor_accessors(func_decl * constructor) {
SASSERT(is_constructor(constructor)); SASSERT(is_constructor(constructor));
ptr_vector<func_decl> * res = 0; ptr_vector<func_decl> * res = 0;
if (m_constructor2accessors.find(constructor, res)) if (m_constructor2accessors.find(constructor, res))
return res; return *res;
res = alloc(ptr_vector<func_decl>); res = alloc(ptr_vector<func_decl>);
m_asts.push_back(constructor); m_asts.push_back(constructor);
m_vectors.push_back(res); m_vectors.push_back(res);
@ -938,7 +939,7 @@ ptr_vector<func_decl> const * datatype_util::get_constructor_accessors(func_decl
m_asts.push_back(d); m_asts.push_back(d);
res->push_back(d); res->push_back(d);
} }
return res; return *res;
} }
func_decl * datatype_util::get_accessor_constructor(func_decl * accessor) { func_decl * datatype_util::get_accessor_constructor(func_decl * accessor) {
@ -988,7 +989,7 @@ bool datatype_util::is_enum_sort(sort* s) {
bool r = false; bool r = false;
if (m_is_enum.find(s, r)) if (m_is_enum.find(s, r))
return r; return r;
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s); ptr_vector<func_decl> const& cnstrs = get_datatype_constructors(s);
r = true; r = true;
for (unsigned i = 0; r && i < cnstrs.size(); ++i) { for (unsigned i = 0; r && i < cnstrs.size(); ++i) {
r = cnstrs[i]->get_arity() == 0; r = cnstrs[i]->get_arity() == 0;
@ -1048,14 +1049,14 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) {
todo.pop_back(); todo.pop_back();
strm << s->get_name() << " =\n"; strm << s->get_name() << " =\n";
ptr_vector<func_decl> const * cnstrs = get_datatype_constructors(s); ptr_vector<func_decl> const & cnstrs = get_datatype_constructors(s);
for (unsigned i = 0; i < cnstrs->size(); ++i) { for (unsigned i = 0; i < cnstrs.size(); ++i) {
func_decl* cns = (*cnstrs)[i]; func_decl* cns = cnstrs[i];
func_decl* rec = get_constructor_recognizer(cns); func_decl* rec = get_constructor_recognizer(cns);
strm << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; strm << " " << cns->get_name() << " :: " << rec->get_name() << " :: ";
ptr_vector<func_decl> const * accs = get_constructor_accessors(cns); ptr_vector<func_decl> const & accs = get_constructor_accessors(cns);
for (unsigned j = 0; j < accs->size(); ++j) { for (unsigned j = 0; j < accs.size(); ++j) {
func_decl* acc = (*accs)[j]; func_decl* acc = accs[j];
sort* s1 = acc->get_range(); sort* s1 = acc->get_range();
strm << "(" << acc->get_name() << ": " << s1->get_name() << ") "; strm << "(" << acc->get_name() << ": " << s1->get_name() << ") ";
if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) {
@ -1090,3 +1091,5 @@ bool datatype_util::is_constructor_of(unsigned num_params, parameter const* para
params[1] == f->get_parameter(1); params[1] == f->get_parameter(1);
} }
#endif

11
src/ast/datatype_decl_plugin.h
View file

@ -16,9 +16,15 @@ Author:
Revision History: Revision History:
--*/ --*/
// define DATATYPE_V2
#ifdef DATATYPE_V2
#include "ast/datatype_decl_plugin2.h"
#else
#ifndef DATATYPE_DECL_PLUGIN_H_ #ifndef DATATYPE_DECL_PLUGIN_H_
#define DATATYPE_DECL_PLUGIN_H_ #define DATATYPE_DECL_PLUGIN_H_
#include "ast/ast.h" #include "ast/ast.h"
#include "util/tptr.h" #include "util/tptr.h"
#include "util/buffer.h" #include "util/buffer.h"
@ -210,7 +216,7 @@ public:
bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); } bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
ptr_vector<func_decl> const * get_datatype_constructors(sort * ty); ptr_vector<func_decl> const & get_datatype_constructors(sort * ty);
unsigned get_datatype_num_constructors(sort * ty) { unsigned get_datatype_num_constructors(sort * ty) {
SASSERT(is_datatype(ty)); SASSERT(is_datatype(ty));
unsigned tid = ty->get_parameter(1).get_int(); unsigned tid = ty->get_parameter(1).get_int();
@ -230,7 +236,7 @@ public:
unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); } unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); }
func_decl * get_non_rec_constructor(sort * ty); func_decl * get_non_rec_constructor(sort * ty);
func_decl * get_constructor_recognizer(func_decl * constructor); func_decl * get_constructor_recognizer(func_decl * constructor);
ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor); ptr_vector<func_decl> const & get_constructor_accessors(func_decl * constructor);
func_decl * get_accessor_constructor(func_decl * accessor); func_decl * get_accessor_constructor(func_decl * accessor);
func_decl * get_recognizer_constructor(func_decl * recognizer); func_decl * get_recognizer_constructor(func_decl * recognizer);
family_id get_family_id() const { return m_family_id; } family_id get_family_id() const { return m_family_id; }
@ -245,3 +251,4 @@ public:
#endif /* DATATYPE_DECL_PLUGIN_H_ */ #endif /* DATATYPE_DECL_PLUGIN_H_ */
#endif /* DATATYPE_V2 */

12
src/ast/datatype_decl_plugin2.cpp
View file

@ -22,6 +22,7 @@ Revision History:
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#ifdef DATATYPE_V2
namespace datatype { namespace datatype {
void accessor::fix_range(sort_ref_vector const& dts) { void accessor::fix_range(sort_ref_vector const& dts) {
@ -49,6 +50,10 @@ namespace datatype {
def const& accessor::get_def() const { return m_constructor->get_def(); } def const& accessor::get_def() const { return m_constructor->get_def(); }
util& accessor::u() const { return m_constructor->u(); } util& accessor::u() const { return m_constructor->u(); }
constructor::~constructor() {
for (accessor* a : m_accessors) dealloc(a);
m_accessors.reset();
}
util& constructor::u() const { return m_def->u(); } util& constructor::u() const { return m_def->u(); }
func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const { func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const {
@ -164,7 +169,7 @@ namespace datatype {
sort* r = to_sort(parameters[i].get_ast()); sort* r = to_sort(parameters[i].get_ast());
S.insert(d->params()[i], r->get_num_elements()); S.insert(d->params()[i], r->get_num_elements());
} }
sort_size ts = d->sort_size()->fold(S); sort_size ts = d->sort_size()->eval(S);
s->set_num_elements(ts); s->set_num_elements(ts);
} }
return s; return s;
@ -278,7 +283,9 @@ namespace datatype {
def& plugin::add(symbol const& name, unsigned n, sort * const * params) { def& plugin::add(symbol const& name, unsigned n, sort * const * params) {
ast_manager& m = *m_manager; ast_manager& m = *m_manager;
def* d = alloc(def, m, u(), name, m_class_id, n, params); def* d = 0;
if (m_defs.find(name, d)) dealloc(d);
d = alloc(def, m, u(), name, m_class_id, n, params);
m_defs.insert(name, d); m_defs.insert(name, d);
m_def_block.push_back(name); m_def_block.push_back(name);
return *d; return *d;
@ -895,3 +902,4 @@ namespace datatype {
} }
} }
} }
#endif

72
src/ast/datatype_decl_plugin2.h
View file

@ -24,12 +24,7 @@ Revision History:
#include "util/symbol_table.h" #include "util/symbol_table.h"
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
namespace datatype { #ifdef DATATYPE_V2
class util;
class def;
class accessor;
class constructor;
enum sort_kind { enum sort_kind {
DATATYPE_SORT DATATYPE_SORT
@ -43,6 +38,14 @@ namespace datatype {
LAST_DT_OP LAST_DT_OP
}; };
namespace datatype {
class util;
class def;
class accessor;
class constructor;
class accessor { class accessor {
symbol m_name; symbol m_name;
sort* m_range; sort* m_range;
@ -109,7 +112,7 @@ namespace datatype {
static size* mk_power(size* a1, size* a2); static size* mk_power(size* a1, size* a2);
virtual size* subst(obj_map<sort, size*>& S) = 0; virtual size* subst(obj_map<sort, size*>& S) = 0;
virtual sort_size fold(obj_map<sort, sort_size> const& S) = 0; virtual sort_size eval(obj_map<sort, sort_size> const& S) = 0;
}; };
struct offset : public size { struct offset : public size {
@ -117,16 +120,16 @@ namespace datatype {
offset(sort_size const& s): m_offset(s) {} offset(sort_size const& s): m_offset(s) {}
virtual ~offset() {} virtual ~offset() {}
virtual size* subst(obj_map<sort,size*>& S) { return this; } virtual size* subst(obj_map<sort,size*>& S) { return this; }
virtual sort_size fold(obj_map<sort, sort_size> const& S) { return m_offset; } virtual sort_size eval(obj_map<sort, sort_size> const& S) { return m_offset; }
}; };
struct plus : public size { struct plus : public size {
size* m_arg1, *m_arg2; size* m_arg1, *m_arg2;
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();} plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); } virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); } virtual size* subst(obj_map<sort,size*>& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size fold(obj_map<sort, sort_size> const& S) { virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->fold(S); sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->fold(S); sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1; if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2; if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1; if (s1.is_very_big()) return s1;
@ -140,9 +143,9 @@ namespace datatype {
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); } virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); } virtual size* subst(obj_map<sort,size*>& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size fold(obj_map<sort, sort_size> const& S) { virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->fold(S); sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->fold(S); sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1; if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2; if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1; if (s1.is_very_big()) return s1;
@ -156,9 +159,9 @@ namespace datatype {
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); } virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); } virtual size* subst(obj_map<sort,size*>& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size fold(obj_map<sort, sort_size> const& S) { virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->fold(S); sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->fold(S); sort_size s2 = m_arg2->eval(S);
// s1^s2 // s1^s2
if (s1.is_infinite()) return s1; if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2; if (s2.is_infinite()) return s2;
@ -176,7 +179,7 @@ namespace datatype {
sparam(sort_ref& p): m_param(p) {} sparam(sort_ref& p): m_param(p) {}
virtual ~sparam() {} virtual ~sparam() {}
virtual size* subst(obj_map<sort,size*>& S) { return S[m_param]; } virtual size* subst(obj_map<sort,size*>& S) { return S[m_param]; }
virtual sort_size fold(obj_map<sort, sort_size> const& S) { return S[m_param]; } virtual sort_size eval(obj_map<sort, sort_size> const& S) { return S[m_param]; }
}; };
}; };
@ -201,6 +204,8 @@ namespace datatype {
{} {}
~def() { ~def() {
if (m_sort_size) m_sort_size->dec_ref(); if (m_sort_size) m_sort_size->dec_ref();
for (constructor* c : m_constructors) dealloc(c);
m_constructors.reset();
} }
void add(constructor* c) { void add(constructor* c) {
m_constructors.push_back(c); m_constructors.push_back(c);
@ -361,5 +366,36 @@ namespace datatype {
}; };
#ifdef DATATYPE_V2
typedef datatype::accessor accessor_decl;
typedef datatype::constructor constructor_decl;
typedef datatype::def datatype_decl;
typedef datatype::decl::plugin datatype_decl_plugin;
typedef datatype::util datatype_util;
class type_ref {
void * m_data;
public:
type_ref():m_data(TAG(void *, static_cast<void*>(0), 1)) {}
type_ref(int idx):m_data(BOXINT(void *, idx)) {}
type_ref(sort * s):m_data(TAG(void *, s, 1)) {}
bool is_idx() const { return GET_TAG(m_data) == 0; }
bool is_sort() const { return GET_TAG(m_data) == 1; }
sort * get_sort() const { return UNTAG(sort *, m_data); }
int get_idx() const { return UNBOXINT(m_data); }
};
inline accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) {
if (t.is_idx()) {
return alloc(accessor_decl, n, t.get_idx());
}
else {
return alloc(accessor_decl, n, t.get_sort());
}
}
#endif
#endif /* DATATYPE_DECL_PLUGIN_H_ */ #endif /* DATATYPE_DECL_PLUGIN_H_ */
#endif DATATYPE_V2

4
src/ast/decl_collector.cpp
View file

@ -28,9 +28,9 @@ void decl_collector::visit_sort(sort * n) {
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n); unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
for (unsigned i = 0; i < num_cnstr; i++) { for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i); func_decl * cnstr = m_dt_util.get_datatype_constructors(n).get(i);
m_decls.push_back(cnstr); m_decls.push_back(cnstr);
ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); ptr_vector<func_decl> const & cnstr_acc = m_dt_util.get_constructor_accessors(cnstr);
unsigned num_cas = cnstr_acc.size(); unsigned num_cas = cnstr_acc.size();
for (unsigned j = 0; j < num_cas; j++) { for (unsigned j = 0; j < num_cas; j++) {
func_decl * accsr = cnstr_acc.get(j); func_decl * accsr = cnstr_acc.get(j);

16
src/ast/rewriter/datatype_rewriter.cpp
View file

@ -47,11 +47,11 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
func_decl * c_decl = a->get_decl(); func_decl * c_decl = a->get_decl();
if (c_decl != m_util.get_accessor_constructor(f)) if (c_decl != m_util.get_accessor_constructor(f))
return BR_FAILED; return BR_FAILED;
ptr_vector<func_decl> const * acc = m_util.get_constructor_accessors(c_decl); ptr_vector<func_decl> const & acc = m_util.get_constructor_accessors(c_decl);
SASSERT(acc && acc->size() == a->get_num_args()); SASSERT(acc.size() == a->get_num_args());
unsigned num = acc->size(); unsigned num = acc.size();
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
if (f == (*acc)[i]) { if (f == acc[i]) {
// found it. // found it.
result = a->get_arg(i); result = a->get_arg(i);
return BR_DONE; return BR_DONE;
@ -70,13 +70,13 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
result = a; result = a;
return BR_DONE; return BR_DONE;
} }
ptr_vector<func_decl> const * acc = m_util.get_constructor_accessors(c_decl); ptr_vector<func_decl> const & acc = m_util.get_constructor_accessors(c_decl);
SASSERT(acc && acc->size() == a->get_num_args()); SASSERT(acc.size() == a->get_num_args());
unsigned num = acc->size(); unsigned num = acc.size();
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
if (f == (*acc)[i]) { if (f == acc[i]) {
new_args.push_back(args[1]); new_args.push_back(args[1]);
} }
else { else {

2
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -130,7 +130,7 @@ struct enum2bv_rewriter::imp {
m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size))); m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
} }
expr_ref f_def(m); expr_ref f_def(m);
ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s); ptr_vector<func_decl> const& cs = m_dt.get_datatype_constructors(s);
f_def = m.mk_const(cs[nc-1]); f_def = m.mk_const(cs[nc-1]);
for (unsigned i = nc - 1; i > 0; ) { for (unsigned i = nc - 1; i > 0; ) {
--i; --i;

12
src/cmd_context/cmd_context.cpp
View file

@ -1954,19 +1954,19 @@ cmd_context::dt_eh::~dt_eh() {
void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) { void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";); TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
ptr_vector<func_decl> const * constructors = m_dt_util.get_datatype_constructors(dt); ptr_vector<func_decl> const & constructors = m_dt_util.get_datatype_constructors(dt);
unsigned num_constructors = constructors->size(); unsigned num_constructors = constructors.size();
for (unsigned j = 0; j < num_constructors; j++) { for (unsigned j = 0; j < num_constructors; j++) {
func_decl * c = constructors->get(j); func_decl * c = constructors[j];
m_owner.insert(c); m_owner.insert(c);
TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";);
func_decl * r = m_dt_util.get_constructor_recognizer(c); func_decl * r = m_dt_util.get_constructor_recognizer(c);
m_owner.insert(r); m_owner.insert(r);
TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";);
ptr_vector<func_decl> const * accessors = m_dt_util.get_constructor_accessors(c); ptr_vector<func_decl> const & accessors = m_dt_util.get_constructor_accessors(c);
unsigned num_accessors = accessors->size(); unsigned num_accessors = accessors.size();
for (unsigned k = 0; k < num_accessors; k++) { for (unsigned k = 0; k < num_accessors; k++) {
func_decl * a = accessors->get(k); func_decl * a = accessors[k];
m_owner.insert(a); m_owner.insert(a);
TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";);
} }

2
src/muz/base/dl_rule.h
View file

@ -65,7 +65,7 @@ namespace datalog {
else if (m_dt.is_accessor(n)) { else if (m_dt.is_accessor(n)) {
sort* s = m.get_sort(n->get_arg(0)); sort* s = m.get_sort(n->get_arg(0));
SASSERT(m_dt.is_datatype(s)); SASSERT(m_dt.is_datatype(s));
if (m_dt.get_datatype_constructors(s)->size() > 1) { if (m_dt.get_datatype_constructors(s).size() > 1) {
m_found = true; m_found = true;
m_func = n->get_decl(); m_func = n->get_decl();
} }

2
src/muz/base/rule_properties.cpp
View file

@ -191,7 +191,7 @@ void rule_properties::operator()(app* n) {
else if (m_dt.is_accessor(n)) { else if (m_dt.is_accessor(n)) {
sort* s = m.get_sort(n->get_arg(0)); sort* s = m.get_sort(n->get_arg(0));
SASSERT(m_dt.is_datatype(s)); SASSERT(m_dt.is_datatype(s));
if (m_dt.get_datatype_constructors(s)->size() > 1) { if (m_dt.get_datatype_constructors(s).size() > 1) {
m_uninterp_funs.insert(n->get_decl(), m_rule); m_uninterp_funs.insert(n->get_decl(), m_rule);
} }
} }

10
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -808,7 +808,7 @@ namespace datalog {
datatype_util dtu(m); datatype_util dtu(m);
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
func_decl* p = r.get_decl(); func_decl* p = r.get_decl();
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m.get_sort(path)); ptr_vector<func_decl> const& succs = dtu.get_datatype_constructors(m.get_sort(path));
// populate substitution of bound variables. // populate substitution of bound variables.
r.get_vars(m, sorts); r.get_vars(m, sorts);
sub.reset(); sub.reset();
@ -871,8 +871,8 @@ namespace datalog {
path_var = m.mk_var(0, m_path_sort); path_var = m.mk_var(0, m_path_sort);
trace_var = m.mk_var(1, pred_sort); trace_var = m.mk_var(1, pred_sort);
// sort* sorts[2] = { pred_sort, m_path_sort }; // sort* sorts[2] = { pred_sort, m_path_sort };
ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(pred_sort); ptr_vector<func_decl> const& cnstrs = dtu.get_datatype_constructors(pred_sort);
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m_path_sort); ptr_vector<func_decl> const& succs = dtu.get_datatype_constructors(m_path_sort);
SASSERT(cnstrs.size() == rls.size()); SASSERT(cnstrs.size() == rls.size());
pred = m.mk_app(mk_predicate(p), trace_var.get(), path_var.get()); pred = m.mk_app(mk_predicate(p), trace_var.get(), path_var.get());
for (unsigned i = 0; i < rls.size(); ++i) { for (unsigned i = 0; i < rls.size(); ++i) {
@ -1039,8 +1039,8 @@ namespace datalog {
sort* trace_sort = m.get_sort(trace); sort* trace_sort = m.get_sort(trace);
func_decl* p = m_sort2pred.find(trace_sort); func_decl* p = m_sort2pred.find(trace_sort);
datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p); datalog::rule_vector const& rules = b.m_rules.get_predicate_rules(p);
ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(trace_sort); ptr_vector<func_decl> const& cnstrs = dtu.get_datatype_constructors(trace_sort);
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m_path_sort); ptr_vector<func_decl> const& succs = dtu.get_datatype_constructors(m_path_sort);
for (unsigned i = 0; i < cnstrs.size(); ++i) { for (unsigned i = 0; i < cnstrs.size(); ++i) {
if (trace->get_decl() == cnstrs[i]) { if (trace->get_decl() == cnstrs[i]) {
svector<std::pair<unsigned, unsigned> > positions; svector<std::pair<unsigned, unsigned> > positions;

2
src/muz/pdr/pdr_prop_solver.cpp
View file

@ -135,7 +135,7 @@ namespace pdr {
func_decl* f = to_app(val)->get_decl(); func_decl* f = to_app(val)->get_decl();
func_decl* r = dt.get_constructor_recognizer(f); func_decl* r = dt.get_constructor_recognizer(f);
conjs[i] = m.mk_app(r, c); conjs[i] = m.mk_app(r, c);
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f); ptr_vector<func_decl> const& acc = dt.get_constructor_accessors(f);
for (unsigned j = 0; j < acc.size(); ++j) { for (unsigned j = 0; j < acc.size(); ++j) {
conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j))); conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j)));
} }

2
src/muz/spacer/spacer_util.cpp
View file

@ -711,7 +711,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs)
func_decl* f = to_app(val)->get_decl(); func_decl* f = to_app(val)->get_decl();
func_decl* r = dt.get_constructor_recognizer(f); func_decl* r = dt.get_constructor_recognizer(f);
conjs[i] = m.mk_app(r, c); conjs[i] = m.mk_app(r, c);
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f); ptr_vector<func_decl> const& acc = dt.get_constructor_accessors(f);
for (unsigned j = 0; j < acc.size(); ++j) { for (unsigned j = 0; j < acc.size(); ++j) {
conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j))); conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j)));
} }

12
src/qe/qe_datatype_plugin.cpp
View file

@ -262,7 +262,7 @@ namespace qe {
} }
func_decl* c = a->get_decl(); func_decl* c = a->get_decl();
func_decl* r = m_util.get_constructor_recognizer(c); func_decl* r = m_util.get_constructor_recognizer(c);
ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c); ptr_vector<func_decl> const & acc = m_util.get_constructor_accessors(c);
SASSERT(acc.size() == a->get_num_args()); SASSERT(acc.size() == a->get_num_args());
// //
// It suffices to solve just the first available equality. // It suffices to solve just the first available equality.
@ -379,7 +379,7 @@ namespace qe {
return false; return false;
} }
func_decl* c = l->get_decl(); func_decl* c = l->get_decl();
ptr_vector<func_decl> const& acc = *m_util.get_constructor_accessors(c); ptr_vector<func_decl> const& acc = m_util.get_constructor_accessors(c);
func_decl* rec = m_util.get_constructor_recognizer(c); func_decl* rec = m_util.get_constructor_recognizer(c);
expr_ref_vector conj(m); expr_ref_vector conj(m);
conj.push_back(m.mk_app(rec, r)); conj.push_back(m.mk_app(rec, r));
@ -626,7 +626,7 @@ namespace qe {
// If 'x' does not yet have a recognizer, then branch according to recognizers. // If 'x' does not yet have a recognizer, then branch according to recognizers.
// //
if (!has_recognizer(x, fml, r, c)) { if (!has_recognizer(x, fml, r, c)) {
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()]; c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()];
r = m_datatype_util.get_constructor_recognizer(c); r = m_datatype_util.get_constructor_recognizer(c);
app* is_c = m.mk_app(r, x); app* is_c = m.mk_app(r, x);
// assert v => r(x) // assert v => r(x)
@ -673,7 +673,7 @@ namespace qe {
// Introduce auxiliary variable to eliminate. // Introduce auxiliary variable to eliminate.
// //
if (!has_recognizer(x, fml, r, c)) { if (!has_recognizer(x, fml, r, c)) {
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()]; c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()];
r = m_datatype_util.get_constructor_recognizer(c); r = m_datatype_util.get_constructor_recognizer(c);
app* is_c = m.mk_app(r, x); app* is_c = m.mk_app(r, x);
fml = m.mk_and(is_c, fml); fml = m.mk_and(is_c, fml);
@ -774,7 +774,7 @@ namespace qe {
return; return;
} }
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()]; c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()];
r = m_datatype_util.get_constructor_recognizer(c); r = m_datatype_util.get_constructor_recognizer(c);
app* is_c = m.mk_app(r, x); app* is_c = m.mk_app(r, x);
@ -794,7 +794,7 @@ namespace qe {
else { else {
SASSERT(vl.is_unsigned()); SASSERT(vl.is_unsigned());
SASSERT(vl.get_unsigned() < m_datatype_util.get_datatype_num_constructors(s)); SASSERT(vl.get_unsigned() < m_datatype_util.get_datatype_num_constructors(s));
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()]; c = m_datatype_util.get_datatype_constructors(s)[vl.get_unsigned()];
} }
subst_constructor(x, c, fml, def); subst_constructor(x, c, fml, def);
} }

6
src/qe/qe_datatypes.cpp
View file

@ -75,7 +75,7 @@ namespace qe {
app_ref arg(m); app_ref arg(m);
SASSERT(dt.is_constructor(m_val)); SASSERT(dt.is_constructor(m_val));
func_decl* f = m_val->get_decl(); func_decl* f = m_val->get_decl();
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f); ptr_vector<func_decl> const& acc = dt.get_constructor_accessors(f);
for (unsigned i = 0; i < acc.size(); ++i) { for (unsigned i = 0; i < acc.size(); ++i) {
arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range()); arg = m.mk_fresh_const(acc[i]->get_name().str().c_str(), acc[i]->get_range());
model.register_decl(arg->get_decl(), m_val->get_arg(i)); model.register_decl(arg->get_decl(), m_val->get_arg(i));
@ -152,7 +152,7 @@ namespace qe {
} }
func_decl* c = a->get_decl(); func_decl* c = a->get_decl();
func_decl* rec = dt.get_constructor_recognizer(c); func_decl* rec = dt.get_constructor_recognizer(c);
ptr_vector<func_decl> const & acc = *dt.get_constructor_accessors(c); ptr_vector<func_decl> const & acc = dt.get_constructor_accessors(c);
SASSERT(acc.size() == a->get_num_args()); SASSERT(acc.size() == a->get_num_args());
// //
// It suffices to solve just the first available equality. // It suffices to solve just the first available equality.
@ -230,7 +230,7 @@ namespace qe {
return false; return false;
} }
func_decl* c = to_app(l)->get_decl(); func_decl* c = to_app(l)->get_decl();
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(c); ptr_vector<func_decl> const& acc = dt.get_constructor_accessors(c);
if (!is_app_of(r, c)) { if (!is_app_of(r, c)) {
lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r)); lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r));
} }

2
src/qe/qe_lite.cpp
View file

@ -671,7 +671,7 @@ namespace eq {
else { else {
func_decl* rec = dt.get_constructor_recognizer(d); func_decl* rec = dt.get_constructor_recognizer(d);
conjs.push_back(m.mk_app(rec, r)); conjs.push_back(m.mk_app(rec, r));
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d); ptr_vector<func_decl> const& acc = dt.get_constructor_accessors(d);
for (unsigned i = 0; i < acc.size(); ++i) { for (unsigned i = 0; i < acc.size(); ++i) {
conjs.push_back(m.mk_eq(c->get_arg(i), m.mk_app(acc[i], r))); conjs.push_back(m.mk_eq(c->get_arg(i), m.mk_app(acc[i], r)));
} }

12
src/smt/proto_model/datatype_factory.cpp
View file

@ -88,8 +88,8 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
// Traverse constructors, and try to invoke get_fresh_value of one of the arguments (if the argument is not a sibling datatype of s). // Traverse constructors, and try to invoke get_fresh_value of one of the arguments (if the argument is not a sibling datatype of s).
// If the argumet is a sibling datatype of s, then // If the argumet is a sibling datatype of s, then
// use get_last_fresh_value. // use get_last_fresh_value.
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = m_util.get_datatype_constructors(s);
for (func_decl * constructor : *constructors) { for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager); expr_ref_vector args(m_manager);
bool found_fresh_arg = false; bool found_fresh_arg = false;
bool recursive = false; bool recursive = false;
@ -151,8 +151,8 @@ expr * datatype_factory::get_fresh_value(sort * s) {
// Traverse constructors, and try to invoke get_fresh_value of one of the // Traverse constructors, and try to invoke get_fresh_value of one of the
// arguments (if the argument is not a sibling datatype of s). // arguments (if the argument is not a sibling datatype of s).
// Two datatypes are siblings if they were defined together in the same mutually recursive definition. // Two datatypes are siblings if they were defined together in the same mutually recursive definition.
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = m_util.get_datatype_constructors(s);
for (func_decl * constructor : *constructors) { for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager); expr_ref_vector args(m_manager);
bool found_fresh_arg = false; bool found_fresh_arg = false;
unsigned num = constructor->get_arity(); unsigned num = constructor->get_arity();
@ -189,8 +189,8 @@ expr * datatype_factory::get_fresh_value(sort * s) {
while(true) { while(true) {
++num_iterations; ++num_iterations;
TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = m_util.get_datatype_constructors(s);
for (func_decl * constructor : *constructors) { for (func_decl * constructor : constructors) {
expr_ref_vector args(m_manager); expr_ref_vector args(m_manager);
bool found_sibling = false; bool found_sibling = false;
unsigned num = constructor->get_arity(); unsigned num = constructor->get_arity();

2
src/smt/smt_value_sort.cpp
View file

@ -52,7 +52,7 @@ namespace smt {
// simple // simple
} }
else if (data.is_datatype(s)) { else if (data.is_datatype(s)) {
ptr_vector<func_decl> const& cs = *data.get_datatype_constructors(s); ptr_vector<func_decl> const& cs = data.get_datatype_constructors(s);
for (unsigned i = 0; i < cs.size(); ++i) { for (unsigned i = 0; i < cs.size(); ++i) {
func_decl* f = cs[i]; func_decl* f = cs[i];
for (unsigned j = 0; j < f->get_arity(); ++j) { for (unsigned j = 0; j < f->get_arity(); ++j) {

37
src/smt/theory_datatype.cpp
View file

@ -97,12 +97,9 @@ namespace smt {
SASSERT(m_util.is_datatype(get_manager().get_sort(n->get_owner()))); SASSERT(m_util.is_datatype(get_manager().get_sort(n->get_owner())));
ast_manager & m = get_manager(); ast_manager & m = get_manager();
ptr_vector<expr> args; ptr_vector<expr> args;
ptr_vector<func_decl> const * accessors = m_util.get_constructor_accessors(c); ptr_vector<func_decl> const & accessors = m_util.get_constructor_accessors(c);
SASSERT(c->get_arity() == accessors->size()); SASSERT(c->get_arity() == accessors.size());
ptr_vector<func_decl>::const_iterator it = accessors->begin(); for (func_decl * d : accessors) {
ptr_vector<func_decl>::const_iterator end = accessors->end();
for (; it != end; ++it) {
func_decl * d = *it;
SASSERT(d->get_arity() == 1); SASSERT(d->get_arity() == 1);
expr * acc = m.mk_app(d, n->get_owner()); expr * acc = m.mk_app(d, n->get_owner());
args.push_back(acc); args.push_back(acc);
@ -123,15 +120,14 @@ namespace smt {
SASSERT(is_constructor(n)); SASSERT(is_constructor(n));
ast_manager & m = get_manager(); ast_manager & m = get_manager();
func_decl * d = n->get_decl(); func_decl * d = n->get_decl();
ptr_vector<func_decl> const * accessors = m_util.get_constructor_accessors(d); ptr_vector<func_decl> const & accessors = m_util.get_constructor_accessors(d);
SASSERT(n->get_num_args() == accessors->size()); SASSERT(n->get_num_args() == accessors.size());
ptr_vector<func_decl>::const_iterator it = accessors->begin(); unsigned i = 0;
ptr_vector<func_decl>::const_iterator end = accessors->end(); for (func_decl * acc : accessors) {
for (unsigned i = 0; it != end; ++it, ++i) {
func_decl * acc = *it;
app * acc_app = m.mk_app(acc, n->get_owner()); app * acc_app = m.mk_app(acc, n->get_owner());
enode * arg = n->get_arg(i); enode * arg = n->get_arg(i);
assert_eq_axiom(arg, acc_app, null_literal); assert_eq_axiom(arg, acc_app, null_literal);
++i;
} }
} }
@ -172,15 +168,12 @@ namespace smt {
func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast()); func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast());
func_decl * con = m_util.get_accessor_constructor(acc); func_decl * con = m_util.get_accessor_constructor(acc);
func_decl * rec = m_util.get_constructor_recognizer(con); func_decl * rec = m_util.get_constructor_recognizer(con);
ptr_vector<func_decl> const * accessors = m_util.get_constructor_accessors(con); ptr_vector<func_decl> const & accessors = m_util.get_constructor_accessors(con);
ptr_vector<func_decl>::const_iterator it = accessors->begin();
ptr_vector<func_decl>::const_iterator end = accessors->end();
app_ref rec_app(m.mk_app(rec, arg1), m); app_ref rec_app(m.mk_app(rec, arg1), m);
ctx.internalize(rec_app, false); ctx.internalize(rec_app, false);
literal is_con(ctx.get_bool_var(rec_app)); literal is_con(ctx.get_bool_var(rec_app));
for (; it != end; ++it) { for (func_decl* acc1 : accessors) {
enode* arg; enode* arg;
func_decl * acc1 = *it;
if (acc1 == acc) { if (acc1 == acc) {
arg = n->get_arg(1); arg = n->get_arg(1);
} }
@ -215,7 +208,7 @@ namespace smt {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
sort * s = m.get_sort(n->get_owner()); sort * s = m.get_sort(n->get_owner());
if (m_util.get_datatype_num_constructors(s) == 1) { if (m_util.get_datatype_num_constructors(s) == 1) {
func_decl * c = m_util.get_datatype_constructors(s)->get(0); func_decl * c = m_util.get_datatype_constructors(s)[0];
assert_is_constructor_axiom(n, c, null_literal); assert_is_constructor_axiom(n, c, null_literal);
} }
else { else {
@ -716,8 +709,8 @@ namespace smt {
enode * r = d->m_recognizers[unassigned_idx]; enode * r = d->m_recognizers[unassigned_idx];
literal consequent; literal consequent;
if (!r) { if (!r) {
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(dt); ptr_vector<func_decl> const & constructors = m_util.get_datatype_constructors(dt);
func_decl * rec = m_util.get_constructor_recognizer(constructors->get(unassigned_idx)); func_decl * rec = m_util.get_constructor_recognizer(constructors[unassigned_idx]);
app * rec_app = get_manager().mk_app(rec, n->get_owner()); app * rec_app = get_manager().mk_app(rec, n->get_owner());
ctx.internalize(rec_app, false); ctx.internalize(rec_app, false);
consequent = literal(ctx.get_bool_var(rec_app)); consequent = literal(ctx.get_bool_var(rec_app));
@ -781,9 +774,9 @@ namespace smt {
for (unsigned idx = 0; it != end; ++it, ++idx) { for (unsigned idx = 0; it != end; ++it, ++idx) {
enode * curr = *it; enode * curr = *it;
if (curr == 0) { if (curr == 0) {
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = m_util.get_datatype_constructors(s);
// found empty slot... // found empty slot...
r = m_util.get_constructor_recognizer(constructors->get(idx)); r = m_util.get_constructor_recognizer(constructors[idx]);
break; break;
} }
else if (!ctx.is_relevant(curr)) { else if (!ctx.is_relevant(curr)) {

17
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -174,11 +174,8 @@ class elim_uncnstr_tactic : public tactic {
if (fid == m_dt_util.get_family_id()) { if (fid == m_dt_util.get_family_id()) {
// In the current implementation, I only handle the case where // In the current implementation, I only handle the case where
// the datatype has a recursive constructor. // the datatype has a recursive constructor.
ptr_vector<func_decl> const * constructors = m_dt_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = m_dt_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin(); for (func_decl * constructor : constructors) {
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
unsigned num = constructor->get_arity(); unsigned num = constructor->get_arity();
unsigned target = UINT_MAX; unsigned target = UINT_MAX;
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
@ -707,10 +704,10 @@ class elim_uncnstr_tactic : public tactic {
app * u; app * u;
if (!mk_fresh_uncnstr_var_for(f, num, args, u)) if (!mk_fresh_uncnstr_var_for(f, num, args, u))
return u; return u;
ptr_vector<func_decl> const * accs = m_dt_util.get_constructor_accessors(c); ptr_vector<func_decl> const & accs = m_dt_util.get_constructor_accessors(c);
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
for (unsigned i = 0; i < accs->size(); i++) { for (unsigned i = 0; i < accs.size(); i++) {
if (accs->get(i) == f) if (accs[i] == f)
new_args.push_back(u); new_args.push_back(u);
else else
new_args.push_back(m().get_some_value(c->get_domain(i))); new_args.push_back(m().get_some_value(c->get_domain(i)));
@ -726,9 +723,9 @@ class elim_uncnstr_tactic : public tactic {
return u; return u;
if (!m_mc) if (!m_mc)
return u; return u;
ptr_vector<func_decl> const * accs = m_dt_util.get_constructor_accessors(f); ptr_vector<func_decl> const & accs = m_dt_util.get_constructor_accessors(f);
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
add_def(args[i], m().mk_app(accs->get(i), u)); add_def(args[i], m().mk_app(accs[i], u));
} }
return u; return u;
} }

2
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -136,7 +136,7 @@ public:
if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
SASSERT(num.is_unsigned()); SASSERT(num.is_unsigned());
expr_ref head(m); expr_ref head(m);
ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range()); ptr_vector<func_decl> const& enums = dt.get_datatype_constructors(f->get_range());
if (enums.size() > num.get_unsigned()) { if (enums.size() > num.get_unsigned()) {
head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
consequences[i] = m.mk_implies(a, head); consequences[i] = m.mk_implies(a, head);

2
src/test/get_consequences.cpp
View file

@ -71,7 +71,7 @@ void test2() {
sort* rgb = new_sorts[0].get(); sort* rgb = new_sorts[0].get();
expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb); expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb);
ptr_vector<func_decl> const& enums = *dtutil.get_datatype_constructors(rgb); ptr_vector<func_decl> const& enums = dtutil.get_datatype_constructors(rgb);
expr_ref r = expr_ref(m.mk_const(enums[0]), m); expr_ref r = expr_ref(m.mk_const(enums[0]), m);
expr_ref g = expr_ref(m.mk_const(enums[1]), m); expr_ref g = expr_ref(m.mk_const(enums[1]), m);
expr_ref b = expr_ref(m.mk_const(enums[2]), m); expr_ref b = expr_ref(m.mk_const(enums[2]), m);