mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

fix #3807

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-10 13:42:20 -07:00
parent fa900c39ab
commit fdabaa6cd2
4 changed files with 25 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/macros/macro_manager.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/ast_translation.h"
#include "ast/recurse_expr_def.h"
@ -95,6 +96,26 @@ void macro_manager::reset() {
m_deps.reset();
}
void macro_manager::copy_to(macro_manager& dst) {
ast_manager& tm = dst.get_manager();
ast_translation tr(m, tm);
for (func_decl* f : m_decls) {
func_decl_ref f2(tr(f), tm);
quantifier_ref q2(tr(m_decl2macro[f]), tm);
proof_ref pr2(tm);
expr_dependency_ref dep2(tm);
proof* pr1 = nullptr;
if (m_decl2macro_pr.find(f, pr1)) {
pr2 = tr(pr1);
}
expr_dependency* dep1 = m_decl2macro_dep[f];
if (dep1) {
dep2 = ::translate(dep1, m, tm);
}
dst.insert(f2, q2, pr2, dep2);
}
}
bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_dependency* dep) {
TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(q, m) << "\n";);

1
src/ast/macros/macro_manager.h
View file

@ -65,6 +65,7 @@ class macro_manager {
public:
macro_manager(ast_manager & m);
~macro_manager();
void copy_to(macro_manager& dst);
ast_manager & get_manager() const { return m; }
macro_util & get_util() { return m_util; }
bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = nullptr);