mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-20 21:20:20 -07:00
commit 17f0377c06
4 changed files with 126 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/api/api_util.h
View file

@ -29,7 +29,6 @@ Revision History:
#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
#define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))
namespace api {
// Generic wrapper for ref-count objects exposed by the API
@ -44,30 +43,30 @@ namespace api {
};
};
inline ast * to_ast(Z3_ast a) { VALIDATE(a); return reinterpret_cast<ast *>(a); }
inline ast * to_ast(Z3_ast a) { return reinterpret_cast<ast *>(a); }
inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }
inline expr * to_expr(Z3_ast a) { VALIDATE(a); return reinterpret_cast<expr*>(a); }
inline expr * to_expr(Z3_ast a) { return reinterpret_cast<expr*>(a); }
inline Z3_ast of_expr(expr* e) { return reinterpret_cast<Z3_ast>(e); }
inline expr * const * to_exprs(Z3_ast const* a) { return reinterpret_cast<expr* const*>(a); }
inline Z3_ast * const * of_exprs(expr* const* e) { return reinterpret_cast<Z3_ast* const*>(e); }
inline app * to_app(Z3_app a) { VALIDATE(a); return reinterpret_cast<app*>(a); }
inline app * to_app(Z3_ast a) { VALIDATE(a); return reinterpret_cast<app*>(a); }
inline app * to_app(Z3_app a) { return reinterpret_cast<app*>(a); }
inline app * to_app(Z3_ast a) { return reinterpret_cast<app*>(a); }
inline Z3_app of_app(app* a) { return reinterpret_cast<Z3_app>(a); }
inline app * const* to_apps(Z3_ast const* a) { VALIDATE(a); return reinterpret_cast<app * const*>(a); }
inline app * const* to_apps(Z3_ast const* a) { return reinterpret_cast<app * const*>(a); }
inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* const*>(a); }
inline sort * to_sort(Z3_sort a) { VALIDATE(a); return reinterpret_cast<sort*>(a); }
inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }
inline func_decl * to_func_decl(Z3_func_decl a) { VALIDATE(a); return reinterpret_cast<func_decl*>(a); }
inline func_decl * to_func_decl(Z3_func_decl a) { return reinterpret_cast<func_decl*>(a); }
inline Z3_func_decl of_func_decl(func_decl* f) { return reinterpret_cast<Z3_func_decl>(f); }
inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinterpret_cast<func_decl*const*>(f); }
@ -75,7 +74,7 @@ inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinter
inline symbol to_symbol(Z3_symbol s) { return symbol::mk_symbol_from_c_ptr(reinterpret_cast<void*>(s)); }
inline Z3_symbol of_symbol(symbol s) { return reinterpret_cast<Z3_symbol>(const_cast<void*>(s.c_ptr())); }
inline Z3_pattern of_pattern(ast* a) { VALIDATE(a); return reinterpret_cast<Z3_pattern>(a); }
inline Z3_pattern of_pattern(ast* a) { return reinterpret_cast<Z3_pattern>(a); }
inline app* to_pattern(Z3_pattern p) { return reinterpret_cast<app*>(p); }
inline Z3_lbool of_lbool(lbool b) { return static_cast<Z3_lbool>(b); }

37
src/api/c++/z3++.h
View file

