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

cleaning defined_names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-13 12:37:03 -08:00
parent 0cf7396707
commit 5b6842fbc5
3 changed files with 101 additions and 78 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

88
src/ast/normal_forms/defined_names.cpp
View file

@ -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<expr, app *> expr2name;
typedef obj_map<expr, proof *> 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<symbol> & 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<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> 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<symbol> 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<symbol> 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();
}

87
src/ast/normal_forms/defined_names.h
View file

@ -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<expr, app *> expr2name;
typedef obj_map<expr, proof *> 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<symbol> & 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<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> 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<symbol> 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<symbol> 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_ */

4
src/smt/asserted_formulas.cpp
View file

@ -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);