From 6457654e2e63deb7debb75bdc5029f85265789bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Sep 2014 14:30:30 -0700 Subject: [PATCH] make self-contained bind-variables Signed-off-by: Nikolaj Bjorner --- src/muz/base/bind_variables.cpp | 154 ++++++++++++++++++++++++++++++++ src/muz/base/bind_variables.h | 51 +++++++++++ src/muz/base/dl_context.cpp | 37 +------- src/muz/base/dl_context.h | 7 +- src/muz/base/hnf.h | 43 +++++---- 5 files changed, 231 insertions(+), 61 deletions(-) create mode 100644 src/muz/base/bind_variables.cpp create mode 100644 src/muz/base/bind_variables.h diff --git a/src/muz/base/bind_variables.cpp b/src/muz/base/bind_variables.cpp new file mode 100644 index 000000000..0cc50625e --- /dev/null +++ b/src/muz/base/bind_variables.cpp @@ -0,0 +1,154 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + bind_variables.cpp + +Abstract: + + Utility to find constants that are declared as variables. + +Author: + + Nikolaj Bjorner (nbjorner) 9-24-2014 + +Notes: + + +--*/ + +#include "bind_variables.h" + +bind_variables::bind_variables(ast_manager & m): + m(m), + m_vars(m), + m_pinned(m) +{} + +bind_variables::~bind_variables() { +} + +expr_ref bind_variables::operator()(expr* fml, bool is_forall) { + if (m_vars.empty()) { + return expr_ref(fml, m); + } + SASSERT(m_pinned.empty()); + expr_ref result = abstract(fml, m_cache, 0); + if (!m_names.empty()) { + m_bound.reverse(); + m_names.reverse(); + result = m.mk_quantifier(is_forall, m_bound.size(), m_bound.c_ptr(), m_names.c_ptr(), result); + } + m_pinned.reset(); + m_cache.reset(); + m_names.reset(); + m_bound.reset(); + for (var2bound::iterator it = m_var2bound.begin(); it != m_var2bound.end(); ++it) { + it->m_value = 0; + } + return result; +} + + +expr_ref bind_variables::abstract(expr* term, cache_t& cache, unsigned scope) { + unsigned sz = m_todo.size(); + m_todo.push_back(term); + m_args.reset(); + expr* b, *arg; + while (m_todo.size() > sz) { + expr* e = m_todo.back(); + if (cache.contains(e)) { + m_todo.pop_back(); + continue; + } + switch(e->get_kind()) { + case AST_VAR: { + SASSERT(to_var(e)->get_idx() < scope); + // mixing bound variables and free is possible for the caller, + // but not proper use. + // So we assert here even though we don't check for it. + cache.insert(e, e); + m_todo.pop_back(); + break; + } + case AST_APP: { + app* a = to_app(e); + var2bound::obj_map_entry* w = m_var2bound.find_core(a); + if (w) { + var* v = w->get_data().m_value; + if (!v) { + // allocate a bound index. + v = m.mk_var(m_names.size(), m.get_sort(a)); + m_names.push_back(a->get_decl()->get_name()); + m_bound.push_back(m.get_sort(a)); + w->get_data().m_value = v; + m_pinned.push_back(v); + } + if (scope == 0) { + cache.insert(e, v); + } + else { + var* v1 = m.mk_var(scope + v->get_idx(), m.get_sort(v)); + m_pinned.push_back(v1); + cache.insert(e, v1); + } + m_todo.pop_back(); + break; + } + bool all_visited = true; + bool some_diff = false; + m_args.reset(); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + arg = a->get_arg(i); + if (!cache.find(arg, b)) { + m_todo.push_back(arg); + all_visited = false; + } + else if (all_visited) { + m_args.push_back(b); + if (b != arg) { + some_diff = true; + } + } + } + if (all_visited) { + if (some_diff) { + b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr()); + m_pinned.push_back(b); + } + else { + b = a; + } + cache.insert(e, b); + m_todo.pop_back(); + } + break; + } + case AST_QUANTIFIER: { + quantifier* q = to_quantifier(e); + expr_ref_buffer patterns(m); + expr_ref result1(m); + unsigned new_scope = scope + q->get_num_decls(); + cache_t new_cache; + for (unsigned i = 0; i < q->get_num_patterns(); ++i) { + patterns.push_back(abstract(q->get_pattern(i), new_cache, new_scope)); + } + result1 = abstract(q->get_expr(), new_cache, new_scope); + b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get()); + m_pinned.push_back(b); + cache.insert(e, b); + m_todo.pop_back(); + break; + } + default: + UNREACHABLE(); + } + } + return expr_ref(cache.find(term), m); +} + +void bind_variables::add_var(app* v) { + m_vars.push_back(v); + m_var2bound.insert(v, 0); +} diff --git a/src/muz/base/bind_variables.h b/src/muz/base/bind_variables.h new file mode 100644 index 000000000..87b2f186b --- /dev/null +++ b/src/muz/base/bind_variables.h @@ -0,0 +1,51 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + bind_variables.h + +Abstract: + + Utility to find constants that are declard as varaibles. + +Author: + + Nikolaj Bjorner (nbjorner) 9-24-2014 + +Notes: + + +--*/ + +#ifndef _BIND_VARIABLES_H_ +#define _BIND_VARIABLES_H_ + +#include"ast.h" + +class bind_variables { + typedef obj_map var2bound; + typedef obj_map cache_t; + ast_manager& m; + app_ref_vector m_vars; + obj_map m_cache; + var2bound m_var2bound; + expr_ref_vector m_pinned; + ptr_vector m_bound; + svector m_names; + ptr_vector m_todo; + ptr_vector m_args; + + + + expr_ref abstract(expr* fml, cache_t& cache, unsigned scope); +public: + bind_variables(ast_manager & m); + ~bind_variables(); + + expr_ref operator()(expr* fml, bool is_forall); + + void add_var(app* v); +}; + +#endif /* _BIND_VARIABLES_H_ */ diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 2b3b70a41..f79a65705 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -210,14 +210,12 @@ namespace datalog { m_rewriter(m), m_var_subst(m), m_rule_manager(*this), - m_elim_unused_vars(m), - m_abstractor(m), m_contains_p(*this), m_check_pred(m_contains_p, m), m_transf(*this), m_trail(*this), m_pinned(m), - m_vars(m), + m_bind_variables(m), m_rule_set(*this), m_transformed_rule_set(*this), m_rule_fmls_head(0), @@ -323,40 +321,11 @@ namespace datalog { } void context::register_variable(func_decl* var) { - m_vars.push_back(m.mk_const(var)); + m_bind_variables.add_var(m.mk_const(var)); } expr_ref context::bind_variables(expr* fml, bool is_forall) { - expr_ref result(m); - app_ref_vector const & vars = m_vars; - rule_manager& rm = get_rule_manager(); - if (vars.empty()) { - result = fml; - } - else { - m_names.reset(); - m_abstractor(0, vars.size(), reinterpret_cast(vars.c_ptr()), fml, result); - m_free_vars(result); - if (m_free_vars.empty()) { - result = fml; - } - else { - m_free_vars.set_default_sort(m.mk_bool_sort()); - for (unsigned i = 0; i < m_free_vars.size(); ++i) { - if (i < vars.size()) { - m_names.push_back(vars[i]->get_decl()->get_name()); - } - else { - m_names.push_back(symbol(i)); - } - } - quantifier_ref q(m); - m_free_vars.reverse(); - q = m.mk_quantifier(is_forall, m_free_vars.size(), m_free_vars.c_ptr(), m_names.c_ptr(), result); - m_elim_unused_vars(q, result); - } - } - return result; + return m_bind_variables(fml, is_forall); } void context::register_predicate(func_decl * decl, bool named) { diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 67520d94f..85d4b7c0e 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -39,9 +39,9 @@ Revision History: #include"model2expr.h" #include"smt_params.h" #include"dl_rule_transformer.h" -#include"expr_abstract.h" #include"expr_functors.h" #include"dl_engine_base.h" +#include"bind_variables.h" struct fixedpoint_params; @@ -178,15 +178,12 @@ namespace datalog { th_rewriter m_rewriter; var_subst m_var_subst; rule_manager m_rule_manager; - unused_vars_eliminator m_elim_unused_vars; - expr_abstractor m_abstractor; contains_pred m_contains_p; check_pred m_check_pred; rule_transformer m_transf; trail_stack m_trail; ast_ref_vector m_pinned; - app_ref_vector m_vars; - svector m_names; + bind_variables m_bind_variables; sort_domain_map m_sorts; func_decl_set m_preds; sym2decl m_preds_by_name; diff --git a/src/muz/base/hnf.h b/src/muz/base/hnf.h index 37339540b..9dc7cccd9 100644 --- a/src/muz/base/hnf.h +++ b/src/muz/base/hnf.h @@ -1,37 +1,36 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - hnf.h - -Abstract: - - Horn normal form convertion. -Author: - - -Notes: - - Very similar to NNF. +/*-- + Module Name: + + hnf.h + + Abstract: + + Horn normal form convertion. + Author: + + + Notes: + + Very similar to NNF. + --*/ - + #ifndef _HNF_H_ #define _HNF_H_ - + #include"ast.h" #include"params.h" #include"defined_names.h" #include"proof_converter.h" - + class hnf { class imp; imp * m_imp; -public: + public: hnf(ast_manager & m); ~hnf(); - + void operator()(expr * n, // [IN] expression that should be put into Horn NF proof* p, // [IN] proof of n expr_ref_vector & rs, // [OUT] resultant (conjunction) of expressions @@ -45,5 +44,5 @@ public: void reset(); func_decl_ref_vector const& get_fresh_predicates(); }; - + #endif /* _HNF_H_ */