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

fix #4049

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-24 11:58:48 -07:00
parent 6ab83466d9
commit 785c9a18ca
5 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -168,6 +168,10 @@ namespace smt {
for (unsigned i = 0; !src_m.proofs_enabled() && i < src_ctx.m_assigned_literals.size(); ++i) { for (unsigned i = 0; !src_m.proofs_enabled() && i < src_ctx.m_assigned_literals.size(); ++i) {
literal lit = src_ctx.m_assigned_literals[i]; literal lit = src_ctx.m_assigned_literals[i];
bool_var_data const & d = src_ctx.get_bdata(lit.var());
if (d.is_theory_atom() && !src_ctx.m_theories.get_plugin(d.get_theory())->is_safe_to_copy(lit.var())) {
continue;
}
expr_ref fml0(src_m), fml1(dst_m); expr_ref fml0(src_m), fml1(dst_m);
src_ctx.literal2expr(lit, fml0); src_ctx.literal2expr(lit, fml0);
fml1 = tr(fml0.get()); fml1 = tr(fml0.get());

2
src/smt/smt_parallel.cpp
View file

@ -183,7 +183,7 @@ namespace smt {
} }
}; };
// num_threads = 1; // for debugging: num_threads = 1;
while (true) { while (true) {
vector<std::thread> threads(num_threads); vector<std::thread> threads(num_threads);

2
src/smt/smt_theory.h
View file

@ -404,6 +404,8 @@ namespace smt {
bool is_representative(theory_var v) const { bool is_representative(theory_var v) const {
return get_representative(v) == v; return get_representative(v) == v;
} }
virtual bool is_safe_to_copy(bool_var v) const { return true; }
unsigned get_num_vars() const { unsigned get_num_vars() const {
return m_var2enode.size(); return m_var2enode.size();

12
src/smt/theory_seq.cpp
View file

@ -1199,6 +1199,17 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
} }
} }
/**
Skolem predicates for automata acceptance are stateful.
They depend on the shape of automata that were used when the predicates
were created. It is unsafe to copy assertions about automata from one context
to another.
*/
bool theory_seq::is_safe_to_copy(bool_var v) const {
context & ctx = get_context();
expr* e = ctx.bool_var2expr(v);
return !m_sk.is_skolem(e);
}
bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) { bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
context& ctx = get_context(); context& ctx = get_context();
@ -3352,6 +3363,7 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
VERIFY(m_autil.is_numeral(idx, _idx)); VERIFY(m_autil.is_numeral(idx, _idx));
VERIFY(aut); VERIFY(aut);
if (aut->is_sink_state(src)) { if (aut->is_sink_state(src)) {
TRACE("seq", { display_expr d(m); aut->display(tout << "sink " << src << "\n", d); });
propagate_lit(nullptr, 1, &lit, false_literal); propagate_lit(nullptr, 1, &lit, false_literal);
return; return;
} }

1
src/smt/theory_seq.h
View file

@ -446,6 +446,7 @@ namespace smt {
theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); } theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
char const * get_name() const override { return "seq"; } char const * get_name() const override { return "seq"; }
bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); } bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); }
bool is_safe_to_copy(bool_var v) const;
theory_var mk_var(enode* n) override; theory_var mk_var(enode* n) override;
void apply_sort_cnstr(enode* n, sort* s) override; void apply_sort_cnstr(enode* n, sort* s) override;
void display(std::ostream & out) const override; void display(std::ostream & out) const override;