mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-24 09:12:43 -07:00
parent 2b0106c199
commit a0a8bc2a62
13 changed files with 452 additions and 156 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast_smt2_pp.cpp
View file

@ -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<format> 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());
}

6
src/ast/ast_smt2_pp.h
View file

@ -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; }
};

15
src/ast/ast_smt_pp.cpp
View file

@ -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 {

85
src/ast/datatype_decl_plugin.cpp
View file

@ -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<parameter> 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<constructor_decl> 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<constructor_decl> 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<app> & 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<func_decl> 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<func_decl> 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) };

33
src/ast/datatype_decl_plugin.h
View file

@ -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<builtin_name> & 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<app> & 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_ */