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

copy declarations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-08 21:20:54 +03:00
parent 19fa5f8cb3
commit 0c9711aad7
6 changed files with 73 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.cpp
View file

@ -1529,12 +1529,15 @@ void ast_manager::raise_exception(char const * msg) {
throw ast_exception(msg);
}
#include "ast/ast_translation.h"
void ast_manager::copy_families_plugins(ast_manager const & from) {
TRACE("copy_families_plugins",
tout << "target:\n";
for (family_id fid = 0; m_family_manager.has_family(fid); fid++) {
tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n";
});
ast_translation trans(const_cast<ast_manager&>(from), *this, false);
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
@ -1555,6 +1558,9 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
SASSERT(new_p->get_family_id() == fid);
SASSERT(has_plugin(fid));
}
if (from.has_plugin(fid)) {
get_plugin(fid)->inherit(from.get_plugin(fid), trans);
}
SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
SASSERT(!from.has_plugin(fid) || has_plugin(fid));

4
src/ast/ast.h
View file

@ -895,6 +895,8 @@ struct ast_eq_proc {
}
};
class ast_translation;
class ast_table : public chashtable<ast*, obj_ptr_hash<ast>, ast_eq_proc> {
public:
void erase(ast * n);
@ -930,6 +932,8 @@ protected:
m_family_id = id;
}
virtual void inherit(decl_plugin* other_p, ast_translation& ) { }
friend class ast_manager;
public:

8
src/ast/ast_translation.cpp
View file

@ -37,11 +37,9 @@ void ast_translation::cleanup() {
}
void ast_translation::reset_cache() {
obj_map<ast, ast*>::iterator it = m_cache.begin();
obj_map<ast, ast*>::iterator end = m_cache.end();
for (; it != end; ++it) {
m_from_manager.dec_ref(it->m_key);
m_to_manager.dec_ref(it->m_value);
for (auto & kv : m_cache) {
m_from_manager.dec_ref(kv.m_key);
m_to_manager.dec_ref(kv.m_value);
}
m_cache.reset();
}

47
src/ast/datatype_decl_plugin2.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include "ast/datatype_decl_plugin2.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_translation.h"
namespace datatype {
@ -53,6 +54,9 @@ namespace datatype {
def const& accessor::get_def() const { return m_constructor->get_def(); }
util& accessor::u() const { return m_constructor->u(); }
accessor* accessor::translate(ast_translation& tr) {
return alloc(accessor, tr.to(), name(), to_sort(tr(m_range.get())));
}
constructor::~constructor() {
for (accessor* a : m_accessors) dealloc(a);
@ -76,6 +80,15 @@ namespace datatype {
return instantiate(sorts);
}
constructor* constructor::translate(ast_translation& tr) {
constructor* result = alloc(constructor, m_name, m_recognizer);
for (accessor* a : *this) {
result->add(a->translate(tr));
}
return result;
}
sort_ref def::instantiate(sort_ref_vector const& sorts) const {
sort_ref s(m);
TRACE("datatype", tout << "instantiate " << m_name << "\n";);
@ -91,6 +104,19 @@ namespace datatype {
return sort_ref(m.substitute(m_sort, sorts.size(), m_params.c_ptr(), sorts.c_ptr()), m);
}
def* def::translate(ast_translation& tr, util& u) {
sort_ref_vector ps(tr.to());
for (sort* p : m_params) {
ps.push_back(to_sort(tr(p)));
}
def* result = alloc(def, tr.to(), u, m_name, m_class_id, ps.size(), ps.c_ptr());
for (constructor* c : *this) {
add(c->translate(tr));
}
if (m_sort) result->m_sort = to_sort(tr(m_sort.get()));
return result;
}
enum status {
GRAY,
BLACK
@ -145,6 +171,27 @@ namespace datatype {
return *(m_util.get());
}
static unsigned stack_depth = 0;
void plugin::inherit(decl_plugin* other_p, ast_translation& tr) {
++stack_depth;
SASSERT(stack_depth < 10);
plugin* p = dynamic_cast<plugin*>(other_p);
svector<symbol> names;
SASSERT(p);
for (auto& kv : p->m_defs) {
def* d = kv.m_value;
if (!m_defs.contains(kv.m_key)) {
names.push_back(kv.m_key);
m_defs.insert(kv.m_key, d->translate(tr, u()));
}
}
m_class_id = m_defs.size();
u().compute_datatype_size_functions(names);
--stack_depth;
}
struct invalid_datatype {};
sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {

6
src/ast/datatype_decl_plugin2.h
View file

@ -75,6 +75,7 @@ namespace datatype {
constructor const& get_constructor() const { return *m_constructor; }
def const& get_def() const;
util& u() const;
accessor* translate(ast_translation& tr);
};
class constructor {
@ -98,6 +99,7 @@ namespace datatype {
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 {
@ -228,6 +230,7 @@ namespace datatype {
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 {
@ -238,6 +241,9 @@ namespace datatype {
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();

18
src/smt/smt_solver.cpp
View file

@ -61,15 +61,14 @@ namespace smt {
}
virtual solver * translate(ast_manager & m, params_ref const & p) {
ast_translation translator(get_manager(), m);
solver * result = alloc(solver, m, p, m_logic);
smt::kernel::copy(m_context, result->m_context);
ast_translation translator(get_manager(), m);
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
for (; it != end; it++)
result->m_name2assertion.insert(translator(it->m_key),
translator(it->m_value));
for (auto & kv : m_name2assertion)
result->m_name2assertion.insert(translator(kv.m_key),
translator(kv.m_value));
return result;
}
@ -264,7 +263,7 @@ namespace smt {
}
void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) {
assrtn_fds.resize(m_name2assertion.size());
assrtn_fds.resize(m_name2assertion.size());
obj_map<expr, expr*>::iterator ait = m_name2assertion.begin();
obj_map<expr, expr*>::iterator aend = m_name2assertion.end();
for (unsigned i = 0; ait != aend; ait++, i++) {
@ -277,10 +276,7 @@ namespace smt {
}
bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) {
func_decl_set::iterator it = pattern_fds.begin();
func_decl_set::iterator end = pattern_fds.end();
for (; it != end; it++) {
func_decl * fd = *it;
for (func_decl * fd : pattern_fds) {
if (assrtn_fds.contains(fd))
return true;
}