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

make self-contained bind-variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-24 14:30:30 -07:00
parent 918d52f1b0
commit 6457654e2e
5 changed files with 231 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

154
src/muz/base/bind_variables.cpp Normal file
View file

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

51
src/muz/base/bind_variables.h Normal file
View file

@ -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<app, var*> var2bound;
typedef obj_map<expr, expr*> cache_t;
ast_manager& m;
app_ref_vector m_vars;
obj_map<expr, expr*> m_cache;
var2bound m_var2bound;
expr_ref_vector m_pinned;
ptr_vector<sort> m_bound;
svector<symbol> m_names;
ptr_vector<expr> m_todo;
ptr_vector<expr> 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_ */

37
src/muz/base/dl_context.cpp
View file

@ -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<expr*const*>(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) {

7
src/muz/base/dl_context.h
View file

@ -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<context> m_trail;
ast_ref_vector m_pinned;
app_ref_vector m_vars;
svector<symbol> m_names;
bind_variables m_bind_variables;
sort_domain_map m_sorts;
func_decl_set m_preds;
sym2decl m_preds_by_name;

43
src/muz/base/hnf.h
View file

@ -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_ */