From 68ace83893aed1302883903810a5a102d5c9bc6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Dec 2018 07:34:56 -0800 Subject: [PATCH 1/2] remove enable trace Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 06e05315d..a26626224 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3767,8 +3767,6 @@ void theory_seq::finalize_model(model_generator& mg) { } void theory_seq::init_model(model_generator & mg) { - enable_trace("seq"); - TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); m_rep.push_scope(); m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); From b40c2b2926edcb88de170b54942a2e796e78e41e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Dec 2018 14:11:00 -0800 Subject: [PATCH 2/2] fix #876 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 11 +++-- src/smt/theory_seq.cpp | 75 ++++++++++++++++++++++--------- src/smt/theory_seq.h | 1 + 3 files changed, 63 insertions(+), 24 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1ad526dc3..25fc5c119 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -386,7 +386,7 @@ eautomaton* re2automaton::seq2aut(expr* e) { br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); - + TRACE("seq", tout << f->get_name() << "\n";); br_status st = BR_FAILED; switch(f->get_decl_kind()) { @@ -400,16 +400,19 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return mk_re_plus(args[0], result); case OP_RE_STAR: SASSERT(num_args == 1); - return mk_re_star(args[0], result); + st = mk_re_star(args[0], result); + break; case OP_RE_OPTION: SASSERT(num_args == 1); return mk_re_opt(args[0], result); case OP_RE_CONCAT: if (num_args == 1) { - result = args[0]; return BR_DONE; + result = args[0]; + return BR_DONE; } SASSERT(num_args == 2); - return mk_re_concat(args[0], args[1], result); + st = mk_re_concat(args[0], args[1], result); + break; case OP_RE_UNION: if (num_args == 1) { result = args[0]; return BR_DONE; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a26626224..e60281bfa 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5272,6 +5272,26 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { new_eq_eh(deps, n1, n2); } +lbool theory_seq::regex_are_equal(expr* r1, expr* r2) { + if (r1 == r2) { + return l_true; + } + expr* d1 = m_util.re.mk_inter(r1, m_util.re.mk_complement(r2)); + expr* d2 = m_util.re.mk_inter(r2, m_util.re.mk_complement(r1)); + expr_ref diff(m_util.re.mk_union(d1, d2), m); + eautomaton* aut = get_automaton(diff); + if (!aut) { + return l_undef; + } + else if (aut->is_empty()) { + return l_true; + } + else { + return l_false; + } +} + + void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { TRACE("seq", tout << expr_ref(n1->get_owner(), m) << " = " << expr_ref(n2->get_owner(), m) << "\n";); if (n1 != n2 && m_util.is_seq(n1->get_owner())) { @@ -5292,28 +5312,23 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { // create an expression for the symmetric difference and imply it is empty. enode_pair_vector eqs; literal_vector lits; - if (!linearize(deps, eqs, lits)) - return; context& ctx = get_context(); - eqs.push_back(enode_pair(n1, n2)); - expr_ref r1(n1->get_owner(), m); - expr_ref r2(n2->get_owner(), m); - ctx.get_rewriter()(r1); - ctx.get_rewriter()(r2); - if (r1 == r2) { - return; + switch (regex_are_equal(n1->get_owner(), n2->get_owner())) { + case l_true: + break; + case l_false: + if (!linearize(deps, eqs, lits)) { + throw default_exception("could not linearlize assumptions"); + } + eqs.push_back(enode_pair(n1, n2)); + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), 0, nullptr))); + break; + default: + throw default_exception("convert regular expressions into automata"); } -#if 0 - expr* d1 = m_util.re.mk_inter(r1, m_util.re.mk_complement(r2)); - expr* d2 = m_util.re.mk_inter(r2, m_util.re.mk_complement(r1)); - expr_ref diff(m_util.re.mk_union(d1, d2), m); - lit = mk_literal(m_util.re.mk_is_empty(diff)); - justification* js = - ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit)); - ctx.assign(lit, js); -#endif } } @@ -5323,6 +5338,26 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { expr_ref e1(n1->get_owner(), m); expr_ref e2(n2->get_owner(), m); SASSERT(n1->get_root() != n2->get_root()); + if (m_util.is_re(n1->get_owner())) { + enode_pair_vector eqs; + literal_vector lits; + context& ctx = get_context(); + switch (regex_are_equal(e1, e2)) { + case l_false: + return; + case l_true: { + literal lit = mk_eq(e1, e2, false); + lits.push_back(~lit); + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), 0, nullptr))); + return; + } + default: + throw default_exception("convert regular expressions into automata"); + } + } m_exclude.update(e1, e2); expr_ref eq(m.mk_eq(e1, e2), m); TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index c5cb242b3..254b6e2fe 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -451,6 +451,7 @@ namespace smt { vector const& ll, vector const& rl); bool set_empty(expr* x); bool is_complex(eq const& e); + lbool regex_are_equal(expr* r1, expr* r2); bool check_extensionality(); bool check_contains();