From a0a8bc2a628274965d995c3fb8db6dba6ff7ee02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Jul 2017 09:12:43 -0700 Subject: [PATCH] fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 10 +- src/ast/ast_smt2_pp.cpp | 8 + src/ast/ast_smt2_pp.h | 6 +- src/ast/ast_smt_pp.cpp | 15 +- src/ast/datatype_decl_plugin.cpp | 85 ++++++-- src/ast/datatype_decl_plugin.h | 33 +++- src/cmd_context/cmd_context.cpp | 32 ++- src/cmd_context/cmd_context.h | 6 +- src/cmd_context/pdecl.cpp | 54 ++++- src/cmd_context/pdecl.h | 24 ++- src/muz/bmc/dl_bmc_engine.cpp | 4 +- src/parsers/smt2/smt2parser.cpp | 329 +++++++++++++++++++++---------- src/test/get_consequences.cpp | 2 +- 13 files changed, 452 insertions(+), 156 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 5096c8e80..647cdc581 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -52,7 +52,7 @@ extern "C" { { datatype_decl * dt = mk_datatype_decl(to_symbol(name), 1, constrs); - bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, tuples); + bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, tuples); del_datatype_decl(dt); if (!is_ok) { @@ -119,7 +119,7 @@ extern "C" { { datatype_decl * dt = mk_datatype_decl(to_symbol(name), n, constrs.c_ptr()); - bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, sorts); + bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, sorts); del_datatype_decl(dt); if (!is_ok) { @@ -180,7 +180,7 @@ extern "C" { sort_ref_vector sorts(m); { datatype_decl * decl = mk_datatype_decl(to_symbol(name), 2, constrs); - bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, sorts); + bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, 0, sorts); del_datatype_decl(decl); if (!is_ok) { @@ -357,7 +357,7 @@ extern "C" { sort_ref_vector sorts(m); { datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors); - bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, sorts); + bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, 0, sorts); del_datatype_decl(data); if (!is_ok) { @@ -420,7 +420,7 @@ extern "C" { datas.push_back(mk_datatype_decl(c,sort_names[i], cl->size(), reinterpret_cast(cl->c_ptr()))); } sort_ref_vector _sorts(m); - bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), _sorts); + bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.c_ptr(), 0, 0, _sorts); del_datatype_decls(datas.size(), datas.c_ptr()); if (!ok) { diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index d5e46548a..8b5f941c8 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -431,6 +431,14 @@ 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":"Re"); } + if (get_dtutil().is_datatype(s)) { + ptr_buffer fs; + unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s); + for (unsigned i = 0; i < sz; i++) { + fs.push_back(pp_sort(get_dtutil().get_datatype_parameter_sort(s, i))); + } + return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str()); + } return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); } diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index f2d177041..c3e72f7bc 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -30,6 +30,7 @@ Revision History: #include"fpa_decl_plugin.h" #include"dl_decl_plugin.h" #include"seq_decl_plugin.h" +#include"datatype_decl_plugin.h" #include"smt2_util.h" class smt2_pp_environment { @@ -50,6 +51,7 @@ public: virtual fpa_util & get_futil() = 0; virtual seq_util & get_sutil() = 0; virtual datalog::dl_decl_util& get_dlutil() = 0; + virtual datatype_util& get_dtutil() = 0; virtual bool uses(symbol const & s) const = 0; virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len); virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg); @@ -74,9 +76,10 @@ class smt2_pp_environment_dbg : public smt2_pp_environment { array_util m_arutil; fpa_util m_futil; seq_util m_sutil; + datatype_util m_dtutil; datalog::dl_decl_util m_dlutil; public: - smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dlutil(m) {} + smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dtutil(m), m_dlutil(m) {} virtual ast_manager & get_manager() const { return m_manager; } virtual arith_util & get_autil() { return m_autil; } virtual bv_util & get_bvutil() { return m_bvutil; } @@ -84,6 +87,7 @@ public: virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } + virtual datatype_util& get_dtutil() { return m_dtutil; } virtual bool uses(symbol const & s) const { return false; } }; diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 706f65ac4..8cf3965cf 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -366,7 +366,20 @@ class smt_printer { return; } else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) { - m_out << m_renaming.get_symbol(s->get_name()); + 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 << " "; + visit_sort(util.get_datatype_parameter_sort(s, i)); + } + m_out << ")"; + } return; } else { diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 4d531d2db..34b092ee9 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -20,6 +20,7 @@ Revision History: #include"warning.h" #include"ast_smt2_pp.h" + /** \brief Auxiliary class used to declare inductive datatypes. */ @@ -124,6 +125,7 @@ static parameter const & read(unsigned num_parameters, parameter const * paramet static int read_int(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { const parameter & r = read(num_parameters, parameters, idx, read_pos); if (!r.is_int()) { + TRACE("datatype", tout << "expected integer parameter at position " << idx << " got: " << r << "\n";); throw invalid_datatype(); } return r.get_int(); @@ -132,11 +134,25 @@ static int read_int(unsigned num_parameters, parameter const * parameters, unsig static symbol read_symbol(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { parameter const & r = read(num_parameters, parameters, idx, read_pos); if (!r.is_symbol()) { + TRACE("datatype", tout << "expected symol parameter at position " << idx << " got: " << r << "\n";); throw invalid_datatype(); } return r.get_symbol(); } +static sort* read_sort(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { + parameter const & r = read(num_parameters, parameters, idx, read_pos); + if (!r.is_ast()) { + TRACE("datatype", tout << "expected ast parameter at position " << idx << " got: " << r << "\n";); + throw invalid_datatype(); + } + ast* a = r.get_ast(); + if (!is_sort(a)) { + throw invalid_datatype(); + } + return to_sort(a); +} + enum status { WHITE, GRAY, @@ -160,7 +176,7 @@ static bool is_recursive_datatype(parameter const * parameters) { continue; } already_found[tid] = GRAY; - unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset + unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); // constructor offset unsigned num_constructors = parameters[o].get_int(); bool can_process = true; for (unsigned s = 1; s <= num_constructors; s++) { @@ -210,7 +226,7 @@ static sort_size get_datatype_size(parameter const * parameters) { continue; } already_found[tid] = GRAY; - unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset + unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); unsigned num_constructors = parameters[o].get_int(); bool is_very_big = false; bool can_process = true; @@ -296,7 +312,7 @@ static bool is_well_founded(parameter const * parameters) { changed = false; for (unsigned tid = 0; tid < num_types; tid++) { if (!well_founded[tid]) { - unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset + unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); // constructor offset unsigned num_constructors = parameters[o].get_int(); for (unsigned s = 1; s <= num_constructors; s++) { unsigned k_i = parameters[o + s].get_int(); @@ -350,9 +366,14 @@ sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, param throw invalid_datatype(); } unsigned tid = read_int(num_parameters, parameters, 1, found); + unsigned num_sort_params = read_int(num_parameters, parameters, 2, found); + for (unsigned j = 0; j < num_sort_params; ++j) { + read_sort(num_parameters, parameters, 3 + j, found); + } + unsigned c_offset = constructor_offset(parameters); for (unsigned j = 0; j < num_types; j++) { - read_symbol(num_parameters, parameters, 2 + 2*j, found); // type name - unsigned o = read_int(num_parameters, parameters, 2 + 2*j + 1, found); + read_symbol(num_parameters, parameters, c_offset + 2*j, found); // type name + unsigned o = read_int(num_parameters, parameters, c_offset + 2*j + 1, found); unsigned num_constructors = read_int(num_parameters, parameters, o, found); if (num_constructors == 0) { throw invalid_datatype(); @@ -368,9 +389,9 @@ sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, param parameter const & a_type = read(num_parameters, parameters, first_accessor + 2*r + 1, found); // accessort type if (!a_type.is_int() && !a_type.is_ast()) { throw invalid_datatype(); - if (a_type.is_ast() && !is_sort(a_type.get_ast())) { - throw invalid_datatype(); - } + } + if (a_type.is_ast() && !is_sort(a_type.get_ast())) { + throw invalid_datatype(); } } } @@ -387,7 +408,7 @@ sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, param // compute datatype size sort_size ts = get_datatype_size(parameters); - symbol const & tname = parameters[2+2*tid].get_symbol(); + symbol const & tname = parameters[c_offset + 2*tid].get_symbol(); return m_manager->mk_sort(tname, sort_info(m_family_id, k, ts, num_parameters, parameters, true)); } @@ -489,7 +510,7 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet } unsigned c_idx = parameters[1].get_int(); unsigned tid = datatype->get_parameter(1).get_int(); - unsigned o = datatype->get_parameter(2 + 2 * tid + 1).get_int(); + unsigned o = datatype_decl_plugin::constructor_offset(datatype, tid); unsigned num_constructors = datatype->get_parameter(o).get_int(); if (c_idx >= num_constructors) { m_manager->raise_exception("invalid parameters for datatype operator"); @@ -504,8 +525,6 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet return 0; } else { - - symbol c_name = datatype->get_parameter(k_i).get_symbol(); unsigned num_accessors = datatype->get_parameter(k_i + 2).get_int(); if (num_accessors != arity) { @@ -577,16 +596,22 @@ func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramet } } -bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, sort_ref_vector & new_types) { +bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_types) { buffer p; p.push_back(parameter(num_datatypes)); p.push_back(parameter(-1)); + p.push_back(parameter(num_params)); + for (unsigned i = 0; i < num_params; ++i) { + p.push_back(parameter(sort_params[i])); + } + + unsigned c_offset = constructor_offset(p.c_ptr()); for (unsigned i = 0; i < num_datatypes; i++) { p.push_back(parameter(datatypes[i]->get_name())); p.push_back(parameter(-1)); // offset is unknown at this point } for (unsigned i = 0; i < num_datatypes; i++) { - p[3+2*i] = parameter(p.size()); // save offset to constructor table + p[c_offset + 1 + 2*i] = parameter(p.size()); // save offset to constructor table ptr_vector const & constructors = datatypes[i]->get_constructors(); unsigned num_constructors = constructors.size(); p.push_back(parameter(num_constructors)); @@ -595,7 +620,7 @@ bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl * } } for (unsigned i = 0; i < num_datatypes; i++) { - unsigned o = p[3+2*i].get_int(); + unsigned o = constructor_offset(p.c_ptr(), i); ptr_vector const & constructors = datatypes[i]->get_constructors(); unsigned num_constructors = constructors.size(); for (unsigned j = 0; j < num_constructors; j++) { @@ -655,7 +680,7 @@ bool datatype_decl_plugin::is_fully_interp(sort const * s) const { parameter const * parameters = s->get_parameters(); unsigned num_types = parameters[0].get_int(); for (unsigned tid = 0; tid < num_types; tid++) { - unsigned o = parameters[2 + 2*tid + 1].get_int(); // constructor offset + unsigned o = datatype_decl_plugin::constructor_offset(s, tid); unsigned num_constructors = parameters[o].get_int(); for (unsigned si = 1; si <= num_constructors; si++) { unsigned k_i = parameters[o + si].get_int(); @@ -692,6 +717,28 @@ bool datatype_decl_plugin::is_value_visit(expr * arg, ptr_buffer & todo) co } } +unsigned datatype_decl_plugin::constructor_offset(sort const* s) { + return constructor_offset(s->get_parameters()); +} + +unsigned datatype_decl_plugin::constructor_offset(parameter const& p) { + return 3 + p.get_int(); +} + +unsigned datatype_decl_plugin::constructor_offset(parameter const* ps) { + return constructor_offset(ps[2]); +} + +unsigned datatype_decl_plugin::constructor_offset(sort const* s, unsigned tid) { + unsigned c_offset = constructor_offset(s->get_parameters()); + return s->get_parameter(c_offset + 1 + 2*tid).get_int(); +} + +unsigned datatype_decl_plugin::constructor_offset(parameter const* ps, unsigned tid) { + unsigned c_offset = constructor_offset(ps[2]); + return ps[c_offset + 1 + 2*tid].get_int(); +} + bool datatype_decl_plugin::is_value(app * e) const { TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";); if (!get_util().is_constructor(e)) @@ -742,7 +789,7 @@ datatype_util::~datatype_util() { func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id) { unsigned tid = ty->get_parameter(1).get_int(); - unsigned o = ty->get_parameter(3 + 2*tid).get_int(); + unsigned o = datatype_decl_plugin::constructor_offset(ty, tid); unsigned k_i = ty->get_parameter(o + c_id + 1).get_int(); unsigned num_accessors = ty->get_parameter(k_i + 2).get_int(); parameter p[2] = { parameter(ty), parameter(c_id) }; @@ -765,7 +812,7 @@ ptr_vector const * datatype_util::get_datatype_constructors(sort * ty m_vectors.push_back(r); m_datatype2constructors.insert(ty, r); unsigned tid = ty->get_parameter(1).get_int(); - unsigned o = ty->get_parameter(3 + 2*tid).get_int(); + unsigned o = datatype_decl_plugin::constructor_offset(ty, tid); unsigned num_constructors = ty->get_parameter(o).get_int(); for (unsigned c_id = 0; c_id < num_constructors; c_id++) { func_decl * c = get_constructor(ty, c_id); @@ -880,7 +927,7 @@ ptr_vector const * datatype_util::get_constructor_accessors(func_decl unsigned c_id = constructor->get_parameter(1).get_int(); sort * datatype = constructor->get_range(); unsigned tid = datatype->get_parameter(1).get_int(); - unsigned o = datatype->get_parameter(3 + 2*tid).get_int(); + unsigned o = datatype_decl_plugin::constructor_offset(datatype, tid); unsigned k_i = datatype->get_parameter(o + c_id + 1).get_int(); unsigned num_accessors = datatype->get_parameter(k_i+2).get_int(); parameter p[3] = { parameter(datatype), parameter(c_id), parameter(-1) }; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index ba0bedd32..b2bcf3ab0 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -100,10 +100,16 @@ public: Contract for sort: parameters[0] - (int) n - number of recursive types. parameters[1] - (int) i - index 0..n-1 of which type is defined. - + + parameters[2] - (int) p - number of type parameters. + + for j = 0..p-1 + parameters[3 + j] - (sort) s - type parameter + + c_offset := 3 + p for j in 0..n-1 - parameters[2 + 2*j] - (symbol) name of the type - parameters[2 + 2*j + 1] - (int) o - offset where the constructors are defined. + parameters[c_offset + 2*j] - (symbol) name of the type + parameters[c_offset + 2*j + 1] - (int) o - offset where the constructors are defined. for each offset o at parameters[2 + 2*j + 1] for some j in 0..n-1 parameters[o] - (int) m - number of constructors @@ -140,7 +146,7 @@ public: virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - bool mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, sort_ref_vector & new_sorts); + bool mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts); virtual expr * get_some_value(sort * s); @@ -152,6 +158,13 @@ public: virtual void get_op_names(svector & op_names, symbol const & logic); + static unsigned constructor_offset(sort const* s); + static unsigned constructor_offset(parameter const& p); + static unsigned constructor_offset(parameter const* ps); + + static unsigned constructor_offset(sort const* s, unsigned tid); + static unsigned constructor_offset(parameter const* ps, unsigned tid); + private: bool is_value_visit(expr * arg, ptr_buffer & todo) const; @@ -201,9 +214,18 @@ public: unsigned get_datatype_num_constructors(sort * ty) { SASSERT(is_datatype(ty)); unsigned tid = ty->get_parameter(1).get_int(); - unsigned o = ty->get_parameter(3 + 2 * tid).get_int(); + unsigned o = datatype_decl_plugin::constructor_offset(ty, tid); return ty->get_parameter(o).get_int(); } + unsigned get_datatype_num_parameter_sorts(sort * ty) { + SASSERT(is_datatype(ty)); + return ty->get_parameter(2).get_int(); + } + sort* get_datatype_parameter_sort(sort * ty, unsigned idx) { + SASSERT(is_datatype(ty)); + SASSERT(idx < get_datatype_num_parameter_sorts(ty)); + return to_sort(ty->get_parameter(3 + idx).get_ast()); + } unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(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); @@ -218,6 +240,7 @@ public: void reset(); void display_datatype(sort *s, std::ostream& strm); + }; #endif /* DATATYPE_DECL_PLUGIN_H_ */ diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index a053fc8e6..45ad08a78 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -258,6 +258,7 @@ protected: array_util m_arutil; fpa_util m_futil; seq_util m_sutil; + datatype_util m_dtutil; datalog::dl_decl_util m_dlutil; @@ -279,7 +280,7 @@ protected: } public: - pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dlutil(o.m()) {} + pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dtutil(o.m()), m_dlutil(o.m()) {} virtual ~pp_env() {} virtual ast_manager & get_manager() const { return m_owner.m(); } virtual arith_util & get_autil() { return m_autil; } @@ -287,6 +288,7 @@ public: virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual seq_util & get_sutil() { return m_sutil; } + virtual datatype_util & get_dtutil() { return m_dtutil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } virtual bool uses(symbol const & s) const { @@ -1218,6 +1220,7 @@ void cmd_context::push() { scope & s = m_scopes.back(); s.m_func_decls_stack_lim = m_func_decls_stack.size(); s.m_psort_decls_stack_lim = m_psort_decls_stack.size(); + s.m_psort_inst_stack_lim = m_psort_inst_stack.size(); s.m_macros_stack_lim = m_macros_stack.size(); s.m_aux_pdecls_lim = m_aux_pdecls.size(); s.m_assertions_lim = m_assertions.size(); @@ -1232,7 +1235,7 @@ void cmd_context::push(unsigned n) { push(); } -void cmd_context::restore_func_decls(unsigned old_sz) { +void cmd_context::restore_func_decls(unsigned old_sz) { SASSERT(old_sz <= m_func_decls_stack.size()); svector::iterator it = m_func_decls_stack.begin() + old_sz; svector::iterator end = m_func_decls_stack.end(); @@ -1243,6 +1246,14 @@ void cmd_context::restore_func_decls(unsigned old_sz) { m_func_decls_stack.resize(old_sz); } +void cmd_context::restore_psort_inst(unsigned old_sz) { + for (unsigned i = old_sz; i < m_psort_inst_stack.size(); ++i) { + pdecl * s = m_psort_inst_stack[i]; + s->reset_cache(*m_pmanager); + } + m_psort_inst_stack.resize(old_sz); +} + void cmd_context::restore_psort_decls(unsigned old_sz) { SASSERT(old_sz <= m_psort_decls_stack.size()); svector::iterator it = m_psort_decls_stack.begin() + old_sz; @@ -1250,9 +1261,7 @@ void cmd_context::restore_psort_decls(unsigned old_sz) { for (; it != end; ++it) { symbol const & s = *it; psort_decl * d = 0; - if (!m_psort_decls.find(s, d)) { - UNREACHABLE(); - } + VERIFY(m_psort_decls.find(s, d)); pm().dec_ref(d); m_psort_decls.erase(s); } @@ -1266,9 +1275,7 @@ void cmd_context::restore_macros(unsigned old_sz) { for (; it != end; ++it) { symbol const & s = *it; macro _m; - if (!m_macros.find(s, _m)) { - UNREACHABLE(); - } + VERIFY (m_macros.find(s, _m)); m().dec_ref(_m.second); m_macros.erase(s); } @@ -1331,7 +1338,9 @@ void cmd_context::pop(unsigned n) { restore_macros(s.m_macros_stack_lim); restore_aux_pdecls(s.m_aux_pdecls_lim); restore_assertions(s.m_assertions_lim); + restore_psort_inst(s.m_psort_inst_stack_lim); m_scopes.shrink(new_lvl); + } void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions) { @@ -1810,7 +1819,7 @@ cmd_context::dt_eh::dt_eh(cmd_context & owner): cmd_context::dt_eh::~dt_eh() { } -void cmd_context::dt_eh::operator()(sort * dt) { +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";); ptr_vector const * constructors = m_dt_util.get_datatype_constructors(dt); unsigned num_constructors = constructors->size(); @@ -1829,8 +1838,13 @@ void cmd_context::dt_eh::operator()(sort * dt) { TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); } } + if (m_owner.m_scopes.size() > 0) { + m_owner.m_psort_inst_stack.push_back(pd); + + } } + std::ostream & operator<<(std::ostream & out, cmd_context::status st) { switch (st) { case cmd_context::UNSAT: out << "unsat"; break; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 74b2f3fbc..171d59a21 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -190,6 +190,8 @@ protected: svector m_func_decls_stack; svector m_psort_decls_stack; svector m_macros_stack; + ptr_vector m_psort_inst_stack; + // ptr_vector m_aux_pdecls; ptr_vector m_assertions; @@ -201,6 +203,7 @@ protected: unsigned m_psort_decls_stack_lim; unsigned m_macros_stack_lim; unsigned m_aux_pdecls_lim; + unsigned m_psort_inst_stack_lim; // only m_assertions_lim is relevant when m_global_decls = true unsigned m_assertions_lim; }; @@ -220,7 +223,7 @@ protected: public: dt_eh(cmd_context & owner); virtual ~dt_eh(); - virtual void operator()(sort * dt); + virtual void operator()(sort * dt, pdecl* pd); }; friend class dt_eh; @@ -246,6 +249,7 @@ protected: void restore_macros(unsigned old_sz); void restore_aux_pdecls(unsigned old_sz); void restore_assertions(unsigned old_sz); + void restore_psort_inst(unsigned old_sz); void erase_func_decl_core(symbol const & s, func_decl * f); void erase_psort_decl_core(symbol const & s); diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 08a29e381..bd2ef849a 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -123,6 +123,10 @@ sort * psort::find(sort * const * s) const { } void psort::finalize(pdecl_manager & m) { + reset_cache(m); +} + +void psort::reset_cache(pdecl_manager& m) { m.del_inst_cache(m_inst_cache); m_inst_cache = 0; } @@ -171,10 +175,11 @@ public: if (other->hcons_kind() != hcons_kind()) return false; return get_num_params() == other->get_num_params() && m_idx == static_cast(other)->m_idx; - } + } virtual void display(std::ostream & out) const { out << "s_" << m_idx; } + unsigned idx() const { return m_idx; } }; class psort_app : public psort { @@ -268,6 +273,10 @@ psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symb } void psort_decl::finalize(pdecl_manager & m) { + reset_cache(m); +} + +void psort_decl::reset_cache(pdecl_manager& m) { m.del_inst_cache(m_inst_cache); m_inst_cache = 0; } @@ -284,6 +293,27 @@ sort * psort_decl::find(sort * const * s) { return m_inst_cache->find(s); } +#if 0 +psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n): + psort_decl(id, num_params, m, n) { +} + +void psort_dt_decl::finalize(pdecl_manager& m) { + psort_decl::finalize(m); +} + + +sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { + UNREACHABLE(); + return 0; +} + +void psort_dt_decl::display(std::ostream & out) const { + out << get_name() << " " << get_num_params(); +} +#endif + + psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p): psort_decl(id, num_params, m, n), m_def(p) { @@ -389,13 +419,15 @@ paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & pdecl(id, num_params), m_name(n), m_type(r) { - if (m_type.kind() == PTR_PSORT) + if (m_type.kind() == PTR_PSORT) { m.inc_ref(r.get_psort()); + } } void paccessor_decl::finalize(pdecl_manager & m) { - if (m_type.kind() == PTR_PSORT) - m.lazy_dec_ref(m_type.get_psort()); + if (m_type.kind() == PTR_PSORT) { + m.lazy_dec_ref(m_type.get_psort()); + } } bool paccessor_decl::has_missing_refs(symbol & missing) const { @@ -576,13 +608,13 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * dts.m_buffer.push_back(instantiate_decl(m, s)); datatype_decl * d_ptr = dts.m_buffer[0]; sort_ref_vector sorts(m.m()); - bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, sorts); + bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, s, sorts); TRACE("pdatatype_decl", tout << "instantiating " << m_name << " is_ok: " << is_ok << "\n";); if (is_ok) { r = sorts.get(0); cache(m, s, r); m.save_info(r, this, n, s); - m.notify_new_dt(r); + m.notify_new_dt(r, this); return r; } } @@ -651,7 +683,7 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { dts.m_buffer.push_back((*it)->instantiate_decl(m, s)); } sort_ref_vector sorts(m.m()); - bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), sorts); + bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), m_num_params, s, sorts); if (!is_ok) return false; it = m_datatypes.begin(); @@ -659,7 +691,7 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { sort * new_dt = sorts.get(i); (*it)->cache(m, s, new_dt); m.save_info(new_dt, *it, m_num_params, s); - m.notify_new_dt(new_dt); + m.notify_new_dt(new_dt, *it); } return true; } @@ -853,6 +885,11 @@ psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const return new (a().allocate(sizeof(psort_user_decl))) psort_user_decl(m_id_gen.mk(), num_params, *this, n, def); } + +//psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & n) { +// return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n); +//} + psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) { return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k); } @@ -862,6 +899,7 @@ sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args) return p->instantiate(*this, args); } + void pdecl_manager::del_decl_core(pdecl * p) { TRACE("pdecl_manager", tout << "del_decl_core:\n"; diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index f03d1b901..31005fe0d 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -46,6 +46,7 @@ public: unsigned get_ref_count() const { return m_ref_count; } unsigned hash() const { return m_id; } virtual void display(std::ostream & out) const {} + virtual void reset_cache(pdecl_manager& m) {} }; class psort_inst_cache; @@ -75,6 +76,7 @@ public: virtual char const * hcons_kind() const = 0; virtual unsigned hcons_hash() const = 0; virtual bool hcons_eq(psort const * other) const = 0; + virtual void reset_cache(pdecl_manager& m); }; // for hash consing @@ -102,6 +104,7 @@ public: // Only builtin declarations can have a variable number of parameters. bool has_var_params() const { return m_num_params == PSORT_DECL_VAR_PARAMS; } symbol const & get_name() const { return m_name; } + virtual void reset_cache(pdecl_manager& m); }; class psort_user_decl : public psort_decl { @@ -131,6 +134,20 @@ public: virtual void display(std::ostream & out) const; }; +#if 0 +class psort_dt_decl : public psort_decl { +protected: + friend class pdecl_manager; + psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n); + virtual size_t obj_size() const { return sizeof(psort_dt_decl); } + virtual void finalize(pdecl_manager & m); + virtual ~psort_dt_decl() {} +public: + virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s); + virtual void display(std::ostream & out) const; +}; +#endif + class datatype_decl_plugin; class datatype_decl; class constructor_decl; @@ -246,7 +263,7 @@ public: class new_datatype_eh { public: virtual ~new_datatype_eh() {} - virtual void operator()(sort * dt) = 0; + virtual void operator()(sort * dt, pdecl* pd) = 0; }; class pdecl_manager { @@ -279,10 +296,11 @@ public: small_object_allocator & a() const { return m_allocator; } family_id get_datatype_fid() const { return m_datatype_fid; } void set_new_datatype_eh(new_datatype_eh * eh) { m_new_dt_eh = eh; } - psort * mk_psort_cnst(sort * s); + psort * mk_psort_cnst(sort * s); psort * mk_psort_var(unsigned num_params, unsigned vidx); psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args); psort * mk_psort_app(psort_decl * d); + // psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n); psort_decl * mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def); psort_decl * mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k); paccessor_decl * mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p); @@ -304,7 +322,7 @@ public: void dec_ref(unsigned num, T * const * ps) { lazy_dec_ref(num, ps); del_decls(); } psort_inst_cache * mk_inst_cache(unsigned num_params); void del_inst_cache(psort_inst_cache * c); - void notify_new_dt(sort * dt) { if (m_new_dt_eh) (*m_new_dt_eh)(dt); } + void notify_new_dt(sort * dt, pdecl* pd) { if (m_new_dt_eh) (*m_new_dt_eh)(dt, pd); } datatype_decl_plugin * get_dt_plugin() const; void save_info(sort * s, psort_decl * d, unsigned num_args, sort * const * args); diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index a7df8db77..8cc5c4f60 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -979,7 +979,7 @@ namespace datalog { sort_ref_vector new_sorts(m); family_id dfid = m.mk_family_id("datatype"); datatype_decl_plugin* dtp = static_cast(m.get_plugin(dfid)); - VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); + VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts)); it = b.m_rules.begin_grouped_rules(); for (unsigned i = 0; it != end; ++it, ++i) { @@ -1021,7 +1021,7 @@ namespace datalog { cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr())); } dts.push_back(mk_datatype_decl(symbol("Path"), cnstrs.size(), cnstrs.c_ptr())); - VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts)); + VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts)); m_path_sort = new_sorts[0].get(); } } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 1486f6e6c..9d59d740a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -53,6 +53,8 @@ namespace smt2 { dictionary m_sort_id2param_idx; dictionary m_dt_name2idx; + dictionary m_dt_name2arity; + svector m_dt_names; scoped_ptr m_psort_stack; scoped_ptr m_sort_stack; @@ -97,6 +99,8 @@ namespace smt2 { symbol m_define_sort; symbol m_declare_sort; symbol m_declare_datatypes; + symbol m_declare_datatype; + symbol m_par; symbol m_push; symbol m_pop; symbol m_get_value; @@ -367,6 +371,13 @@ namespace smt2 { symbol const & curr_id() const { return m_scanner.get_id(); } rational curr_numeral() const { return m_scanner.get_number(); } + unsigned curr_unsigned() { + rational n = curr_numeral(); + if (!n.is_unsigned()) + throw parser_exception("invalid indexed identifier, index is too big to fit in an unsigned machine integer"); + return n.get_unsigned(); + } + bool curr_is_identifier() const { return curr() == scanner::SYMBOL_TOKEN; } bool curr_is_keyword() const { return curr() == scanner::KEYWORD_TOKEN; } @@ -400,6 +411,8 @@ namespace smt2 { void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); } void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); } void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); } + symbol check_identifier_next(char const * msg) { check_identifier(msg); symbol s = curr_id(); next(); return s; } + char const * m_current_file; void set_current_file(char const * s) { m_current_file = s; } @@ -550,7 +563,7 @@ namespace smt2 { return r; } - psort * parse_psort_name(bool ignore_unknow_sort = false) { + psort * parse_psort_name(bool ignore_unknown_sort = false) { SASSERT(curr_is_identifier()); symbol id = curr_id(); psort_decl * d = m_ctx.find_psort_decl(id); @@ -567,10 +580,10 @@ namespace smt2 { return pm().mk_psort_var(m_sort_id2param_idx.size(), idx); } else { - if (ignore_unknow_sort) - return 0; - unknown_sort(id); - UNREACHABLE(); + if (!ignore_unknown_sort) { + unknown_sort(id); + UNREACHABLE(); + } return 0; } } @@ -580,19 +593,15 @@ namespace smt2 { SASSERT(curr_is_identifier()); SASSERT(curr_id_is_underscore()); next(); - check_identifier("invalid indexed sort, symbol expected"); - symbol id = curr_id(); + symbol id = check_identifier_next("invalid indexed sort, symbol expected"); psort_decl * d = m_ctx.find_psort_decl(id); if (d == 0) unknown_sort(id); - next(); sbuffer args; while (!curr_is_rparen()) { check_int("invalid indexed sort, integer or ')' expected"); - rational n = curr_numeral(); - if (!n.is_unsigned()) - throw parser_exception("invalid indexed sort, index is too big to fit in an unsigned machine integer"); - args.push_back(n.get_unsigned()); + unsigned u = curr_unsigned(); + args.push_back(u); next(); } if (args.empty()) @@ -608,8 +617,17 @@ namespace smt2 { SASSERT(curr_is_identifier()); symbol id = curr_id(); psort_decl * d = m_ctx.find_psort_decl(id); - if (d == 0) - unknown_sort(id); + int idx = 0; + if (d == 0) { + if (m_dt_name2idx.find(id, idx)) { + unsigned num_params = m_dt_name2arity.find(id); + throw parser_exception("smtlib 2.6 parametric datatype sorts are not supported"); + // d = pm().mk_psort_dt_decl(num_params, id); + } + else { + unknown_sort(id); + } + } next(); void * mem = m_stack.allocate(sizeof(psort_frame)); new (mem) psort_frame(*this, d, psort_stack().size()); @@ -627,6 +645,7 @@ namespace smt2 { TRACE("smt2parser", tout << "num: " << num << ", d->get_num_params(): " << d->get_num_params() << "\n";); throw parser_exception("invalid number of parameters to sort constructor"); } + psort * r = pm().mk_psort_app(m_sort_id2param_idx.size(), d, num, psort_stack().c_ptr() + spos); psort_stack().shrink(spos); psort_stack().push_back(r); @@ -634,13 +653,13 @@ namespace smt2 { next(); } - void parse_psort() { + void parse_psort(bool ignore_unknown_sort = false) { unsigned stack_pos = psort_stack().size(); (void)stack_pos; unsigned num_frames = 0; do { if (curr_is_identifier()) { - psort_stack().push_back(parse_psort_name()); + psort_stack().push_back(parse_psort_name(false)); } else if (curr_is_rparen()) { if (num_frames == 0) @@ -743,43 +762,46 @@ namespace smt2 { unsigned parse_symbols() { unsigned sz = 0; check_lparen_next("invalid list of symbols, '(' expected"); - while (!curr_is_rparen()) { - check_identifier("invalid list of symbols, symbol or ')' expected"); - m_symbol_stack.push_back(curr_id()); - next(); + while (!curr_is_rparen()) { + m_symbol_stack.push_back(check_identifier_next("invalid list of symbols, symbol or ')' expected")); sz++; } next(); return sz; } + ptype parse_ptype() { + SASSERT(curr_is_identifier()); + psort * p = parse_psort_name(true); + ptype result; + if (p != 0) { + result = ptype(p); + } + else { + // parse_psort_name failed, identifier was not consumed. + int idx; + if (m_dt_name2idx.find(curr_id(), idx)) { + result = ptype(idx); + } + else { + result = ptype(curr_id()); + } + SASSERT(curr_is_identifier()); + next(); + } + return result; + } + // [ '(' identifier sort ')' ]+ void parse_accessor_decls(paccessor_decl_ref_buffer & a_decls) { while (!curr_is_rparen()) { check_lparen_next("invalid datatype declaration, '(' or ')' expected"); - check_identifier("invalid accessor declaration, symbol (accessor name) expected"); - symbol a_name = curr_id(); - next(); - if (curr_is_identifier()) { - psort * p = parse_psort_name(true); - if (p != 0) { - a_decls.push_back(pm().mk_paccessor_decl(m_sort_id2param_idx.size(), a_name, ptype(p))); - } - else { - // parse_psort_name failed, identifier was not consumed. - int idx; - if (m_dt_name2idx.find(curr_id(), idx)) { - a_decls.push_back(pm().mk_paccessor_decl(m_sort_id2param_idx.size(), a_name, ptype(idx))); - } - else { - a_decls.push_back(pm().mk_paccessor_decl(m_sort_id2param_idx.size(), a_name, ptype(curr_id()))); - } - SASSERT(curr_is_identifier()); - next(); - } + symbol a_name = check_identifier_next("invalid accessor declaration, symbol (accessor name) expected"); + if (curr_is_identifier()) { + a_decls.push_back(pm().mk_paccessor_decl(m_sort_id2param_idx.size(), a_name, parse_ptype())); } else { - parse_psort(); + parse_psort(true); a_decls.push_back(pm().mk_paccessor_decl(m_sort_id2param_idx.size(), a_name, ptype(psort_stack().back()))); psort_stack().pop_back(); } @@ -816,46 +838,53 @@ namespace smt2 { if (ct_decls.empty()) throw parser_exception("invalid datatype declaration, datatype does not have any constructors"); } - + void parse_declare_datatypes() { SASSERT(curr_is_identifier()); SASSERT(curr_id() == m_declare_datatypes); next(); unsigned line = m_scanner.get_line(); unsigned pos = m_scanner.get_pos(); - parse_sort_decl_params(); m_dt_name2idx.reset(); + bool is_smt2_6 = parse_sort_decl_or_params(); unsigned i = 0; pdatatype_decl_ref_buffer new_dt_decls(pm()); check_lparen_next("invalid datatype declaration, '(' expected"); + pdatatype_decl_ref d(pm()); while (!curr_is_rparen()) { - check_lparen_next("invalid datatype declaration, '(' or ')' expected"); - check_identifier("invalid datatype declaration, symbol (datatype name) expected"); - symbol dt_name = curr_id(); - next(); - m_dt_name2idx.insert(dt_name, i); pconstructor_decl_ref_buffer new_ct_decls(pm()); - parse_constructor_decls(new_ct_decls); - new_dt_decls.push_back(pm().mk_pdatatype_decl(m_sort_id2param_idx.size(), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr())); - check_rparen_next("invalid datatype declaration, ')' expected"); + if (is_smt2_6) { + if (i >= m_dt_names.size()) { + throw parser_exception("invalid datatype declaration, too many data-type bodies defined"); + } + symbol dt_name = m_dt_names[i]; + parse_datatype_dec(new_ct_decls); + d = pm().mk_pdatatype_decl(m_dt_name2arity.find(dt_name), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr()); + } + else { + check_lparen_next("invalid datatype declaration, '(' or ')' expected"); + symbol dt_name = check_identifier_next("invalid datatype declaration, symbol (datatype name) expected"); + m_dt_name2idx.insert(dt_name, i); + parse_constructor_decls(new_ct_decls); + d = pm().mk_pdatatype_decl(m_sort_id2param_idx.size(), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr()); + check_rparen_next("invalid datatype declaration, ')' expected"); + } + new_dt_decls.push_back(d); i++; } + if (i < m_dt_names.size()) { + throw parser_exception("invalid datatype declaration, too few datatype definitions compared to declared sorts"); + } next(); check_rparen("invalid datatype declaration"); unsigned sz = new_dt_decls.size(); if (sz == 0) { - m_ctx.print_success(); - next(); + m_ctx.print_success(); + next(); return; - } + } else if (sz == 1) { - symbol missing; - if (new_dt_decls[0]->has_missing_refs(missing)) { - std::string err_msg = "invalid datatype declaration, unknown sort '"; - err_msg += missing.str(); - err_msg += "'"; - throw parser_exception(err_msg, line, pos); - } + check_missing(new_dt_decls[0], line, pos); } else { SASSERT(sz > 1); @@ -874,12 +903,7 @@ namespace smt2 { pdatatype_decl * d = new_dt_decls[i]; SASSERT(d != 0); symbol duplicated; - if (d->has_duplicate_accessors(duplicated)) { - std::string err_msg = "invalid datatype declaration, repeated accessor identifier '"; - err_msg += duplicated.str(); - err_msg += "'"; - throw parser_exception(err_msg, line, pos); - } + check_duplicate(d, line, pos); m_ctx.insert(d); if (d->get_num_params() == 0) { // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors... @@ -890,7 +914,85 @@ namespace smt2 { TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n"; for (unsigned i = 0; i < sz; i++) tout << new_dt_decls[i]->get_name() << "\n";); m_ctx.print_success(); - next(); + next(); + } + + // (declare-datatypes ( sort_dec n+1 ) ( datatype_dec n+1 ) ) + + void parse_declare_datatypes_smt2() { + + } + + + // ( declare-datatype symbol datatype_dec) + void parse_declare_datatype() { + SASSERT(curr_is_identifier()); + SASSERT(curr_id() == m_declare_datatype); + next(); + unsigned line = m_scanner.get_line(); + unsigned pos = m_scanner.get_pos(); + symbol dt_name = curr_id(); + next(); + + m_dt_name2idx.reset(); + m_dt_name2idx.insert(dt_name, 0); + + m_sort_id2param_idx.reset(); + + pdatatype_decl_ref d(pm()); + pconstructor_decl_ref_buffer new_ct_decls(pm()); + parse_datatype_dec(new_ct_decls); + d = pm().mk_pdatatype_decl(m_sort_id2param_idx.size(), dt_name, new_ct_decls.size(), new_ct_decls.c_ptr()); + + check_missing(d, line, pos); + check_duplicate(d, line, pos); + + m_ctx.insert(d); + if (d->get_num_params() == 0) { + // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors... + sort_ref s(m()); + s = d->instantiate(pm(), 0, 0); + } + check_rparen_next("invalid end of datatype declaration, ')' expected"); + m_ctx.print_success(); + } + + + // datatype_dec ::= ( constructor_dec+ ) | ( par ( symbol+ ) ( constructor_dec+ ) ) + + void parse_datatype_dec(pconstructor_decl_ref_buffer & ct_decls) { + check_lparen_next("invalid datatype declaration, '(' expected"); + if (curr_id() == m_par) { + next(); + parse_sort_decl_params(); + check_lparen_next("invalid constructor declaration after par, '(' expected"); + parse_constructor_decls(ct_decls); + check_rparen_next("invalid datatype declaration, ')' expected"); + } + else { + parse_constructor_decls(ct_decls); + } + check_rparen_next("invalid datatype declaration, ')' expected"); + } + + void check_missing(pdatatype_decl* d, unsigned line, unsigned pos) { + symbol missing; + if (d->has_missing_refs(missing)) { + std::string err_msg = "invalid datatype declaration, unknown sort '"; + err_msg += missing.str(); + err_msg += "'"; + throw parser_exception(err_msg, line, pos); + } + } + + void check_duplicate(pdatatype_decl* d, unsigned line, unsigned pos) { + symbol duplicated; + if (d->has_duplicate_accessors(duplicated)) { + std::string err_msg = "invalid datatype declaration, repeated accessor identifier '"; + err_msg += duplicated.str(); + err_msg += "'"; + throw parser_exception(err_msg, line, pos); + } } void name_expr(expr * n, symbol const & s) { @@ -970,10 +1072,8 @@ namespace smt2 { fr->m_last_symbol = symbol::null; TRACE("consume_attributes", tout << "id: " << id << ", expr_stack().size(): " << expr_stack().size() << "\n";); if (id == m_named) { - next(); - check_identifier("invalid attribute value, symbol expected"); - name_expr(expr_stack().back(), curr_id()); - next(); + next(); + name_expr(expr_stack().back(), check_identifier_next("invalid attribute value, symbol expected")); } else if (id == m_lblpos || id == m_lblneg) { next(); @@ -989,18 +1089,13 @@ namespace smt2 { check_in_quant_ctx(fr); next(); check_int("invalid weight attribute, integer expected"); - rational n = curr_numeral(); - if (!n.is_unsigned()) - throw parser_exception("invalid weight attribute, value is too big to fit in an unsigned machine integer"); - store_weight(fr, n.get_unsigned()); + store_weight(fr, curr_unsigned()); next(); } else if (id == m_skid) { check_in_quant_ctx(fr); - next(); - check_identifier("invalid attribute value, symbol expected"); - store_skid(fr, curr_id()); - next(); + next(); + store_skid(fr, check_identifier_next("invalid attribute value, symbol expected")); } else if (id == m_qid) { check_in_quant_ctx(fr); @@ -1207,10 +1302,8 @@ namespace smt2 { unsigned num_indices = 0; while (!curr_is_rparen()) { if (curr_is_int()) { - rational n = curr_numeral(); - if (!n.is_unsigned()) - throw parser_exception("invalid indexed identifier, index is too big to fit in an unsigned machine integer"); - m_param_stack.push_back(parameter(n.get_unsigned())); + unsigned u = curr_unsigned(); + m_param_stack.push_back(parameter(u)); next(); } else if (curr_is_identifier() || curr_is_lparen()) { @@ -1786,8 +1879,8 @@ namespace smt2 { } void parse_sort_decl_params() { - check_lparen_next("invalid sort declaration, parameters missing"); m_sort_id2param_idx.reset(); + check_lparen_next("invalid sort declaration, parameters missing"); unsigned i = 0; while (!curr_is_rparen()) { check_identifier("invalid sort parameter, symbol or ')' expected"); @@ -1795,7 +1888,43 @@ namespace smt2 { i++; next(); } - next(); + next(); + } + + bool parse_sort_decl_or_params() { + m_sort_id2param_idx.reset(); + m_dt_name2arity.reset(); + m_dt_name2idx.reset(); + m_dt_names.reset(); + check_lparen_next("invalid sort declaration, parameters missing"); + unsigned i = 0; + bool first = true; + bool is_decl = false; + while (!curr_is_rparen()) { + if (first) { + is_decl = curr_is_lparen(); + first = false; + } + if (is_decl) { + check_lparen_next("invalid sort declaration, '(' expected"); + symbol dt_name = check_identifier_next("invalid sort name, identified expected"); + check_int("invalid sort declaration, arity expected"); + unsigned u = curr_unsigned(); + next(); + m_dt_name2idx.insert(dt_name, i); + m_dt_name2arity.insert(dt_name, u); + m_dt_names.push_back(dt_name); + check_rparen("invalid sort declaration, ')' expected"); + } + else { + check_identifier("invalid sort parameter, symbol or ')' expected"); + m_sort_id2param_idx.insert(curr_id(), i); + } + i++; + next(); + } + next(); + return is_decl; } void parse_declare_sort() { @@ -1814,10 +1943,8 @@ namespace smt2 { } else { check_int("invalid sort declaration, arity () or ')' expected"); - rational n = curr_numeral(); - if (!n.is_unsigned()) - throw parser_exception("invalid sort declaration, arity is too big to fit in an unsigned machine integer"); - psort_decl * decl = pm().mk_psort_user_decl(n.get_unsigned(), id, 0); + unsigned u = curr_unsigned(); + psort_decl * decl = pm().mk_psort_user_decl(u, id, 0); m_ctx.insert(decl); next(); check_rparen("invalid sort declaration, ')' expected"); @@ -2222,9 +2349,7 @@ namespace smt2 { if (curr_is_keyword() && (curr_id() == ":model-index" || curr_id() == ":model_index")) { next(); check_int("integer index expected to indexed model evaluation"); - if (!curr_numeral().is_unsigned()) - throw parser_exception("expected unsigned integer index to model evaluation"); - index = curr_numeral().get_unsigned(); + index = curr_unsigned(); next(); } @@ -2315,10 +2440,8 @@ namespace smt2 { next(); while (!curr_is_rparen()) { check_int("invalid indexed function declaration reference, integer or ')' expected"); - rational n = curr_numeral(); - if (!n.is_unsigned()) - throw parser_exception("invalid indexed function declaration reference, index is too big to fit in an unsigned machine integer"); - indices.push_back(n.get_unsigned()); + unsigned u = curr_unsigned(); + indices.push_back(u); next(); } if (indices.empty()) @@ -2350,10 +2473,8 @@ namespace smt2 { switch (k) { case CPK_UINT: { check_int("invalid command argument, unsigned integer expected"); - rational n = curr_numeral(); - if (!n.is_unsigned()) - throw parser_exception("invalid command argument, numeral is too big to fit in an unsigned machine integer"); - m_curr_cmd->set_next_arg(m_ctx, n.get_unsigned()); + unsigned u = curr_unsigned(); + m_curr_cmd->set_next_arg(m_ctx, u); next(); break; } @@ -2554,6 +2675,10 @@ namespace smt2 { parse_declare_datatypes(); return; } + if (s == m_declare_datatype) { + parse_declare_datatype(); + return; + } if (s == m_get_value) { parse_get_value(); return; @@ -2610,6 +2735,8 @@ namespace smt2 { m_define_sort("define-sort"), m_declare_sort("declare-sort"), m_declare_datatypes("declare-datatypes"), + m_declare_datatype("declare-datatype"), + m_par("par"), m_push("push"), m_pop("pop"), m_get_value("get-value"), diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index febff0151..f7da4edd7 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -66,7 +66,7 @@ void test2() { constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0); constructor_decl* constrs[3] = { R, G, B }; datatype_decl * enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs); - VERIFY(dt.mk_datatypes(1, &enum_sort, new_sorts)); + VERIFY(dt.mk_datatypes(1, &enum_sort, 0, 0, new_sorts)); del_constructor_decls(3, constrs); sort* rgb = new_sorts[0].get();