mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
support for smtlib2.6 datatype parsing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
5492d0e135
commit
5d17e28667
29 changed files with 374 additions and 206 deletions
|
|
@ -1287,10 +1287,8 @@ decl_kind user_sort_plugin::register_name(symbol s) {
|
|||
|
||||
decl_plugin * user_sort_plugin::mk_fresh() {
|
||||
user_sort_plugin * p = alloc(user_sort_plugin);
|
||||
svector<symbol>::iterator it = m_sort_names.begin();
|
||||
svector<symbol>::iterator end = m_sort_names.end();
|
||||
for (; it != end; ++it)
|
||||
p->register_name(*it);
|
||||
for (symbol const& s : m_sort_names)
|
||||
p->register_name(s);
|
||||
return p;
|
||||
}
|
||||
|
||||
|
|
@ -1410,26 +1408,20 @@ ast_manager::~ast_manager() {
|
|||
dec_ref(m_true);
|
||||
dec_ref(m_false);
|
||||
dec_ref(m_undef_proof);
|
||||
ptr_vector<decl_plugin>::iterator it = m_plugins.begin();
|
||||
ptr_vector<decl_plugin>::iterator end = m_plugins.end();
|
||||
for (; it != end; ++it) {
|
||||
if (*it)
|
||||
(*it)->finalize();
|
||||
for (decl_plugin* p : m_plugins) {
|
||||
if (p)
|
||||
p->finalize();
|
||||
}
|
||||
it = m_plugins.begin();
|
||||
for (; it != end; ++it) {
|
||||
if (*it)
|
||||
dealloc(*it);
|
||||
for (decl_plugin* p : m_plugins) {
|
||||
if (p)
|
||||
dealloc(p);
|
||||
}
|
||||
m_plugins.reset();
|
||||
while (!m_ast_table.empty()) {
|
||||
DEBUG_CODE(std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl;);
|
||||
ptr_vector<ast> roots;
|
||||
ast_mark mark;
|
||||
ast_table::iterator it_a = m_ast_table.begin();
|
||||
ast_table::iterator end_a = m_ast_table.end();
|
||||
for (; it_a != end_a; ++it_a) {
|
||||
ast* n = (*it_a);
|
||||
for (ast * n : m_ast_table) {
|
||||
switch (n->get_kind()) {
|
||||
case AST_SORT: {
|
||||
sort_info* info = to_sort(n)->get_info();
|
||||
|
|
@ -1462,9 +1454,7 @@ ast_manager::~ast_manager() {
|
|||
break;
|
||||
}
|
||||
}
|
||||
it_a = m_ast_table.begin();
|
||||
for (; it_a != end_a; ++it_a) {
|
||||
ast* n = *it_a;
|
||||
for (ast * n : m_ast_table) {
|
||||
if (!mark.is_marked(n)) {
|
||||
roots.push_back(n);
|
||||
}
|
||||
|
|
@ -1659,11 +1649,8 @@ bool ast_manager::is_bool(expr const * n) const {
|
|||
|
||||
#ifdef Z3DEBUG
|
||||
bool ast_manager::slow_not_contains(ast const * n) {
|
||||
ast_table::iterator it = m_ast_table.begin();
|
||||
ast_table::iterator end = m_ast_table.end();
|
||||
unsigned num = 0;
|
||||
for (; it != end; ++it) {
|
||||
ast * curr = *it;
|
||||
for (ast * curr : m_ast_table) {
|
||||
if (compare_nodes(curr, n)) {
|
||||
TRACE("nondet_bug",
|
||||
tout << "id1: " << curr->get_id() << ", id2: " << n->get_id() << "\n";
|
||||
|
|
|
|||
|
|
@ -284,7 +284,7 @@ public:
|
|||
}
|
||||
unsigned num_args = to_app(n)->get_num_args();
|
||||
if (num_args > 0)
|
||||
m_out << "(";
|
||||
m_out << "(_ ";
|
||||
display_name(to_app(n)->get_decl());
|
||||
display_params(to_app(n)->get_decl());
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
|
|
|
|||
|
|
@ -431,7 +431,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
|
|||
fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
|
||||
return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx");
|
||||
}
|
||||
#if 0
|
||||
#ifdef DATATYPE_V2
|
||||
if (get_dtutil().is_datatype(s)) {
|
||||
ptr_buffer<format> fs;
|
||||
unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
|
||||
|
|
|
|||
|
|
@ -21,17 +21,17 @@ Revision History:
|
|||
|
||||
#include<sstream>
|
||||
#include<iostream>
|
||||
#include "util/vector.h"
|
||||
#include "util/smt2_util.h"
|
||||
#include "ast/ast_smt_pp.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/datatype_decl_plugin.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/fpa_decl_plugin.h"
|
||||
#include "util/vector.h"
|
||||
#include "ast/for_each_ast.h"
|
||||
#include "ast/decl_collector.h"
|
||||
#include "util/smt2_util.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
|
||||
// ---------------------------------------
|
||||
// smt_renaming
|
||||
|
|
@ -210,7 +210,19 @@ class smt_printer {
|
|||
void pp_decl(func_decl* d) {
|
||||
symbol sym = m_renaming.get_symbol(d->get_name());
|
||||
if (d->get_family_id() == m_dt_fid) {
|
||||
#ifdef DATATYPE_V2
|
||||
std::cout << "printing " << sym << "\n";
|
||||
datatype_util util(m_manager);
|
||||
if (util.is_recognizer(d)) {
|
||||
std::cout << d->get_num_parameters() << "\n";
|
||||
visit_params(false, sym, d->get_num_parameters(), d->get_parameters());
|
||||
}
|
||||
else {
|
||||
m_out << sym;
|
||||
}
|
||||
#else
|
||||
m_out << sym;
|
||||
#endif
|
||||
}
|
||||
else if (m_manager.is_ite(d)) {
|
||||
if (!m_is_smt2 && is_bool(d->get_range())) {
|
||||
|
|
@ -366,14 +378,15 @@ class smt_printer {
|
|||
return;
|
||||
}
|
||||
else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
|
||||
#ifndef DATATYPE_V2
|
||||
m_out << m_renaming.get_symbol(s->get_name());
|
||||
#if 0
|
||||
#else
|
||||
datatype_util util(m_manager);
|
||||
unsigned num_sorts = util.get_datatype_num_parameter_sorts(s);
|
||||
if (num_sorts > 0) {
|
||||
m_out << "(";
|
||||
}
|
||||
|
||||
m_out << m_renaming.get_symbol(s->get_name());
|
||||
if (num_sorts > 0) {
|
||||
for (unsigned i = 0; i < num_sorts; ++i) {
|
||||
m_out << " ";
|
||||
|
|
@ -533,7 +546,8 @@ class smt_printer {
|
|||
pp_arg(curr, n);
|
||||
m_out << ")";
|
||||
|
||||
} else if (m_manager.is_distinct(decl)) {
|
||||
}
|
||||
else if (m_manager.is_distinct(decl)) {
|
||||
ptr_vector<expr> args(num_args, n->get_args());
|
||||
unsigned idx = 0;
|
||||
m_out << "(and";
|
||||
|
|
@ -915,7 +929,7 @@ public:
|
|||
// collect siblings and sorts that have not already been printed.
|
||||
for (unsigned h = 0; h < rec_sorts.size(); ++h) {
|
||||
s = rec_sorts[h];
|
||||
ptr_vector<func_decl> const& 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) {
|
||||
func_decl* f = decls[i];
|
||||
|
|
@ -954,11 +968,11 @@ public:
|
|||
m_out << "(";
|
||||
m_out << m_renaming.get_symbol(s->get_name());
|
||||
m_out << " ";
|
||||
ptr_vector<func_decl> const& 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) {
|
||||
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) {
|
||||
m_out << "(";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ public:
|
|||
type_ref const & get_type() const { return m_type; }
|
||||
};
|
||||
|
||||
accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) {
|
||||
accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) {
|
||||
return alloc(accessor_decl, n, t);
|
||||
}
|
||||
|
||||
|
|
@ -95,7 +95,7 @@ public:
|
|||
ptr_vector<constructor_decl> const & get_constructors() const { return m_constructors; }
|
||||
};
|
||||
|
||||
datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
|
||||
datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_params, sort * const* params, unsigned num_constructors, constructor_decl * const * cs) {
|
||||
return alloc(datatype_decl, n, num_constructors, cs);
|
||||
}
|
||||
|
||||
|
|
@ -803,11 +803,11 @@ func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id) {
|
|||
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));
|
||||
ptr_vector<func_decl> * r = 0;
|
||||
if (m_datatype2constructors.find(ty, r))
|
||||
return *r;
|
||||
return r;
|
||||
r = alloc(ptr_vector<func_decl>);
|
||||
m_asts.push_back(ty);
|
||||
m_vectors.push_back(r);
|
||||
|
|
@ -820,7 +820,7 @@ ptr_vector<func_decl> const & datatype_util::get_datatype_constructors(sort * ty
|
|||
m_asts.push_back(c);
|
||||
r->push_back(c);
|
||||
}
|
||||
return *r;
|
||||
return r;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -855,7 +855,7 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
|
|||
// 1) T_i's are not recursive
|
||||
// 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
|
||||
ptr_vector<func_decl> const & constructors = get_datatype_constructors(ty);
|
||||
ptr_vector<func_decl> const & constructors = *get_datatype_constructors(ty);
|
||||
// step 1)
|
||||
unsigned sz = constructors.size();
|
||||
++m_start;
|
||||
|
|
@ -916,11 +916,11 @@ func_decl * datatype_util::get_constructor_recognizer(func_decl * constructor) {
|
|||
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));
|
||||
ptr_vector<func_decl> * res = 0;
|
||||
if (m_constructor2accessors.find(constructor, res))
|
||||
return *res;
|
||||
return res;
|
||||
res = alloc(ptr_vector<func_decl>);
|
||||
m_asts.push_back(constructor);
|
||||
m_vectors.push_back(res);
|
||||
|
|
@ -939,7 +939,7 @@ ptr_vector<func_decl> const & datatype_util::get_constructor_accessors(func_decl
|
|||
m_asts.push_back(d);
|
||||
res->push_back(d);
|
||||
}
|
||||
return *res;
|
||||
return res;
|
||||
}
|
||||
|
||||
func_decl * datatype_util::get_accessor_constructor(func_decl * accessor) {
|
||||
|
|
@ -989,7 +989,7 @@ bool datatype_util::is_enum_sort(sort* s) {
|
|||
bool r = false;
|
||||
if (m_is_enum.find(s, 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;
|
||||
for (unsigned i = 0; r && i < cnstrs.size(); ++i) {
|
||||
r = cnstrs[i]->get_arity() == 0;
|
||||
|
|
@ -1049,12 +1049,12 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) {
|
|||
todo.pop_back();
|
||||
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) {
|
||||
func_decl* cns = cnstrs[i];
|
||||
func_decl* rec = get_constructor_recognizer(cns);
|
||||
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) {
|
||||
func_decl* acc = accs[j];
|
||||
sort* s1 = acc->get_range();
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
//define DATATYPE_V2
|
||||
// define DATATYPE_V2
|
||||
#ifdef DATATYPE_V2
|
||||
#include "ast/datatype_decl_plugin2.h"
|
||||
#else
|
||||
|
|
@ -78,15 +78,11 @@ class constructor_decl;
|
|||
class datatype_decl;
|
||||
class datatype_util;
|
||||
|
||||
accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t);
|
||||
//void del_accessor_decl(accessor_decl * d);
|
||||
//void del_accessor_decls(unsigned num, accessor_decl * const * as);
|
||||
accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t);
|
||||
// Remark: the constructor becomes the owner of the accessor_decls
|
||||
constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * const * acs);
|
||||
//void del_constructor_decl(constructor_decl * d);
|
||||
//void del_constructor_decls(unsigned num, constructor_decl * const * cs);
|
||||
// Remark: the datatype becomes the owner of the constructor_decls
|
||||
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
|
||||
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort * const* params, unsigned num_constructors, constructor_decl * const * cs);
|
||||
void del_datatype_decl(datatype_decl * d);
|
||||
void del_datatype_decls(unsigned num, datatype_decl * const * ds);
|
||||
|
||||
|
|
@ -216,7 +212,7 @@ public:
|
|||
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_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) {
|
||||
SASSERT(is_datatype(ty));
|
||||
unsigned tid = ty->get_parameter(1).get_int();
|
||||
|
|
@ -236,7 +232,7 @@ public:
|
|||
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_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_recognizer_constructor(func_decl * recognizer);
|
||||
family_id get_family_id() const { return m_family_id; }
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ namespace datatype {
|
|||
func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const {
|
||||
ast_manager& m = ps.get_manager();
|
||||
unsigned n = ps.size();
|
||||
SASSERT(m_range);
|
||||
SASSERT(n == get_def().params().size());
|
||||
sort_ref range(m.substitute(m_range, n, get_def().params().c_ptr(), ps.c_ptr()), m);
|
||||
sort_ref src(get_def().instantiate(ps));
|
||||
|
|
@ -79,13 +80,14 @@ namespace datatype {
|
|||
sort_ref s(m);
|
||||
if (!m_sort) {
|
||||
vector<parameter> ps;
|
||||
ps.push_back(parameter(m_name));
|
||||
for (sort * s : m_params) ps.push_back(parameter(s));
|
||||
m_sort = m.mk_sort(u().get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr());
|
||||
}
|
||||
if (sorts.empty()) {
|
||||
return m_sort;
|
||||
}
|
||||
return sort_ref(m.substitute(m_sort, sorts.size(), sorts.c_ptr(), m_params.c_ptr()), m);
|
||||
return sort_ref(m.substitute(m_sort, sorts.size(), m_params.c_ptr(), sorts.c_ptr()), m);
|
||||
}
|
||||
|
||||
enum status {
|
||||
|
|
@ -135,6 +137,7 @@ namespace datatype {
|
|||
|
||||
util & plugin::u() const {
|
||||
SASSERT(m_manager);
|
||||
SASSERT(m_family_id != null_family_id);
|
||||
if (m_util.get() == 0) {
|
||||
m_util = alloc(util, *m_manager);
|
||||
}
|
||||
|
|
@ -146,9 +149,11 @@ namespace datatype {
|
|||
sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
|
||||
try {
|
||||
if (k != DATATYPE_SORT) {
|
||||
TRACE("datatype", tout << "invalid kind parameter to datatype\n";);
|
||||
throw invalid_datatype();
|
||||
}
|
||||
if (num_parameters < 1) {
|
||||
TRACE("datatype", tout << "at least one parameter expected to datatype declaration\n";);
|
||||
throw invalid_datatype();
|
||||
}
|
||||
parameter const & name = parameters[0];
|
||||
|
|
@ -169,13 +174,17 @@ namespace datatype {
|
|||
def* d = 0;
|
||||
if (m_defs.find(s->get_name(), d) && d->sort_size()) {
|
||||
obj_map<sort, sort_size> S;
|
||||
for (unsigned i = 1; i < num_parameters; ++i) {
|
||||
sort* r = to_sort(parameters[i].get_ast());
|
||||
for (unsigned i = 0; i + 1 < num_parameters; ++i) {
|
||||
sort* r = to_sort(parameters[i + 1].get_ast());
|
||||
S.insert(d->params()[i], r->get_num_elements());
|
||||
}
|
||||
sort_size ts = d->sort_size()->eval(S);
|
||||
TRACE("datatype", tout << name << " has size " << ts << "\n";);
|
||||
s->set_num_elements(ts);
|
||||
}
|
||||
else {
|
||||
TRACE("datatype", tout << "not setting size for " << name << "\n";);
|
||||
}
|
||||
return s;
|
||||
}
|
||||
catch (invalid_datatype) {
|
||||
|
|
@ -227,14 +236,12 @@ namespace datatype {
|
|||
return m.mk_func_decl(symbol("update-field"), arity, domain, range, info);
|
||||
}
|
||||
|
||||
#define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function");
|
||||
|
||||
func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range) {
|
||||
ast_manager& m = *m_manager;
|
||||
SASSERT(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range));
|
||||
if (num_parameters != 1 || !parameters[0].is_symbol() || !range || !u().is_datatype(range)) {
|
||||
m_manager->raise_exception("invalid parameters for datatype constructor");
|
||||
}
|
||||
VALIDATE_PARAM(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range));
|
||||
// we blindly trust other conditions are met, including domain types.
|
||||
symbol name = parameters[0].get_symbol();
|
||||
func_decl_info info(m_family_id, OP_DT_CONSTRUCTOR, num_parameters, parameters);
|
||||
|
|
@ -245,27 +252,27 @@ namespace datatype {
|
|||
func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort *) {
|
||||
ast_manager& m = *m_manager;
|
||||
SASSERT(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast()));
|
||||
SASSERT(u().is_datatype(domain[0]));
|
||||
VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast()));
|
||||
VALIDATE_PARAM(u().is_datatype(domain[0]));
|
||||
// blindly trust that parameter is a constructor
|
||||
sort* range = m_manager->mk_bool_sort();
|
||||
func_decl* f = to_func_decl(parameters[0].get_ast());
|
||||
func_decl_info info(m_family_id, OP_DT_RECOGNISER, num_parameters, parameters);
|
||||
info.m_private_parameters = true;
|
||||
symbol name = to_func_decl(parameters[0].get_ast())->get_name();
|
||||
return m.mk_func_decl(name, arity, domain, range);
|
||||
return m.mk_func_decl(symbol("is"), arity, domain, range, info);
|
||||
}
|
||||
|
||||
func_decl * decl::plugin::mk_accessor(unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range)
|
||||
{
|
||||
ast_manager& m = *m_manager;
|
||||
SASSERT(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[0].is_symbol());
|
||||
SASSERT(u().is_datatype(domain[0]));
|
||||
VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[1].is_symbol());
|
||||
VALIDATE_PARAM(u().is_datatype(domain[0]));
|
||||
SASSERT(range);
|
||||
func_decl_info info(m_family_id, OP_DT_ACCESSOR, num_parameters, parameters);
|
||||
info.m_private_parameters = true;
|
||||
symbol name = parameters[0].get_symbol();
|
||||
return m.mk_func_decl(name, arity, domain, range);
|
||||
return m.mk_func_decl(name, arity, domain, range, info);
|
||||
}
|
||||
|
||||
func_decl * decl::plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
|
|
@ -290,15 +297,20 @@ namespace datatype {
|
|||
return alloc(def, m, u(), name, m_class_id, n, params);
|
||||
}
|
||||
|
||||
#if 0
|
||||
def& plugin::add(symbol const& name, unsigned n, sort * const * params) {
|
||||
ast_manager& m = *m_manager;
|
||||
def* d = 0;
|
||||
if (m_defs.find(name, d)) dealloc(d);
|
||||
if (m_defs.find(name, d)) {
|
||||
TRACE("datatype", tout << "delete previous version for " << name << "\n";);
|
||||
dealloc(d);
|
||||
}
|
||||
d = alloc(def, m, u(), name, m_class_id, n, params);
|
||||
m_defs.insert(name, d);
|
||||
m_def_block.push_back(name);
|
||||
return *d;
|
||||
}
|
||||
#endif
|
||||
|
||||
void plugin::end_def_block() {
|
||||
ast_manager& m = *m_manager;
|
||||
|
|
@ -325,7 +337,11 @@ namespace datatype {
|
|||
bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) {
|
||||
begin_def_block();
|
||||
for (unsigned i = 0; i < num_datatypes; ++i) {
|
||||
if (m_defs.find(datatypes[i]->name(), d)) dealloc(d);
|
||||
def* d = 0;
|
||||
if (m_defs.find(datatypes[i]->name(), d)) {
|
||||
TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";);
|
||||
dealloc(d);
|
||||
}
|
||||
m_defs.insert(datatypes[i]->name(), datatypes[i]);
|
||||
m_def_block.push_back(datatypes[i]->name());
|
||||
}
|
||||
|
|
@ -391,6 +407,7 @@ namespace datatype {
|
|||
}
|
||||
|
||||
void plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
|
||||
op_names.push_back(builtin_name("is", OP_DT_RECOGNISER));
|
||||
if (logic == symbol::null) {
|
||||
op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD));
|
||||
}
|
||||
|
|
@ -548,6 +565,10 @@ namespace datatype {
|
|||
}
|
||||
return param_size::size::mk_offset(s->get_num_elements());
|
||||
}
|
||||
|
||||
bool util::is_declared(sort* s) const {
|
||||
return m_plugin->is_declared(s);
|
||||
}
|
||||
|
||||
void util::compute_datatype_size_functions(svector<symbol> const& names) {
|
||||
map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
|
||||
|
|
@ -668,17 +689,18 @@ namespace datatype {
|
|||
m_asts(m),
|
||||
m_start(0) {
|
||||
m_plugin = dynamic_cast<decl::plugin*>(m.get_plugin(m_family_id));
|
||||
SASSERT(m_plugin);
|
||||
}
|
||||
|
||||
util::~util() {
|
||||
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> const & util::get_datatype_constructors(sort * ty) {
|
||||
ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
|
||||
SASSERT(is_datatype(ty));
|
||||
ptr_vector<func_decl> * r = 0;
|
||||
if (m_datatype2constructors.find(ty, r))
|
||||
return *r;
|
||||
return r;
|
||||
r = alloc(ptr_vector<func_decl>);
|
||||
m_asts.push_back(ty);
|
||||
m_vectors.push_back(r);
|
||||
|
|
@ -689,14 +711,15 @@ namespace datatype {
|
|||
m_asts.push_back(f);
|
||||
r->push_back(f);
|
||||
}
|
||||
return *r;
|
||||
return r;
|
||||
}
|
||||
|
||||
ptr_vector<func_decl> const & util::get_constructor_accessors(func_decl * con) {
|
||||
ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) {
|
||||
SASSERT(is_constructor(con));
|
||||
ptr_vector<func_decl> * res = 0;
|
||||
if (m_constructor2accessors.find(con, res))
|
||||
return *res;
|
||||
if (m_constructor2accessors.find(con, res)) {
|
||||
return res;
|
||||
}
|
||||
res = alloc(ptr_vector<func_decl>);
|
||||
m_asts.push_back(con);
|
||||
m_vectors.push_back(res);
|
||||
|
|
@ -706,12 +729,14 @@ namespace datatype {
|
|||
for (constructor const* c : d) {
|
||||
if (c->name() == con->get_name()) {
|
||||
for (accessor const* a : *c) {
|
||||
res->push_back(a->instantiate(datatype));
|
||||
func_decl_ref fn = a->instantiate(datatype);
|
||||
res->push_back(fn);
|
||||
m_asts.push_back(fn);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
return *res;
|
||||
return res;
|
||||
}
|
||||
|
||||
func_decl * util::get_constructor_recognizer(func_decl * constructor) {
|
||||
|
|
@ -752,7 +777,7 @@ namespace datatype {
|
|||
bool r = false;
|
||||
if (m_is_enum.find(s, 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;
|
||||
for (unsigned i = 0; r && i < cnstrs.size(); ++i) {
|
||||
r = cnstrs[i]->get_arity() == 0;
|
||||
|
|
@ -833,7 +858,7 @@ namespace datatype {
|
|||
// 1) T_i's are not recursive
|
||||
// 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
|
||||
ptr_vector<func_decl> const& constructors = get_datatype_constructors(ty);
|
||||
ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
|
||||
// step 1)
|
||||
unsigned sz = constructors.size();
|
||||
++m_start;
|
||||
|
|
@ -928,12 +953,12 @@ namespace datatype {
|
|||
todo.pop_back();
|
||||
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) {
|
||||
func_decl* cns = cnstrs[i];
|
||||
func_decl* rec = get_constructor_recognizer(cns);
|
||||
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) {
|
||||
func_decl* acc = accs[j];
|
||||
sort* s1 = acc->get_range();
|
||||
|
|
@ -949,9 +974,9 @@ namespace datatype {
|
|||
}
|
||||
}
|
||||
|
||||
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
|
||||
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) {
|
||||
datatype::decl::plugin* p = u.get_plugin();
|
||||
datatype::def( d = p->mk(n, 0, 0);
|
||||
datatype::def* d = p->mk(n, num_params, params);
|
||||
for (unsigned i = 0; i < num_constructors; ++i) {
|
||||
d->add(cs[i]);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -50,19 +50,19 @@ namespace datatype {
|
|||
|
||||
|
||||
class accessor {
|
||||
symbol m_name;
|
||||
sort* m_range;
|
||||
symbol m_name;
|
||||
sort_ref m_range;
|
||||
unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed.
|
||||
constructor* m_constructor;
|
||||
public:
|
||||
accessor(symbol const& n, sort* range):
|
||||
accessor(ast_manager& m, symbol const& n, sort* range):
|
||||
m_name(n),
|
||||
m_range(range),
|
||||
m_range(range, m),
|
||||
m_index(UINT_MAX)
|
||||
{}
|
||||
accessor(symbol const& n, unsigned index):
|
||||
accessor(ast_manager& m, symbol const& n, unsigned index):
|
||||
m_name(n),
|
||||
m_range(0),
|
||||
m_range(m),
|
||||
m_index(index)
|
||||
{}
|
||||
sort* range() const { return m_range; }
|
||||
|
|
@ -262,8 +262,6 @@ namespace datatype {
|
|||
|
||||
void end_def_block();
|
||||
|
||||
def& add(symbol const& name, unsigned n, sort * const * params);
|
||||
|
||||
def* mk(symbol const& name, unsigned n, sort * const * params);
|
||||
|
||||
void del(symbol const& d);
|
||||
|
|
@ -272,7 +270,7 @@ namespace datatype {
|
|||
|
||||
def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
|
||||
def& get_def(symbol const& s) { return *(m_defs[s]); }
|
||||
|
||||
bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); }
|
||||
private:
|
||||
bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
|
||||
|
||||
|
|
@ -337,6 +335,7 @@ namespace datatype {
|
|||
util(ast_manager & m);
|
||||
~util();
|
||||
ast_manager & get_manager() const { return m; }
|
||||
// sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params);
|
||||
bool is_datatype(sort const* s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); }
|
||||
bool is_enum_sort(sort* s);
|
||||
bool is_recursive(sort * ty);
|
||||
|
|
@ -348,13 +347,13 @@ namespace datatype {
|
|||
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_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_parameter_sorts(sort * ty);
|
||||
sort* get_datatype_parameter_sort(sort * ty, unsigned idx);
|
||||
func_decl * get_non_rec_constructor(sort * ty);
|
||||
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_recognizer_constructor(func_decl * recognizer) const;
|
||||
family_id get_family_id() const { return m_family_id; }
|
||||
|
|
@ -362,11 +361,13 @@ namespace datatype {
|
|||
bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);
|
||||
bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f);
|
||||
void reset();
|
||||
bool is_declared(sort* s) const;
|
||||
void display_datatype(sort *s, std::ostream& strm);
|
||||
bool is_fully_interp(sort * s) const;
|
||||
sort_ref_vector datatype_params(sort * s) const;
|
||||
unsigned get_constructor_idx(func_decl * f) const;
|
||||
unsigned get_recognizer_constructor_idx(func_decl * f) const;
|
||||
decl::plugin* get_plugin() { return m_plugin; }
|
||||
};
|
||||
|
||||
};
|
||||
|
|
@ -390,12 +391,12 @@ public:
|
|||
int get_idx() const { return UNBOXINT(m_data); }
|
||||
};
|
||||
|
||||
inline accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) {
|
||||
inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) {
|
||||
if (t.is_idx()) {
|
||||
return alloc(accessor_decl, n, t.get_idx());
|
||||
return alloc(accessor_decl, m, n, t.get_idx());
|
||||
}
|
||||
else {
|
||||
return alloc(accessor_decl, n, t.get_sort());
|
||||
return alloc(accessor_decl, m, n, t.get_sort());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -410,7 +411,7 @@ inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r
|
|||
|
||||
|
||||
// Remark: the datatype becomes the owner of the constructor_decls
|
||||
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
|
||||
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs);
|
||||
inline void del_datatype_decl(datatype_decl * d) {}
|
||||
inline void del_datatype_decls(unsigned num, datatype_decl * const * ds) {}
|
||||
|
||||
|
|
|
|||
|
|
@ -28,9 +28,9 @@ void decl_collector::visit_sort(sort * n) {
|
|||
|
||||
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
|
||||
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);
|
||||
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();
|
||||
for (unsigned j = 0; j < num_cas; j++) {
|
||||
func_decl * accsr = cnstr_acc.get(j);
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
|
|||
func_decl * c_decl = a->get_decl();
|
||||
if (c_decl != m_util.get_accessor_constructor(f))
|
||||
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.size() == a->get_num_args());
|
||||
unsigned num = acc.size();
|
||||
for (unsigned i = 0; i < num; ++i) {
|
||||
|
|
@ -70,7 +70,7 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
|
|||
result = a;
|
||||
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.size() == a->get_num_args());
|
||||
unsigned num = acc.size();
|
||||
ptr_buffer<expr> new_args;
|
||||
|
|
|
|||
|
|
@ -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)));
|
||||
}
|
||||
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]);
|
||||
for (unsigned i = nc - 1; i > 0; ) {
|
||||
--i;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue