diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 1f9c89f89..ab5095328 100644 --- a/src/qe/nlqsat.cpp +++ b/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 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 }; }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 9830a16b4..597348589 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -397,15 +397,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 xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m); - expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m); - literal_vector lits; - lits.push_back(~lit); + expr_ref ysY1(mk_concat(ys)); + expr_ref xsE(mk_concat(xs)); + expr_ref Y1Y2(mk_concat(Y1, Y2)); dependency* dep = e.dep(); - propagate_eq(dep, lits, x, ysY1, true); - propagate_eq(dep, lits, y, Y1Y2, true); - propagate_eq(dep, lits, Y2, xsE, true); + propagate_eq(dep, ~lit, x, ysY1); + propagate_eq(dep, ~lit, y, Y1Y2); + propagate_eq(dep, ~lit, Y2, xsE); } else { ctx.mark_as_relevant(lit); @@ -471,9 +469,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; - lits.push_back(lit); - propagate_eq(dep, lits, X, R, true); + propagate_eq(dep, lit, X, R); TRACE("seq", tout << "propagate " << mk_pp(X, m) << " " << R << "\n";); } else { @@ -506,11 +502,10 @@ bool theory_seq::branch_variable_mb() { for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j]; 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 r = mk_concat(e.rs().size(), e.rs().c_ptr()); + expr_ref l = mk_concat(e.ls()); + 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(), lits, lnl, lnr, false); + propagate_eq(e.dep(), lnl, lnr, false); change = true; continue; } @@ -626,8 +621,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 Y1Y2(m_util.str.mk_concat(Y1, Y2), m); + expr_ref bY1 = mk_concat(b, Y1); + expr_ref Y1Y2 = mk_concat(Y1, Y2); propagate_eq(dep, lits, X, bY1, true); propagate_eq(dep, lits, Y, Y1Y2, true); } @@ -1317,6 +1312,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(); @@ -1662,19 +1669,18 @@ 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 r(m_util.str.mk_concat(r1, rs1), m); + expr_ref l = mk_concat(l1, ls1); + 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); literal lit = mk_eq(lenl, lenr, false); if (ctx.get_assignment(lit) == l_true) { - literal_vector lits; expr_ref_vector lhs(m), rhs(m); lhs.append(l2, ls2); 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; } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index d4686c835..46f803f5b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -410,6 +410,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 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); @@ -436,7 +438,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 m_branch_start;