mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

remove V2 reference

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-10 15:32:53 +03:00
parent 4fe55cf8e5
commit 070c699ffc
10 changed files with 1377 additions and 2896 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/CMakeLists.txt
View file

@ -14,7 +14,6 @@ z3_add_component(ast
ast_util.cpp
bv_decl_plugin.cpp
datatype_decl_plugin.cpp
datatype_decl_plugin2.cpp
decl_collector.cpp
dl_decl_plugin.cpp
expr2polynomial.cpp

2
src/ast/ast_smt2_pp.cpp
View file

@ -434,7 +434,6 @@ 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");
}
#ifdef DATATYPE_V2
if (get_dtutil().is_datatype(s)) {
unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
if (sz > 0) {
@ -445,7 +444,6 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());
}
}
#endif
return format_ns::mk_string(get_manager(), s->get_name().str().c_str());
}

71
src/ast/ast_smt_pp.cpp
View file

@ -204,19 +204,13 @@ 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)) {
m_out << "ite";
@ -314,9 +308,6 @@ class smt_printer {
sym = "Array";
}
else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
#ifndef DATATYPE_V2
m_out << m_renaming.get_symbol(s->get_name());
#else
datatype_util util(m_manager);
unsigned num_sorts = util.get_datatype_num_parameter_sorts(s);
if (num_sorts > 0) {
@ -330,7 +321,6 @@ class smt_printer {
}
m_out << ")";
}
#endif
return;
}
else {
@ -787,8 +777,6 @@ public:
datatype_util util(m_manager);
SASSERT(util.is_datatype(s));
#ifdef DATATYPE_V2
sort_ref_vector ps(m_manager);
ptr_vector<datatype::def> defs;
util.get_defs(s, defs);
@ -839,65 +827,6 @@ public:
m_out << ")";
}
m_out << "))";
#else
ptr_vector<sort> rec_sorts;
rec_sorts.push_back(s);
mark.mark(s, true);
// 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);
for (unsigned i = 0; i < decls.size(); ++i) {
func_decl* f = decls[i];
for (unsigned j = 0; j < f->get_arity(); ++j) {
sort* s2 = f->get_domain(j);
if (!mark.is_marked(s2)) {
if (m_manager.is_uninterp(s2)) {
pp_sort_decl(mark, s2);
}
else if (!util.is_datatype(s2)) {
// skip
}
else if (util.are_siblings(s, s2)) {
rec_sorts.push_back(s2);
mark.mark(s2, true);
}
else {
pp_sort_decl(mark, s2);
}
}
}
}
}
m_out << "(declare-datatypes () (";
bool first_sort = true;
for (sort * s : rec_sorts) {
if (!first_sort) m_out << " "; else first_sort = false;
m_out << "(";
m_out << m_renaming.get_symbol(s->get_name());
m_out << " ";
bool first_constr = true;
for (func_decl* f : *util.get_datatype_constructors(s)) {
if (!first_constr) m_out << " "; else first_constr = false;
m_out << "(";
m_out << m_renaming.get_symbol(f->get_name());
for (func_decl* a : *util.get_constructor_accessors(f)) {
m_out << " (" << m_renaming.get_symbol(a->get_name()) << " ";
visit_sort(a->get_range());
m_out << ")";
}
m_out << ")";
}
m_out << ")";
}
m_out << "))";
#endif
newline();
}

2003
src/ast/datatype_decl_plugin.cpp
View file

File diff suppressed because it is too large Load diff

