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

Adding translation to ackr_model_converter.

Browse source
This commit is contained in:
Mikolas Janota 2016-06-06 18:06:45 +01:00
parent 736f2bef46
commit 9df2a183d6
2 changed files with 29 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/ackermannization/ackr_info.h
View file

@ -20,6 +20,7 @@ Revision History:
#include"ast.h" #include"ast.h"
#include"ref.h" #include"ref.h"
#include"expr_replacer.h" #include"expr_replacer.h"
#include"ast_translation.h"
/** \brief /** \brief
Information about how a formula is being converted into Information about how a formula is being converted into
@ -35,7 +36,6 @@ class ackr_info {
public: public:
ackr_info(ast_manager& m) ackr_info(ast_manager& m)
: m_m(m) : m_m(m)
, m_consts(m)
, m_er(mk_default_expr_replacer(m)) , m_er(mk_default_expr_replacer(m))
, m_subst(m_m) , m_subst(m_m)
, m_ref_count(0) , m_ref_count(0)
@ -43,16 +43,20 @@ class ackr_info {
{} {}
virtual ~ackr_info() { virtual ~ackr_info() {
m_consts.reset(); for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) {
m_m.dec_ref(i->m_key);
m_m.dec_ref(i->m_value);
}
} }
inline void set_abstr(app* term, app* c) { inline void set_abstr(app* term, app* c) {
SASSERT(!m_sealed); SASSERT(!m_sealed);
SASSERT(c); SASSERT(c && term);
m_t2c.insert(term,c); m_t2c.insert(term,c);
m_c2t.insert(c->get_decl(),term); m_c2t.insert(c->get_decl(),term);
m_subst.insert(term, c); m_subst.insert(term, c);
m_consts.push_back(c); m_m.inc_ref(term);
m_m.inc_ref(c);
} }
inline void abstract(expr * e, expr_ref& res) { inline void abstract(expr * e, expr_ref& res) {
@ -77,6 +81,17 @@ class ackr_info {
m_er->set_substitution(&m_subst); m_er->set_substitution(&m_subst);
} }
virtual ackr_info * translate(ast_translation & translator) {
ackr_info * const retv = alloc(ackr_info, translator.to());
for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) {
app * const k = translator(i->m_key);
app * const v = translator(i->m_value);
retv->set_abstr(k, v);
}
if (m_sealed) retv->seal();
return retv;
}
// //
// Reference counting // Reference counting
// //
@ -94,7 +109,6 @@ class ackr_info {
t2ct m_t2c; // terms to constants t2ct m_t2c; // terms to constants
c2tt m_c2t; // constants to terms (inversion of m_t2c) c2tt m_c2t; // constants to terms (inversion of m_t2c)
expr_ref_vector m_consts; // the constants introduced during abstraction
// replacer and substitution used to compute abstractions // replacer and substitution used to compute abstractions
scoped_ptr<expr_replacer> m_er; scoped_ptr<expr_replacer> m_er;

11
src/ackermannization/ackr_model_converter.cpp
View file

@ -53,7 +53,16 @@ public:
//void display(std::ostream & out); //void display(std::ostream & out);
virtual model_converter * translate(ast_translation & translator) {NOT_IMPLEMENTED_YET();} virtual model_converter * translate(ast_translation & translator) {
ackr_info_ref retv_info = info->translate(translator);
if (fixed_model) {
model_ref retv_mod_ref = abstr_model->translate(translator);
return alloc(ackr_model_converter, translator.to(), retv_info, retv_mod_ref);
}
else {
return alloc(ackr_model_converter, translator.to(), retv_info);
}
}
protected: protected:
ast_manager& m; ast_manager& m;
const ackr_info_ref info; const ackr_info_ref info;