From 5b6842fbc5b559a86e65fc3825b4ecccf0f49a86 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Dec 2012 12:37:03 -0800 Subject: [PATCH] cleaning defined_names Signed-off-by: Leonardo de Moura --- src/ast/normal_forms/defined_names.cpp | 88 ++++++++++++++++++++++++++ src/ast/normal_forms/defined_names.h | 87 ++++--------------------- src/smt/asserted_formulas.cpp | 4 +- 3 files changed, 101 insertions(+), 78 deletions(-) diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index dab0ca0d8..91acacf61 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -17,11 +17,64 @@ Revision History: --*/ #include"defined_names.h" +#include"obj_hashtable.h" #include"used_vars.h" #include"var_subst.h" #include"ast_smt2_pp.h" #include"ast_pp.h" +struct defined_names::impl { + typedef obj_map expr2name; + typedef obj_map expr2proof; + ast_manager & m_manager; + symbol m_z3name; + + /** + \brief Mapping from expressions to their names. A name is an application. + If the expression does not have free variables, then the name is just a constant. + */ + expr2name m_expr2name; + /** + \brief Mapping from expressions to the apply-def proof. + That is, for each expression e, m_expr2proof[e] is the + proof e and m_expr2name[2] are observ. equivalent. + + This mapping is not used if proof production is disabled. + */ + expr2proof m_expr2proof; + + /** + \brief Domain of m_expr2name. It is used to keep the expressions + alive and for backtracking + */ + expr_ref_vector m_exprs; + expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive. + proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive. + + + unsigned_vector m_lims; //!< Backtracking support. + + impl(ast_manager & m, char const * prefix); + virtual ~impl(); + + app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer & var_names); + void cache_new_name(expr * e, app * name); + void cache_new_name_intro_proof(expr * e, proof * pr); + void bound_vars(sort_ref_buffer const & sorts, buffer const & names, expr * def_conjunct, app * name, expr_ref & result); + void bound_vars(sort_ref_buffer const & sorts, buffer const & names, expr * def_conjunct, app * name, expr_ref_buffer & result); + virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer const & var_names, expr_ref & new_def); + bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr); + void push_scope(); + void pop_scope(unsigned num_scopes); + void reset(); +}; + +struct defined_names::pos_impl : public defined_names::impl { + pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {} + virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer const & var_names, expr_ref & new_def); +}; + + defined_names::impl::impl(ast_manager & m, char const * prefix): m_manager(m), m_exprs(m), @@ -222,5 +275,40 @@ void defined_names::impl::reset() { m_lims.reset(); } +defined_names::defined_names(ast_manager & m, char const * fresh_prefix) { + m_impl = alloc(impl, m, fresh_prefix); + m_pos_impl = alloc(pos_impl, m, fresh_prefix); +} + +defined_names::~defined_names() { + dealloc(m_impl); + dealloc(m_pos_impl); +} + +bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) { + return m_impl->mk_name(e, new_def, new_def_pr, n, pr); +} + +bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) { + return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr); +} + +void defined_names::push() { + m_impl->push_scope(); + m_pos_impl->push_scope(); +} + +void defined_names::pop(unsigned num_scopes) { + m_impl->pop_scope(num_scopes); + m_pos_impl->pop_scope(num_scopes); +} + +void defined_names::reset() { + m_impl->reset(); + m_pos_impl->reset(); +} + + + diff --git a/src/ast/normal_forms/defined_names.h b/src/ast/normal_forms/defined_names.h index c5e4a116f..d720a2fa3 100644 --- a/src/ast/normal_forms/defined_names.h +++ b/src/ast/normal_forms/defined_names.h @@ -21,7 +21,6 @@ Revision History: #define _DEFINED_NAMES_H_ #include"ast.h" -#include"obj_hashtable.h" /** \brief Mapping from expressions to skolem functions that are used to name them. @@ -29,62 +28,13 @@ Revision History: The mapping supports backtracking using the methods #push_scope and #pop_scope. */ class defined_names { - - struct impl { - typedef obj_map expr2name; - typedef obj_map expr2proof; - ast_manager & m_manager; - symbol m_z3name; - - /** - \brief Mapping from expressions to their names. A name is an application. - If the expression does not have free variables, then the name is just a constant. - */ - expr2name m_expr2name; - /** - \brief Mapping from expressions to the apply-def proof. - That is, for each expression e, m_expr2proof[e] is the - proof e and m_expr2name[2] are observ. equivalent. - - This mapping is not used if proof production is disabled. - */ - expr2proof m_expr2proof; - - /** - \brief Domain of m_expr2name. It is used to keep the expressions - alive and for backtracking - */ - expr_ref_vector m_exprs; - expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive. - proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive. - - - unsigned_vector m_lims; //!< Backtracking support. - - impl(ast_manager & m, char const * prefix); - virtual ~impl(); - - app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer & var_names); - void cache_new_name(expr * e, app * name); - void cache_new_name_intro_proof(expr * e, proof * pr); - void bound_vars(sort_ref_buffer const & sorts, buffer const & names, expr * def_conjunct, app * name, expr_ref & result); - void bound_vars(sort_ref_buffer const & sorts, buffer const & names, expr * def_conjunct, app * name, expr_ref_buffer & result); - virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer const & var_names, expr_ref & new_def); - bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr); - void push_scope(); - void pop_scope(unsigned num_scopes); - void reset(); - }; - - struct pos_impl : public impl { - pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {} - virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer const & var_names, expr_ref & new_def); - }; - - impl m_impl; - pos_impl m_pos_impl; + struct impl; + struct pos_impl; + impl * m_impl; + pos_impl * m_pos_impl; public: - defined_names(ast_manager & m, char const * fresh_prefix = "z3name"):m_impl(m, fresh_prefix), m_pos_impl(m, fresh_prefix) {} + defined_names(ast_manager & m, char const * fresh_prefix = "z3name"); + ~defined_names(); // ----------------------------------- // @@ -113,9 +63,7 @@ public: Remark: the definitions are closed with an universal quantifier if e contains free variables. */ - bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) { - return m_impl.mk_name(e, new_def, new_def_pr, n, pr); - } + bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr); /** \brief Create a name for a positive occurrence of the expression \c e. @@ -127,24 +75,11 @@ public: Remark: the definitions are closed with an universal quantifier if e contains free variables. */ - bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) { - return m_pos_impl.mk_name(e, new_def, new_def_pr, n, pr); - } + bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr); - void push_scope() { - m_impl.push_scope(); - m_pos_impl.push_scope(); - } - - void pop_scope(unsigned num_scopes) { - m_impl.pop_scope(num_scopes); - m_pos_impl.pop_scope(num_scopes); - } - - void reset() { - m_impl.reset(); - m_pos_impl.reset(); - } + void push(); + void pop(unsigned num_scopes); + void reset(); }; #endif /* _DEFINED_NAMES_H_ */ diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6da2c15f5..5552050db 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -189,7 +189,7 @@ void asserted_formulas::push_scope() { s.m_asserted_formulas_lim = m_asserted_formulas.size(); SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead); s.m_inconsistent_old = m_inconsistent; - m_defined_names.push_scope(); + m_defined_names.push(); m_bv_sharing.push_scope(); commit(); } @@ -201,7 +201,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { unsigned new_lvl = m_scopes.size() - num_scopes; scope & s = m_scopes[new_lvl]; m_inconsistent = s.m_inconsistent_old; - m_defined_names.pop_scope(num_scopes); + m_defined_names.pop(num_scopes); m_asserted_formulas.shrink(s.m_asserted_formulas_lim); if (m_manager.proofs_enabled()) m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);