582
src/ast/datatype_decl_plugin.h
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -11,55 +11,390 @@ Abstract:
Author:
Leonardo de Moura (leonardo) 2008-01-09.
Nikolaj Bjorner (nbjorner) 2017-9-1
Revision History:
--*/
#define DATATYPE_V2
#ifdef DATATYPE_V2
#include "ast/datatype_decl_plugin2.h"
#else
rewritten to support SMTLIB-2.6 parameters from
Leonardo de Moura (leonardo) 2008-01-09.
--*/
#ifndef DATATYPE_DECL_PLUGIN_H_
#define DATATYPE_DECL_PLUGIN_H_
#include "ast/ast.h"
#include "util/tptr.h"
#include "util/buffer.h"
#include "util/symbol_table.h"
#include "util/obj_hashtable.h"
enum datatype_sort_kind {
enum sort_kind {
DATATYPE_SORT
};
enum datatype_op_kind {
enum op_kind {
OP_DT_CONSTRUCTOR,
OP_DT_RECOGNISER,
OP_DT_ACCESSOR,
OP_DT_IS,
OP_DT_ACCESSOR,
OP_DT_UPDATE_FIELD,
LAST_DT_OP
};
/**
\brief Auxiliary class used to declare inductive datatypes.
It may be a sort or an integer. If it is an integer,
then it represents a reference to a recursive type.
namespace datatype {
For example, consider the datatypes
Datatype
Tree = tree(value:Real, children:TreeList)
TreeList = cons_t(first_t:Tree, rest_t:Tree)
| nil_t
End
The recursive occurrences of Tree and TreeList will have idx 0 and
1 respectively.
class util;
class def;
class accessor;
class constructor;
class accessor {
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(ast_manager& m, symbol const& n, sort* range):
m_name(n),
m_range(range, m),
m_index(UINT_MAX)
{}
accessor(ast_manager& m, symbol const& n, unsigned index):
m_name(n),
m_range(m),
m_index(index)
{}
sort* range() const { return m_range; }
void fix_range(sort_ref_vector const& dts);
symbol const& name() const { return m_name; }
func_decl_ref instantiate(sort_ref_vector const& ps) const;
func_decl_ref instantiate(sort* dt) const;
void attach(constructor* d) { m_constructor = d; }
constructor const& get_constructor() const { return *m_constructor; }
def const& get_def() const;
util& u() const;
accessor* translate(ast_translation& tr);
};
class constructor {
symbol m_name;
symbol m_recognizer;
ptr_vector<accessor> m_accessors;
def* m_def;
public:
constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {}
~constructor();
void add(accessor* a) { m_accessors.push_back(a); a->attach(this); }
symbol const& name() const { return m_name; }
symbol const& recognizer() const { return m_recognizer; }
ptr_vector<accessor> const& accessors() const { return m_accessors; }
ptr_vector<accessor>::const_iterator begin() const { return m_accessors.begin(); }
ptr_vector<accessor>::const_iterator end() const { return m_accessors.end(); }
ptr_vector<accessor>::iterator begin() { return m_accessors.begin(); }
ptr_vector<accessor>::iterator end() { return m_accessors.end(); }
func_decl_ref instantiate(sort_ref_vector const& ps) const;
func_decl_ref instantiate(sort* dt) const;
void attach(def* d) { m_def = d; }
def const& get_def() const { return *m_def; }
util& u() const;
constructor* translate(ast_translation& tr);
};
namespace param_size {
class size {
unsigned m_ref;
public:
size(): m_ref(0) {}
virtual ~size() {}
void inc_ref() { ++m_ref; }
void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
static size* mk_offset(sort_size const& s);
static size* mk_param(sort_ref& p);
static size* mk_plus(size* a1, size* a2);
static size* mk_times(size* a1, size* a2);
static size* mk_plus(ptr_vector<size>& szs);
static size* mk_times(ptr_vector<size>& szs);
static size* mk_power(size* a1, size* a2);
virtual size* subst(obj_map<sort, size*>& S) = 0;
virtual sort_size eval(obj_map<sort, sort_size> const& S) = 0;
};
struct offset : public size {
sort_size m_offset;
offset(sort_size const& s): m_offset(s) {}
virtual ~offset() {}
virtual size* subst(obj_map<sort,size*>& S) { return this; }
virtual sort_size eval(obj_map<sort, sort_size> const& S) { return m_offset; }
};
struct plus : public size {
size* m_arg1, *m_arg2;
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) + rational(s2.size(), rational::ui64());
return sort_size(r);
}
};
struct times : public size {
size* m_arg1, *m_arg2;
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
return sort_size(r);
}
};
struct power : public size {
size* m_arg1, *m_arg2;
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
if (s1.size() == 1) return s1;
if (s2.size() == 1) return s1;
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
return sort_size(r);
}
};
struct sparam : public size {
sort_ref m_param;
sparam(sort_ref& p): m_param(p) {}
virtual ~sparam() {}
virtual size* subst(obj_map<sort,size*>& S) { return S[m_param]; }
virtual sort_size eval(obj_map<sort, sort_size> const& S) { return S[m_param]; }
};
};
class def {
ast_manager& m;
util& m_util;
symbol m_name;
unsigned m_class_id;
param_size::size* m_sort_size;
sort_ref_vector m_params;
mutable sort_ref m_sort;
ptr_vector<constructor> m_constructors;
public:
def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params):
m(m),
m_util(u),
m_name(n),
m_class_id(class_id),
m_sort_size(0),
m_params(m, num_params, params),
m_sort(m)
{}
~def() {
if (m_sort_size) m_sort_size->dec_ref();
for (constructor* c : m_constructors) dealloc(c);
m_constructors.reset();
}
void add(constructor* c) {
m_constructors.push_back(c);
c->attach(this);
}
symbol const& name() const { return m_name; }
unsigned id() const { return m_class_id; }
sort_ref instantiate(sort_ref_vector const& ps) const;
ptr_vector<constructor> const& constructors() const { return m_constructors; }
ptr_vector<constructor>::const_iterator begin() const { return m_constructors.begin(); }
ptr_vector<constructor>::const_iterator end() const { return m_constructors.end(); }
ptr_vector<constructor>::iterator begin() { return m_constructors.begin(); }
ptr_vector<constructor>::iterator end() { return m_constructors.end(); }
sort_ref_vector const& params() const { return m_params; }
util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; }
void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); m_sort = 0; }
def* translate(ast_translation& tr, util& u);
};
namespace decl {
class plugin : public decl_plugin {
mutable scoped_ptr<util> m_util;
map<symbol, def*, symbol_hash_proc, symbol_eq_proc> m_defs;
svector<symbol> m_def_block;
unsigned m_class_id;
util & u() const;
virtual void inherit(decl_plugin* other_p, ast_translation& tr);
public:
plugin(): m_class_id(0) {}
virtual ~plugin();
virtual void finalize();
virtual decl_plugin * mk_fresh() { return alloc(plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual expr * get_some_value(sort * s);
virtual bool is_fully_interp(sort * s) const;
virtual bool is_value(app* e) const;
virtual bool is_unique_value(app * e) const { return is_value(e); }
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void begin_def_block() { m_class_id++; m_def_block.reset(); }
void end_def_block();
def* mk(symbol const& name, unsigned n, sort * const * params);
void remove(symbol const& d);
bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);
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;
func_decl * mk_update_field(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_constructor(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_accessor(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_recognizer(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_is(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
symbol datatype_name(sort * s) const {
//SASSERT(u().is_datatype(s));
return s->get_parameter(0).get_symbol();
}
};
}
class util {
ast_manager & m;
family_id m_family_id;
mutable decl::plugin* m_plugin;
obj_map<sort, ptr_vector<func_decl> *> m_datatype2constructors;
obj_map<sort, func_decl *> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
obj_map<func_decl, func_decl *> m_constructor2recognizer;
obj_map<func_decl, func_decl *> m_recognizer2constructor;
obj_map<func_decl, func_decl *> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector m_asts;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start;
mutable ptr_vector<sort> m_fully_interp_trail;
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
friend class decl::plugin;
bool is_recursive_core(sort * s) const;
sort_size get_datatype_size(sort* s0);
void compute_datatype_size_functions(svector<symbol> const& names);
param_size::size* get_sort_size(sort_ref_vector const& params, sort* s);
bool is_well_founded(unsigned num_types, sort* const* sorts);
def& get_def(symbol const& s) { return m_plugin->get_def(s); }
void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;
public:
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);
bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }
bool is_recognizer0(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_is(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_IS); }
bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);}
bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);}
bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
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);
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);
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; }
bool are_siblings(sort * s1, sort * s2);
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; }
void get_defs(sort* s, ptr_vector<def>& defs);
def const& get_def(sort* s) const;
};
};
typedef datatype::accessor accessor_decl;
typedef datatype::constructor constructor_decl;
typedef datatype::def datatype_decl;
typedef datatype::decl::plugin datatype_decl_plugin;
typedef datatype::util datatype_util;
This is a transient value, it is only used to declare a set of
recursive datatypes.
*/
class type_ref {
void * m_data;
public:
@ -73,178 +408,29 @@ public:
int get_idx() const { return UNBOXINT(m_data); }
};
class accessor_decl;
class constructor_decl;
class datatype_decl;
class datatype_util;
inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) {
if (t.is_idx()) {
return alloc(accessor_decl, m, n, t.get_idx());
}
else {
return alloc(accessor_decl, m, n, t.get_sort());
}
}
inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) {
constructor_decl* c = alloc(constructor_decl, n, r);
for (unsigned i = 0; i < num_accessors; ++i) {
c->add(acs[i]);
}
return c;
}
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);
// Remark: the datatype becomes the owner of the constructor_decls
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);
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) {}
class datatype_decl_plugin : public decl_plugin {
mutable scoped_ptr<datatype_util> m_util;
datatype_util & get_util() const;
public:
datatype_decl_plugin() {}
virtual ~datatype_decl_plugin();
virtual void finalize();
virtual decl_plugin * mk_fresh() { return alloc(datatype_decl_plugin); }
/**
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[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
parameters[o+1] - (int) k_1 - offset for constructor definition
...
parameters[o+m] - (int) k_m - offset for constructor definition
for each offset k_i at parameters[o+s] for some s in 0..m-1
parameters[k_i] - (symbol) name of the constructor
parameters[k_i+1] - (symbol) name of the recognizer
parameters[k_i+2] - (int) m' - number of accessors
parameters[k_i+3+2*r] - (symbol) name of the r accessor
parameters[k_i+3+2*r+1] - (int or type_ast) type of the accessor. If integer, then the value must be in [0..n-1], and it
represents an reference to the recursive type.
The idea with the additional offsets is that
access to relevant constructors and types can be performed using
a few address calculations.
*/
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
/**
Contract for constructors
parameters[0] - (ast) datatype ast.
parmaeters[1] - (int) constructor idx.
Contract for accessors
parameters[0] - (ast) datatype ast.
parameters[1] - (int) constructor idx.
parameters[2] - (int) accessor idx.
Contract for tester
parameters[0] - (ast) datatype ast.
parameters[1] - (int) constructor idx.
*/
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, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);
virtual expr * get_some_value(sort * s);
virtual bool is_fully_interp(sort * s) const;
virtual bool is_value(app* e) const;
virtual bool is_unique_value(app * e) const { return is_value(e); }
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;
func_decl * mk_update_field(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
};
class datatype_util {
ast_manager & m_manager;
family_id m_family_id;
func_decl * get_constructor(sort * ty, unsigned c_id) const;
obj_map<sort, ptr_vector<func_decl> *> m_datatype2constructors;
obj_map<sort, func_decl *> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
obj_map<func_decl, func_decl *> m_constructor2recognizer;
obj_map<func_decl, func_decl *> m_recognizer2constructor;
obj_map<func_decl, func_decl *> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
ast_ref_vector m_asts;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start;
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
func_decl * get_constructor(sort * ty, unsigned c_id);
public:
datatype_util(ast_manager & m);
~datatype_util();
ast_manager & get_manager() const { return m_manager; }
bool is_datatype(sort * s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); }
bool is_enum_sort(sort* s);
bool is_recursive(sort * ty);
bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
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);
unsigned get_datatype_num_constructors(sort * ty) {
SASSERT(is_datatype(ty));
unsigned tid = ty->get_parameter(1).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);
func_decl * get_constructor_recognizer(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; }
bool are_siblings(sort * s1, sort * s2);
bool is_func_decl(datatype_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();
void display_datatype(sort *s, std::ostream& strm);
};
#endif /* DATATYPE_DECL_PLUGIN_H_ */
#endif /* DATATYPE_V2 */

1077
src/ast/datatype_decl_plugin2.cpp
View file

File diff suppressed because it is too large Load diff

439
src/ast/datatype_decl_plugin2.h
View file

@ -1,439 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
datatype_decl_plugin.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2017-9-1
Revision History:
rewritten to support SMTLIB-2.6 parameters from
Leonardo de Moura (leonardo) 2008-01-09.
--*/
#ifndef DATATYPE_DECL_PLUGIN2_H_
#define DATATYPE_DECL_PLUGIN2_H_
#include "ast/ast.h"
#include "util/buffer.h"
#include "util/symbol_table.h"
#include "util/obj_hashtable.h"
#ifdef DATATYPE_V2
enum sort_kind {
DATATYPE_SORT
};
enum op_kind {
OP_DT_CONSTRUCTOR,
OP_DT_RECOGNISER,
OP_DT_IS,
OP_DT_ACCESSOR,
OP_DT_UPDATE_FIELD,
LAST_DT_OP
};
namespace datatype {
class util;
class def;
class accessor;
class constructor;
class accessor {
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(ast_manager& m, symbol const& n, sort* range):
m_name(n),
m_range(range, m),
m_index(UINT_MAX)
{}
accessor(ast_manager& m, symbol const& n, unsigned index):
m_name(n),
m_range(m),
m_index(index)
{}
sort* range() const { return m_range; }
void fix_range(sort_ref_vector const& dts);
symbol const& name() const { return m_name; }
func_decl_ref instantiate(sort_ref_vector const& ps) const;
func_decl_ref instantiate(sort* dt) const;
void attach(constructor* d) { m_constructor = d; }
constructor const& get_constructor() const { return *m_constructor; }
def const& get_def() const;
util& u() const;
accessor* translate(ast_translation& tr);
};
class constructor {
symbol m_name;
symbol m_recognizer;
ptr_vector<accessor> m_accessors;
def* m_def;
public:
constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {}
~constructor();
void add(accessor* a) { m_accessors.push_back(a); a->attach(this); }
symbol const& name() const { return m_name; }
symbol const& recognizer() const { return m_recognizer; }
ptr_vector<accessor> const& accessors() const { return m_accessors; }
ptr_vector<accessor>::const_iterator begin() const { return m_accessors.begin(); }
ptr_vector<accessor>::const_iterator end() const { return m_accessors.end(); }
ptr_vector<accessor>::iterator begin() { return m_accessors.begin(); }
ptr_vector<accessor>::iterator end() { return m_accessors.end(); }
func_decl_ref instantiate(sort_ref_vector const& ps) const;
func_decl_ref instantiate(sort* dt) const;
void attach(def* d) { m_def = d; }
def const& get_def() const { return *m_def; }
util& u() const;
constructor* translate(ast_translation& tr);
};
namespace param_size {
class size {
unsigned m_ref;
public:
size(): m_ref(0) {}
virtual ~size() {}
void inc_ref() { ++m_ref; }
void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
static size* mk_offset(sort_size const& s);
static size* mk_param(sort_ref& p);
static size* mk_plus(size* a1, size* a2);
static size* mk_times(size* a1, size* a2);
static size* mk_plus(ptr_vector<size>& szs);
static size* mk_times(ptr_vector<size>& szs);
static size* mk_power(size* a1, size* a2);
virtual size* subst(obj_map<sort, size*>& S) = 0;
virtual sort_size eval(obj_map<sort, sort_size> const& S) = 0;
};
struct offset : public size {
sort_size m_offset;
offset(sort_size const& s): m_offset(s) {}
virtual ~offset() {}
virtual size* subst(obj_map<sort,size*>& S) { return this; }
virtual sort_size eval(obj_map<sort, sort_size> const& S) { return m_offset; }
};
struct plus : public size {
size* m_arg1, *m_arg2;
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) + rational(s2.size(), rational::ui64());
return sort_size(r);
}
};
struct times : public size {
size* m_arg1, *m_arg2;
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
return sort_size(r);
}
};
struct power : public size {
size* m_arg1, *m_arg2;
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
if (s1.is_infinite()) return s1;
if (s2.is_infinite()) return s2;
if (s1.is_very_big()) return s1;
if (s2.is_very_big()) return s2;
if (s1.size() == 1) return s1;
if (s2.size() == 1) return s1;
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
return sort_size(r);
}
};
struct sparam : public size {
sort_ref m_param;
sparam(sort_ref& p): m_param(p) {}
virtual ~sparam() {}
virtual size* subst(obj_map<sort,size*>& S) { return S[m_param]; }
virtual sort_size eval(obj_map<sort, sort_size> const& S) { return S[m_param]; }
};
};
class def {
ast_manager& m;
util& m_util;
symbol m_name;
unsigned m_class_id;
param_size::size* m_sort_size;
sort_ref_vector m_params;
mutable sort_ref m_sort;
ptr_vector<constructor> m_constructors;
public:
def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params):
m(m),
m_util(u),
m_name(n),
m_class_id(class_id),
m_sort_size(0),
m_params(m, num_params, params),
m_sort(m)
{}
~def() {
if (m_sort_size) m_sort_size->dec_ref();
for (constructor* c : m_constructors) dealloc(c);
m_constructors.reset();
}
void add(constructor* c) {
m_constructors.push_back(c);
c->attach(this);
}
symbol const& name() const { return m_name; }
unsigned id() const { return m_class_id; }
sort_ref instantiate(sort_ref_vector const& ps) const;
ptr_vector<constructor> const& constructors() const { return m_constructors; }
ptr_vector<constructor>::const_iterator begin() const { return m_constructors.begin(); }
ptr_vector<constructor>::const_iterator end() const { return m_constructors.end(); }
ptr_vector<constructor>::iterator begin() { return m_constructors.begin(); }
ptr_vector<constructor>::iterator end() { return m_constructors.end(); }
sort_ref_vector const& params() const { return m_params; }
util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; }
void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); m_sort = 0; }
def* translate(ast_translation& tr, util& u);
};
namespace decl {
class plugin : public decl_plugin {
mutable scoped_ptr<util> m_util;
map<symbol, def*, symbol_hash_proc, symbol_eq_proc> m_defs;
svector<symbol> m_def_block;
unsigned m_class_id;
util & u() const;
virtual void inherit(decl_plugin* other_p, ast_translation& tr);
public:
plugin(): m_class_id(0) {}
virtual ~plugin();
virtual void finalize();
virtual decl_plugin * mk_fresh() { return alloc(plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual expr * get_some_value(sort * s);
virtual bool is_fully_interp(sort * s) const;
virtual bool is_value(app* e) const;
virtual bool is_unique_value(app * e) const { return is_value(e); }
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void begin_def_block() { m_class_id++; m_def_block.reset(); }
void end_def_block();
def* mk(symbol const& name, unsigned n, sort * const * params);
void remove(symbol const& d);
bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);
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;
func_decl * mk_update_field(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_constructor(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_accessor(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_recognizer(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_is(
unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
symbol datatype_name(sort * s) const {
//SASSERT(u().is_datatype(s));
return s->get_parameter(0).get_symbol();
}
};
}
class util {
ast_manager & m;
family_id m_family_id;
mutable decl::plugin* m_plugin;
obj_map<sort, ptr_vector<func_decl> *> m_datatype2constructors;
obj_map<sort, func_decl *> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
obj_map<func_decl, func_decl *> m_constructor2recognizer;
obj_map<func_decl, func_decl *> m_recognizer2constructor;
obj_map<func_decl, func_decl *> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector m_asts;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start;
mutable ptr_vector<sort> m_fully_interp_trail;
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
friend class decl::plugin;
bool is_recursive_core(sort * s) const;
sort_size get_datatype_size(sort* s0);
void compute_datatype_size_functions(svector<symbol> const& names);
param_size::size* get_sort_size(sort_ref_vector const& params, sort* s);
bool is_well_founded(unsigned num_types, sort* const* sorts);
def& get_def(symbol const& s) { return m_plugin->get_def(s); }
void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;
public:
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);
bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }
bool is_recognizer0(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); }
bool is_is(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_IS); }
bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); }
bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); }
bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);}
bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);}
bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
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);
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);
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; }
bool are_siblings(sort * s1, sort * s2);
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; }
void get_defs(sort* s, ptr_vector<def>& defs);
def const& get_def(sort* s) const;
};
};
typedef datatype::accessor accessor_decl;
typedef datatype::constructor constructor_decl;
typedef datatype::def datatype_decl;
typedef datatype::decl::plugin datatype_decl_plugin;
typedef datatype::util datatype_util;
class type_ref {
void * m_data;
public:
type_ref():m_data(TAG(void *, static_cast<void*>(0), 1)) {}
type_ref(int idx):m_data(BOXINT(void *, idx)) {}
type_ref(sort * s):m_data(TAG(void *, s, 1)) {}
bool is_idx() const { return GET_TAG(m_data) == 0; }
bool is_sort() const { return GET_TAG(m_data) == 1; }
sort * get_sort() const { return UNTAG(sort *, m_data); }
int get_idx() const { return UNBOXINT(m_data); }
};
inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) {
if (t.is_idx()) {
return alloc(accessor_decl, m, n, t.get_idx());
}
else {
return alloc(accessor_decl, m, n, t.get_sort());
}
}
inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) {
constructor_decl* c = alloc(constructor_decl, n, r);
for (unsigned i = 0; i < num_accessors; ++i) {
c->add(acs[i]);
}
return c;
}
// Remark: the datatype becomes the owner of the constructor_decls
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) {}
#endif /* DATATYPE_DECL_PLUGIN_H_ */
#endif /* DATATYPE_V2 */

62
src/cmd_context/pdecl.cpp
View file

@ -355,13 +355,8 @@ psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m
sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
#ifndef DATATYPE_V2
UNREACHABLE();
return 0;
#else
SASSERT(n == m_num_params);
return m.instantiate_datatype(this, m_name, n, s);
#endif
}
void psort_dt_decl::display(std::ostream & out) const {
@ -581,7 +576,6 @@ struct datatype_decl_buffer {
~datatype_decl_buffer() { del_datatype_decls(m_buffer.size(), m_buffer.c_ptr()); }
};
#ifdef DATATYPE_V2
sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
sort * r = m.instantiate_datatype(this, m_name, n, s);
@ -615,37 +609,6 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
return r;
}
#else
sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
SASSERT(m_num_params == n);
sort * r = find(s);
if (r)
return r;
if (m_parent != 0) {
if (m_parent->instantiate(m, s)) {
r = find(s);
SASSERT(r);
return r;
}
}
else {
datatype_decl_buffer dts;
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, 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, this);
return r;
}
}
return 0;
}
#endif
void pdatatype_decl::display(std::ostream & out) const {
out << "(declare-datatype " << m_name;
@ -666,7 +629,6 @@ void pdatatype_decl::display(std::ostream & out) const {
out << ")";
}
#ifdef DATATYPE_V2
bool pdatatype_decl::commit(pdecl_manager& m) {
TRACE("datatype", tout << m_name << "\n";);
sort_ref_vector ps(m.m());
@ -683,7 +645,6 @@ bool pdatatype_decl::commit(pdecl_manager& m) {
}
return is_ok;
}
#endif
pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m,
@ -714,7 +675,6 @@ bool pdatatypes_decl::fix_missing_refs(symbol & missing) {
return true;
}
#ifdef DATATYPE_V2
sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s) {
TRACE("datatype", tout << name << " "; for (unsigned i = 0; i < n; ++i) tout << s[i]->get_name() << " "; tout << "\n";);
pdecl_manager& m = *this;
@ -746,28 +706,7 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
UNREACHABLE();
return false;
}
#else
bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
datatype_decl_buffer dts;
for (auto d : m_datatypes) {
dts.m_buffer.push_back(d->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(), m_num_params, s, sorts);
if (!is_ok)
return false;
unsigned i = 0;
for (auto d : m_datatypes) {
sort * new_dt = sorts.get(i++);
d->cache(m, s, new_dt);
m.save_info(new_dt, d, m_num_params, s);
m.notify_new_dt(new_dt, d);
}
return true;
}
#endif
#ifdef DATATYPE_V2
bool pdatatypes_decl::commit(pdecl_manager& m) {
datatype_decl_buffer dts;
for (pdatatype_decl* d : m_datatypes) {
@ -789,7 +728,6 @@ bool pdatatypes_decl::commit(pdecl_manager& m) {
}
return is_ok;
}
#endif
struct pdecl_manager::sort_info {
psort_decl * m_decl;

4
src/cmd_context/pdecl.h
View file

@ -241,9 +241,7 @@ public:
virtual void display(std::ostream & out) const;
bool has_missing_refs(symbol & missing) const;
bool has_duplicate_accessors(symbol & repeated) const;
#ifdef DATATYPE_V2
bool commit(pdecl_manager& m);
#endif
};
/**
@ -263,10 +261,8 @@ public:
pdatatype_decl const * const * children() const { return m_datatypes.c_ptr(); }
pdatatype_decl * const * begin() const { return m_datatypes.begin(); }
pdatatype_decl * const * end() const { return m_datatypes.end(); }
#ifdef DATATYPE_V2
// commit declaration
bool commit(pdecl_manager& m);
#endif
};
class new_datatype_eh {

32
src/parsers/smt2/smt2parser.cpp
View file

@ -877,9 +877,7 @@ namespace smt2 {
}
else if (sz == 1) {
check_missing(new_dt_decls[0], line, pos);
#ifdef DATATYPE_V2
new_dt_decls[0]->commit(pm());
#endif
}
else {
SASSERT(sz > 1);
@ -892,27 +890,9 @@ namespace smt2 {
err_msg += "'";
throw parser_exception(err_msg, line, pos);
}
#ifndef DATATYPE_V2
m_ctx.insert_aux_pdecl(dts.get());
#else
dts->commit(pm());
m_ctx.insert_aux_pdecl(dts.get());
#endif
m_ctx.insert_aux_pdecl(dts.get());
}
#ifndef DATATYPE_V2
for (unsigned i = 0; i < sz; i++) {
pdatatype_decl * d = new_dt_decls[i];
SASSERT(d != 0);
symbol duplicated;
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);
}
}
#else
for (unsigned i = 0; i < sz; i++) {
pdatatype_decl * d = new_dt_decls[i];
symbol duplicated;
@ -922,7 +902,6 @@ namespace smt2 {
m_ctx.insert(d);
}
}
#endif
TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n";
for (unsigned j = 0; j < new_dt_decls.size(); ++j) tout << new_dt_decls[j]->get_name() << "\n";);
m_ctx.print_success();
@ -952,16 +931,7 @@ namespace smt2 {
check_missing(d, line, pos);
check_duplicate(d, line, pos);
#ifndef DATATYPE_V2
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);
}
#else
d->commit(pm());
#endif
check_rparen_next("invalid end of datatype declaration, ')' expected");
m_ctx.print_success();
}