Merge branch 'master' of https://github.com/Z3Prover/z3 into Z3Prover-master

Conflicts:
	src/smt/theory_seq.cpp

src/qe/nlqsat.cpp

@@ -886,174 +886,6 @@ namespace qe {
         tactic * translate(ast_manager & m) {
             return alloc(nlqsat, m, m_mode, m_params);
         }
-
-#if 0        
-
-        /**
-         
-           Algorithm:
-           I := true
-           while there is M, such that M |= ~B & I:
-              find P, such that M => P => exists y . ~B & I
-              ; forall y B => ~P
-              C := core of P with respect to A
-              ; A => ~ C => ~ P 
-              I := I & ~C
-
-
-           Alternative Algorithm: 
-           R := false
-           while there is M, such that M |= A & ~R:
-              find I, such that M => I => forall y . B
-              R := R | I              
-              
-         */
-
-        lbool interpolate(expr* a, expr* b, expr_ref& result) {
-            SASSERT(m_mode == interp_t);
-            
-            reset();
-            app_ref enableA(m), enableB(m);
-            expr_ref A(m), B(m), fml(m);
-            expr_ref_vector fmls(m), answer(m);
-
-            // varsB are private to B.
-            nlsat::var_vector vars;
-            uint_set fvars;
-            private_vars(a, b, vars, fvars);
-            
-            enableA = m.mk_const(symbol("#A"), m.mk_bool_sort());
-            enableB = m.mk_not(enableA);
-            A = m.mk_implies(enableA, a);
-            B = m.mk_implies(enableB, m.mk_not(b));
-            fml = m.mk_and(A, B);
-            hoist(fml);
-
-            
-
-            nlsat::literal _enableB = nlsat::literal(m_a2b.to_var(enableB), false);
-            nlsat::literal _enableA = ~_enableB;
-
-            while (true) {
-                m_mode = qsat_t;
-                // enable B
-                m_assumptions.reset();
-                m_assumptions.push_back(_enableB);
-                lbool is_sat = check_sat();
-
-                switch (is_sat) {
-                case l_undef:
-                    return l_undef;
-                case l_true:                    
-                    break;
-                case l_false:
-                    result = mk_and(answer);
-                    return l_true;
-                }
-
-                // disable B, enable A
-                m_assumptions.reset();
-                m_assumptions.push_back(_enableA);
-                // add blocking clause to solver.
-
-                nlsat::scoped_literal_vector core(m_solver);
-                
-                m_mode = elim_t;
-
-                mbp(vars, fvars, core);
-
-                // minimize core.
-                nlsat::literal_vector _core(core.size(), core.c_ptr());
-                _core.push_back(_enableA);
-                is_sat = m_solver.check(_core); // TBD: only for quantifier-free A. Generalize output of elim_t to be a core.
-                switch (is_sat) {
-                case l_undef: 
-                    return l_undef;
-                case l_true:
-                    UNREACHABLE();
-                case l_false:
-                    core.reset();
-                    core.append(_core.size(), _core.c_ptr());
-                    break;
-                }
-                negate_clause(core);
-                // keep polarity of enableA, such that clause is only 
-                // used when checking satisfiability of B.
-                for (unsigned i = 0; i < core.size(); ++i) {
-                    if (core[i].var() == _enableA.var()) core.set(i, ~core[i]);
-                }
-                add_clause(core);                   // Invariant is added as assumption for B.
-                answer.push_back(clause2fml(core)); // TBD: remove answer literal.
-            }
-        }
-
-        /**
-           \brief extract variables that are private to a (not used in b).
-           vars cover the real variables, and fvars cover the Boolean variables.
-
-           TBD: We want fvars to be the complement such that returned core contains
-                Shared boolean variables, but not the ones private to B.
-         */
-        void private_vars(expr* a, expr* b, nlsat::var_vector& vars, uint_set& fvars) {
-            app_ref_vector varsA(m), varsB(m);
-            obj_hashtable<expr> varsAS;
-            pred_abs abs(m);
-            abs.get_free_vars(a, varsA);
-            abs.get_free_vars(b, varsB);
-            insert_set(varsAS, varsA);
-            for (unsigned i = 0; i < varsB.size(); ++i) {
-                if (varsAS.contains(varsB[i].get())) {
-                    varsB[i] = varsB.back();
-                    varsB.pop_back();
-                    --i;
-                }
-            }
-            for (unsigned j = 0; j < varsB.size(); ++j) {
-                app* v = varsB[j].get();
-                if (m_a2b.is_var(v)) {
-                    fvars.insert(m_a2b.to_var(v));
-                }
-                else if (m_t2x.is_var(v)) {
-                    vars.push_back(m_t2x.to_var(v));                    
-                }
-            }
-        }
-
-        lbool maximize(app* _x, expr* _fml, scoped_anum& result, bool& unbounded) {
-            expr_ref fml(_fml, m);
-            reset();
-            hoist(fml);
-            nlsat::literal_vector lits;
-            lbool is_sat = l_true;
-            nlsat::var x = m_t2x.to_var(_x);  
-            m_mode = qsat_t;
-            while (is_sat == l_true) {
-                is_sat = check_sat();
-                if (is_sat == l_true) {
-                    // m_asms is minimized set of literals that satisfy formula.
-                    nlsat::explain& ex = m_solver.get_explain();
-                    polynomial::manager& pm = m_solver.pm();
-                    anum_manager& am = m_solver.am();
-                    ex.maximize(x, m_asms.size(), m_asms.c_ptr(), result, unbounded);
-                    if (unbounded) {
-                        break;
-                    }
-                    // TBD: assert the new bound on x using the result.
-                    bool is_even = false;
-                    polynomial::polynomial_ref pr(pm);
-                    pr = pm.mk_polynomial(x);
-                    rational r;
-                    am.get_upper(result, r);
-                    // result is algebraic numeral, but polynomials are not defined over extension field.
-                    polynomial::polynomial* p = pr;
-                    nlsat::bool_var b = m_solver.mk_ineq_atom(nlsat::atom::GT, 1, &p, &is_even);
-                    nlsat::literal bound(b, false);
-                    m_solver.mk_clause(1, &bound);
-                }
-            }
-            return is_sat;
-        }
-#endif
     };
 };
 

src/smt/theory_seq.cpp

@@ -415,15 +415,13 @@ bool theory_seq::branch_binary_variable(eq const& e) {
         expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m);
         expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m);
         ys.push_back(Y1);
-        expr_ref ysY1(m_util.str.mk_concat(ys.size(), ys.c_ptr()), m);
+        expr_ref ysY1(mk_concat(ys));
-        expr_ref xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m);
+        expr_ref xsE(mk_concat(xs));
-        expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
+        expr_ref Y1Y2(mk_concat(Y1, Y2)); 
-        literal_vector lits;
-        lits.push_back(~lit);
         dependency* dep = e.dep();
-        propagate_eq(dep, lits, x, ysY1, true);
+        propagate_eq(dep, ~lit, x, ysY1);
-        propagate_eq(dep, lits, y, Y1Y2, true);
+        propagate_eq(dep, ~lit, y, Y1Y2);
-        propagate_eq(dep, lits, Y2, xsE, true);
+        propagate_eq(dep, ~lit, Y2, xsE);
     }
     else {
         ctx.mark_as_relevant(lit);
@@ -489,9 +487,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
         literal lit = mk_eq(m_autil.mk_int(lX), m_util.str.mk_length(X), false);
         if (l_true == ctx.get_assignment(lit)) {
             expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
-            literal_vector lits;
+            propagate_eq(dep, lit, X, R);
-            lits.push_back(lit);
-            propagate_eq(dep, lits, X, R, true);
             TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";);
         }
         else {
@@ -1390,11 +1386,10 @@ bool theory_seq::branch_variable_mb() {
         for (rational elem : len2) l2 += elem;
         if (l1 != l2) {
             TRACE("seq", tout << "lengths are not compatible\n";);
-            expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr());
+            expr_ref l = mk_concat(e.ls());
-            expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr());
+            expr_ref r = mk_concat(e.rs());
             expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
-            literal_vector lits;
+            propagate_eq(e.dep(), lnl, lnr, false);
-            propagate_eq(e.dep(), lits, lnl, lnr, false);
             change = true;
             continue;
         }
@@ -1510,8 +1505,8 @@ bool theory_seq::split_lengths(dependency* dep,
         SASSERT(is_var(Y));
         expr_ref Y1(mk_skolem(symbol("seq.left"), X, b, Y), m);
         expr_ref Y2(mk_skolem(symbol("seq.right"), X, b, Y), m);
-        expr_ref bY1(m_util.str.mk_concat(b, Y1), m);
+        expr_ref bY1 = mk_concat(b, Y1);
-        expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
+        expr_ref Y1Y2 = mk_concat(Y1, Y2);
         propagate_eq(dep, lits, X, bY1, true);
         propagate_eq(dep, lits, Y, Y1Y2, true);
     }
@@ -2207,6 +2202,18 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
     enforce_length_coherence(n1, n2);
 }
 
