Merge branch 'master' of https://github.com/z3prover/z3

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;

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);
@@ -5274,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())) {
@@ -5294,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));
+        switch (regex_are_equal(n1->get_owner(), n2->get_owner())) {
-        expr_ref r1(n1->get_owner(), m);
+        case l_true:
-        expr_ref r2(n2->get_owner(), m);
+            break;
-        ctx.get_rewriter()(r1);
+        case l_false:
-        ctx.get_rewriter()(r2);
+            if (!linearize(deps, eqs, lits)) {
-        if (r1 == r2) {
+                throw default_exception("could not linearlize assumptions");
-            return;
             }
-#if 0
+            eqs.push_back(enode_pair(n1, n2));
-        expr* d1 = m_util.re.mk_inter(r1, m_util.re.mk_complement(r2));
+            ctx.set_conflict(
-        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(
+                    ext_theory_conflict_justification(
-                    get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit));
+                        get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), 0, nullptr)));
-        ctx.assign(lit, js);        
+            break;
-#endif
+        default:
+            throw default_exception("convert regular expressions into automata");            
+        }
     }
 }
 
@@ -5325,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";);

src/smt/theory_seq.h

@@ -451,6 +451,7 @@ namespace smt {
                            vector<rational> const& ll, vector<rational> 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();