mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 00:35:47 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-30 09:39:23 -08:00
commit a412a554eb
21 changed files with 334 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/params/smt_params_helper.pyg
View file

@ -63,5 +63,6 @@ def_module_params(module_name='smt',
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances')
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core')
))

2
src/smt/smt_context.cpp
View file

@ -2040,11 +2040,13 @@ namespace smt {
v.shrink(old_size);
}
#if 0
void context::mark_as_deleted(clause * cls) {
SASSERT(!cls->deleted());
remove_cls_occs(cls);
cls->mark_as_deleted(m_manager);
}
#endif
/**
\brief Undo variable assignments.

14
src/smt/smt_solver.cpp
View file

@ -37,6 +37,7 @@ namespace smt {
symbol m_logic;
bool m_minimizing_core;
bool m_core_extend_patterns;
unsigned m_core_extend_patterns_max_distance;
obj_map<expr, expr*> m_name2assertion;
public:
@ -46,12 +47,14 @@ namespace smt {
m_params(p),
m_context(m, m_smt_params),
m_minimizing_core(false),
m_core_extend_patterns(false) {
m_core_extend_patterns(false),
m_core_extend_patterns_max_distance(UINT_MAX) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
}
virtual solver * translate(ast_manager & m, params_ref const & p) {
@ -119,7 +122,8 @@ namespace smt {
SASSERT(n <= lvl);
unsigned new_lvl = lvl - n;
unsigned old_sz = m_scopes[new_lvl];
for (unsigned i = cur_sz - 1; i >= old_sz; i--) {
for (unsigned i = cur_sz; i > old_sz; ) {
--i;
expr * key = m_assumptions[i].get();
SASSERT(m_name2assertion.contains(key));
expr * value = m_name2assertion.find(key);
@ -283,7 +287,7 @@ namespace smt {
func_decl_set pattern_fds;
vector<func_decl_set> assrtn_fds;
do {
for (unsigned d = 0; d < m_core_extend_patterns_max_distance; d++) {
new_core_literals.reset();
unsigned sz = core.size();
@ -308,8 +312,10 @@ namespace smt {
}
core.append(new_core_literals.size(), new_core_literals.c_ptr());
if (new_core_literals.empty())
break;
}
while (!new_core_literals.empty());
}
};
};

41
src/smt/theory_seq.cpp
View file

@ -2940,8 +2940,8 @@ void theory_seq::deque_axiom(expr* n) {
encode that s is not contained in of xs1
where s1 is all of s, except the last element.
lit or s = "" or s = s1*(unit c)
lit or s = "" or !contains(x*s1, s)
s = "" or s = s1*(unit c)
s = "" or !contains(x*s1, s)
*/
void theory_seq::tightest_prefix(expr* s, expr* x) {
expr_ref s1 = mk_first(s);
@ -2958,22 +2958,19 @@ void theory_seq::tightest_prefix(expr* s, expr* x) {
let i = Index(t, s, offset):
offset >= len(t) => i = -1
offset fixed to 0:
len(t) != 0 & !contains(t, s) => i = -1
len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
offset = 0 & len(t) != 0 & contains(t, s) => t = xsy & i = len(x)
tightest_prefix(x, s)
offset not fixed:
0 <= offset < len(t) => xy = t &
len(x) = offset &
(-1 = indexof(y, s, 0) => -1 = i) &
(indexof(y, s, 0) >= 0 => indexof(t, s, 0) + offset = i)
if offset < 0
under specified
offset < 0 => i = -1
optional lemmas:
(len(s) > len(t) -> i = -1)
@ -2987,17 +2984,19 @@ void theory_seq::add_indexof_axiom(expr* i) {
expr_ref minus_one(m_autil.mk_int(-1), m);
expr_ref zero(m_autil.mk_int(0), m);
expr_ref xsy(m);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal i_eq_m1 = mk_eq(i, minus_one, false);
add_axiom(cnt, i_eq_m1);
literal s_eq_empty = mk_eq_empty(s);
add_axiom(~s_eq_empty, mk_eq(i, zero, false));
add_axiom(s_eq_empty, ~mk_eq_empty(t), i_eq_m1);
if (!offset || (m_autil.is_numeral(offset, r) && r.is_zero())) {
expr_ref x = mk_skolem(m_indexof_left, t, s);
expr_ref y = mk_skolem(m_indexof_right, t, s);
xsy = mk_concat(x, s, y);
expr_ref lenx(m_util.str.mk_length(x), m);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal s_eq_empty = mk_eq_empty(s);
add_axiom(cnt, mk_eq(i, minus_one, false));
add_axiom(~s_eq_empty, mk_eq(i, zero, false));
add_axiom(s_eq_empty, ~mk_eq_empty(t), mk_eq(i, minus_one, false));
add_axiom(~cnt, s_eq_empty, mk_seq_eq(t, xsy));
add_axiom(~cnt, s_eq_empty, mk_eq(i, lenx, false));
tightest_prefix(s, x);
@ -3024,10 +3023,13 @@ void theory_seq::add_indexof_axiom(expr* i) {
add_axiom(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false));
add_axiom(~offset_ge_0, offset_ge_len,
~mk_eq(indexof0, minus_one, false), mk_eq(i, minus_one, false));
~mk_eq(indexof0, minus_one, false), i_eq_m1);
add_axiom(~offset_ge_0, offset_ge_len,
~mk_literal(m_autil.mk_ge(indexof0, zero)),
mk_eq(offset_p_indexof0, i, false));
// offset < 0 => -1 = i
add_axiom(offset_ge_0, i_eq_m1);
}
}
@ -3817,6 +3819,15 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
solve_eqs(m_eqs.size()-1);
enforce_length_coherence(n1, n2);
}
else if (n1 != n2 && m_util.is_re(n1->get_owner())) {
warning_msg("equality between regular expressions is not yet supported");
eautomaton* a1 = get_automaton(n1->get_owner());
eautomaton* a2 = get_automaton(n2->get_owner());
// eautomaton* b1 = mk_difference(*a1, *a2);
// eautomaton* b2 = mk_difference(*a2, *a1);
// eautomaton* c = mk_union(*b1, *b2);
// then some emptiness check.
}
}
void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {