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

move to abstract symbols

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-10 12:14:13 -08:00
parent 78a1736bd2
commit 541658fe02
16 changed files with 117 additions and 93 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast.h
View file

@ -109,7 +109,7 @@ private:
union {
int m_int; // for PARAM_INT
ast* m_ast; // for PARAM_AST
void const* m_symbol; // for PARAM_SYMBOL
symbol m_symbol; // for PARAM_SYMBOL
rational* m_rational; // for PARAM_RATIONAL
double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
unsigned m_ext_id; // for PARAM_EXTERNAL
@ -121,11 +121,11 @@ public:
explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {}
explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {}
explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {}
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {}
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
parameter(parameter const&);
@ -176,7 +176,7 @@ public:
int get_int() const { SASSERT(is_int()); return m_int; }
ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
symbol get_symbol() const { SASSERT(is_symbol()); return symbol::mk_symbol_from_c_ptr(m_symbol); }
symbol get_symbol() const { SASSERT(is_symbol()); return m_symbol; }
rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; }
double get_double() const { SASSERT(is_double()); return m_dval; }
unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }

54
src/ast/dl_decl_plugin.cpp
View file

@ -632,24 +632,30 @@ namespace datalog {
}
void dl_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
}
dl_decl_util::ast_plugin_registrator::ast_plugin_registrator(ast_manager& m)
{
// ensure required plugins are installed into the ast_manager
reg_decl_plugins(m);
}
dl_decl_util::dl_decl_util(ast_manager& m):
m_plugin_registrator(m),
m(m),
m_arith(m),
m_bv(m),
m_fid(m.mk_family_id(symbol("datalog_relation")))
m_fid(null_family_id)
{}
bv_util& dl_decl_util::bv() const {
if (!m_bv) m_bv = alloc(bv_util, m);
return *m_bv;
}
family_id dl_decl_util::get_family_id() const {
if (m_fid == null_family_id) {
m_fid = m.mk_family_id(symbol("datalog_relation"));
}
return m_fid;
};
arith_util& dl_decl_util::arith() const {
if (!m_arith) m_arith = alloc(arith_util, m);
return *m_arith;
}
// create a constant belonging to a given finite domain.
app* dl_decl_util::mk_numeral(uint64_t value, sort* s) {
@ -659,13 +665,13 @@ namespace datalog {
m.raise_exception("value is out of bounds");
}
parameter params[2] = { parameter(rational(value, rational::ui64())), parameter(s) };
return m.mk_const(m.mk_func_decl(m_fid, OP_DL_CONSTANT, 2, params, 0, (sort*const*)nullptr));
return m.mk_const(m.mk_func_decl(get_family_id(), OP_DL_CONSTANT, 2, params, 0, (sort*const*)nullptr));
}
if (m_arith.is_int(s) || m_arith.is_real(s)) {
return m_arith.mk_numeral(rational(value, rational::ui64()), s);
if (arith().is_int(s) || arith().is_real(s)) {
return arith().mk_numeral(rational(value, rational::ui64()), s);
}
if (m_bv.is_bv_sort(s)) {
return m_bv.mk_numeral(rational(value, rational::ui64()), s);
if (bv().is_bv_sort(s)) {
return bv().mk_numeral(rational(value, rational::ui64()), s);
}
if (m.is_bool(s)) {
if (value == 0) {
@ -699,7 +705,7 @@ namespace datalog {
}
rational val;
unsigned bv_size = 0;
if (m_bv.is_numeral(e, val, bv_size) && bv_size < 64) {
if (bv().is_numeral(e, val, bv_size) && bv_size < 64) {
SASSERT(val.is_uint64());
v = val.get_uint64();
return true;
@ -719,8 +725,8 @@ namespace datalog {
if (is_numeral(c)) return true;
rational val;
unsigned bv_size = 0;
if (m_arith.is_numeral(c, val) && val.is_uint64()) return true;
if (m_bv.is_numeral(c, val, bv_size) && bv_size < 64) return true;
if (arith().is_numeral(c, val) && val.is_uint64()) return true;
if (bv().is_numeral(c, val, bv_size) && bv_size < 64) return true;
return m.is_true(c) || m.is_false(c);
}
@ -731,7 +737,7 @@ namespace datalog {
throw default_exception(sstm.str());
}
parameter params[2] = { parameter(name), parameter(rational(domain_size, rational::ui64())) };
return m.mk_sort(m_fid, DL_FINITE_SORT, 2, params);
return m.mk_sort(get_family_id(), DL_FINITE_SORT, 2, params);
}
bool dl_decl_util::try_get_size(const sort * s, uint64_t& size) const {
@ -745,16 +751,16 @@ namespace datalog {
app* dl_decl_util::mk_lt(expr* a, expr* b) {
expr* args[2] = { a, b };
return m.mk_app(m_fid, OP_DL_LT, 0, nullptr, 2, args);
return m.mk_app(get_family_id(), OP_DL_LT, 0, nullptr, 2, args);
}
app* dl_decl_util::mk_le(expr* a, expr* b) {
expr* args[2] = { b, a };
return m.mk_not(m.mk_app(m_fid, OP_DL_LT, 0, nullptr, 2, args));
return m.mk_not(m.mk_app(get_family_id(), OP_DL_LT, 0, nullptr, 2, args));
}
sort* dl_decl_util::mk_rule_sort() {
return m.mk_sort(m_fid, DL_RULE_SORT);
return m.mk_sort(get_family_id(), DL_RULE_SORT);
}
app* dl_decl_util::mk_rule(symbol const& name, unsigned num_args, expr* const* args) {

36
src/ast/dl_decl_plugin.h
View file

@ -139,28 +139,14 @@ namespace datalog {
};
class dl_decl_util {
/**
Some plugins need to be registered in the ast_manager before we
create some of the member objects (the bv_util requires bv plugin
installed).
Doing this in the constructor of the dl_decl_plugin object is too late (as
member objects are created before we get into the constructor), so we
have this auxiliary object that is the first object of the context,
so that it gets created first. It's only purpose is that in its
constructor the required plugins are added to the ast manager.
*/
class ast_plugin_registrator {
public:
ast_plugin_registrator(ast_manager& m);
};
ast_plugin_registrator m_plugin_registrator;
ast_manager& m;
arith_util m_arith;
bv_util m_bv;
family_id m_fid;
mutable scoped_ptr<arith_util> m_arith;
mutable scoped_ptr<bv_util> m_bv;
mutable family_id m_fid;
bv_util& bv() const;
arith_util& arith() const;
public:
dl_decl_util(ast_manager& m);
@ -172,9 +158,9 @@ namespace datalog {
app* mk_le(expr* a, expr* b);
bool is_lt(const expr* a) const { return is_app_of(a, m_fid, OP_DL_LT); }
bool is_lt(const expr* a) const { return is_app_of(a, get_family_id(), OP_DL_LT); }
bool is_numeral(const expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); }
bool is_numeral(const expr* c) const { return is_app_of(c, get_family_id(), OP_DL_CONSTANT); }
bool is_numeral(const expr* e, uint64_t& v) const;
@ -191,7 +177,7 @@ namespace datalog {
bool try_get_size(const sort *, uint64_t& size) const;
bool is_finite_sort(sort* s) const {
return is_sort_of(s, m_fid, DL_FINITE_SORT);
return is_sort_of(s, get_family_id(), DL_FINITE_SORT);
}
bool is_finite_sort(expr* e) const {
@ -199,7 +185,7 @@ namespace datalog {
}
bool is_rule_sort(sort* s) const {
return is_sort_of(s, m_fid, DL_RULE_SORT);
return is_sort_of(s, get_family_id(), DL_RULE_SORT);
}
sort* mk_rule_sort();
@ -210,7 +196,7 @@ namespace datalog {
ast_manager& get_manager() const { return m; }
family_id get_family_id() const { return m_fid; }
family_id get_family_id() const;
};

8
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -486,25 +486,25 @@ void bv2fpa_converter::display(std::ostream & out) {
for (auto const& kv : m_const2bv) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
unsigned indent = n.display_size() + 4;
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (auto const& kv : m_rm_const2bv) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
unsigned indent = n.display_size() + 4;
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (auto const& kv : m_uf2bvuf) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
unsigned indent = n.display_size() + 4;
out << mk_ismt2_pp(kv.m_value, m, indent) << ")";
}
for (auto const& kv : m_min_max_specials) {
const symbol & n = kv.m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
unsigned indent = n.display_size() + 4;
out << mk_ismt2_pp(kv.m_value.first, m, indent) << "; " <<
mk_ismt2_pp(kv.m_value.second, m, indent) << ")";
}

4
src/ast/pp.cpp
View file

@ -26,8 +26,8 @@ static std::pair<unsigned, bool> space_upto_line_break(ast_manager & m, format *
decl_kind k = f->get_decl_kind();
switch(k) {
case OP_STRING: {
size_t len = strlen(f->get_decl()->get_parameter(0).get_symbol().bare_str());
return std::make_pair(static_cast<unsigned>(len), false);
unsigned len = f->get_decl()->get_parameter(0).get_symbol().display_size();
return std::make_pair(len, false);
}
case OP_CHOICE:
return space_upto_line_break(m, to_app(f->get_arg(0)));

2
src/ast/seq_decl_plugin.cpp
View file

@ -523,7 +523,7 @@ void seq_decl_plugin::init() {
if (m_init) return;
ast_manager& m = *m_manager;
m_init = true;
sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0));
sort* A = m.mk_uninterpreted_sort(symbol(0u));
sort* strT = m_string;
parameter paramA(A);
parameter paramS(strT);