+void theory_seq::propagate_eq(dependency* dep, expr* e1, expr* e2, bool add_eq) {
+    literal_vector lits;
+    propagate_eq(dep, lits, e1, e2, add_eq);
+}
+
+void theory_seq::propagate_eq(dependency* dep, literal lit, expr* e1, expr* e2, bool add_to_eqs) {
+    literal_vector lits;
+    lits.push_back(lit);
+    propagate_eq(dep, lits, e1, e2, add_to_eqs);
+}
+
+
 void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
     expr* o1 = n1->get_owner();
     expr* o2 = n2->get_owner();
@@ -2696,8 +2703,8 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
     }
     SASSERT(0 < l1 && l1 < ls.size());
     SASSERT(0 < r1 && r1 < rs.size());
-    expr_ref l(m_util.str.mk_concat(l1, ls1), m);
+    expr_ref l = mk_concat(l1, ls1);
-    expr_ref r(m_util.str.mk_concat(r1, rs1), m);            
+    expr_ref r = mk_concat(r1, rs1);
     expr_ref lenl(m_util.str.mk_length(l), m);
     expr_ref lenr(m_util.str.mk_length(r), m);
     expr_ref len_eq(m.mk_eq(lenl, lenr), m);
@@ -2709,7 +2716,7 @@ bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vect
         rhs.append(r2, rs2);
         deps = mk_join(deps, lit);
         m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
-        propagate_eq(deps, lits, l, r, true);
+        propagate_eq(deps, l, r, true);
         TRACE("seq", tout << "propagate eq\nlhs: " << lhs << "\nrhs: " << rhs << "\n";);
         return true;
     }

src/smt/theory_seq.h

@@ -441,6 +441,8 @@ namespace smt {
         expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
         expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
         expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); }
+        expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty());  return mk_concat(es.size(), es.c_ptr()); }
+        expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr()); }
         expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); }
         expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); }
         bool solve_nqs(unsigned i);
@@ -467,7 +469,9 @@ namespace smt {
         void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
         void propagate_eq(dependency* dep, enode* n1, enode* n2);
         void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
-        void propagate_eq(dependency* dep, literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
+        void propagate_eq(dependency* dep, literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs = true);
+        void propagate_eq(dependency* dep, expr* e1, expr* e2, bool add_to_eqs = true);
+        void propagate_eq(dependency* dep, literal lit, expr* e1, expr* e2, bool add_to_eqs = true);
         void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
 
         u_map<unsigned> m_branch_start;