mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add shortcuts for concatenation and equality propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c8d9be0bbf
commit
faebbc5384
|
|
@ -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
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<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);
|
||||
|
|
@ -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<unsigned> m_branch_start;
|
||||
|
|
|
|||
Loading…
Reference in a new issue