@ -872,7 +872,18 @@ namespace z3 {
\brief Return a simplified version of this expression. The parameter \c p is a set of parameters for the Z3 simplifier.
*/
expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
};
/**
\brief Apply substitution. Replace src expressions by dst.
*/
expr substitute(expr_vector const& src, expr_vector const& dst);
/**
\brief Apply substitution. Replace bound variables by expressions.
*/
expr substitute(expr_vector const& dst);
};
/**
\brief Wraps a Z3_ast as an expr object. It also checks for errors.
@ -1680,6 +1691,30 @@ namespace z3 {
d.check_error();
return expr(d.ctx(), r);
}
inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
assert(src.size() == dst.size());
array<Z3_ast> _src(src.size());
array<Z3_ast> _dst(dst.size());
for (unsigned i = 0; i < src.size(); ++i) {
_src[i] = src[i];
_dst[i] = dst[i];
}
Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
check_error();
return expr(ctx(), r);
}
inline expr expr::substitute(expr_vector const& dst) {
array<Z3_ast> _dst(dst.size());
for (unsigned i = 0; i < dst.size(); ++i) {
_dst[i] = dst[i];
}
Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
check_error();
return expr(ctx(), r);
}
};

102
src/muz_qe/dl_compiler.cpp
View file

@ -146,7 +146,7 @@ namespace datalog {
}
void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val,
reg_idx & result, instruction_block & acc) {
reg_idx & result, bool & dealloc, instruction_block & acc) {
reg_idx singleton_table;
if(!m_constant_registers.find(s, val, singleton_table)) {
singleton_table = get_single_column_register(s);
@ -155,16 +155,18 @@ namespace datalog {
m_constant_registers.insert(s, val, singleton_table);
}
if(src==execution_context::void_register) {
make_clone(singleton_table, result, acc);
result = singleton_table;
dealloc = false;
}
else {
variable_intersection empty_vars(m_context.get_manager());
make_join(src, singleton_table, empty_vars, result, acc);
dealloc = true;
}
}
void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result,
instruction_block & acc) {
bool & dealloc, instruction_block & acc) {
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
IF_VERBOSE(3, {
@ -173,25 +175,35 @@ namespace datalog {
verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n"
<< mk_ismt2_pp(e, m_context.get_manager()) << "\n";
});
reg_idx total_table = get_single_column_register(s);
relation_signature sig;
sig.push_back(s);
acc.push_back(instruction::mk_total(sig, pred, total_table));
reg_idx total_table;
if (!m_total_registers.find(s, pred, total_table)) {
total_table = get_single_column_register(s);
relation_signature sig;
sig.push_back(s);
m_top_level_code.push_back(instruction::mk_total(sig, pred, total_table));
m_total_registers.insert(s, pred, total_table);
}
if(src == execution_context::void_register) {
result = total_table;
dealloc = false;
}
else {
variable_intersection empty_vars(m_context.get_manager());
make_join(src, total_table, empty_vars, result, acc);
make_dealloc_non_void(total_table, acc);
dealloc = true;
}
}
void compiler::make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result,
instruction_block & acc) {
SASSERT(sig.empty());
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
if (m_empty_tables_registers.find(pred, result))
return;
result = get_fresh_register(sig);
acc.push_back(instruction::mk_total(sig, pred, result));
m_top_level_code.push_back(instruction::mk_total(sig, pred, result));
m_empty_tables_registers.insert(pred, result);
}
@ -233,6 +245,7 @@ namespace datalog {
reg_idx src,
const svector<assembling_column_info> & acis0,
reg_idx & result,
bool & dealloc,
instruction_block & acc) {
TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
@ -277,7 +290,9 @@ namespace datalog {
if(!src_cols_to_remove.empty()) {
reg_idx new_curr;
make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.c_ptr(), new_curr, acc);
make_dealloc_non_void(curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
dealloc = true;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
@ -298,16 +313,19 @@ namespace datalog {
unsigned bound_column_index;
if(acis[i].kind!=ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) {
reg_idx new_curr;
bool new_dealloc;
bound_column_index=curr_sig->size();
if(acis[i].kind==ACK_CONSTANT) {
make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, acc);
make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, new_dealloc, acc);
}
else {
SASSERT(acis[i].kind==ACK_UNBOUND_VAR);
make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, acc);
make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, new_dealloc, acc);
handled_unbound.insert(acis[i].var_index,bound_column_index);
}
make_dealloc_non_void(curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
dealloc = new_dealloc;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
SASSERT(bound_column_index==curr_sig->size()-1);
@ -328,7 +346,9 @@ namespace datalog {
}
reg_idx new_curr;
make_duplicate_column(curr, col, new_curr, acc);
make_dealloc_non_void(curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
dealloc = true;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
unsigned bound_column_index=curr_sig->size()-1;
@ -356,7 +376,9 @@ namespace datalog {
reg_idx new_curr;
make_rename(curr, permutation.size(), permutation.c_ptr(), new_curr, acc);
make_dealloc_non_void(curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
dealloc = true;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
}
@ -365,6 +387,7 @@ namespace datalog {
SASSERT(src==execution_context::void_register);
SASSERT(acis0.size()==0);
make_full_relation(head_pred, empty_signature, curr, acc);
dealloc = false;
}
result=curr;
@ -416,6 +439,9 @@ namespace datalog {
//by the join operation
unsigned second_tail_arg_ofs;
// whether to dealloc the previous result
bool dealloc = true;
if(pt_len == 2) {
reg_idx t1_reg=tail_regs[0];
reg_idx t2_reg=tail_regs[1];
@ -488,8 +514,7 @@ namespace datalog {
}
}
if(single_res==t_reg) {
//we may be modifying the register later, so we need a local copy
make_clone(t_reg, single_res, acc);
dealloc = false;
}
}
@ -500,7 +525,7 @@ namespace datalog {
single_res=execution_context::void_register;
}
add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, acc);
add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc);
int2ints var_indexes;
@ -515,7 +540,10 @@ namespace datalog {
if(is_app(exp)) {
SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
relation_element value = to_app(exp);
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_equal(m_context.get_manager(), filtered_res, value, i));
dealloc = true;
}
else {
SASSERT(is_var(exp));
@ -542,7 +570,10 @@ namespace datalog {
//condition!)
continue;
}
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_identical(filtered_res, indexes.size(), indexes.c_ptr()));
dealloc = true;
}
//enforce negative predicates
@ -565,9 +596,12 @@ namespace datalog {
relation_sort arg_sort;
m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, acc);
bool new_dealloc;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
make_dealloc_non_void(filtered_res, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg; // here filtered_res value gets changed !!
t_cols.push_back(single_res_expr.size());
@ -577,8 +611,11 @@ namespace datalog {
SASSERT(t_cols.size()==neg_cols.size());
reg_idx neg_reg = m_pred_regs.find(neg_pred);
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
t_cols.c_ptr(), neg_cols.c_ptr()));
dealloc = true;
}
//enforce interpreted tail predicates
@ -639,9 +676,12 @@ namespace datalog {
reg_idx new_reg;
TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, acc);
bool new_dealloc;
make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc);
make_dealloc_non_void(filtered_res, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg; // here filtered_res value gets changed !!
unsigned unbound_column_index = single_res_expr.size();
@ -659,7 +699,10 @@ namespace datalog {
expr_ref renamed(m);
m_context.get_var_subst()(t, binding.size(), binding.c_ptr(), renamed);
app_ref app_renamed(to_app(renamed), m);
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
dealloc = true;
}
{
@ -704,11 +747,12 @@ namespace datalog {
SASSERT(head_acis.size()==head_len);
reg_idx new_head_reg;
make_assembling_code(r, head_pred, filtered_res, head_acis, new_head_reg, acc);
make_assembling_code(r, head_pred, filtered_res, head_acis, new_head_reg, dealloc, acc);
//update the head relation
make_union(new_head_reg, head_reg, delta_reg, use_widening, acc);
make_dealloc_non_void(new_head_reg, acc);
if (dealloc)
make_dealloc_non_void(new_head_reg, acc);
}
finish:
@ -716,7 +760,7 @@ namespace datalog {
}
void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr,
instruction_block & acc) {
bool & dealloc, instruction_block & acc) {
uint_set pos_vars;
u_map<expr*> neg_vars;
ast_manager& m = m_context.get_manager();
@ -750,7 +794,13 @@ namespace datalog {
expr* e = it->m_value;
if (!pos_vars.contains(v)) {
single_res_expr.push_back(e);
make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), single_res, acc);
reg_idx new_single_res;
bool new_dealloc;
make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), new_single_res, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(single_res, acc);
dealloc = new_dealloc;
single_res = new_single_res;
TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";);
}
}

10
src/muz_qe/dl_compiler.h
View file

@ -114,6 +114,8 @@ namespace datalog {
reg_idx m_new_reg;
vector<relation_signature> m_reg_signatures;
obj_pair_map<sort, app, reg_idx> m_constant_registers;
obj_pair_map<sort, decl, reg_idx> m_total_registers;
obj_map<decl, reg_idx> m_empty_tables_registers;
instruction_observer m_instruction_observer;
/**
@ -163,20 +165,20 @@ namespace datalog {
with empty signature.
*/
void make_assembling_code(rule* compiled_rule, func_decl* head_pred, reg_idx src, const svector<assembling_column_info> & acis0,
reg_idx & result, instruction_block & acc);
reg_idx & result, bool & dealloc, instruction_block & acc);
void make_dealloc_non_void(reg_idx r, instruction_block & acc);
void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val,
reg_idx & result, instruction_block & acc);
reg_idx & result, bool & dealloc, instruction_block & acc);
void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result,
instruction_block & acc);
bool & dealloc, instruction_block & acc);
void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result,
instruction_block & acc);
void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr,
instruction_block& acc);
bool & dealloc, instruction_block& acc);
void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc);