mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

cleanup bit2bool from models #3847

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 03:05:11 -07:00
parent 5c9fd90031
commit 8e6bb30c82
3 changed files with 15 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/model/model.cpp
View file

@ -22,6 +22,7 @@ Revision History:
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/array_decl_plugin.h" #include "ast/array_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "ast/used_symbols.h" #include "ast/used_symbols.h"
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
@ -410,6 +411,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
ptr_buffer<expr> args; ptr_buffer<expr> args;
todo.push_back(e); todo.push_back(e);
array_util autil(m); array_util autil(m);
bv_util bv(m);
func_interp* fi = nullptr; func_interp* fi = nullptr;
unsigned pid = 0; unsigned pid = 0;
expr_ref new_t(m); expr_ref new_t(m);
@ -457,6 +459,10 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
var_subst vs(m, false); var_subst vs(m, false);
new_t = vs(fi->get_interp(), args.size(), args.c_ptr()); new_t = vs(fi->get_interp(), args.size(), args.c_ptr());
} }
else if (bv.is_bit2bool(t)) {
unsigned idx = f->get_parameter(0).get_int();
new_t = m.mk_eq(bv.mk_extract(idx, idx, args[0]), bv.mk_numeral(1, 1));
}
#if 0 #if 0
else if (is_uninterp_const(a) && !get_const_interp(f)) { else if (is_uninterp_const(a) && !get_const_interp(f)) {
new_t = get_some_value(f->get_range()); new_t = get_some_value(f->get_range());

8
src/muz/spacer/spacer_context.cpp
View file

@ -1121,13 +1121,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
// adjust result according to model converter. // adjust result according to model converter.
unsigned arity = m_head->get_arity(); unsigned arity = m_head->get_arity();
model_ref md = alloc(model, m); model_ref md = alloc(model, m);
if (arity == 0) { md->register_decl(m_head, result);
md->register_decl(m_head, result);
} else {
func_interp* fi = alloc(func_interp, m, arity);
fi->set_else(result);
md->register_decl(m_head, fi);
}
model_converter_ref mc = ctx.get_model_converter(); model_converter_ref mc = ctx.get_model_converter();
apply(mc, md); apply(mc, md);
if (p_orig->get_arity() == 0) { if (p_orig->get_arity() == 0) {

23
src/muz/spacer/spacer_manager.cpp
View file

@ -73,7 +73,7 @@ expr_ref inductive_property::fixup_clauses(expr* fml) const
expr_ref result(m); expr_ref result(m);
flatten_and(fml, conjs); flatten_and(fml, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) { for (unsigned i = 0; i < conjs.size(); ++i) {
conjs[i] = fixup_clause(conjs[i].get()); conjs[i] = fixup_clause(conjs.get(i));
} }
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result); bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result);
return result; return result;
@ -83,19 +83,17 @@ std::string inductive_property::to_string() const
{ {
std::stringstream stm; std::stringstream stm;
model_ref md; model_ref md;
expr_ref result(m);
to_model(md); to_model(md);
model_smt2_pp(stm, m, *md.get(), 0); stm << *md;
return stm.str(); return stm.str();
} }
void inductive_property::to_model(model_ref& md) const void inductive_property::to_model(model_ref& md) const {
{
md = alloc(model, m); md = alloc(model, m);
vector<relation_info> const& rs = m_relation_info; vector<relation_info> const& rs = m_relation_info;
expr_ref_vector conjs(m); expr_ref_vector conjs(m);
for (unsigned i = 0; i < rs.size(); ++i) { for (relation_info const& ri_ : rs) {
relation_info ri(rs[i]); relation_info ri(ri_);
func_decl * pred = ri.m_pred; func_decl * pred = ri.m_pred;
expr_ref prop = fixup_clauses(ri.m_body); expr_ref prop = fixup_clauses(ri.m_body);
func_decl_ref_vector const& sig = ri.m_vars; func_decl_ref_vector const& sig = ri.m_vars;
@ -105,16 +103,11 @@ void inductive_property::to_model(model_ref& md) const
sig_vars.push_back(m.mk_const(sig[sig.size() - j - 1])); sig_vars.push_back(m.mk_const(sig[sig.size() - j - 1]));
} }
expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q); expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q);
if (sig.empty()) { md->register_decl(pred, q);
md->register_decl(pred, q);
} else {
func_interp* fi = alloc(func_interp, m, sig.size());
fi->set_else(q);
md->register_decl(pred, fi);
}
} }
TRACE("spacer", model_smt2_pp(tout, m, *md, 0);); TRACE("spacer", tout << *md;);
apply(const_cast<model_converter_ref&>(m_mc), md); apply(const_cast<model_converter_ref&>(m_mc), md);
md->compress();
} }
expr_ref inductive_property::to_expr() const expr_ref inductive_property::to_expr() const